SPIN NEWS - Nr. 2 - January 15, 1995

Feel free to submit items that could be of interest to other SPIN users for this NewsLetter. Two submitted items are included at the end of this mailing.

Contents of this NewsLetter:

• Spin URLs
• Purpose and Statistics of the Distribution
• Toolchest Returns
• Some Frequently Asked Questions
• Generating a Display of the Reachability Graph
• Recent Changes
• Appendix 1: Project Description (by Thierry Cattel)
• Appendix 2: Jobhunt (by Kartik Subramanian)

There is now a URL on the WWW with an index that gives access to previous and current SPIN NewsLetters:

	http://netlib.bell-labs.com/netlib/spin/news.html

	http://netlib.bell-labs.com/netlib/spin/index.html

	http://netlib.bell-labs.com/netlib/spin/upgrade*.Z

Although this is a little unusual, the SPIN software will continue to be distributed only in source form. The reason for doing so is to help in the creation of a more open research environment in formal verification. If one of us publishes the results of a verification experiment, all of us should be able to reproduce it in detail, to consider variations in the algorithms used - while keeping all other factors that may affect the outcome of the experiment constant - and study how the results are affected by such changes.
All of this is only possible if everyone can have access to the sources of at least a few reference implementations of the algorithms that we use.

To maintain this capability, the SPIN software will probably continue to evolve also in the coming years. The criterion for adopting new algorithms into the basic SPIN software is that the algorithms are well-documented and understood, have predictable performance, and can be implemented robustly.

In the 48 months from 1/1991 to 1/1995 there have been 48 updates to the sources. Half of these updates concerned extensions or improvements of existing functionality. The other half concerned the unavoidable bug-fixes. To maintain the integrity of the distribution, a deliberate effort is made to be honest about any bugs in the software that are found, be they large or small. Every change to the software, as well as the reason for the change is listed in the updates files, and will remain available for the lifetime of the software, whatever that may be.

A quick count of the size of the sources, in total lines of source:

	Version 1.0.0	01/01/91    4,444 lines
	Version 1.6.6	12/24/94    5,609 lines
	Version 2.0.4	15/01/95   10,482 lines.

The current mailing list contains 71 active SPIN users. About 140 different sites have installed the new version of the software in the last two weeks. (As an aside, the names of these sites are no longer logged by our netlib software, to preserve anonymity of ftp accesses to the database.)

Toolchest Returns

SPIN was originally available only through the UNIX systems Toolchest. The phone numbers listed on p.434 of the book, however, stopped working when the Toolchest software left AT&T, first to USL (UNIX Systems Laboratories) and later to Novell - which is a competitor of AT&T.
The Toolchest distribution system has now returned to AT&T, and distribution of SPIN through that channel has become possible again. (No worry: the free netlib distribution will not be affected.)

In two cases you may want to contact the Toolchest distribution people to obtain SPIN sources:

1. if you have no access to anonymous FTP to retrieve the sources yourself from netlib, and
2. if you want to use SPIN for commercial purposes.

1. Compilation

The most frequently made observation about the installation of the version 2 sources was that compilation with non-ansi C compilers can fail if the include file is not present in the default include directories. The particular include file is needed for the compilation of just one procedure with a variable number of arguments (yyerror), but the error serves as a good warning that the compiler that issues it isn't ANSI compatible.

The problem can be avoided by switching to, for instance, the Gnu-C compiler (gcc), which is available on most systems. If gcc is needed to compile the SPIN sources, however, you will also have to twiddle two files from the Xspin directory. The following bourne shell (/bin/sh) script will do the job:

	cd Xspin
	for i in *.tcl
	do
		sed "s/cc -o pan/gcc -o pan/" $i > foo
		mv foo $i
	done

2. Use of printf statements

If you use a printf statement in the PROMELA model, and you leave it in during verification, you get a flurry of output, that is generally hard to interpret. The verifier makes no distinction between the various types of statements that are part of a PROMELA model. If a statement is executable (and a printf statement always is), it gets executed, and it adds transitions to the reachability graph. Of course, the order in which the printfs are executed is determined by the depth-first search traversal of the reachability graph, which does not necessarily make sense if you try to interpret it as being part of a single straight execution. To avoid the clutter, the SPIN documentation recommends to comment out the printfs. If no arguments are used, this can be done as:

	#define printf(x)	skip

