m3.smv

MODULE main

/--
Na terceira fase é adicionado o pormenor das engrenagens. Agora, quando as portas são
abertas, as engrenagens transitam gradualmente até que se encontrem totalmente extendidas
ou retraídas, dependendo do estado em que se encontravam gradualmente. Esta transição não
pode ser interrompida pelo piloto.

Segundo a figura 4 do enunciado, quando o piloto interrompe o sistema após as engrenagens
terem sido completamente extendidas (retraídas), estas passam imediatamente a retraídas
(extendidas) sem passar pelos estados intermédios.
--/

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

    dstate: {open, closed};
    lstate: {locked, unlocked};
    interruptible: boolean;

    /--
    A variável 'gstate', que no M2 era apenas uma variável auxiliar, é agora uma variável
    que descreve um dos componentes a ser modelados: as engrenagens. Dado o aumento de
    complexidade no movimento das engrenagens, foi necessário acrescentar novos estados.
    --/
    gstate: {extended, extending, retracted, retracting};
    
DEFINE
    BUTTON_CHANGES := button != next(button);
    SWAP_GEARS := gstate = extended ? retracted : extended;

    /--
    Dado o aumento de complexidade nos estados em que a porta está aberta foi necessário
    especificar mais detalhe quando é esta ainda não se encontra aberta.
    --/
    PRE_OPEN_UP := dstate = closed & phase = moving_up & gstate = extended;
    POS_OPEN_UP := dstate = closed & phase = moving_up & gstate = retracted;   
    PRE_OPEN_DN := dstate = closed & phase = moving_down & gstate = retracted;
    POS_OPEN_DN := dstate = closed & phase = moving_down & gstate = extended;

    PRE_OPEN := PRE_OPEN_UP | PRE_OPEN_DN;
    POS_OPEN := POS_OPEN_UP | POS_OPEN_DN;

    /--
    Estas três novas cláusulas descrevem o momento em que as engrenagens terminam a sua
    extensão/retração.
    --/
    GEARS_MOVED_DN := phase = moving_down & gstate = extended;
    GEARS_MOVED_UP := phase = moving_up & gstate = retracted;
    GEARS_MOVED := GEARS_MOVED_DN | GEARS_MOVED_UP;

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

    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;

    /--
    Anteriormente a porta era fechada sempre que estivesse aberta. Nesta terceira fase
    é necessário esperar que as engrenagens se extendam/retraiam.
    --/
    next(dstate) := case !BUTTON_CHANGES & PRE_OPEN & lstate = unlocked: open;
                         !BUTTON_CHANGES & dstate = open & GEARS_MOVED: closed;

                         TRUE: dstate;
                    esac;

    next(lstate) := case !BUTTON_CHANGES & lstate = locked & PRE_OPEN: unlocked;
                         !BUTTON_CHANGES & dstate = closed & POS_OPEN: locked;

                         TRUE: lstate;
                    esac;

    /--
    Nesta fase foram adicionados novos estados que não podem ser interrompidos. Estes
    devem-se ao facto que, quando o processo de extensão/retração é iniciado, este não
    pode ser interrompido.
    --/
    next(interruptible) := case BUTTON_CHANGES & lstate = locked & phase in {moving_up, moving_down}: FALSE;
                                dstate = closed & next(dstate) = open: FALSE;
                                next(gstate) in {retracting, extending}: FALSE;

                                TRUE: TRUE;
                           esac;

    /--
    Quando as portas se encontra abertas, o sistema de retração/extensão inicia-se,
    fazendo com que as engrenagens se comecem a mover. Quando estas se estão a mover,
    no próximo ficam completamente retraídas/extendidas.

    Quando o processo de mover as engrenagens termina, caso o piloto altere o estado do
    botão, as engrenagens passam de extendidas (retraídas) a retraídas (extendidas) sem
    passar novamente pelos estados de transição.
    --/
    next(gstate) := case dstate = open & phase = moving_down & gstate = retracted: extending;
                         dstate = open & phase = moving_up & gstate = extended: retracting;
                         gstate = extending: extended;
                         gstate = retracting: retracted;
                         BUTTON_CHANGES & dstate = open: SWAP_GEARS;

                         TRUE: gstate;
                    esac;

TRANS
    !interruptible -> next(button) = button;

/--
Aqui verificamos que o modelo construído, para além de verificar as condições impostas
por M2, verifica também algumas novas condições que consideramos necessárias para
comprovar a validade do modelo. Verificamos também que os requisitos R21 e R22 são
cumpridos.

Dois dos requisitos impostos por M2 relativos ao momento em que a porta se encontra
aberta foram retirados por não fazerem sentido nesta terceira fase.
--/

LTLSPEC
    G (G button = down -> F (phase = halt_down & lstate = locked))

LTLSPEC
    G (G button = up -> F (phase = halt_up & lstate = locked))

LTLSPEC
    /--
    R21: Se o botão estiver para baixo então a sequência de retração não se verifica.
    --/
    G (G button = down -> gstate != retracting)

LTLSPEC
    /--
    R22: Se o botão estiver para cima então a sequência de extensão não se verifica.
    --/
    G (G button = up -> gstate != extending)



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

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

LTLSPEC
    G (dstate = open -> lstate = unlocked)

LTLSPEC
    G (lstate = locked -> dstate = closed)

LTLSPEC
    G (phase = halt_down -> gstate = extended)

LTLSPEC
    G (phase = halt_up -> gstate = retracted)

LTLSPEC
    G (PRE_OPEN_UP & lstate = locked & phase = moving_down -> !BUTTON_CHANGES)

LTLSPEC
    G (PRE_OPEN_DN & lstate = locked & phase = moving_up -> !BUTTON_CHANGES)

LTLSPEC
    /--
    A sequência opening_up -> retracting_gears é ininterruptível.
    --/
    G (dstate = open & gstate = extended & phase = moving_up -> !BUTTON_CHANGES) 

LTLSPEC
    /--
    A sequência opening_up -> extending_gears é ininterruptível.
    --/
    G (dstate = open & gstate = retracted & phase = moving_down -> !BUTTON_CHANGES) 

LTLSPEC
    /--
    As sequências retracting_gears -> retraction e extending_gears -> extension são
    ininterruptíveis.
    --/
    G (gstate in {retracting, extending} -> !BUTTON_CHANGES)

LTLSPEC
    /--
    Se o sistema está a realizar a sequência de retração/extensão, a porta encontra-se
    aberta.
    --/
    G (gstate in {retracting, extending} -> dstate = open)

LTLSPEC
    /--
    Se o sistema não está a realizar a sequência de retração/extensão, as engrenagens
    ou estão completamente retraídas ou estão completamente extendidas.
    --/
    G (dstate = closed -> gstate in {retracted, extended})