NuSMV for Fairness
On this page one can find the source code of the prototype tool where we implemented our algorithm for fair formulas in LTL. We also give some fair formulas in different categories. The source code can be downloaded here NuSMV-2.5.4.
Note that the source code has only been tested on an Ubuntu system. To build the source code, please do the following steps:
go to directory NuSMV-2.5.4
cd cudd-2.4.1.1
make -f <Make_file_consistent_with_your_system>
cd ../nusmv
./configure
make
It may take a while to build the executable file which by default has the name NuSMV. After that, one may want to print the usage of NuSMV by following command:
./NuSMV -h
To use our algorithm to check fair formulas, please type
./NuSMV -fairltl <model_file>
To use the original algorithm in NuSMV, one can type
./NuSMV <model_fil
If permission problem occurs, use following command to make them executable
chmod +x <executable_file>
We also provide several cases in different categories. One can download them below.