File: Intro.html

package info (click to toggle)
spin 6.4.5%2Bdfsg-3
links: PTS, VCS
area: main
in suites: stretch
size: 2,636 kB
ctags: 2,878
sloc: ansic: 40,035; yacc: 996; makefile: 37; sh: 5
file content (1039 lines) | stat: -rw-r--r-- 30,399 bytes
parent folder | download | duplicates (2)
<body bgcolor=#ffffff>
<html>
<title>Promela Reference -- Intro</title>
<table cols=3 width=100%>
<tr>
<td valign=top><h3><tt>
<a href="Intro.html">Promela</a></tt></h3></td>
<td valign=top align=center><h3><tt>
<a name=N0 href="promela.html#section0"> Document Structure</a></tt></h3></td>
<td valign=top align=right><h3><tt>
Intro</tt></h3>
</td></tr>
</table>
<p><b><tt>INTRODUCTION </tt></b>
<br>
Five parts of the <i>Promela</i> language are discussed
in separate sections of this manual.  A sixt section
gives a brief motivation for things that are
intentionally outside the language.  The sections are:
<ul>
<li><b><tt>
1. </tt></b>
Meta Terms (translated by preprocessors into vanilla <i>Promela</i>)
<li><b><tt>
2. </tt></b>
Declarators (for defining process, channel, and data objects)
<li><b><tt>
3. </tt></b>
Control Flow Constructors (separators, compound statements, jumps, labels, etc.)
<li><b><tt>
4. </tt></b>
Basic Statements (such as send, receive, assignment, etc.)
<li><b><tt>
5. </tt></b>
Predefined Functions and Operators (such as len, run, nempty, etc.)
<li><b><tt>
6. </tt></b>
Omissions (such as floating point, probabilities, etc.)
</ul>
<p>
References to terms defined in this manual are linked to the
corresponding manual page, e.g.
<a href="send.html"><b><tt>send</tt></b></a>,
<a href="len.html"><b><tt>len</tt></b></a>. <p>
In the tradition of the <i>Unix</i>
manuals, each manual page that follows this introduction
contains some or all of the following defining elements.
<ul>
<li><b><tt>
NAME </tt></b>
<br>
A one sentence synopsis of the construct and its main purpose.
<li><b><tt>
SYNTAX </tt></b>
<br>
In the syntax rules text is reproduced as it is typed.
Optional terms are enclosed in (non-quoted) square brackets.
The Kleene star
<b>*</b> is used to indicate zero or more
repetitions of an optional term.
When the special symbols
<b>'['</b>, <b>']'</b>, <b>'*'</b>, appear as literals, they are quoted.  For instance, in
<pre>chan <i>name</i> = '[' <i>const</i> ']' of { <i>typename</i> [ , <i>typename</i> ] * }
</pre>
the first two square brackets are literals, and the last two enclose
an optional part of the definition.
</ul>
<p>
All terms set in
<i>italic , </i>
such as
<a href="grammar.html#name"><i>name </i></a><a href="grammar.html#,"><i>, </i></a><a href="grammar.html#const,"><i>const, </i></a>and
<a href="grammar.html#typename"><i>typename </i></a><a href="grammar.html#,"><i>, </i></a>refer to the grammar rules.
<ul>
<li><b><tt>
EXECUTABILITY </tt></b>
<br>
In Section 4, defines all conditions that must be satisfied for a
basic statement to be eligible for execution.
Some standard parts of this condition are implied, and not
repeated throughout.  One such implied condition is, for instance,
that there is a process that has reached the point in its code
where the basic statement is defined.
Implied conditions of this type are defined
in the section titled
<b>Semantics</b> below.
If the executability clause is described as
<tt>True , </tt>
no
conditions
<i>other </i>
<i>than </i>
the implied conditions apply.
<li><b><tt>
EFFECT </tt></b>
<br>
In Section 4,
defines the effect that the execution of a basic
statement will cause on any data, channel, or process objects.
One standard part of the effect is implied,
and not repeated everywhere:  the execution of the statement may
change the local state of the executing process.
If the effect clause is described as
<tt>None , </tt>
no effect
<i>other </i>
<i>than </i>
the implicit change in local state is defined.
See also the description under
<b>Semantics</b> below.
<li><b><tt>
DESCRIPTION </tt></b>
<br>
Describes in informal terms what the purpose and use is of the
language element being defined.
<li><b><tt>
EXAMPLES </tt></b>
<br>
Gives some typical applications of the construct.
<li><b><tt>
NOTES </tt></b>
<br>
Adds some additional notes about special circumstances or cautions.
<li><b><tt>
SEE ALSO </tt></b>
<br>
Gives references to other parts of this reference manual that may
provide additional explanations.
</ul>
<p>
<p><b><tt>SEMANTICS </tt></b>
<br>
The semantics of the language is defined in terms
of an operational model.
The model contains one or more ``processes,''
zero or more ``variables,'' zero or more message ``channels,''
and a ``semantics engine'' that defines how the
actions of the processes may be interleaved in time.
The processes are defined by labeled transition systems,
which are in turn derived from
<tt>proctype </tt>
declarations.
Similarly, the domains of values that variables can hold are
derived from variable type declarations.
<p>
The semantics engine executes the model in a step by step manner.
In each step, one
<i>executable </i>
basic statement is selected at random.  To determine if a statement
is executable or not, one of the conditions that must be
evaluated is the corresponding
<i>executability </i>
clause, as described in this manual.
For the selected statement, the
<i>effect </i>
clause from the statement is then applied, as also described
in this manual, and the current state of the process that
contained the statement is updated.
The semantics engine continues executing statements until
no executable statements remain, which happens if either
the number of active processes goes to zero, or when a
valid or invalid end-state is reached.
<p>
Declarators, defined in Section 2, define the basic elements of
the system.
Control flow statements, defined in Section 3,
affect only the structure of the underlying
transition system.
Basic statements, defined in Section 4, are the only language
elements that define state changes.
Smaller building blocks for the system, such as predefined variables
and functions, are defined in Section 5.
<p>
Central to the operational semantics definition is the description
of the semantics engine that defines when and how statements
may be executed.  Before giving the definition of this engine,
we give a definition of the formal objects that this
engine manipulates: variables, message channels, and processes.
We also define what the main component of a transition
and of a global system state are.  Not defined here are more
basic terms, such as
<i>sets , </i>
<i>identifiers , </i>
<i>integers , </i>
and
<i>Booleans . </i>
<ul>
<li><b><tt>
(S.1) </tt></b>
A
<b>variable </b>
is a tuple
<tt>{name,scope,domain,inival,curval} </tt>
<br>
where
<ul>
<li><b><tt>
</tt></b>
<tt>name </tt>
is an
<i>identifier </i>
that is unique within
<tt>scope , </tt>
<li><b><tt>
</tt></b>
<tt>scope </tt>
is defined by an
<i>integer </i>
(see below).
<li><b><tt>
</tt></b>
<tt>domain </tt>
is a finite set of
<i>integer s. </i>
<li><b><tt>
</tt></b>
<tt>inival , </tt>
 the initial value, is an
