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
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.