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

Question

模块主要

IVAR v1 ：布尔值；

变量 v2：布尔值；

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

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

Answer 1

在 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

解决方法：

使用LTL:

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

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

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

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)?

nusmv

ctl