SPIN NEWS - Nr. 15 - 19 January 1997

Contents of this NewsLetter:

SPIN96 AMS Proceedings

The proceedings of the 1996 Spin Workshop are now being printed by the AMS and will soon be available. Once available the volume will be included in the list of AMS publications that can be browsed at:

(follow the links for 'Books' and 'What's New')

The full title for the volume is:

	The Spin  Verification System - Second Workshop
	on the Spin Verification System - Proceedings
	of a DIMACS Workshop
but among friends the bibliographic reference may be given as:
	Proc. Second Workshop on the Spin Verification System
	held August 5, 1996, Rutgers University, New Brunswick, NJ.
	Ed. J-C. Gregoire, G.J. Holzmann, and D.A. Peled.
	Publ. American Mathematical Society, DIMACS/39.
(In the listing at the AMS URL you can already find the proceedings for the POMIV workshop on Partial Order Methods, numbered DIMACS/29)

SPIN97 Workshop Reminder

The deadline for contributions to the 1997 Spin Workshop is:
	15 Februari 1997
The workshop is held as a satellite of TACAS97 at Twente University, The Netherlands, on 5 April this year.

We are looking forward to many participants, good demos, and inspiring talks. Send a note to one of the organizers, e.g., Rom Langerak ([email protected]) if you would like to organize a demo, intend to submit a paper, or have proposals for tutorials, panel discussions or anything else that comes to mind to make this workshop of value to you.

Attending the SPIN workshop is free (including lunch). A shuttle-bus will run on April 5 between hotel an workshop. More info, with registration and hotel information:


Useful Tools and URLs

Jean-Philippe Cottin ([email protected]) writes:
The new version of a2ps, maintained by Akim Demaille, includes pretty-printing capabilities for Promela specs. Comments are welcome. The sources for a2ps can be found at
a2ps recognizes a file by its extension. A Promela file is recognized by the extension ".pml" -- or one can use the explicit a2ps option "-kpromela"

A little course (in French) for Spin and Promela can also be found at


Spin Version 2.9.5

The current version of Spin is still 2.9.4, from 4 November 1996. There have been few interesting changes since then -- things are pretty much stable. The upcoming new release will contain these changes: Version 2.9.5 will be available in another few weeks (quicker if you need access to the code to test some of the features, or to experiment with extensions -- please send mail if this applies to you).

Frequently Asked Questions

Matching the value of a variable in a receive

In a standard receive operation, only constant fields can be used to make the receive conditional on the value of specific parts in the incoming message. For instance, if 'msg' is a constant declared in an mtype definition, or in a #define macro, and 'data' is a variable, then
will only be executable if the first field in the incoming message also contains the value 'msg.'

A predefined function 'eval()' is part of Spin versions 2.9.3 and later. The eval() function is used to evaluate a variable to yield a value that can be used inside receive arguments as if it were a constant. This makes it possible to make a conditional receive that matches a possibly changing value of a variable. For instance

will only be executable for incoming messages with a first field that quals the value of _pid. Note that using
instead would specify that the value of (predefined) variable _pid is to be overwritten by the value of the first field in the message, whatever that happens to be.
The function eval() can be used for any message field - the argument can be any local or global variable reference, but it cannot be an expression.

Some Recent Papers

If you have published a paper related to Spin and would like to have a pointer included in an upcoming newsletter, send the details to: [email protected]

End of Newsletter Nr. 15.

Gerard J. Holzmann ([email protected])