Error with NuSMV -

module main var     x : 0 .. 2; assign     init (x) := 2;     next (x) :=         case             x = 2 : x = 10;         esac; spec ag x = 2 -> ag x x = 20 

at token "x": syntax error - why syntax error?

i try use keyword x never succeeded.

the problem using ltl operator within ctl formula.

in ctl, have 2 options talk next state:

• ax p : along outgoing paths, in next state p holds
• ex p : along @ least 1 of outgoing paths, in next state p holds

---

see picture:

---

as side note, have syntax error on line 6 because assigning bool integer variable. might want change x = 10 10 first, change domain of values variable x , add exhaustive conditions case ... esac construct.