<i>integer </i>
within
<tt>domain , </tt>
 and
<li><b><tt>
</tt></b>
<tt>curval , </tt>
 the current value, is an
<i>integer </i>
within
<tt>domain . </tt>
</ul>
</ul>
<p>
In the remainder of this section we refer to the elements of
a tuple with a dot notation.  For instance, if
<tt>v </tt>
is a variable,
then
<tt>v.scope </tt>
is its scope.
<p>
The
<tt>scope </tt>
of a variable either identifies
<i>all </i>
active processes
(for globally declared variables) or
<i>one </i>
specific active process.
For the purposes of this definition, we can assume that a positive
integer identifies the
<tt>pid </tt>
(S.4) of one active process, and a
negative integer identifies all active processes.
The type of a variable determines its
<tt>domain . </tt>
For instance,
a variable of type
<tt>bit </tt>
(see
<a href="datatypes.html"><b><tt>datatypes</tt></b></a>) has domain {0,1}.
<ul>
<li><b><tt>
(S.2) </tt></b>
A
<b>message </b>
is an ordered set of
<b>variables </b>
(S.1).
<li><b><tt>
(S.3) </tt></b>
A
<b>channel </b>
is a tuple
<tt>{ch_id,nslots,contents} </tt>
<br>
where
<ul>
<li><b><tt>
</tt></b>
<tt>ch_id </tt>
is an
<i>integer </i>
(see below),
<li><b><tt>
</tt></b>
<tt>nslots </tt>
is an
<i>integer , </i>
and
<li><b><tt>
</tt></b>
<tt>contents </tt>
is an ordered set of
<b>messages </b>
(S.2) with maximum cardinality
<tt>nslots . </tt>
</ul>
</ul>
<p>
A positive
<tt>ch_id </tt>
will be used to identify an
<i>active </i>
<i>channel , </i>
while a negative number will identify a
<i>channel </i>
<i>template </i>
from which more channels of the same type may be instantiated.
Note that the definition of a channel does not contain a
<tt>scope , </tt>
like the definition of a variable.
The reason is that a channel always has global scope.  It can be created
either globally or locally, by an active process, but its method of
creation will not affect its scope in <i>Promela</i>, i.e., every channel is
in principle accessible to every active process,
by knowledge of the identifying
<tt>ch_id . </tt>
<ul>
<li><b><tt>
(S.4) </tt></b>
A
<b>process </b>
is a tuple
<tt>{pid,lvars,lstates,initial,curstate,trans} </tt>
<br>
where
<ul>
<li><b><tt>
</tt></b>
<tt>pid </tt>
is an
<i>integer </i>
(see below),
<li><b><tt>
</tt></b>
<tt>lvars </tt>
is a finite set of
<b>variables </b>
(S.1), each with
<tt>scope=pid , </tt>
<li><b><tt>
</tt></b>
<tt>lstates </tt>
is a finite set of
<i>integers </i>
(see below),
<li><b><tt>
</tt></b>
<tt>initial </tt>
and
<tt>curstate </tt>
are elements of set
<tt>lstates , </tt>
and
<li><b><tt>
</tt></b>
<tt>trans </tt>
is
<b>transition </b>
relation (S.5) defined on
<tt>lstates . </tt>
</ul>
For the purpose of definition S.4, we can assume that a positive
value of
<tt>pid </tt>
identifies an
<i>active </i>
<i>process , </i>
while a negative value for the
<tt>pid </tt>
field identifies a
<i>process </i>
<i>template </i>
from which extra active processes of the same type may be instantiated.
In the initial state of a newly instantiated process (see
<a href="active.html"><b><tt>active</tt></b></a>, <a href="run.html"><b><tt>run</tt></b></a>) <tt>curstate=initial , </tt>
 and all elements of
