实数的NuXMV使用

Question

我正在使用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。请注意，这只是一个没有具体意义的示例。

现在在科曼德I行输入

$ nuXmv <fileName>

，以运行程序并检查是否已实现该属性，但将显示此消息。

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

因此，我发现的问题是在变量Real上使用t。是否有一种方法可以指定像我在变量r (wich类型为Integer)上使用的值那样的Real范围？我知道，如果存在这种情况，可以解决这个问题，如果没有，我如何在我的程序中使用Reals？

提前谢谢你抽出时间。

Answer 1

完整的错误消息确实告诉您如何绕过这个问题：

在这个版本的nuXmv中，包含无限域变量的模型不能使用批处理模式。 您可以进入交互模式调用： ./nuXmv -int file_name.smv 或者，您可以在文件中写入要执行的命令，然后调用： ./nuXmv -source file_name.smv

AFAIK，为了处理无限域变量，您应该利用基于MathSAT 5 Solver的模型检查技术。这意味着，当您使用msat作为看手册的前缀或后缀时，您应该将重点放在它们的名称中。

注意，虽然msat_ LTL和不变体模型检查是可用的，但是在nuXmv中没有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

你问：

是否有一种方法可以指定像我在变量r (类型为Integer)上使用的值那样的Real范围？

不，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.

如果要向real/integer变量添加范围约束，可以使用INVAR。

INVAR 0.0 <= rv & rv <= 500.0 ;