Search code examples
nusmvctl

Specification name

I want to know how to attribute names to properties inside SMV file.

I have done this but only from the terminal (see the following code) 

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

  • According to the documentation, one can assign a name to each specification as follows:

    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 [;]

    where NAME is a keyword and name is the designed label for the given specification.