next up previous
Next: LTL module. Up: System Architecture Previous: Model Checking.

Explanation module.

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 <>