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
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 panYou 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.
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.