I have started learning NuSMV these days. I have this code:
MODULE main
VAR
state: {a,b,c,d,e};
ASSIGN
init(state) := a;
next(state) := case
(state = a) : b;
(state = b) : c;
(state = c) : d;
(state = d) : e;
TRUE:Stages;
esac;
I want to verify that every time we are in the state "a" the next state will be the state "b". which one is the correct (even if I tried both of them and they give me both of them true):
check_ctlspec -p "AG (state=a -> AX state=b)"
check_ctlspec -p "AF (state=a -> AX state=b)"
check_ctlspec -p "AF (state=a -> AF state=b)"
check_ctlspec -p "AF (state=a -> state=b)"
My second question is: In the model above there is no a transition from the state "d" to the state "a" but when I verify this using
check_ctlspec -p "AF (state=d -> AX state=a)"
the result was true. Why is this the case?
First of all, let me rename state
with my_var
in your model. This avoids confusing the actual state of the automaton with the state
variable you have introduced.
AG (my_var = a -> AX my_var = b)
In every state of every possible execution, if
my_var
is equal toa
then it must be necessarily the case that in the next statemy_var
is equal tob
.
This is the property you want to verify.
AF (my_var=a -> AX my_var=b)
Sooner or later, if
my_var
is equal toa
then it must be necessarily the case that in the next statemy_var
is equal tob
.
Notice that an implication is true in two cases:
So the implication is trivially made true by any state for which the premise my_var=a
is not verified, that is, any state other than the initial state. Since you use AF
, you require the implication to be verified only on (at least) one state for each possible execution path.
In a sense, this is "too weak" with respect to what you want to verify.
AF (my_var=a -> AF my_var=b)
Sooner or later, if
my_var
is equal toa
then it must be necessarily the case at some point in the future (wrt. the state in whichmy_var
is equal toa
)my_var
becomes equal tob
.
Similar as previous one, this is even weaker because it does not even specify at what point my_var
becomes equal to b
.
AF (my_var=a -> my_var=b)
Notice that the implication (my_var=a -> my_var=b)
is only true when my_var=a
is false, because my_var
cannot be con-temporarily assigned to both a
and b
. Nevertheless, this condition is verified by any state other than the initial state, so again the property is trivially verified.
AF (my_var=d -> AX my_var=a)
Again, this condition is too weak because you are using AF
and not AG
. The implication is made true by any state for which my_var != d
, so it is sufficient for the whole property to be verified.
I would invite you to take a look to this stack-overflow Q/A or to these slides for learning more about the tool and the language.