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 from Getting the NuSMV Binary Code (e.g. 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 text editor Gedit can colour syntax of the script and execute it to show results of script verification.
Prepare yourself to work with NuSMV. In Gedit:
- Execute menu Edit -> Prefferences to open a window Gedit Prefferences.
- Choose a tab Plugins and switch on External tools.
- 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 its left pane press +.
- In its 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
- 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.
To execute your script in Gedit: save it and press Alt+2. The result will show.