<tt>lvars </tt>
have
<tt>curval=inival . </tt>
</ul>
<p>
We will refer to the elements of set
<tt>lstates </tt>
as the
<i>local </i>
<i>states </i>
of a
<b>process </b>
(S.4).
The integer values suffice to uniquely identify each state within the set,
but hold no more information.
<ul>
<li><b><tt>
(S.5) </tt></b>
A
<b>transition </b>
relation is a finite set of tuples
<tt>{tr_id,source,target,cond,effect,prty,rv} </tt>
<br>
where
<ul>
<li><b><tt>
</tt></b>
<tt>tr_id </tt>
is a non-negative
<i>integer , </i>
<li><b><tt>
</tt></b>
<tt>source </tt>
and
<tt>target </tt>
are local
<i>states </i>
(i.e.,
<i>integer s), </i>
<li><b><tt>
</tt></b>
<tt>cond </tt>
is a Boolean
<a href="condition.html"><b><tt>condition</tt></b></a> on the global
<b>system </b>
<b>state </b>
(S.6),
<li><b><tt>
</tt></b>
<tt>effect </tt>
is a function that modifies the global
<b>system </b>
<b>state </b>
(S.6),
<li><b><tt>
</tt></b>
<tt>prty </tt>
and
<tt>rv </tt>
are
<i>integer s. </i>
</ul>
</ul>
<p>
The elements
<tt>prty </tt>
and
<tt>rv </tt>
are used in
<tt>cond </tt>
and
<tt>effect </tt>
definitions to enforce the semantics of, respectively, the
<a href="unless.html"><b><tt>unless</tt></b></a> construct, and of synchronous message passing operations, see
<a href="send.html"><b><tt>send</tt></b></a>. <ul>
<li><b><tt>
(S.6) </tt></b>
A global
<b>system </b>
<b>state </b>
is a tuple of the form
<tt>{gvars,procs,chans,exclusive,handshake,timeout,else,stutter} </tt>
<br>
where
<ul>
<li><b><tt>
</tt></b>
<tt>gvars </tt>
is a finite set of global
<b>variables </b>
(S.1), each with
<tt>scope=-1 , </tt>
<li><b><tt>
</tt></b>
<tt>procs </tt>
is a finite set of active
<b>processes </b>
(S.4), each with
<tt>pid>0 , </tt>
<li><b><tt>
</tt></b>
<tt>chans </tt>
is a finite set of
<b>channels </b>
(S.3), each with
<tt>ch_id>0 , </tt>
<li><b><tt>
</tt></b>
<tt>exclusive , </tt>
and
<tt>handshake </tt>
are
<i>integer s, </i>
and
<li><b><tt>
</tt></b>
<tt>timeout , </tt>
<tt>else , </tt>
and
<tt>stutter </tt>
are
<i>Boolean s. </i>
</ul>
<li><b><tt>
</tt></b>
In the
<i>initial </i>
<b>system </b>
<b>state </b>
all elements of
<tt>procs </tt>
are in their initial state (see S.4), all elements of
<tt>gvars </tt>
have
<tt>curval=inival </tt>
(see S.1),
all elements of
<tt>chans </tt>
have
<tt>contents={} </tt>
(i.e., the empty set) (see S.3),
<tt>exclusive </tt>
and
<tt>handshake </tt>
are zero, and
<tt>timeout </tt>
and
<tt>else </tt>
are
<tt>False . </tt>
The initial value of
<tt>stutter </tt>
is also
<tt>False . </tt>
(It can be set to
<tt>True </tt>
only by the verifier, when it replaces the default check for
safety properties with a check for liveness properties.)
</ul>
</ul>
<p>
The definitions S.1 to S.6 capture the minimal information
that is needed to define the semantics of the <i>Promela</i> language
in terms of an operational model, with processes defined as
transition systems.  The purpose of the definition of the semantics engine
in the next subsection is to offer a mechanism for resolving
questions about the interpretation of <i>Promela</i> constructs that is
independent of the <i>Spin</i> tool.
<p><b><tt>OPERATIONAL MODEL, SEMANTICS ENGINE </tt></b>
<br>
The semantics engine executes the system, at least conceptually,
in a stepwise manner:  selecting and executing one basic
statement at a time. 
At the highest level of abstraction, the behavior of this engine
can be defined as follows.
<p>
Let
<tt>E </tt>
be a set of pairs {
<tt>p,t }, </tt>
with
<tt>p </tt>
a process, and
<tt>t </tt>
a transition.
Let
<tt>executable(s) </tt>
be a function,
yet to be defined, that returns a set of such pairs, one
for each executable transitions in system state
<tt>s . </tt>
The semantics engine then performs as follows.
<pre>  1 while ((E = executable(s)) != {})
  2 {
  3 	for some {p,t} from E
  4 	{	s' = apply(t.effect, s)
  5 
  6 		if (<b>handshake</b> == 0)
  7 		{	p.curstate = t.target
  8 			s = s'
  9 		} else
 10 		{	# try to complete an rv handshake
 11 			E' = executable(s')
 12 			# if E' is {}, s remains unchanged
 13 
 14 			for some {p',t'} from E'
 15 			{	p.curstate = t.target
 16 				s = apply(t'.effect, s')
 17 				p'.curstate = t'.target
 18 			}
 19 			<b>handshake</b> = 0
 20 	}	}	
 21 }
 22 while (<b>stutter</b>) { s = s }	/* the 'stutter' extension */
