Extended NuSMV.
The NuSMV project is a symbolic model checker
originated by CMU and ITC-irst
As an exercise, we adapted NuSMV (ver 2.4.3) and made it support ETL and AFL symbolic model
checking and enable users to customize temporal connectives.
The adapted version of NuSMV can be freely downloaded via the below links.
Here is the user manual. Compilation and Installation
Download enusmv.tar.gz and uncompress it.
Compile the cudd library:
> cd cudd-<ver> %
Currently, <ver> is 2.4.1.0
> make
% Notice that you might use a "-f Makefile_64bit"
parameter on a 64-bit mechine.
Complie NuSMV:
> cd nusmv
> ./configure %
Note: this step provides richful options. For example, if you want to filinaly install NuSMV in a desired directory, you might need
the suffix "--prefix=<dir>", here <dir> must be an
absolute path; and on a 64-bit mechine, the option "--with-expat-libdir=/usr/lib64"
is needed to specify an extra 64-bit library path.
make
make check %
This step is optional.
make install
Test and Run.
If you've down loaded and tested it, it is appreciated to inform Wanwei Liu(wwliu \at nudt.edu.cn).
And it is gratitude to report bugs (on ETL/AFL part) to us.