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因为您将 a 分配Bool给integer变量。您可能想先更改x = 10为10，然后更改变量的值域x并为该case ... esac构造添加一些详尽的条件。