- Download the NuSMV-2.4.3 version here (version 20100824)
- Download the NuSMV-2.5.0 version here (version 20100824)
- Download the NuSMV-2.5.4 version here (version 20120913)
The tool is actually a tool chain consisting of:
- A composition script written in PHP. This script will parse and compose a base system with a feature.
- A NuSMV preprocessing script written in PHP. This script basically adds (syntactic) universal quantification to the NuSMV input language. For instance, you can write[forall i=1..n]foobar%i% : boolean;[/forall]
and the preprocessor will expand this for n = 4 into
foobar1 : boolean;
foobar2 : boolean;
foobar3 : boolean;
foobar4 : boolean;
This script is a standalone script that is independent from our NuSMV FTS extension. But since quantifiers are used in some of the examples it is included in the distribution.
- A patch for NuSMV. The patch adds a new command line switch -fbdd to NuSMV.
- For the NuSMV 2.4.3 version: A postprocessing script written in PHP. This script takes the -fbdd output of NuSMV and pretty-prints it. In the NuSMV 2.5.0 version, the pretty-printing is done by NuSMV itself.
The PHP scripts work on text and can be chained with pipes. Their parameter signature is shown if they are executed without any parameters. The composition script is also able to do normal composition as defined in the paper by Plath and Ryan.