Next:
Symbolic Tool Models Up: Model Checking Benchmarking Scripts Previous: Model Checking Benchmarking Scripts

Explicit Tool Models

To benchmark LTL formula translations, we use for the SPIN model a universal Promela program, enumerating all possible traces over $Prop$. For example, when $Prop = \{a, b\}$, (and therefore the number $n$of variables is 2), the Promela model is:

/*File: 2vars.pml*/

bool A,B;

/* define an active procedure to generate values for A and B */

active proctype generateValues()
{ do
   :: atomic{ A = 0; B = 0; }
   :: atomic{ A = 0; B = 1; }
   :: atomic{ A = 1; B = 0; }
   :: atomic{ A = 1; B = 1; }
  od }

We use the atomic{} construct to ensure that the Boolean variables change value in one unbreakable step. Note that the size of this model is exponential in the number of atomic propositions.

The variables in $Prop$are defined in the accompanying file 2vars.define , which is prepended to the never-claim we are testing.

These two files are generated automatically for any given value of $n$by any one of the following scripts. (Just for simplicity, there are 3 versions of the same script here.):


Script Name Variable Set Recommended Input Formulas
generateValues.pl Prop = a, b, c, ..., aa, bb, cc, ... Use with random and counter formulas.
generatePvalues.pl Prop = p1, p2, p3, ... Use with pattern formulas.
generateAlphaPvalues.pl Prop = po, pt, ph, ... Use with pattern formulas, for tools
    which don't allow numbers in variable names


Usage: generateValues.pl number_of_variables


Here is an example of how to use these scripts to run SPIN on a generated Promela never-claim with a universal model:

#Preceed the formula with a 'next time' operator to skip
#  SPIN's nondeterministic assignment upon declaration
$LTL_to_automata_tool_binary ``(X($input_formula))" >& $temp #generate the automaton
generateValues.pl $n
cp -f $nvars.define pan.ltl
cat $temp � pan.ltl
rm -f $temp
cp -f $nvars.pml pan_in
spin -a -X -N pan.ltl pan_in
gcc -w -o pan -D_POSIX_SOURCE -DMEMLIM=128 -DXUSAFE -DNOFAIR  pan.c
./pan -v -X -m10000 -w19  -a -c1



Next:
Symbolic Tool Models Up:Model Checking Benchmarking Scripts Previous:Model Checking Benchmarking Scripts
Kristin Yvonne Rozier 2007-05-10