If the printf's use varying numbers of arguments, they can be mapped onto skips with the following little sed-script, that was suggested by Michael Griffioen at NCR/GIS/AT&T, in the Netherlands:

	sed "s/printf.*\)/skip/" spec.in > spec.out

	add_log ""
	catch "eval exec sed s/printf.*\)/skip/ pan.in > _p" err
	catch "eval exec mv _p pan.in" err

	add_log "spin $a_options pan.in"; update

3. Remote referencing

It was noted by Pierre-Alain Etique from Switzerland that since `init' is not a valid proctype name, it is not possible to refer to the state of the init process with a remote reference:

	init[0]@label	/* no good */

	active proctype main()
	{
	label:	printf("my instantiation nr is %d\n", _pid)
	}

	main[0]@label

The output produced by a verbose run of the verifiers produced by SPIN contains enough information to convert it into a complete reachability graph of the system. There is a little awk-script that can be used to extract the required information, and convert it into the proper input formal for `dag' (a tool for drawing directed acyclic graphs). The format can probably be converted relatively easily for other graph drawing tools, such as `dot.' Clearly, this only works for relatively small graphs, say of less than a thousand states, but it may be a useful tool for small tests and demonstrations. An awk-script for the conversion is 44 lines. Send mail if you're interested in obtaining this script, or seeing it included in the next mailing.

Recent Changes

There have been a few small changes in the SPIN 2.0 sources. All changes, from this point on, will be made available both in the spin tar file from the distribution and in a small bourne shell script called `upgrades.' By retrieving and executing only the shell script, you can always bring your sources up to date within minimal hassle. This will work reliably no matter which version of the SPIN sources you have installed (as long as it is version 2.0 from 1/1/95 or later) and will work independent of whether or not you've run a previous version of the upgrades script before.

This policy applies only to the SPIN C-sources (the most bulky part of the distribution, and the part most likely to change once in a while). The (smaller) Xspin sources are updated in-place. Xspin and SPIN, however, each have their own tar-file in the distribution from now on so that you can retrieve them separately.

A short recap of the recent changes follows.

SPIN source changes - none of the changes are critical.

2.0.1 - 7 Jan 95:
	Changed the lexical analyzer to accept redundant
	text at the end of preprocessor directives, that
	some versions of cpp produce.
2.0.2 - 10 Jan 95:
	Two small updates to avoid problems on systems when
	(1) compiling pan.c for runtime profiling on (cc -p)
	(2) when using the new predefined function `enabled()' 
	in combination with partial order reduction.
2.0.3 - 12 Jan 95:
	Added listing of the mappings from label names to the
	state numbers used in the verifier with SPIN option -d.
2.0.4 - 12 Jan 95:
	made the use of a semicolon or arrow after an `else'
	statement optional; preventing complaints about a common
	and easily recoverable syntax error.

*	On some systems the format of the /bin/ps -e appears
	to be very verbose, which can make the execution-tracking
	in Validation.tcl fail (symptom: the run appears to go
	on forever - when in fact it has long terminated).
	To fix this, three lines were changed in Validation.tcl.
*	A small change in Simulation.tcl to redirect more output
	from a run from the log window to the process window, and
	to avoid misinterpreting output from printf statements
	in the model.

Application:

Developed by:

Formal method/specification language:

Tools:

Domain:

Period:

Size:

Description:

Conclusions:

Relevant publications:

Contacts:

	Thierry Cattel
	Computer Networking Laboratory
	Laboratoire de Teleinformatique (LTI)
	Swiss Federal Institute of Technology  (EPFL)
	Address: EPFL-DI-LTI, CH-1015 Lausanne, Switzerland
	E-mail:  cattel@di.epfl.ch
	Phone:   +41(21) 693 67 76 (Central European Time)
	Fax:     +41(21) 693 66 00
	WWW:     http://ltiwww.epfl.ch/~cattel

	Morven Gentleman
	Software Engineering Laboratory
	National Research Council of Canada
	K1A OR6 Ottawa, Canada
	E-mail : gentleman@iit.nrc.ca
	Phone:   +1 (613) 993 3857
	Fax:     +1 (613) 952 7998
	WWW:     http://wwwsel.iit.nrc.ca

Further remarks:

I am on the lookout for a full time position in the Networking area. If you know of a company that is hiring please let me know. Expertise with SPIN verification, ATM networks and willing to work in the areas of protocols and networking. Kartik
Email: s0093080@moncol.monmouth.edu

End of NewsLetter Nr. 2