This page contains the source code holding modifications to NuSMV 2.5.4 and MiniSAT 1.14p for component-oriented interpolation. A report on this work can be found in "Compositional Analysis Using Component-Oriented Interpolation" (in submission).
The zipfile containing the source code can be downloaded here.
Ensure you have GCC, make and the autoconf tools installed. Then do the following:
1. cd cudd-2.4.1.1
2. make
3. cd ../MiniSAT
4. ./build.sh
5. cd ../nusmv
6. autoreconf -i
7. ./configure --enable-addons=isc
8. make
After compilation, you will find a binary
called "NuSMV"
Furthermore note that the command ÒautoreconfÓ has to be launched whenever the automake scripts are modified (e.g. new source files added), or if the files generated by automake are deleted. Depending on the architecture (i.e. 32 versus 64 bit), separate makefiles exist for the CUDD package (see cudd folder). For further compilation options for nusmv, run Ò./configure –helpÓ. Debugging code for the ISC package can be enabled in the file ÒiscInt.hÓ. The two flags are:
á ISC DEBUG enables all the debugging and development helpers including automatic sanity checks
á ISC CONSISTENCY CHECKS enables checks for validation of the component-oriented interpolated environment transition relation
1. cd MiniSat
2. ./clean.sh
3. cd cudd-2.4.1.1
4. make clean
5. cd nusmv
6. make clean
Instead of Òmake cleanÓ one can also use Òmake distcleanÓ, which removes almost all generated files. In this case it is necessary to re-run ÒconfigureÓ.
For this project we used ÒMiniSat v1.14 (with proof logging)Ó, and added functionalities for storing the proof graph in a data structure that can be accessed from NuSMV. See files Solver C.h for interface functions between NuSMV and Minisat.
The main part of this projects contribution is located in the package ÒiscÓ. For branch 2.5.4, this is in Ònusmv/src/addons-core/iscÓ, and for branch 2.4.3 it is in Ònusmv/src/iscÓ. Beside these new files, modifications were made in the packages ÒbeÓ, ÒrbcÓ, Òsat/solversÓ, plus a few system files and automake scripts to accomodate the new ÒiscÓ package. For a detailed display of the differences and additions one can use a directory-wide diff program such as Meld1, and compare the vanilla nusmv sources with the project sources.
The new functionalities added by this project are accessible through the command "isc check invar", and has the following command line options.
usage: isc check invar -a "algorithm" (-n idx — -p "formula") [-m "module"] [-s "splitmode"] [-h]
á -a "algorithm". Uses the specified algorithm. Valid values are: noitp, noitpsplit, standard, compositional.
á -n idx. Checks the INVAR property specified with <idx>.
á -p "formula". Checks the specified INVAR property.
á -m "module". Module name for module/environment split.
á -s "splitmode". Valid values are: formula_modules, formula_variables, formula_component (incompatible with '-m').
á -h. Prints the command usage. The options are now discussed in more detail.
These are the available algorithms:
á noitp: Only available in debugging mode. This is a simple BMC-based algorithm that checks if the invariant holds up to a certain bound k.
á noitpsplit: Only available in debugging mode. Same as noitp, but internally it uses two FSMs, one for the component of interest, and one for the environment. It requires a split specification (flags -s or -m).
á standard: This is the McMillan algorithm for verifying invariant properties.
á compositional: This is the component-oriented interpolation algorithm for verifying invariant properties. It requires a split specification (flags -s or -m).
The property of interest can be specified with the flags -n and -p. To identify the index of a property specified in the SMV file, type Òshow propertyÓ at the NuSMV command prompt.
NuSMV and the changes we made to it are under Lesser GPL 2.1. The package also contains CUDD and MiniSAT, which are licensed under their respective licenses.