Usage of LWAASpin

SPIN compile-time options

-DLWAA This option compiles SPIN with the LWAA extension. If omitted, the original SPIN version 4.1.1 is compiled.
-DLWAA_USEBDD This option enables the use of BDDs for successor calculation (see for an explanation of the algorithm). Using BDDs will produce larger pan sources, but it can be faster under given circumstances. As using the direct algorithm seems more convenient (although we cannot claim that it is), we opted to use the direct approach as a default and have the BDD-based approach as a backup option.
-DBFTYPE This option sets the width of the data type used to store bitfields. Can be set to 32 (default) and 8, using a 32bit-word, or a byte accordingly. It is recommended to use the 32 default, unless you are in a very tight situation with your memory (and got the pan sources compiled).

SPIN runtime-options

-L Enables the use of linear weak alternating automata for liveness prop-
erty checking. The LTL formula has to be passed with either -f or -F. LWAASpin will output some statistics on the LWAA and generate the code accordingly.

PAN compile-time options

-DTARJAN Use Tarjan's algorithm instead of the CVWY algorithm normally
employed in SPIN. This option implies some other options, like -DNOFAIR, and disables options like -DHC. If a collision is detected, pan will inform you on invocation.

PAN COMPILE-TIME OPTIONS

-DLWAA Again, this option is required to enable the linear weak alternating algorithm in SPIN. If omitted, the formula passed to LWAASpin cannot be checked, however safety checking is still possible. This option implies -DTARJAN, which in turn implies other options, like mentioned above.
-DLWAA_STAT Output some statistics to a file named <input>.stat. This file contains a line with the following tab-separated fields:
  • a field with CE if a counterexample was found, and NOCE otherwise
  • three fields containing the number of successor calculation, the total sum of successors calculated (containing duplicates, of course) and the maximum number of successors calculated for a single configuration graph state
  • three fields containing the number of SCCs detected, the number of elements found in SCCs and the maximum size of a SCC found
  • a field containing the number of trivial SCCs, that is dead ends or states leading into a SCC, but not being included in one
  • a field containing the depth of the root node of the satisfying SCC in the recursion stack (0 if no counterexample was found)
  • a field containing the size of the scc stack at the point of detecting the satisfying SCC (1 if no counterexample was found)
  • a field containing the length of the counterexample (0 if no counterexample was found)
  • five fields containing information about the linear weak alternating automaton: the number of locations, the number of locations with an odd rank, the total number of transitions, the maximum number of transitions for any node, and the rank of the root node (which is the maximum rank encountered)
  • finally, a field with the name of the input file
A second line is written by the successor calculation package. It contains
  • if the BDD-Package is used, six values:
    • the token "BDD"
    • the number of BDD nodes built
    • the number of BDD hash table resolutions
    • the number of BDD hash table collisions
    • the number of BDD cache resolutions
    • the number of BDD cache collisions
  • if the BMP-approach is used, six values:
    • the token "BMP"
    • two fields: the number of pages allocated, and the size of a page
    • two fields: the total number of successor configurations seen, and the number of successor configurations pruned (number of successor configurations evaluated is the first minus the second value)
    • one field: the maximum number of successor configurations pruned for an automaton configuration
Our distribution contains a tool named lwaastats that will print the resulting file in an understandable way.
-DLWAA_NOCE Disables the extended algorithm for counterexample extraction. As mentioned in , this requires additional data which will increase the size of the SCC stack. As longer counterexamples are mostly ununderstandable anyway, they can be turned off using this option. pan will output a warning and use SPIN's algorithm. The counterexample might be missing important chunks, but the run will be valid. If you do not care about counterexamples anyway, use this option and do not look at them.
-DSCC_SIZE_MULTIPLIER The factor to multiply with the maximum depth to obtain the size of the SCC stack. Default is 2, which was enough in our tests.
-DLWAA_NOSUBSETPRUNING When using the BMP approach, this option turns off subset pruning, which saves a lot of time during successor calculation; however redun-
dant LWAA states will have to be processed afterwards. Implemented for comparison purposes; in our examples pruning did decrease the runtime slightly, and does not require additional memory.
-DLWAA_BMPPAGESIZE Set to a value of n, the BMP page size is set to 2n. Good values are 1 to 7, with 7 being the default value. Note that for n 8, more memory will be required to store the fill counter for each page (which should be OK, as fewer pages are required).

A quick walk-through


Using LWAASpin from the command line (which is recommended) always follows this pattern:
Imagine you compiled SPIN with -DLWAA. You got a model file named model.spin and a LTL formula (preferably very big) named model.ltl. Generate the pan sources like this: 
lwaaspin -a -L -F model.ltl model.spin
LWAASpin will produce six pan-files. It might be well worth to check the size of pan.l, which can become a few megabytes for large formulae. Compile the sources with 
gcc -DLWAA pan.c -o pan
The SPIN GUI applies a -O3 option by default, but this is not recommended if your model gets large, as it will take forever to compile. Run the compiled pan: 
./pan -a
Our LWAASpin distribution contains a shell script named runtest, which performs the steps mentioned above.