NuSMV is a tool to model a system as automata and to verify corretcness of their work, using temporal logic.
Installation on linux (e.g. Ubuntu)
- Download NuSMV from Getting the NuSMV Binary Code (the latest version is NuSMV-2.6.0-linux64.tar.gz) and unpack it in the directory /home/<user>/.NuSMV, where <user> is your system user name.
- Add environment paths to the file /etc/environment, using superuser privilledges (e.g. execute sudo gedit/etc/environment):
- Add to the PATH: /home/<user>/.NuSMV/NuSMV-2.6.0-Linux/bin
- Add below: NuSMV_LIBRARY_PATH=”/home/<user>/.NuSMV/NuSMV-2.6.0-Linux/share/nusmv”
- Log-in again, to read the new paths into the system.
How to use text editor Gedit to write and execute your smv script
The default Ubuntu text editor Gedit can colour syntax of the NuSMV script and execute it, to show results of the script verification.
Prepare Gedit to work with NuSMV:
- Execute menu Edit → Prefferences to open a window Gedit Prefferences.
- Choose the tab Plugins and switch External tools on.
- Close and open Gedit again.
- Execute menu Tools → Manage external tools… to open a window Manage external tools. If the option Manage external tools… is not available, eneable (as a superuser) for you or your group the right to create and delete files in the directory ~/.config/gedit.
- In the left pane press + and name the new tool e.g. NuSMV.
- In the right pane write:
#!/bin/sh ulimit -s unlimited NuSMV -v 1 $GEDIT_CURRENT_DOCUMENT_NAME
- In the right pane set the following fields (their names cab be different):
- shortkey: Alt+2
- save: The current document
- input file:The current document
- output window: show in the lower panel
- use for: all documents
- choose NuSMV for the button All languages.
- Add the file nusmv.lang to the directory /home/<user>/.local/share/gtksourceview-3.0/language-specs/ in order to have Gedit collored syntax of smv files. Create the directory, if it does not exist.
To execute your script in Gedit: save it and press Alt+2 (or execute menu Tools → External Tools → NuSMV). The result will show.