m2.smv

MODULE main

/--
Nesta segunda fase foi aumentada a complexidade da transição do estado 'halt_down' para
'halt_up' e vice-versa. Foram acrescentados dois novos componentes ao sistema: a porta
e o cadeado da porta. Para transitar de um estado em que o sistema se encontra parado,
para a fase oposta, é necessário primeiro abrir e fechar a porta. Para que esta
abra, o cadeado deve ser primeiro desbloqueado.

Segunda a figura 3 do enunciado, todas as ações são interruptíveis, com exceção do PD2 e
do PU2, os quais uma vez executados, devem seguir obrigatoriamente para o CompletePD2 e 
CompletePU2.

Escolhemos ainda não utilizar as variáveis 'p', 'l' e 'i' que surgem no modelo de Event-B. 
Isto porque, para além não compreendermos a semântica e o comportamento destas três
variáveis, concluímos que conseguiamos modelar corretamente o sistema especificado em M2
recorrendo a apenas duas variáveis auxiliares com uma semântica bem definida.
--/

VAR
    button: {down, up};
    phase: {moving_down, halt_down, moving_up, halt_up};

    /--
    A variável 'dstate' descreve o estado da porta, podendo estar aberta ou fechada.
    --/
    dstate: {open, closed};

    /--
    A variável 'lstate' descreve o estado do cadeado da porta, podendo estar bloqueado 
    ou não.
    --/
    lstate: {locked, unlocked};

    /--
    A variável 'gstate' é uma variável auxiliar que é necessária para distinguir certos
    estados do sistema que possuem os mesmos valores mas em alturas diferentes.
    --/
    gstate: {retracted, extended};

    /--
    A variável 'interruptible' é outra variável auxiliar. Esta é necessária porque algumas
    das ações não podem ser interrompidas, ou seja, o estado do botão não pode ser
    alterado enquanto a ação estiver a ocorrer.
    --/
    interruptible: boolean;

/--
Nesta fase decidimos utilizar o DEFINE para aumentar a legibilidade de alguns padrões que
ocorrem várias vezes.
--/
DEFINE
    /--
    'BUTTON_CHANGES' verifica se o botão mudará na próxima fase.
    --/
    BUTTON_CHANGES := button != next(button);

    /--
    'SWAP_GEARS' altera o valor da variável 'gstate' da mesma forma que '!' altera
    o valor de um boleano.
    --/
    SWAP_GEARS := gstate = extended ? retracted : extended;

    /--
    Descreve quatro fases diferentes do sistema de acordo com o estado da porta
    e a direção do movimento.
    --/
    -- O sistema encontra-se a subir e ainda não abriu as portas.
    PRE_OPEN_UP := phase = moving_up & gstate = extended;
    -- O sistema encontra-se a subir e já abriu as portas. 
    POS_OPEN_UP := phase = moving_up & gstate = retracted;   
    -- O sistema encontra-se a descer e ainda não abriu as portas.
    PRE_OPEN_DN := phase = moving_down & gstate = retracted;
    -- O sistema encontra-se a descer e já abriu as portas.
    POS_OPEN_DN := phase = moving_down & gstate = extended;

    /--
    Descreve duas fases diferentes do sistema de acordo com o estado da porta.
    --/
    PRE_OPEN := PRE_OPEN_UP | PRE_OPEN_DN;
    POS_OPEN := POS_OPEN_UP | POS_OPEN_DN;

