规格名称

Question

我想知道如何为 SMV 文件中的属性命名。

我已经这样做了，但只是从终端（见下面的代码）

NuSMV > add_property  -c -p "AG !(Object1.state = ready &  AX Object2.state = running)" -n "first"        
NuSMV > check_property

Answer 1

根据documentation，可以给每一个规格命名如下：

LTLSPEC   NAME name := ltl_expr     [;]
CTLSPEC   NAME name := (rt)ctl_expr [;]
INVARSPEC NAME name := next_expr    [;]
PSLSPEC   NAME name := psl_expr     [;]
SPEC      NAME name := (rt)ctl_expr [;]

其中 NAME 是关键字，name 是针对给定规范设计的标签。

规格名称

Specification name

ctl

nusmv