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.