LWAASpin is an extension of the SPIN model checker to use linear weak alternating automata instead of nondeterministic Büchi automata. This allows for much larger LTL formulae than accessible by the normal SPIN/ltl2ba combination. It also introduces Tarjans algorithm to SPIN, which can be used for nondeterministic Büchi automata checking as well.
LWAASpin is an extension of SPIN 4.1.1. It implements an algorithm proposed by Stephan Merz and Ali Sezgin. Their paper on emptiness checks on linear weak alternating automata can be found here.
The SPIN extension has been developed by Moritz Hammer as part of his diploma thesis. For feedback, questions, criticism and suggestions, please send an e-mail to:

hammer "at" pst.ifi.lmu.de

News

• Minor implementation related changes are listed on a separate page

Download

The sources can be obtained here: sources.tar.gz.

Some scaleable examples, including Perl scripts to create them, can be obtained here: examples.tar.gz.

Some tools we implemented to help us in modifying SPIN can be obtained here: tools.tar.gz.

Publications

The theoretical foundation of LWAASpin is described in our TACAS05 paper ``Truly on-the-fly model checking''.
Further information on LWAASpin can be found in the appendix of my diploma thesis.
SPIN itself has been very well documented on the SPIN homepage.
To understand the core code of SPIN, chapter 13 of "Design and Validation of Computer Protocols" by Gerard J. Holzmann is a recommended reading. It can be found online too.

Further information on the theoretical background of LWAA and Tarjan's algorithm can be found in the following papers:

• Paul Gastin and Denis Oddoux: Fast LTL to Büchi Automata Translation
• Heikki Tauriainen: On Translating Linear Temporal Logic into Alternating and Nondeterministic Automata
• Stefan Schwoon and Javier Esparza. A note on on-the-fly verification algorithms

Usage

LWAASpin preserves most of SPINs usage. To generate the pan sources for a given model, invoke lwaaspin like this:

lwaaspin -a -L -F <ltlfile> <modelfile>

or

lwaaspin -a -L -f <formula> <modelfile>

When compiling the pan sources, pass a -DLWAA preprocessor directive to the compiler:

gcc -DLWAA pan.c -o pan

You can use LWAASpin to use Tarjans algorithm on nondeterministic Büchi automata, too: Invoke LWAASpin as usual:

lwaaspin -a -N <never claim> <model file>

and compile the sources using a -DTARJAN preprocessor directive. The use of ltl2ba is highly recommended to obtain the never claim.

Using linear weak alternating automata and/or Tarjans algorithm is incompatible with many of SPINs options, like supertrace hashing, or fairness. If incompatible preprocessor directives are combined, pan will tell you so on invocation. A list of the added preprocessor directives can be found here.

Results

LWAASpin is usually slower than the original SPIN, as it performs calculation of the underlying automaton on the fly. However, for large LTL formulae, LWAASpin can outperform SPIN by many magnitudes: For formulae with about 10 strong fairness conditions, LWAASpin will perform the actual search in a matter of seconds, whereas ltl2ba will take days to generate the never claim! We obtained this findings with a self-written model checker and decided to incorporate the algorithm into SPIN, as it offers a very sophisticated input language and many other algorithms we were not capable of implementing ourselves within the given time frame. We do hope that the ability to check very large LTL formulae might have some impact on abstraction research.