Symbolic Tool Models
Next: Input Formulas Up: Model Checking Benchmarking Scripts Previous: Explicit Tool Models

Symbolic Tool Models

We can also benchmark LTL formula modeling with CadenceSMV and NuSMV. To check whether a LTL formula $\varphi$ is satisfiable, we model check $\neg\varphi$ against a universal SMV model. For example, if $\varphi = (X (a))$ , we provide the following input to NuSMV:

MODULE main
  VAR
    a : boolean;
    b : boolean;
    c : boolean;
  LTLSPEC !(X(a=1 ))
  FAIRNESS
    1

(The ``FAIRNESS'' line varies with versions of NuSMV. The CadenceSMV model is very similar.) SMV negates the specification, $\neg\varphi$ , symbolically compiles $\varphi$ into $A_{\varphi }$ , and conjoins $A_{\varphi }$ with the universal model. If the automaton is not empty, then SMV finds a fair path, which satisfies the formula $\varphi$ . In this way, SMV acts as both a symbolic compiler and a search engine.

Kristin Yvonne Rozier 2007-05-10