Component-Oriented Interpolation

Introduction

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).

Sources

The zipfile containing the source code can be downloaded here.

Compilation

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

Cleaning

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”.

Code Organization

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.

Usage

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.

Licenses

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.