SPIN NEWS - Nr. 4 - March 22, 1995

Contents of this NewsLetter:

A Planned SPIN Workshop

The following is a preliminary announcement for a first workshop on the use of SPIN that is being organized by Jean Charles Gregoire from INRS. Reactions and suggestions welcome!

Workshop on PROMELA/SPIN

October 16th, Montreal, QC (just before FORTE'95)

SPIN is a reachability analysis tool designed for the general verification of distributed systems. First made available publicly in 1991, a completely new version has recently been released. SPIN is used both for teaching and for industrial applications. It has inspired many other tools in various ways.

This workshop aims at bringing together the community of users and researchers interested in SPIN as a tool, as well as an experimentation or a research vehicle. It will be an opportunity to discuss the current status of the tool, and the evolution of SPIN.

We have identified the following areas of interest for this workshop:

Further suggestions are most welcome.
Participants are invited to present a position statement to be presented and discussed at the workshop.

Workshop Organizer:
INRS-Te'le'communications

All Correspondance:
[email protected]

One More New Feature: Interactive Simulation

Following the request of many SPIN users, and the example of Patrice Godefroid, who made an initial implementation of interactive simulation long ago in his sleep-set extension of SPIN version 1.6, SPIN version 2.2 now has full support for interactive simulation.

Normally in a random simulation all nondeterminism is resolved with the help of a builtin pseudo random number generator. To make runs reproducible, so far the only option was to fix the seed of the random number generator with the -n option, but the specific way in which nondeterminism is being resolved is always unpredictable this way.

When the new version of SPIN is invoked as ``spin -i'' the user will be prompted for a choice whenever nondeterminism has to be resolved. The user can now directly guide a simulation run towards a particularly interesting, or suspect, piece of the code.

Interactive simulation is also supported from within XSPIN. When using XSPIN, a button menu will appear whenever a user selection is required.

Similar functionality existed for a long time in other verification tools - so this does seem to fill a gap in SPIN's functionality so far.

Other Recent Changes

The current version of SPIN is 2.2.6 from March 21 1995. Apart from the extension of functionality related to the implementation of interactive simulation, not much changed. A series of small bug fixes was again made - a new, optional compiler directive -DREACH was added - by request, support for the binary exclusive-or operator ('^') was added (the normal binary-or operator ('|') was already supported). More details on all updates is always available in the standard SPIN distribution file Doc/V2.Updates.

Some Frequently Asked Questions

1. Is there a good translator for LTL -> Promela never claims ?

Based on a new efficient algorithm from Doron Peled, Rob Gerth, Pierre Wolper, and Moshe Vardi, we now have a full implementation of a good translator that takes arbitrary LTL formulae as input, and produces the equivalent never claim, complete with the required labeling of acceptance states. It was already known that the size of the never claim (i.e., Buchi Automaton) is, in the worst case, exponential in the number of temporal operators in the the LTL formula. In practice, though, one rarely uses (or understands!) a formula with more than 2 or 3 operators, so this appears to be not much of a problem. We hope to be able to integrate the new algorithm into SPIN later - so that we can extend the Promela syntax with linear time temporal logic itself... Instead of a never claim, one could then specify the correctness claims directly as LTL formulae. (SPIN version 3?) Stay tuned.

2. Are there plans to support CTL in SPIN ?

Also a question that is asked a lot. Unfortunately we do not know of a good method to implement CTL model checking in an on-the-fly algorithm. Some methods have been suggested, but they do not seem to be a clear win. Also, we do not know of good examples of CTL formulae that cannot be expressed equally well in (perhaps several) LTL formulae. This is a point of debate though, and your suggestions are welcome on this or any other point!

Appendix: Porting SPIN to DOS

The following report is from Prof. Michael J. Ferguson Email: [email protected] and included here with his permission: It describes a successful attempt to port SPIN to a notebook PC - running under DOS. Many other SPIN users have asked about the possibility of this.

---
I have just successfully ported SPIN to my 486 PC
subnotebook --- not without a few trials. Some details:

** Compiler ---Djgpp (GCC 2.6.3)

** Spin problems ...
-- y.out.c and y.out.h are illegal DOS file names ---
Bison (DOS) produces spin_tab.c and spin_tab.h ---
all the y.out.h includes needed modifying.

-- The linker would not produce an output file with
multiple definitions of malloc, realmalloc, and free.
I renamed malloc to smalloc in pangen1.h and its
prototype in pangen3.h

-- The "tmp" file could not be created. gcc usually
inputs path names in unix format, and converts them,
at some low level (I think) to DOS comaptible paths.
Here it seemed to be interpreted with respect to the
current path. Since spin uses only one temprorary file,
I was able to hardwire one in. It also appears that the
file is unlinked too soon. I removed the unlink.. with
it there I obtained a  "parse error in line 1: hello"
This does not seem to be a problem on unix?

** gcc problems ...
gcc has several incompatible prototypes in its library
atoi(const char*) to atoi(char*)
time(unsigned long*) to time(long*)
extern void *(alloca) (long unsigned) 
to extern void *(alloca) (unsigned)
tempnam(const char*, const char*)
to tempnam(char*, char*)

It runs well on my 486 subnotebook but not on my 386
(no 387) desktop. I am not certain why. Now I have to
get some more memory for my subnote.

Michael
---

End of Newsletter Nr. 4.