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
解决方法:
使用LTL
:
MODULE main
IVAR
v1 : boolean;
VAR
v2 : boolean;
LTLSPEC NAME p1 := G (v1 & v2);
将v1
声明为普通变量,但将其用作输入变量。为此,不要对 v1
的初始值和未来值施加任何约束,即不要写 init(v1) :=
或 next(v1) :=
或等效约束。
模块 主要
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
解决方法:
使用
LTL
:MODULE main IVAR v1 : boolean; VAR v2 : boolean; LTLSPEC NAME p1 := G (v1 & v2);
将
v1
声明为普通变量,但将其用作输入变量。为此,不要对v1
的初始值和未来值施加任何约束,即不要写init(v1) :=
或next(v1) :=
或等效约束。