</pre>
As long as there are executable transitions (corresponding to
the basic statements of <i>Promela</i>), the semantics engine
will select one of them at random and execute it.
<p>
To verify liveness properties with <i>Spin</i>, we must be able to treat
finite executions as special cases of infinite executions.  The
standard way of doing so is to define a <i>stutter extension</i> of
finite executions, where the final state is repeated <i>ad infinitum</i>.
The semantics engine above uses the system variable <b>stutter</b> to
determine if the stuttering rule is in effect.  Only the verification
system can change this variable.  More on verification, which is
strictly seen outside the semantics definition, follows at the
end of these notes.
<p>
The function
<tt>apply() </tt>
applies the
<tt>effect </tt>
of the selected transition
to the system state, possibly modifying system and local variables,
the contents of channels, or even the values of
<tt>exclusive </tt>
and
<tt>handshake , </tt>
as defined in the
<i>effect </i>
clauses from
<a href="atomic.html"><b><tt>atomic</tt></b></a>, and
<a href="send.html"><b><tt>send</tt></b></a>, respectively.
If no rendezvous offer was made (line 6), the current state of the
process that executed the transition is updated (line 7),
and the global state change takes effect by an update of the
system state itself (line 8).
If a rendezvous offer was made in the last transition, it cannot
result in a global state change unless the offer can also be accepted
(cf.
<a href="send.html"><b><tt>send</tt></b></a>). On line 11 the transitions that have now become executable are
selected.  The definition of the function
<tt>executable() </tt>
below guarantees that this set can only contain accepting transitions
for the given offer.  If there are none, the global state change
is declined, and execution proceeds with the selection of a new
executable candidate transition from the original set
<tt>E . </tt>
If the offer can be matched, the global state change takes effect.
The current states of both processes are now updated from
source to target state (where the two may, of course, be equal).
<p>
The main part of the semantics definition is in the definition
of what precisely constitutes an
<i>executable </i>
transition.
One part will be clear:  in the current system state the
<i>executability </i>
clause
<tt>t.cond </tt>
must be satisfied.  But there is more.
<p>
The following specification of the function
<tt>executable() </tt>
resolves these issues.
To avoid confusion, the state variables
<b>timeout</b>, <b>else</b> and
<b>exclusive</b> are set in bold.  These variables are the
only ones that can be modified within this function, as part of
the selection process.
<pre>  1 Set
  2 executable(State s)
  3 {	new Set E
  4 	new Set e
  5 
  6 	E = {}
  7 	<b>timeout</b> = <i>False</i>
  8 AllProcs:
  9 	for each active process p
 10 	{	if (exclusive == 0
 11 		or  exclusive == p.pid)
 12 		{	for u from high to low	# priority ('unless')
 13 			{	e = {};  <b>else</b> = <i>False</i>
 14 OneProc:			for each transition t in p.trans
 15 				{	if (t.source == p.curstate
 16 					and t.prty == u
 17 					and (handshake == 0
 18 					or   handshake == t.rv)
 19 					and  eval(t.cond) == <i>True</i>)
 20 					{	add {p,t} to set e
 21 				}	}
 22 				if (e != {})
 23 				{	add all elements of e to set E
 24 					break	# on to next process
 25 				} else if (<b>else</b> == <i>False</i>)
 26				{	<b>else</b> = <i>True</i>
 27					goto OneProc
 28				} # or else lower the priority
 29 	}	}	}
 30 
 31 	if (E == {} and <b>exclusive</b> != 0)
 32 	{	<b>exclusive</b> = 0
 33 		goto AllProcs
 34 	}
 35 	if (E == {} and <b>timeout</b> == <i>False</i>)
 36 	{	<b>timeout</b> = <i>True</i>
 37 		goto AllProcs
 38 	}
 39 
 40 	return E	# defining the set of executable transitions
 41 }
