syntax - nuXmv syntax error when using variable instead of integer

Question

I have a model in muXmv, where I initialize with a range of values like -

VAR 
  x : 0..100;
ASSIGN
  init(x) := 10..50;

this works perfectly fine.

However, when I use variable instead of values,

ASSIGN 
  init(x) := LB..UB;

DEFINE
  LB := 10;
  UB := 50;

it throw syntax error -

line 14: at token "..": syntax error

line 14: Parser error

Not sure where I am going wrong?

Also is there a better way to declare constants in nuxmv?

score 0 · Accepted Answer

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

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;

如果您真的发现自己在为许多常量值而苦恼，一个选择是编写一个通用的TEMPLATE模型，然后使用正则表达式+脚本工具来自动生成您需要的各种具体模型。

1 回答 1