Go to the first, previous, next, last section, table of contents.

B New reserved words

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.