Nusmv cannot check ctl properties with input variables (IVAR) 报错如何处理?

How to deal with the error that Nusmv cannot check ctl properties with input variables (IVAR)?

模块 主要

IVAR v1 :布尔值;

变量 v2:布尔值;

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

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

NuSMV 2.6 user manual 的第 24-25 页,它写道:

[...] input variables cannot occur in:

[...]

  • Some specification kinds: CTLSPEC, SPEC, INVARSPEC, COMPUTE, PSLSPEC. For example:

    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) := 或等效约束。