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

Question

模块 主要

IVAR v1 ：布尔值；

VAR v2：布尔值；

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

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

Answer 1

在NuSMV 2.6 用户手册的第 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
  

---

解决方法：

1. 使用LTL：

   MODULE main
   IVAR
     v1 : boolean;
   VAR
     v2 : boolean;
   
   LTLSPEC NAME p1 := G (v1 & v2);
   

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