Next: LTL module.
Up: System Architecture
Previous: Model Checking.
The routines for counterexamples and witness generation and
inspection. Counterexamples and witnesses can be produced with
different levels of verbosity, in the form of reusable data
structures, and can subsequently be inspected and navigated. These
routines are independent of the particular method used to represent
the FSM.
NuSMV <
>