SPIN NEWS - Nr. 5 - May 8, 1995

Contents of this NewsLetter:

• Statistics - Domain Names
• A New Language Feature in Promela
• Frequently Asked Question
  • Modeling Conditional Rendez-Vous Operations
• The First SPIN Users Workshop in On
• Appendix 1: A Useful Shell-script (by Ted Ewanchyna)
• Appendix 2: Spin Project Description (by Thierry Cattel)

In the category of idle statistics ... a quick count of email domain names shows that the subscribers to the SPIN Newsletter are spread over no less than 22 different countries. About 40% of the subscribers are from the U.S., about equally divided between companies (.com) and universities (.edu). 30% has an email destination in Europe, 13% in Canada, and 17% lives elsewhere (australia, new zealand, south africa, hong kong, israel, japan, taiwan, venezuela).

A New Language Feature in Promela

There have been nine small upgrades of the SPIN sources since the last newsletter. The current version is 2.3.4 dated May 1 1995. Starting with version 2.3.0 a new type of receive operation is supported for asynchronous message channels: the channel poll operator.

Together with random receive and channel testing, this now makes for a total of six different ways to perform a receive operation on an asynchronous message channel. The six are listed below, with a brief explanation of their purpose. The last two operations in this list are new.

1. q?var1,const,var2 or q?var1(const,var2)
   the standard fifo receive, where any field can be either a constant or a variable-name. all constant fields must be matched by the incoming message, for the receive to be executable. if this operation is executed, the oldest message is removed from the channel.
2. q??var1,const,var or q??var1(const,var2)
   the random receive operation that was first introduced in version 2.0. the semantics are as in (1), but in this case any message stored in the channel can be matched, it is not required to be the oldest one as in (1). if this operation is executed, the oldest message that matches (not necessarily the oldest message stored) is removed from the channel
3. q?[ var1,const,var2 ]
   the standard boolean test of executability of a receive operation of type (1). this is a condition that can be evaluated without side-effects, and it can therefore be used freely inside expressions. the state of the channel is the same before and after this condition is evaluated.
4. q??[ var1,const,var2 ]
   as (3), but this time the condition is true iff the corresponding receive operation of type (2) is executable. again, the condition can be evaluated without side-effects.
5. q?<< var1,const,var2 >>
   a new operation that is called a `fifo poll' it behaves as an operation of type (1), with just one difference: when executed, no message is removed from the channel. the effect is that all variables are set to the value of the corresponding fields of the message stored in the channel, but the channel contents itself is not disturbed. the operation has side-effects (on the variables), so it cannot be used inside expressions like (3).
6. q??<< var1,const,var2 >>
   new operation called `random receive poll' it behaves as an operation of type (2), again with the one difference that no message is removed from the channel when this operation is executed. it cannot be used inside expressions, for the same reason as (5).

Modeling Conditional Rendez-Vous Operations

The question has come up several times how one can faithfully model rendez-vous operations as they are used in, for instance, the ADA language. Unlike for asynchronous operations, as illustrated above, there is no boolean test or poll operation in Promela for synchronous receives. The reason is lies in the semantics of the rendez-vous operation itself. A complete rendez-vous operation is defined to be indivisible: there is no system `state' the would correspond to the point in between the send and the receive half of the rendez-vous handshake, where the receiver could test or poll the contents of the message channel.

Consider the sample rendez-vous arrangement:

	global:		chan port = [0] of { mtype, int };
	sender:		port!mesg(12)
	receiver:	port?mesg(data)

	sender:		atomic { P -> port!mesg(12) }
	receiver:	atomic { Q -> port?mesg(data) }

Another strategy is needed. The following solution requires the definition of 2 additional channels, but since rendez-vous channels do not take up any memory in the verification process this imposes no overhead during verifications.

	global:		chan port[3] = [0] { mtype, int };
	sender:		port[(1-P)]!mesg(12)
	receiver:	port[(2-Q)]?mesg(data

When:

Topics:

For More Information, Suggestions, Participation:

See Also:

Problem:

Description:

 #!/bin/sh
 sed '1,$s;;;g' $* |
 awk '
 BEGIN {print "#!/usr/loca./binexpect -f";print "spawn spin -i test-fc.pr"}
 /Select\ \[.*\]:*/ {
 printf ("expect {");
 for (i = 1; i < NF; i++) printf ("%s ",$i);
 printf ("}\n");
 printf ("exp_send \"")
 printf ("%s\\n\"\n",$i)
 }
 END {print "interact"}
 ' > $*.inter
 chmod +x $*.inter

	Thierry Cattel
       	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

	Adil Mesbahi
	mesbahi@di.epfl.ch or mesbahi@rubis.iie.cnam.fr