One of the most important functionalities of symbolic model checking is the ability to generate a counterexample for unsatisfied properties. The algorithms used in NUSMV as a basis to perform the computation of counterexamples are the same as those implemented in CMU SMV and are those presented in [24].
>