How to use NuSMV

NuSMV is a tool to model a system as automata and to verify correctness of their operation  using temporal logic.

This program can be used in every operating system with the Java virtual machine.

Program installation in linux

Download the file NuSMV-2.6.0-zchaff-linux64.tar.gz (or a newer version) from  the website Getting the NuSMV Binary Code and unpack it to create a catalog NuSMV-2.6.0-Linux.

Change the name and position of the catalog to e.g. ~/.nusmv

Add environment paths to the file  /etc/environment, with administrator’s authorization:

  • add to the path PATH (together with the colon):
    :/home/username/.nusmv/bin
  • below add the path:
    NUSMV LIBRARY PATH=”/home/username/.nusmv/share/nusmv”
    (instead of the username write your name of the home catalogue)
  • log in again, so that the environment paths are loaded.

Configuration of the gedit notepad

NuSMV scripts are text files in an smv format. You can edit and compile them also in a text editor gedit.

Define the syntax of smv scripts so that gedit (and another dedicated program) can color their contents by placing the nusmv.lang file in a directory:

  • ∼/.local/share/gtksourceview-3.0/language-specs
    (for older versions of Gnome environment)
  • ∼/.local/share/gtksourceview-4/language-specs
    (for newer versions of Gnome environment)

Start gedit, and next:

  • enable the use of external tools, if it is disabled:
    Preferences menu » Preferences window » Plugins tab:
    check External Tools and restart the program
  • open the External Tools Management window:
    Manage External Tools… menu
  • add an external tool by clicking +
  • enter the device name, e.g. Run NuSMV
  • in the window on the right enter the smv script compilation command:
    #!/bin/sh
    ulimit -s unlimited
    NuSMV -v 1 $GEDIT CURRENT DOCUMENT NAME
    (the number after the v is a verbosity level of the program)
  • set a hotkey for automatic script compilation:
    next to Hotkey press e.g. Shift+Ctrl+N
  • set saving script before compilation:
    next to Save select Current document
  • set the script as input file:
    next to Input file select Current document
  • enable showing results of the script execution at the bottom of the screen:
    next to Output window select Display in the bottom pane
  • let each file execute:
    next to Applicability select All documents
  • select the syntax coloring method:
    click All languages and select NuSMV.

The names written in italics above are translated from Polish, and they may be different than what is shown in Your program.

If External Tools Management is not available, you (as „sudo”) should give your account (or a group with its name) „create” and „delete” file permissions for the ~/.config/gedit catalog.

Comments are closed.