Error with NuSMV

Question

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 to use the keyword X but never succeeded.

Answer 1

The problem is that you are using an LTL operator within a CTL formula.

In CTL, you have two options to talk about the next state:

• AX P : along all outgoing paths, in the next state P holds
• EX P : along at least one of the outgoing paths, in the next state P holds

---

See this picture:

---

As a side note, you have a syntax error on line 6 because you are assigning a Bool to an integer variable. You might want to change x = 10 into 10 first, then change the domain of values for variable x and add some exhaustive conditions to that case ... esac construct.