31 lines
757 B
Plaintext
31 lines
757 B
Plaintext
|
|
------------------------------------------------------------------------
|
|
-- 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_B;
|
|
|
|
LTLSPEC
|
|
X b;
|
|
LTLSPEC
|
|
F a;
|
|
LTLSPEC
|
|
G( a -> F(b));
|