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:
Spin Version 4.2.1
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:
Embedded C-Code Questions
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.
End of Newsletter Nr. 40.
To subscribe/unsubscribe: [email protected]