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构造添加一些详尽的条件。