syntax-error - 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-为什么语法错误？

我尝试使用关键字 X，但从未成功。

Answer 1

问题是您正在CTL公式中使用LTL运算符。

在CTL中，有两个选项可以讨论下一个状态:

AX P :沿着所有传出路径，在下一状态P拥有

EX P :沿至少一个传出路径，在下一状态P保留

看到这张图片:



附带说明，由于您正在将 6分配给 Bool变量，因此在 integer行上存在语法错误。您可能需要先将 x = 10更改为 10，然后更改变量 x的值域，并向 case ... esac构造添加一些详尽的条件。