NewsLetter 40 - October 10, 2004:

The Next Spin Workshop

The next Spin workshop will be held at the Stanford Court Hotel in San Francisco, California, from August 22-24 2005, co-located with CONCUR-2005.

This will be a full three-day workshop (only the second three-day workshop in the series so far) and is organized by Patrice Godefroid from Bell Labs. The last two days of SPIN2005 will overlap with CONCUR, which is held August 23-26, 2005 at the same location.

The deadline for submitting abstracts is April 1st, 2005.
The workshop details can be found at:

http://cm.bell-labs.com/cm/cs/what/spin2005//

Alternating Automata

Moritz Hammer has completed an adaption of Spin for the use of linear weak alternating automata (LWAA) instead of standard Buchi automata. Instead of precalculating the Buchi automaton, their modified version of Spin calculates the automaton on the fly. For large LTL formulae (with 5 to 8 strong fairness constraints) this can be an advantage. Another key difference is the replacement of the nested-depth first search algorithm from Spin with a version of Tarjan's algorithm. This version of Spin can be downloaded from:
http://www.pst.ifi.lmu.de/projekte/lwaaspin/

Spin Version 4.2.1

The current version of Spin is Version 4.2.1. The most interesting change since the book came out is the addition of a broader range of multi-bit hashing options, courtesy of Peter Dillinger and his PhD advisor Pete Manolios from Georgia Tech. The default bitstate hashing is now set to 3 hash-functions, but it can be set to any number. When the pan.c source is compiled with the extra directive -DCOVEST, and compiled with -lm, the program will also try to compute which number of hash is expected to give the best results (the greatest coverage).

Another new feature of 4.2.1 is an improved version of partial order reduction for breadth-first searches, courtesy of Dragan Bosnacki from Eindhoven University.

You can download the new version from:

http://spinroot.com/spin/Src/index.html

Embedded C-Code Questions

Pieter Hartel from The Netherlands asked:
"Would it be possible to define an extra primitive c_init { } that would make it possible to initialize external C data without performing an initial transition of the model?

I'm using spin as a data base engine, where Xpath queries are translated into LTL formulae, and the XML data base is generated by an automaton. In Xpath it is common to say I want to know if this node has a child node with particular properties. Going to a child translates into the X operator. So I found myself having to add spurious X operators at the beginning of each query to skip over initialisation.

Others are playing the same game, see for example:

L. Afanasiev, M. Franceschet, M. Marx, M. de Rijke,
CTL Model Checking for Processing Simple XPath Queries,
In 11th Int. Symp. on Temporal Representation and Reasoning (TIME),
IEEE Computer Society Press, Los Alamitos, California,
Tatihou, France, Jul. 2004, pp. 117-124."

The answer turns out to be relatively simple. There is already a little-known feature in Spin that allows you to define C statements that should be executed in pan.c just before the actual search begins. The trick is to compile pan.c with the extra directive -DPROV=\"file\" and to place the addition C code inside the file specified. This feature is described more fully in the new Spin book, on page 529-530.

JPL Internships

If you're interested in an internship at the Laboratory for Reliable Software at NASA/JPL in Pasadena, California, or if you're interested in a pretty cool job working on logic model checking techniques for space missions, drop us a note. (Because of the nature of the work, we can unfortunately only consider people with permanent residency or citizenship in the USA.)

End of Newsletter Nr. 40.

Spin Homepage
Newsletter Index
To subscribe/unsubscribe: [email protected]