We assume that every NuSMV command is followed by a
RET keystroke. In the following examples,
NuSMV commands are written in a bold face to
distinguish them from system output messages.
In NuSMV a LTL specification are introduced by
the keyword `LTLSPEC' (see section LTL Specifications).
In the current version of
NuSMV, compassion constraints are supported only for BDD-based
LTL model checking. We plan to add support for compassion constraints
also for CTL specifications and in Bounded Model Checking in the next
releases of NuSMV.
This document was generated on 9 July 2002 using texi2html 1.56k.