CSCI P545 Computer Science Department Indiana University Mon Mar 3 13:02:36 EST 2008 © [SDJ]

Introduction to SMV

The lecture notes Example: The Observer-Reporter Problem [PDF] explains how this problem can be modeled in SMV. The SMV source file or.smv contains the resulting model.

Running SMV

You can obtain a copy of SMV from Cadence Berkely Labs, or run it on any CS Linux machine. The graphical interface for SMV is called vw. To configure vw, you need to set environment variables. Add the following commands to your shell initialization file: 
setenv SMV_DIR /l/ddd/smv
setenv PATH $SMV_DIR/bin:$PATH
setenv MANPATH $SMV_DIR/man:$MANPATH
setenv LD_LIBRARY_PATH $SMV_DIR/lib:$LD_LIBRARY_PATH
NOTE: This example uses the TCSH command-line shell whose initialization file is ~/.cshrc. Other shells have (e.g. BASH) have different syntax for setting ENV variables, and different initialization files. It is a good idea, to enter these commands manually first, to verify that they work. If not, the likely reason is that LD_LIBRAY_PATH does not exist in your environment. In this case, omit the ":$LD_LIBRARY_PATH" from the last line above. The vi program is at /l/ddd/smv/bin/vw.

Part A

  1. Run vw on or.smv and verify the SPEC formulas.
  2. Examine the counter-examples to determine what they say.
  3. Add a SPEC formula to or.smv saying, "It is (im)possible for an event to be counted more than once." Again use vw, to generate a trace in which a single event is counted more than once.
  4. Is it possible to count a single even two, three, or four times? Add SPEC statements to verify this and generate counter-scenarios.
  5. Write a explanation of these results and include it in your directory under the name or-report