Go to the first, previous, next, last section, table of contents.
The list of the new reserved words of NuSMV w.r.t. CMU
SMV is the following:
F
-
It is the sometimes temporal operator. It is used to write LTL
formulas.
G
-
It is the always temporal operator. It is used to write LTL
formulas.
X
-
It is the next time temporal operator. It is used to write LTL
formulas.
LTLSPEC
-
It is used to introduce LTL specifications.
INVARSPEC
-
It is used to introduce invariant specifications.
IVAR
-
It is used to introduce input variables.
Go to the first, previous, next, last section, table of contents.