T-79.146 Logic in Computer Science: Special Topics I Spring 2005 Instructions for the SMV tool needed in the third home assignment This note explains how to use SMV tool in Computing Centre workstations. The SMV software has been installed to the Computing Centre Linux workstations (see http://www.hut.fi/atk/luokat/). Some examples and SMV manual can be found from directory /v/gen/misc/smv/latest/. If you prefer to use SMV on your own PC, you can download the SMV source on http://www-2.cs.cmu.edu/~modelcheck/smv.html and follow the installation instructions therein. In part two of home assignment 3, you need to write CTL formulas in the CTL syntax for SMV which can be found on p. 13 of the SMV manual (see /v/gen/misc/smv/latest/doc/smvmanual.ps ). Once you have written down the CTL formulas and logged in a workstation you may proceed in the following way. 1. Make a directory for the analysis and copy the model of the mutual exclusion algorithm there from the course web page. (Suppose we name the file as kt3.smv) 2. Add the CTL formulas in the end of the model file by inserting a line SPEC ctl_form for each formula ctl_form. For instance, if the desired property is "All executions of the system can reach a state where process 3 is in the critical section and process 2 is in the trying section", then we add the line SPEC AF (state3 = c3 & state2=t2) in the end of the file kt3.smv . NOTE. In earlier versions of the SMV manual there was a small inaccuracy in the definition of the syntax of until path formulas where parentheses "[" ... "]" were missing. Actually SMV requires that until formulas are written, for example, as follows SPEC A [state1 = t2 U state2 = c2] as described in the latest version of the manual (see e.g. /v/gen/misc/smv/latest/doc/smvmanual.ps ). 3. Check the properties with SMV using the Unix command smv input_file SMV then outputs the verification results, together with possible counterexamples for the formulas. For instance, when SMV is run on the above example input file, SMV produces the following output: ----------------------------------------------------------------- bash-2.05a$ smv kt3.smv -- specification AF (state3 = c3 & state2 = t3) is false -- as demonstrated by the following execution sequence state 1.1: state1 = n1 state2 = n2 state3 = n3 turn = 1 state 1.2: state1 = t1 state2 = t2 state3 = t3 -- loop starts here -- state 1.3: state1 = c1 state 1.4: state1 = n1 state 1.5: state1 = t1 state2 = c2 state3 = c3 state 1.6: state2 = n2 state3 = n3 state 1.7: state1 = c1 state2 = t2 state3 = t3 resources used: user time: 0.01 s, system time: 0 s BDD nodes allocated: 2102 Bytes allocated: 1245184 BDD nodes representing transition relation: 94 + 10 bash-2.05a$ -----------------------------------------------------------------