------------------------------------------------------------------------
-- Generated using Kripkomat
------------------------------------------------------------------------
MODULE main
VAR
state : { STATE_I,STATE_C,STATE_D,STATE_A,STATE_B };
ASSIGN
    init(state) := STATE_I;
    next(state) :=
        case
            state = STATE_I : {STATE_A,STATE_B};
            state = STATE_C : {STATE_A};
            state = STATE_D : {STATE_B};
            state = STATE_A : {STATE_C,STATE_D};
            state = STATE_B : {STATE_C};
        esac;
DEFINE
    -- Property "p_fsm->m_b<=true"
    a := state = STATE_C | state = STATE_B;

    -- Property "p_fsm->m_a<=true"
    b := state = STATE_A | state = STATE_B;

LTLSPEC
    X b;
LTLSPEC
    F a;
LTLSPEC
    G( a -> F(b));