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。请注意，这只是一个示例，没有具体含义。

现在我在命令行输入

$ nuXmv <fileName>

为了运行程序，检查属性是否实现，但是出现这个信息

"In this version of nuXmv, batch mode is not available with models containing infinite domain variables."

所以我确定的问题是在变量 t 上使用 Real。有没有一种方法可以指定一系列 Real 值，就像我在变量 r 上使用的那样（它是 Integer 类型）？我知道如果存在可以解决问题的方法，如果不存在，我该如何在我的程序中使用 Reals？

提前感谢您的宝贵时间。

Answer 1

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

In this version of nuXmv, batch mode is not available with models containing infinite domain variables.

You can enter interactive mode calling:
./nuXmv -int file_name.smv
Alternatively, you can write the commands you want to execute in a file and then call:
./nuXmv -source <command-file> file_name.smv

AFAIK，要处理无限域变量，您应该利用基于MathSAT 5 SMT Solver. This means that you should focus on commands which have msat as prefix or suffix in their name when you look at the manual.

请注意 nuXmv 中没有 msat_ 命令用于执行 CTL 模型检查，尽管 LTL和不变模型检查可用，所以你应该改变你的属性

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

你问：

Is there a way to specify a range of Real values like the one I have used on variable r (which is of type 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.

如果你想给一个real/integer变量添加范围约束，你可以使用INVAR:

INVAR 0.0 <= rv & rv <= 500.0 ;

NuXMV 使用实数

NuXMV use of Real numbers

model-checking

nuxmv