15-414 Assignments, NuSMV Information
 

The NuSMV Website (download here)

NuSMV Tutorial (pdf) (ps)

Location for using NuSMV on unix.andrew.cmu.edu:
/afs/andrew.cmu.edu/usr24/mtschant/15414-f07/NuSMV-2.4.3-i686-pc-linux-gnu/bin/NuSMV

To model check the file counter.smv, use:
/afs/andrew.cmu.edu/usr24/mtschant/15414-f07/NuSMV-2.4.3-i686-pc-linux-gnu/bin/NuSMV counter.smv
in the directory that hold counter.smv

To run NuSMV interactively, use the -int option. For example:
/afs/andrew.cmu.edu/usr24/mtschant/15414-f07/NuSMV-2.4.3-i686-pc-linux-gnu/bin/NuSMV -int counter.smv
Some useful commands for interactive mode are:
  • go -- compile the file into a FSM (run first)
  • pick_state -- start at the start state (run second)
  • simulate -r 5 -- simulate five random transisitions (run third)
  • show_traces -v -- show the simulation (run forth)
  • check_ctlspec -- do model checking for CTL (can run right after go)
  • quit -- exit (run last)