使用变量而不是整数时nuXmv语法错误

Question

我在muXmv中有一个模型，在这个模型中，我用一系列的值初始化-

变量x: 0..100；赋值init(x) := 10.50；

这个很好用。

但是，当我使用变量而不是值时，

分配init(x) := LB..UB；定义LB := 10；UB := 50；

它会引发语法错误-

第14行: at token ".."：语法错误

第14行:解析器错误

不知道我哪里出了问题？

还有更好的方法来声明nuxmv中的常量吗？

Answer 1

定义不一定是常量，它只是表达式的名称(其值在每次转换后可能发生变化)。(例如)

MODILE main()
VAR
    x : 0..100;
    y : 0..100;
DEFINE
    sum := x + y;

...

我不知道为什么NuSMV/nuXmv的语法不允许使用一对标识符而不是一对常量来写入间隔。

另一种选择是：

MODULE main()
VAR
    x : 0..100;

ASSIGN
  init(x) := INTERVAL;

DEFINE
  INTERVAL := 10 .. 50;

另一种选择是使用约束样式方法：

MODULE main()
VAR
    x : 0..100;

DEFINE
    LB := 10;
    UB := 50;

INIT
    LB <= x & x <= UB;

如果您真的发现自己遇到了许多常量值的问题，可以选择编写一个通用模板模型，然后使用正则表达式+脚本工具自动生成所需的各种具体模型。