Nusmv无法用输入变量（IVAR）检查ctl属性的错误如何处理？

【问题标题】：How to deal with the error that Nusmv cannot check ctl properties with input variables (IVAR)?Nusmv无法用输入变量（IVAR）检查ctl属性的错误如何处理？
【发布时间】：2018-04-10 06:42:11
【问题描述】：

模块主要的

伊娃 v1 ：布尔值;

VAR v2 : 布尔值;

规格名称 p1 := AG (v1&v2);

文件 ltlerror.smv：第 8 行：属性包含输入变量：

【问题讨论】：

请添加一些上下文并告诉我们您想要实现的目标

标签： nusmv ctl

【解决方案1】：

NuSMV 2.6 user manual 第 24-25 页上写着：

[...] 输入变量不能出现在：

[...]
一些规范类型：CTLSPEC、SPEC、INVARSPEC、COMPUTE、PSLSPEC。例如：
IVAR i : boolean;
VAR s : boolean;
SPEC AF (i -> s) – this is NOT allowed 
LTLSPEC F (X i -> s) – this is allowed

解决方法：

使用LTL:

MODULE main
IVAR
  v1 : boolean;
VAR
  v2 : boolean;

LTLSPEC NAME p1 := G (v1 & v2);

将v1 声明为普通变量，但将其用作输入变量。为此，不要对v1 的初始值和未来值施加任何约束，即不要写init(v1) := 或next(v1) := 或等效约束。

【讨论】：