The ability to generate counterexamples for properties that are not verified is very useful in the design phase and is common to the majority of model checkers. In NUSMV it is also possible to navigate and inspect counterexamples, similarly to what a programmer can do in a debugger for a programming language. The user can jump from state to state, possibly between different counterexamples, and evaluate CTL expressions in a given state of a counterexample, thus generating a possible new debug trace. These functionalities are available via commands of the interactive shell.
>