NuSMVfair is an extension of the NuSMV model checker with strong fairness model checking for LTL formula. The algorithm that is implemented is described in the following conference paper:

Y. Kesten, A. Pnueli, and L. Raviv. Algorithmic Verification of Linear Temporal Logic Specifications, In K.G. Larsen, S. Skyum, and G. Winskel, editors, Proceedings of the 25th International Colloquium on Automata, Languages, and Programming (ICALP 1998), volume 1443 of Lecture Notes in Computer Science, pages 1-16. Springer-Verlag, 1998

Strongly fair LTL model checking is (currently) not possible in interactive mode. The TLV model checker supports strongly fair model checking in interactive mode (but not in batch mode).

NuSMVfair is used in connection with TCM to verify workflow models that are specified in UML activity diagrams. The additional source code for NuSMVfair is freely available.

To obtain NuSMVfair do the following:

  1. get the source distribution of NuSMV  and build it;
  2. download the additional source files for NuSMVfair: nusmvfair.tar.gz  and gunzip it;
  3. unpack the nusmvfair.tar file in the nusmv-1.1 directory;
  4. do a `make clean' on the original NuSMV source files;
  5. see the README.NuSMVfair file in the distribution for installation instructions.
The resulting executable NuSMVfair works similar to the orginal NuSMV executable, except that it has an extra option `-spec'  for the batch mode:

NuSMVfair -spec ltlspecfile intput-file

where the ltlspecfile contains an LTL formula in NuSMV syntax.
If the -spec option is used, all other options are ignored.

In the inputfile two new keywords can be used, JUSTICE and COMPASSION, in the following way:

JUSTICE j1 , j2 , .. , jn

where j1,j2,..,jn are all simple expressions, i.e., they do not contain a temporal operator

COMPASSION (p1,q1) , (p2,q2) , .. , (pn,qn)

where p1,p2,..,pn,q1,q2,..,qn are all simple expressions again.

These new keywords only have a meaning if option -spec is used. In that case, the keyword FAIRNESS and the resulting declaration is ignored; use JUSTICE instead.

Rik Eshuis (eshuis@cs.utwente.nl) , 20-9-2001