2

我在我正在开发的作品上使用nuXmv，但我在使用 Reals 时遇到了麻烦。

假设我有程序：

MODULE main

VAR
  t : Real;
  r : 0..5000;

ASSIGN
  init(t):=0;
  init(r):=0;

TRANS
    case
      r>=500 :next(r)=0 & next(t)=0 & r<600;
      r<500 : next(t)-t>0 -> next(r)=r+t & next(r)<600;
    esac;

SPEC
    AG r<=600

我试图证明的这个例子的属性是 r 总是小于或等于 600。请注意，这只是一个说明性的例子，没有具体含义。

现在在命令行上我输入

$ nuXmv <fileName>

为了运行程序并检查属性是否实现，但出现此消息

“在这个版本的 nuXmv 中，批处理模式不适用于包含无限域变量的模型。”

所以我发现的问题是使用Realon variable t。有没有办法像我在变量上使用的那样指定一系列实数值r（它是整数类型）？我知道如果这存在可以解决问题，如果没有，我如何在我的程序中使用 Reals？

提前感谢您的宝贵时间。

4

1 回答 1

1

完整的错误消息确实告诉您如何解决此问题：

在这个版本的 nuXmv 中，批处理模式不适用于包含无限域变量的模型。

您可以进入交互模式调用：

./nuXmv -int file_name.smv

或者，您可以将要执行的命令写入文件中，然后调用：

./nuXmv -source <command-file> file_name.smv

AFAIK，为了处理无限的域变量，您应该利用基于MathSAT 5 SMT Solver 的模型检查技术。这意味着当您查看手册msat时，您应该关注名称中带有 as 前缀或后缀的命令。

请注意，尽管LTL 和不变模型检查可用，但在nuXmv中没有msat_用于执行CTL 模型检查的命令，因此您应该更改您的属性

SPEC AG r <= 600

进入

LTLSPEC G r <= 600

然后，您可以按如下方式验证模型：

     ~$ nuXmv -int
nuXmv > reset ;
nuXmv > read_model -i file_name.smv ;
nuXmv > go_msat ;
nuXmv > msat_check_ltlspec_bmc

你问：

有没有一种方法可以指定一系列 Real 值，例如我在变量上使用的值r（其类型为 Integer）？

不，0.0..500.0是非法的。

您有以下选择

rv : real ;      -- can represent any rational value, infinite domain
iv : integer ;   -- can represent any integer value, infinite domain
fv : LB..UB ;    -- can represent any integer value in the domain [LB, UB]
sv : {0, 2, 4} ; -- can represent either 0, 2 or 4.

如果要向实数/整数变量添加范围约束，可以使用INVAR：

INVAR 0.0 <= rv & rv <= 500.0 ;
于 2017-05-26T14:04:21.260 回答