</pre>
For a transition to be added to the set of executable transitions it
has to pass a number of tests.
<ul>
<li><b><tt>
</tt></b>
The test on line 10-11 checks the value of the system
variable
<tt>exclusive . </tt>
By default it is zero, and the semantics engine itself will never
change the value to non-zero.  Any transition that is part of an
<tt>atomic </tt>
sequence (see
<a href="atomic.html"><b><tt>atomic</tt></b></a>) will set
<tt>exclusive </tt>
to the value of the
<tt>p.pid , </tt>
to make sure that the sequence is not interrupted by other processes,
unless the sequence itself blocks.  In the latter case the semantics
engine will restore the defaults (line 32).
<li><b><tt>
</tt></b>
The test on line 16 checks the priority level, set on line 12.  Within each
process, the semantics engine selects the highest priority transitions
that are executable.  Note that priorities can affect the selection
of transitions within a process, not
<i>between </i>
processes.
Priorities are defined in <i>Promela</i> with the unless construct, see
<a href="unless.html"><b><tt>unless</tt></b></a>. <li><b><tt>
</tt></b>
The test on line 15 matches the source state of the transition
in the labeled transition system with the current state of the process,
selected on line 9.
<li><b><tt>
</tt></b>
The test on line 17-18 makes sure that either no rendezvous
offer is outstanding, or, if one is, that the transition being considered
can accept the offer on the corresponding rendezvous port.
<li><b><tt>
</tt></b>
The test on line 19, finally, checks if the
<i>executability </i>
condition for the transition itself is satisfied.
</ul>
<p>
If no transitions are found to be executable with the default
value
<tt>False </tt>
for system variable
<b>else</b>, the transitions
of the current process are checked again, this time with
<b>else</b> equal to
<tt>True </tt>
(line 26-27).
If no transitions are executable in any process,
the value of system variable
<b>timeout</b> is changed to
<tt>True </tt>
and
the entire selection process is repeated (line 32-35).
The new value of
<b>timeout</b> will stick for just one step (line 7), but it can
cause any number of transitions in any number of processes to become
executable in the current global system state.
The syntax of <i>Promela</i> prohibits the use of both
<b>else</b> and
<b>timeout</b> within a single condition statement.
<p>
Note that the semantics engine does not establish the
validity or invalidity of correctness requirements.
<p><b><tt>INTERPRETING PROMELA SEMANTICS </tt></b>
<br>
The basic objects that are manipulated by the semantics engine
we have defined above are, of course, intended to correspond
to the basic objects of a <i>Promela</i> specification.  Much of the language,
however, merely provides a convenient mechanism for dealing with
the underlying objects.
Section 1 of this manual, for instance, describes some ``pseudo''
language features, or meta-terms, that are translated into <i>Promela</i>
proper by preprocessors.
Section 2 defines the <i>Promela</i> syntax for declaration of variables,
processes, and channels.  Section 3 defines how <i>Promela</i>'s control-flow
constructs correspond to the underlying transition relations.
An
<tt>if </tt>
statement, for instance, merely defines how multiple
transitions can exit from the same local process state.  The semantics
engine does not have to know anything about
<tt>if , </tt>
<tt>do , </tt>
<tt>break , </tt>
or
<tt>goto ; </tt>
it merely deals with local states and transitions.
<p>
Some <i>Promela</i> constructs cannot be translated away.  The semantics model
is defined in such a way that these primitive constructs correspond
directly to the transitions as defined in S.5.
We call these <i>Promela</i> constructs
<i>basic </i>
<i>statements . </i>
Section 4 defines the transition elements for each
<i>basic </i>
<i>statement </i>
in the language.
Section 5 of this manual, together with the grammar definition, defines the
remaining <i>Promela</i> syntax rules for the elements of a basic statement.
<p><b><tt>THREE EXAMPLES </tt></b>
<br>
Consider the following <i>Promela</i> system.
<pre>chan x = [0] of { bit };
chan y = [0] of { bit };
active proctype A() { x?0 unless y!0 }
active proctype B() { y?0 unless x!0 }
</pre>
Only one of two possible rendezvous handshakes can take place.
Do the semantics rules tell us which one?  If so, can the same
rules also resolve the following, very similar, situation?
<pre>chan x = [0] of { bit };
chan y = [0] of { bit };
active proctype A() { x!0 unless y!0 }
active proctype B() { y?0 unless x?0 }
</pre>
And, finally, what should we expect to happen in this case.
<pre>chan x = [0] of { bit };
chan y = [0] of { bit };
active proctype A() { x!0 unless y?0 }
active proctype B() { y!0 unless x?0 }
</pre>
Each of these cases can be hard to resolve without guidance
from a semantics definition.  The semantics rules for handling
rendezvous communication and for handling unless statements
seem to conflict here.  This is what we know.
<ul>
<li><b><tt>
</tt></b>
The definition of
<a href="unless.html"><b><tt>unless</tt></b></a> states that the statement that precedes the unless
keyword has a lower execution priority than the statement
that follows it.  These priorities must be used to resolve
executability conflicts between the two transitions within each process.
<li><b><tt>
</tt></b>
Rendezvous handshakes occur in two parts: the send statement
constitutes a rendezvous offer, which can succeed if it is
matched by a receive operation on the same channel in the
immediately following execution step by the other process.
To make the offer, the send statement must be executable by
the rules of the semantics engine, and to accept the offer
the matching receive operation must be executable.
<li><b><tt>
</tt></b>
The
<i>effect </i>
clause of the rendezvous send operation,
<a href="send.html"><b><tt>send</tt></b></a>, states that the value of
<b>handshake</b> will be set the value of
<tt>ch_id </tt>
for the channel used.
Lines 17-18 in the semantics engine then imply that no
statement can now be executed unless it has the
<tt>rv </tt>
parameter
on that transition set to the same value, which is only
the case for receive operations that target the same channel.
A global state transition in the main execution loop of the
semantics engine can only take place for rendezvous operations
if the offer can be accepted.
</ul>
<p>
We are now ready to resolve the semantics questions for each
of the three cases.
<p>
In the
<i>first </i>
<i>example , </i>
according to the priority
rule enforced by the unless operator, two statements
will be executable in the initial state:
<tt>x!0 </tt>
and
<tt>y!0 . </tt>
Either one could be selected for execution.
If the first is executed, we enter a rendezvous offer, with
<b>handshake</b> set to the
<tt>ch_id </tt>
of channel
<tt>x . </tt>
In the intermediate global state
<tt>s' </tt>
then reached (line 11-18
in the main execution loop of the semantics engine),
only one statement can be added to set
<tt>E' , </tt>
namely
<tt>x?0 . </tt>
The final successor state will have
<b>handshake</b> == 0 and both
processes in their final state.
Alternatively,
<tt>y!0 </tt>
could be selected for execution, with an
analogous result.
<p>
In the
<i>second </i>
<i>example , </i>
only one statement is executable in the initial system state:
<tt>y!0 , </tt>
and only the corresponding handshake can take place.
<p>
In the
<i>third </i>
<i>example , </i>
the first two statements considered, at the
highest priority, are both unexecutable.  One priority level lower,
though, two statements become executable: 
<tt>x!0 </tt>
and
<tt>y!0 , </tt>
and the resulting two system executions are again analogous to those
from the first example.
<p><b><tt>NOTES ON VERIFICATION </tt></b>
<br>
The addition of a verification option does not affect
the semantics of a <i>Promela</i> model as it is defined here.
Note, for instance, that the semantics engine does not include
any special mention or interpretation of end states,
accepting states, non-progress states, or assertions,
and it does not include a definition for the semantics of a
<tt>never </tt>
claim.  The reason is that these language elements have no formal
semantics <i>within</i> the model: they cannot be used to
define any part of the behavior of a model.
<p>
Assertions, special labels, and
<tt>never </tt>
claims are used for making meta statements <i>about</i> the
semantics of a model.
The verifier determines how such meta statements are to
be interpreted.
<p>
When the verifier checks for safety properties, it is
interested in cases where an
<tt>assert </tt>
statement can fail, or in the presence of finite executions
with a final state that violate some proper termination
condition (e.g., with all processes in a valid end-state, and
all message channels empty).
The predefined system variable <i>stutter</i>, used in the
definition of the semantics engine on line 22, is set to
<tt>False </tt>
in this case, and any mechanism can be in principle used to generate
the executions of the system, in search of the violations.
<p>
When the verifier checks for liveness properties, it is
interested in the presence of infinite executions that
either contain finitely many traversals of user-defined
<i>progress</i> states, or infinitely many traversals of
user-defined <i>accept</i> states.
The predefined system variable <i>stutter</i>, used in the
definition of the semantics engine on line 22, is set to
<tt>True </tt>
in this case, and, again, any mechanism can
be used to generate the infinite executions, as long as it
conforms to the semantics as defined before.
<p><b><tt>THE NEVER CLAIM </tt></b>
<br>
For purposes of verification it is not necessary that indeed
<i>all </i>
finite or infinite executions that comply with the formal
semantics are also generated.
In fact, the verifier <i>Spin</i> will make every effort to avoid
generating all possible executions, and instead concentrate
its efforts on a minimal set of executions that could
possibly produce counter-examples.
This is where the
<tt>never </tt>
claim comes in:  the
<tt>never </tt>
claim does not define new semantics,
but is used to <i>identify</i> that part of the
existing semantics that violates an independently stated
correctness criterion.
<p>
The interpretation of the
<tt>never </tt>
claim by the verifier in the context of the semantics
engine is as follows.
Note that the purpose of the claim is to <i>suppress</i> the
inspection of executions that could not possibly lead to
a counter-example.  To accomplish this, the verifier will
reject some valid executions as soon as possible.
The evaluation whether an execution should be rejected or
continued can happen in two places: at line 2 of the semantics
engine, and at line 22.
<pre>  1 while ((E = executable(s)) != {})
 *2 {	if (check_fails()) <b>Stop</b>;
  3 	for some {p,t} from E
    . . .
 21 }
