sam
sam

Reputation: 53

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

Upvotes: 1

Views: 108

Answers (1)

Patrick Trentin
Patrick Trentin

Reputation: 7342

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.

Upvotes: 1

Related Questions