Computer Science Department Logo
15-414 Bug Catching: Automated Program Verification and Testing
Main Page
  
Main Page 
 
Lecture Schedule, Notes and Readings
Assignments, Exams and Solutions
 Syllabus
Assignments
Grading and Policies
Textbook and Other Resources
Grading 
Reading 
Professor
Professor 
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)