FV: Getting Started with NuSMV & nuXmv
Installation instructions and directions on basic usage for both NuSMV and the newer fully-compatible nuXmv model checker.
Installation of NuSMV
NuSMV is already installed on the student.compute DICE machine and can be run there with the command `NuSMV' in a shell. NuSMV is a command-line program, there is no GUI. Alternatively, if you wish to install it on your own machine, visit the the NuSMV website for both the sources and compiled binaries for Windows, macOS and Linux. The latest NuSMV distribution is from 2015 and it is not clear if the distributed binaries will run on all recent OS versions. Alternatively, you could install instead the successor tool nuXmv which runs identically to NuSMV as far as this course is concerned.
Installation of nuXmv
Binaries for Linux, Mac and Windows can be downloaded from the Download section of the nuXmv website. The downloaded file includes both an executable binary, the nuXmv manual and a number of examples.
Running nuXmv on DICE machines
As of September 2023, the v2.0.0 Linux binary runs fine under the current versions of Linux available on Informatics DICE machines. The distributed file bundle is in tar format, compressed with gzip. To unpack, use
% tar xf nuXmv-2.0.0-linux64.tar.gz
This creates a directory nuXmv-2.0.0-linux64 containing the distribution directories and files. For convenience of running nuXmv, define an alias. If you unpacked the tar file in subdirectory nuxmv of your home directory, type something like:
% alias nuXmv=/home/s1234567/nuxmv/nuXmv-2.0.0-Linux/bin/nuXmv
Insert this alias command in your DICE .brc file in your home directory to have the alias defined each time you start a new shell.
Basic commands for nuXmv & NuSMV
The following instructions are written for NuSMV, but also apply to nuXmv.
The simplest way to run NuSMV is in batch mode: type NuSMV a.smv at a Unix command-line prompt to run NuSMV on file a.smv. Useful NuSMV command-line options include:
- -n i
Check only specification i (numbered from 0). If there are both CTL and LTL specifications, then the CTL specifications are numbered first. - -dcx
Disable display of counter-examples to false specifications
NuSMV also has an interactive mode which allows much finer control of NuSMV's behaviour. To run in interactive mode on file a.smv, use the command NuSMV -int a.smv. Useful commands at the NuSMV> interactive prompt include
- go
Run the commands read_model, flatten_hierarchy, encode_variables, build_model. This gets NuSMV ready for doing model checking. - check_ltlspec
Model check each of the LTL specifications from the SMV source file.- Use option "-n i" to check only the specification with index i (starting from 0).
- Use option "-P name" to check only the specification named name.
- pick_state
Pick an initial state for a simulation of the model. - simulate -p n
Run a simulation for n steps, printing out at each step the values of state variables that have changed. When there are multiple next states, the choice is deterministic. Options for the simulate and pick_state commands allow random and interactive choices of states. - quit
Exit NuSMV
For a brief description of the options supported by a command, run the command with option -h.
For further details, consult the following NuSMV and nuXmv documentation: