NuSMV CTL specification

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?

Solution

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 to a then it must be necessarily the case that in the next statemy_var is equal to b.

This is the property you want to verify.

AF (my_var=a -> AX my_var=b)

Sooner or later, if my_var is equal to a then it must be necessarily the case that in the next statemy_var is equal to b.

Notice that an implication is true in two cases:

when the premise is true and the conclusion is true, or
when the premise is false

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 to a then it must be necessarily the case at some point in the future (wrt. the state in which my_var is equal to a) my_var becomes equal to b.

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.