NuXMV使用实数

我正在使用nuXmv在我正在开发的工作上，我遇到了使用Reals的麻烦。NuXMV使用实数

Supose我有计划：

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 请注意，这只是没有一个说明性的例子具体的意义。

现在的COMAND行I型

$ nuXmv <fileName>

为了运行程序，并检查是否取得财产，但出现此消息

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

所以我发现的问题是使用Real变量t。有没有办法指定一个真实值的范围，就像我在变量r（这是Integer类型）上使用的范围？我知道如果存在可以解决问题的问题，那么我该如何在我的程序中使用Reals？

预先感谢您的时间。

来源

2017-05-26 Daniel Soares

完整的错误消息，并告诉你如何来解决这个问题：

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

您可以输入交互模式电话：
./nuXmv -int file_name.smv 
或者，你可以写下你想在一个文件来执行命令，然后拨打：
./nuXmv -source <command-file> file_name.smv 

AFAIK，处理个无限域变量，预计您将利用基于SMT解算器的模型检查技术。这意味着当您使用look at the manual时，您应该将注意力集中在名称前缀或后缀为msat的命令上。

发现，有做CTL模型内nuXmv检查没有msat_命令，虽然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

你问：

是否有指定范围，像一个真正的价值的一种方式我已经变r（它是整数类型）使用？

不，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-26 14:04:21

优秀的解释上怎么运行的。实际上，我对于答案的完美程度无言以对。 –

@DanielSoares很高兴帮助，并欢迎S.O. –

NuXMV使用实数

回答

相关问题