*22 while (<b>stutter</b>) { s = s; if (check_fails()) <b>Stop</b>; }
</pre>
The check is implemented in <i>Spin</i> as a check to see if the
<tt>never </tt>
claim automaton can execute at least one more transition.
When the claim is generated from an
<tt>LTL </tt>
formula, all its transitions are
<tt>condition </tt>
statements, formalizing atomic propositions on the global system state.
Only infinite executions that are consistent with the formal semantics
of the model <i>and</i> with the constraint expressed by the
<tt>never </tt>
claim can now be generated.
<p>
With or without a constraint provided by a
<tt>never </tt>
claim, a verifier hunting for violations of liveness
properties can check infinite executions for those that constitute
counter-examples to a correctness property.
The precise method that the verifier uses to recognize
and report those infinite executions is of course critical
to the verification process, but irrelevant to the <i>Promela</i> semantics
definition given here.
<p><p><p><hr>
<table cols=3 width=100%>
<tr>
<td valign=top>
<a href="index.html">Spin Online References</a><br>
<a href="promela.html">Promela Manual Index</a><br>
<a href="grammar.html">Promela Grammar</a><br>
<a href="http://spinroot.com/spin/">Spin HomePage</a>
</td>
<td valign=top align=center></td>
<td valign=top align=right>
<font size="3"><b><tt>(Page Updated: 28 November 2004)</tt></font></b></td></tr>
</table>
</html>