ASSIGN
    -- Declarações iniciais de acordo com a figura 3 do enunciado.
    init(button) := down;
    init(phase) := halt_down;
    init(dstate) := closed;
    init(lstate) := locked;
    init(gstate) := extended;
    init(interruptible) := TRUE;

    /--
    Dada a introdução das novas variáveis, foi necessário especificar de forma mais
    precisa as condições necessárias para que o sistema atinja uma das fases finais.
    --/
    next(phase) := case BUTTON_CHANGES & button = down: moving_up;
                        BUTTON_CHANGES & button = up: moving_down;

                        !BUTTON_CHANGES & dstate = closed & POS_OPEN_UP: halt_up;
                        !BUTTON_CHANGES & dstate = closed & POS_OPEN_DN: halt_down;

                        TRUE: phase;
                   esac;

    /--
    Sempre que o sistema esteja em movimento, caso a porta ainda não tenha sido aberta 
    mas o cadeado já se encontra desbloqueado, esta abre-se. Sempre que porta esteja
    aberta, esta fecha-se.
    --/
    next(dstate) := case !BUTTON_CHANGES & PRE_OPEN & lstate = unlocked: open;
                         !BUTTON_CHANGES & dstate = open: closed;

                         TRUE: dstate;
                    esac;

    /--
    Sempre que o sistema esteja em movimento, caso o cadeado se encontre fechado mas 
    a porta ainda não tenha sido aberta, este desbloqueia-se. Assim que a porta já 
    tenha sido aberta e novamente fechada, este bloqueia-se.
    --/
    next(lstate) := case !BUTTON_CHANGES & lstate = locked & PRE_OPEN: unlocked;
                         !BUTTON_CHANGES & dstate = closed & POS_OPEN: locked;

                         TRUE: lstate;
                    esac;

    /--
    Se o sistema se encontra em movimento e o cadeado ainda não foi desbloqueado, 
    a próxima ação não poderá ser interrompida. Isto permite que o sistema volte a 
    um estado em que se encontre parado tal como descrito na figura 3 do enunciado.
    --/
    next(interruptible) := case BUTTON_CHANGES & lstate = locked & phase in {moving_up, moving_down}: FALSE;
                                TRUE: TRUE;
                           esac;

    /--
    Assim que as portas se abram, as engrenagens passam de 'retraídas' para 'extendidas' e
    vice-versa. Caso a direção do movimento seja alterada enquanto as portas se encontrem
    abertas, o estado das engrenagens inverte-se novamente.
    --/
    next(gstate) := case BUTTON_CHANGES & dstate = open: SWAP_GEARS;
                        next(dstate) = open: SWAP_GEARS;

                        TRUE: gstate;
                   esac;

/-- 
Decidimos tirar partido do TRANS para eliminar todas as transições em que o estado do botão
muda quando a ação não pode ser interrompida. Garantimos assim que, quando uma ação não é
interruptível, o estado do botão mantem-se constante.
--/
TRANS
    !interruptible -> next(button) = button;

/--
Aqui verificamos que o modelo construído, para além de verificar as condições impostas
pelo M1, verifica também algumas condições que consideramos necessárias para comprovar
a validade do modelo.
--/

LTLSPEC
    /--
    Foi necessário atualizar o R11bis com as novas variáveis: Para todos os estado, 
    se o botão estiver para baixo e continuar para baixo, então eventualmente vamos 
    chegar à fase halt_down e as portas vão estar fechadas.
    --/
    G (G button = down -> F (phase = halt_down & lstate = locked))

LTLSPEC
    /--
    Foi necessário atualizar o R12bis com as novas variáveis: Para todos os estados,
    se o botão estiver para cima e continuar para cima, então eventualmente vamos chegar
    à fase halt_up e as portas vão estar fechadas.
    --/
    G (G button = up -> F (phase = halt_up & lstate = locked))



LTLSPEC
    G (phase in {moving_up, halt_up} -> button = up)

LTLSPEC
    G (phase in {moving_down, halt_down} -> button = down)

LTLSPEC
    /--
    Para todos os estados que a porta se encontra aberta, o cadeado está desbloqueado.
    --/
    G (dstate = open -> lstate = unlocked)

LTLSPEC
    /--
    Para todos os estados que o cadeado se encontra bloqueado, a porta está fechada.
    --/
    G (lstate = locked -> dstate = closed)

LTLSPEC
    /--
    Sempre que a porta está aberta e o sistema está a extender-se, as engrenagens
    estão extendidas.
    --/
    G (dstate = open & phase = moving_down -> gstate = extended)

LTLSPEC
    /--
    Sempre que a porta está aberta e o sistema está a retrair-se, as engrenagens
    estão retraídas.
    --/
    G (dstate = open & phase = moving_up -> gstate = retracted)

LTLSPEC
    /--
    Sempre que a o sistema está completamento extendido, as engrenagens estão
    extendidas.
    --/
    G (phase = halt_down -> gstate = extended)

LTLSPEC
    /--
    Sempre que a o sistema está completamento retraído, as engrenagens estão
    retraídas.
    --/
    G (phase = halt_up -> gstate = retracted)

LTLSPEC
    /--
    A sequência PD2 -> CompletePD2 é ininterruptível.
    --/
    G (PRE_OPEN_UP & lstate = locked & phase = moving_down -> button = next(button))

LTLSPEC
    /--
    A sequência PU2 -> CompletePU2 é ininterruptível.
    --/
    G (PRE_OPEN_DN & lstate = locked & phase = moving_up -> button = next(button))