File: Quick.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 (1077 lines) | stat: -rw-r--r-- 44,366 bytes
parent folder | download | duplicates (2)
<html>
<body bgcolor="#ffffff">
<head>
<title>Concise Promela Reference</title>
<h1><tt>Concise Promela Reference</tt></h1>
<h3><tt>by Rob Gerth, June 1997</tt></h3>
This is a quick reference for 
things that can be found in the <tt><b>Spin</b></tt> man pages.
It is less cursory on matters the discussion of which is scattered
through the various <tt><b>Spin</b></tt> documentation files or
only found in papers.
In particular, sections <a href="#exec"><tt><b>Execution</b></tt></a> and <a href="#anal"><tt><b>Analysis</b></tt></a> are more descriptive.
This reference is based on <tt><b>Spin</b></tt> version 2.9.7.
For a slightly more detailed
description see the <a href="Manual.html">Basic Spin Manual</a>.
A full description can be found in the
<a href="http://spinroot.com/spin/Doc/Book_extras/index.html">Spin book</a>.
</head>

<h2><tt>Introduction</tt></h2>

<tt><b>Spin</b></tt> is a tool for analyzing the logical consistency of distributed
systems, specifically of data communication protocols.  The  system is
described in a modeling language called <tt><b>Promela</b></tt> (Process or
Protocol Meta Language).
The language allows for the dynamic creation of concurrent
processes.  Communication  via message channels can be defined to be
synchronous (i.e., rendez-vous), or asynchronous (i.e., buffered).
<tt><b>Xspin</b></tt> is a graphical front-end to drive <tt><b>Spin</b></tt> (written in
Tcl/Tk).
<p>
Given a model system specified in <tt><b>Promela</b></tt>, <tt><b>Spin</b></tt> can perform random or
interactive simulations of the system's execution or it can generate a
<tt><b>C</b></tt> program that performs a fast exhaustive verification of the system
state space. 
During  simulations and verifications <tt><b>Spin</b></tt> checks for the
absence of deadlocks, unspecified receptions, and unexecutable code.
The verifier can also be used to prove the correctness of system
invariants and it can find non-progress execution cycles.  Finally, it
supports the verification of linear time temporal constraints; either
with <tt><b>Promela</b></tt> never-claims or by directly formulating the constraints
in temporal logic.
<p>
The verifier is setup to be fast and to use a minimal amount of
memory.  The exhaustive verifications performed by <tt><b>Spin</b></tt> are conclusive.
They establish with certainty whether or not a system's behavior is
error-free.  Very large verification runs, that can ordinarily not be
performed with automated techniques, can be done in <tt><b>Spin</b></tt> with a ``bit
state space'' technique. With this method the state space is collapsed
to a few bits per system state stored.
Although this technique doesn't guarantee certainty, the coverage is
better, and often much better, than that obtained with traditional
random simulation.

<h2><tt><tt>Promela</tt></tt></h2>
Spin models consist of 3 types of objects:
<em>processes</em>, message <em>channels</em>,
and <em>variables</em>.
Processes are global objects.  Message channels
and variables can be declared either globally or locally within a
process.  Processes specify behavior, channels and global variables
define the environment in which the processes run.
<p>
The syntax of <tt><b>Promela</b></tt> is <tt><b>C</b></tt>-like.
Below, our tendency
is to use examples for those parts that are similar to <tt><b>C</b></tt>,
but we attempt to be more precise elsewhere.

<h3><tt>Lexical conventions</tt></h3>
There are five classes of tokens: identifiers, keywords, constants,
operators and statement separators. Blanks, tabs, newlines, formfeeds and
comments serve only to separate tokens.
If more than one interpretation is possible, a token is taken to be the
longest string of characters that can constitute a token.

<h3><tt>Comments</tt></h3>
A comment starts with <tt>/*</tt> and terminates with <tt>*/</tt>.  Comments may 
not be nested.

<h3><tt>Identifiers</tt></h3>
An identifier is a single letter, period, or underscore followed by
zero or more letters, digits, periods, or underscores.

<h3><tt>Keywords</tt></h3>
The following identifiers are reserved for use as keywords.

<pre>
	active		assert		atomic		bit
	bool		break		byte		chan
	d_step		D_proctype	do		else
	empty		enabled		fi		full
	goto		hidden		if		init
	int		len		mtype		nempty
	never		nfull		od		of
	pc_value	printf		priority	proctype
	provided	run		short		skip
	timeout		typedef		unless		unsigned
	xr		xs
</pre>

<h3><tt>Labels</tt></h3>
A label is an identifier followed by a colon (<tt>:</tt>).
Any statement can be labeled.
Labels that start with one of the sequences <tt>end</tt>, <tt>progress</tt>
or <tt>accept</tt> have a special meaning, discussed in Section <a href="#anal"><tt><b>Analysis</b></tt></a>
below.

<h3><tt>Constants</tt></h3>
A constant is a sequence of digits representing a decimal integer.  There 
are no floating point numbers in <tt><b>Promela</b></tt>.  Symbolic names for constants can 
be defined in two ways.  The first method is to use a <tt><b>C</b></tt>-style macro 
definition
<pre>
	#define NAME	5 
</pre>
The second method 
is to use the keyword <tt>mtype</tt>; see <a href="#symconst">symconst</a>.

<h3><tt>Expressions</tt></h3>
The following operators and functions can be used to build expressions:
<pre>
	+	-	*	/	%	>
	>=	<	<=	==	!=	!
	&	||	&&	|	~	>>
	<<	^	++	--
	len()	empty()	nempty()	nfull()	full()
	run	eval()	enabled()	pc_value()
</pre>
Most operators are binary.
The logical negation (<tt>!</tt>) and the minus (<tt>-</tt>) operator can be
both unary and binary, depending on context.
The <tt>++</tt> and <tt>--</tt> operators are unary suffix operators, like
they are defined in <tt><b>C</tt></b>.
The exclusive-or is <tt>^</tt>.

The functions on the one-but-last line are unary and apply only to message
channels (see <a href="#MsgChan">MsgChan</a>);
<tt>len</tt> measures the number of messages an existing channel holds;
the other channel operators have the expected meaning and are
introduced to assist partial order reductions; see <a href="#pored">pored</a>.
These functions cannot be used in larger expressions.
E.g., <tt>!empty(q)</tt> will result in a syntax error and <tt>nempty(q)</tt>
should be used instead.

The unary functions on the last line are special. The first operator is
used for process instantiation (see <a href="#Processes">Processes</a> below).
When executed it yields the instantiation number of the instance it
created.
The second one is discussed in <a href="#ChanOps">ChanOps</a> and the others in <a href="#never">never</a>.

The operators on the first four lines are defined as in <tt><b>C</tt></b>.
<tt><b>Promela</b></tt> follows the <tt><b>C</b></tt>-convention that the boolean false-condition
corresponds with the value 0; any non-zero value denotes truth.


<h4>Conditional expressions</h4>
<pre>
	(expr1 -> expr2 : expr3)
</pre>
has the value of <tt>expr3</tt> if <tt>expr1</tt> evaluates to zero, and the
value of <tt>expr2</tt> otherwise.  Note that <tt>-></tt> is required here and
cannot be replaced by a <tt>;</tt>.

<h3><tt>Declarations</tt></h3>
Processes, channels, variables, etc. must be declared before they can be 
used.  Variables and channels can be declared either locally, within a 
process, or globally.  A process can only be declared globally in a
<tt>proctype</tt> declaration.  Local declarations may appear anywhere in
a process body.

<h4>Variables</h4>
A variable declaration is started by a keyword indicating the basic data 
type of the variable, <tt>bit</tt>, <tt>bool</tt>, <tt>byte</tt>, <tt>short</tt> or 
<tt>int</tt>, followed by one or more identifiers, optionally followed by an 
initializer:
<pre>
	byte name1, name2 = 4, name3
</pre>
An initializer, if specified, must be a constant.  By default variables 
are initialized to zero.
The bit-widths of these basic types are, respectively, 1, 1, 8, 16 and 32.
The last two are <em>signed</em> quantities; the first three are unsigned.

A variable can have a user-defined type as well; see <a href="#structs">structs</a>.

<h4>Arrays</h4>
An array of variables is declared, e.g., by
<pre>
	int name[4]
</pre>
An array can have a <em>single</em> constant as an initializer,
initializing all array elements.  Array indices start at 0,
as in <tt><b>C</b></tt>;
hence, the largest index would be 3 in this case.

<h4><a name="symconst">Symbolic constants</a></h4>
Symbolic constants can be declared by
<pre>
	mtype = {OK, READY, ACK}
</pre>
and variables of this type by
<pre>
	mtype Status = OK;
</pre>
Only one <tt>mtype</tt>-definition is allowed which must be global and at
most 256 symbolic constants can be declared; an <tt>mtype</tt> variable is
8 bits wide.
<p>
The advantage of <tt>mtype</tt>s over <tt>#define</tt>s is that the former type
of symbolic constants is recognized by <tt><b>Spin</b></tt> and during simulations the
symbolic names are used instead of the values they represent.

<h4><a name="MsgChan">Message channels</a></h4>
Message channels are declared, e.g., by
<pre>
	chan Transfer  = [2] of {mtype, bit, short, chan};
	chan Device[3] = [0] of {byte};
	chan Channel;
</pre>
Here, <tt>Transfer</tt> can store up to 2 messages in the channel; the message 
type is indicated between the braces (in this case each message consists of 
4 parts).  <tt>Device</tt> is an <em>array</em> of channels; each channel is 
synchronous, i.e., sends and receives must synchronize as no messages can 
be stored.  Finally, <tt>Channel</tt> is an uninitialized channel that can be 
used only after an initialized channel has been assigned to it.
<p>
Note that an object of type <tt>chan</tt> can be part of a message
declaration in another channel.

<h4>Exclusive receive (<tt>xr</tt>) and send (<tt>xs</tt>) on channels</h4>
<pre>
	xr Transfer;
	xs Channel;
</pre> 
in some process, declares that this process is the <em>only</em> one to
receive messages on <tt>Transfer</tt> and the <em>only</em> one to send on
<tt>Channel</tt>.
<p>
It is a run-time error if during analysis it turns out that some other
process receives from <tt>Transfer</tt> or sends to <tt>Channel</tt>.
<p>
See <a href="#pored">Reductions</a> for more detail.


<h4><a name="structs">Structures</a></h4>
User-defined data types are supported through <tt>typedef</tt> definitions,
<pre>
	typedef Msg {
		byte a[3], b;
		chan p
	}
</pre>
that can be used in variable declarations and, more generally, wherever
a type definition is needed:
<pre>
	Msg foo;
	chan stream =[0] of {mtype,Msg}
</pre>
Elements of structures are accessed as in C; e.g.,
<pre>
	foo.a[1]
</pre>

<h4>Hidden variables</h4>
<pre>
   hidden int foo
</pre>
A <tt>hidden</tt> variable is not part of the system state (see <a href="#exec"><tt><b>Execution</b></tt></a>)
and its value is always undefined, although it can be assigned to.
It is useful when a `scratch' variable is needed, e.g., to flush the
values in a channel buffer, because it does not add to the size of the
state-vector during analysis and thus reduces the memory requirements
for analysis; cf. <a href="#MemTim">MemTim</a>.
<p>
Only global declarations can be thus qualified; elements of a structure
are considered local.
Bit, bool and channel variables cannot be hidden.
<p>
There is a pre-declared hidden variable, <tt>_</tt>, which can be assigned
to in any context.
Its (implicit) type is <tt>int</tt> so that it can be used to assign <tt>bit</tt>,
<tt>bool</tt>, <tt>byte</tt>, <tt>mtype</tt>, <tt>short</tt> and <tt>int</tt> values to.


<h3><tt><a name="Processes">Processes</a></tt></h3> 
A basic process declaration has the form
<pre>
	proctype pname( chan In, Out; byte id )
	{ statements }
</pre>
Such a process is instantiated by a run-operation:
<pre>
	run pname(Transfer, Device[0], 0)
</pre>
that first assigns the actual parameters to the formal ones and 
then executes the <tt>statements</tt> in the body.
Each process instance has a unique, positive instantiation number,
which is yielded by the run-operator (and by <tt>pid</tt>);
see <a href="#specvar">specvar</a>.
A process-instance remains active until the process' body terminates
(if ever).
<p>
Processes cannot have arrays as (part of) a formal parameter type,
but structures are allowed.
<p>
Process declarations can be augmented in various ways. The most general
form is
<pre>
	active [N] proctype pname(...) provided (E) priority M
</pre>
The <tt>active</tt> modifier causes <tt>N</tt> instances of the proctype to be 
active in the initial system state, where <tt>N</tt> is a constant.
If <tt>[N]</tt> is absent, only one instance is activated.
Formal parameters of instances activated through the <tt>active</tt> modifier
are initialized to 0; i.e. actual parameters can only be passed using
<tt>run</tt>-statements. 
<p>
A proctype can have an <em>enabling</em> condition <tt>E</tt> associated with
it, which is a general side-effect free expression
that may contain constants, global variables,
the predefined variables <tt>timeout</tt> and <tt>pid</tt>, but not other local
variables or parameters, and no remote references.
Enabling conditions are evaluated once, in the initial state.
<p>
For use during random simulations, a process instance can run with a 
priority <tt>M</tt>, a constant >=1.
Such a process is <tt>M</tt> times as likely to be scheduled than a
default (priority 1) process.
Execution priorities can be used in a run-statement as well:
<pre>
	run pname(...) priority M
</pre>
A process instantiated with a <tt>run</tt> statement always gets the priority
that is explicitly or implicitly specified there (the default is 1).
<p>
Note that priorities have no effect during analysis.

<h4>Deterministic processes</h4>
<pre>
	D_proctype pname( chan In, Out; byte id )
	{ statements }
</pre>
declares that any instance of <tt>pname</tt> is deterministic.
It has no other effect, then causing an error during analysis if some
instance is not.
<p>
Note that determinism is a dynamic property.
E.g., if <tt>pname</tt> has in its body the statement
<pre>
	if
	:: In?v  -> ...
	:: Out!e -> ...
	fi
</pre>
then non-determinism is flagged only if during some computation, there
is an instance of <tt>pname</tt> for which the receive and send on the actual
channels bound to <tt>In</tt> and <tt>Out</tt> are simultaneously enabled.

<h4>Init process</h4>
<pre>
	init { statements }
</pre>
This process, if present, is instantiated once, and is often
used to prepare the true initial state of a system by initializing
variables and running the appropriate process-instances.

<h4><a name="never">Never claim</a></h4>
<pre>
	never { statements }
</pre>
is a special type of process that, if present, is instantiated once.
As explained further in <a href="#tempclaim">tempclaim</a>, never claims are used to
detect behaviors that are considered undesirable or illegal.
<p>
The individual statements in <tt>statements</tt> are interpreted as
conditions (see <a href="#Exec">Exec</a> and <a href="#ExprStat">ExprStat</a>) and, therefore, should
not have side-effects (although this will cause warnings rather than
syntax-errors).
<p>
Statements that can have side-effect are assignments,
auto-increment and decrement operations, communications, run
and assert statements.
<p>

Never claims can use three additional functions:
<ul>
<li><tt>enabled(pid)</tt>	
	This boolean function returns true if
	the process with instantiation number denoted by <tt>pid</tt> is
	able to perform an operation.
	This function can only be used in systems that do not admit
	<em>synchronous</em> communication
<li><tt>pc_value(pid)</tt>	
	This function returns the number of the state that the
	process with instantiation number denoted by <tt>pid</tt> is
	currently in. (With state-numbers as given by the <tt>-d</tt> runtime option.)
<li><tt>_np</tt>	
	This predicate is true if the system is in a non-progress state
	and is false otherwise. It is introduced to enable more efficient
	searches for non-progress cycles. See <a href="#ProgSt">progress</a>
	and <a href="#SearchNPC">SearchNPC</a>.
</ul>


<h4><a name="specvar">Special variables</a></h4>
<pre>
	_pid, _last
</pre>
<tt>_pid</tt> is a predefined local variable that holds the instantiation
number of the process' instance.  <tt>_last</tt> is a predefined global
variable that holds the instantiation number of the process instance that
performed the last step in the current execution sequence.  Initially,
<tt>_last</tt> is zero.

<h4><a name="RmtRef">Remote references</a></h4>
The expression
<pre>
	procname[pid]@label
</pre>
is true precisely if the process with instantiation number <tt>pid</tt>
of proctype <tt>procname</tt> is currently at the statement
labeled with <tt>label</tt>.

<h3><tt>Statements</tt></h3>
The following can be used as statements:
<pre>
	assert		assignment	atomic		break
	declaration	d_step		else		expression
	goto		receive		selection	skip
	repetition	send		timeout		unless
</pre>
In particular, note that expressions can be used as statements as well.
<p>
Statements are separated by either a semi-colon (<tt>;</tt>) or, equivalently,
an arrow (<tt>-></tt>).  The arrow is sometimes used to indicate a causal
relation between successive statements and also in selection and repetition
statements to separate the guard from the statements it is guarding;
see <a href="#select">select</a> and <a href="#repet">repet</a>.
<p>
Statements that have no smaller statements as a constituent, are called
<em>basic</em>.
E.g., an assignment is a basic statement whereas a selection is not.

<h4><a name="Exec">Executability</a></h4> 
The execution of a statement is conditional on its <em>enabledness</em>
(or ``executability'').  
Statements are either enabled or <em>blocked</em>.
Of the above listed statements, assignments, declarations,
<tt>assert</tt>, <tt>skip</tt>, <tt>goto</tt> and <tt>break</tt> are always enabled.
If a statement is blocked, execution at that point halts until the statement
becomes enabled.

<h4>Assert</h4>
<pre>
	assert( expression )
</pre>
aborts the program if the <tt>expression</tt> returns a zero result;
otherwise it is just passed.

<h4>Atomic</h4>
<pre>
	atomic { statements }
</pre>
attempts to execute the <tt>statements</tt> in one indivisible step;
i.e., without interleaved execution of other processes.
An atomic statement is enabled if its first statement is.
<p>
Making local computations atomic can effect important reductions of the
complexity of the verification system; cf. <a href="#MemAtD">MemAtD</a>.
<p>
During its execution, control can only be transferred outside the scope
of an atomic statement by an explicit <tt>goto</tt> or at a point where a
statement within its scope becomes blocked.  If this statement
subsequently becomes enabled again, execution may continue at that
point.
<p>
There is no constraint on what may occur inside the scope.  In
particular, it is possible to jump to any (labeled) location within the
scope of an <tt>atomic</tt>.
<p>
The body of a process instance activated by a <tt>run</tt>-statement
is considered to be outside the scope of the atomic statement performing
the activation.

<h4>Break</h4> See <a href="#repet">Repetition</a>.

<h4>Goto</h4>
<pre>
	goto label
</pre>
transfers control to the statement labeled by <tt>label</tt> which has to 
occur in the same procedure as the goto.

<h4>Deterministic step</h4>
<pre>
	d_step { statements }
</pre>
has the same effect as <tt>atomic</tt> but is even more efficient;
cf. <a href="#MemAtD">MemAtD</a>.
However, <tt>statements</tt> within its scope must be completely
deterministic; they may not jump to labels outside the <tt>d_step</tt>'s
scope; there may be no jumps from the outside to labeled statements
within the scope; remote references (see <a href="#RmtRef">RmtRef</a>) are disallowed.
Finally, statements other than the first may not block.  A <tt>d_step</tt>
is enabled precisely if its first statement is.

<tt><b>Promela</b></tt> considers the location in front of the <tt>d_step</tt> to be
within its scope and the location just after its last statement to be
outside.  Hence, to achieve the intended effect of the following
<em>incorrect</em> code-fragment:
<pre>
	goto label;
	...
label:
	d_step {
		...
		do
		...
			break
		...
		od
	}
</pre>
use this code instead:
<pre>
	goto label;
	...
label: skip;
	d_step {
		...
		do
		...
			break
		...
	od; skip
	}
</pre>

<h4>Else</h4>
See <a href="#select">select</a>.

<h4><a name="ExprStat">Expressions</a></h4>
Any expression that does not use auto-increment or decrement operations
(<tt>++</tt> or <tt>--</tt>) can be used as a statement.
In that case, it is enabled precisely if it evaluates to a non-zero value.
An enabled expression is just passed, without affecting the state.
<p>
For example, instead of writing a busy wait loop
<pre>
	while (a != b) skip
</pre>
the same effect is achieved in <tt><b>Promela</b></tt> by the statement
<pre>
	(a == b)
</pre>

<h4><a name="ChanOps">Channel operations</a></h4>
<pre>
 	q!var1,const,var2,...  or, equivalently  q!var1(const,var2,...)
	q?var1,const,var2,...  or, equivalently  q?var1(const,var2,...)
</pre>
Are the standard channel operations; the first is a send statement, the
second a receive.  Here, <tt>q</tt> denotes a channel and the list
<tt>var1,const,var2,...</tt> should be compatible with the channel's
message type.  For a send or receive to be enabled, <tt>q</tt> has to be
initialized.  Furthermore, if the channel is buffered, a send is
enabled if the buffer is not full; a receive is enabled if the buffer
is non-empty.  On an unbuffered channel, a send (receive) is enabled
only if there is a corresponding receive (send) that can be executed
simultaneously.  A receive statement executes by reading the oldest
message on the channel; if the channel is unbuffered, it reads the
message of the simultaneously executing send statement. A send
statement executes by putting its message in the buffer (if there is
one).
Note that a channel operation on an unbuffered channel can only execute
if a matching operation executes simultaneously.
<p>
Constants in the list of a receive, constrain its enabledness by
forcing the corresponding values in the oldest message (or matching
send) to be the same; if not, the receive is blocked.
<p>
It is possible to use a local or global variable to likewise constrain
a channel operation's enabledness:
<pre>
	q?var1,eval(var2),var3
</pre>
blocks in case a matching send's 2nd value does not equal the <em>value</em>
of <tt>var2</tt>. Note that the value of <tt>var2</tt> is not changed.
<p>

For <em>buffered</em> channels, there are additional operations:
<ul>
<li><tt>q?[var1,const,var2]</tt>	 returns true (i.e. a non-zero value)
	precisely if the corresponding receive operation would be enabled.
<li><tt>q?&#60var1,const,var2&#62</tt>	 like a standard receive operation
	except that the message is <em>not</em> removed from the buffer.
<li><tt>q!!var1,const,var</tt>	 <em>sorted send</em>; it inserts its
	message into the buffer immediately ahead of (so that it will be
	younger than) the oldest message that succeeds it in numerical,
	lexicographic order.
<li><tt>q??var1,const,var</tt>	 <em>random receive</em>; it executes if
	there is <em>some</em> message in the buffer for which it is enabled
	and then retrieves the oldest such message.
<li><tt>q??[var1,const,var2]</tt>	 returns true (i.e. a non-zero value)
	precisely if the corresponding receive operation would be enabled.
<li><tt>q??&#60var1,const,var2&#62</tt>	 like a standard random receive
	operation except that the message is <em>not</em> removed from
	the buffer.
</ul>

The behavior of buffered channels can be influenced by the
<tt><b>Spin</b></tt> command line switch <tt>-m</tt>:
in that case, send actions on a
channel do not block if the channnel's buffer is full; instead,
messages send when the buffer is full are lost.

<h4><a name="select">Selection</a></h4>
<pre>
	if
	:: statements
	...
	:: statements
	fi
</pre>

Selects one among its <em>options</em> (each of them starts with <tt>::</tt>) 
and executes it.  An option can be selected if its <em>first</em> statement 
(the <em>guard</em>) is enabled.  A selection blocks until there is at least 
one selectable branch.  If more than one option is selectable, one will be 
selected at random.

The special guard <tt>else</tt> can be used (once) in selection and repetition 
statements and is enabled precisely if all other guards are blocked.
It may not be used if a send or receive statement is used as guard.

<h4><a name="repet">Repetition</a></h4>
<pre>
	do
	:: statements
	...
	:: statements
	od
</pre>

Similar to a selection, except that the statement is executed
repeatedly, until control is explicitly transferred to outside the
statement by a <tt>goto</tt> or <tt>break</tt>.
A <tt>break</tt> will terminate
the innermost repetition statement in which it is executed and cannot
be used outside a repetition.

<h4>Skip</h4>
Has no effect and is mainly used to satisfy syntactic requirements.

<h4>Timeout</h4>
A <tt>timeout</tt> statement becomes enabled precisely when every other
statement in the system is blocked. It has no effect when executed.

<h4>Unless</h4>
<pre>
	{ statements-1 } unless { statements-2 }
</pre>
Starts execution in <tt>statements-1</tt>.
Before each statement in <tt>statements-1</tt> (including the first one)
is executed, enabledness of <tt>statements-2</tt> is checked and if it
is, execution of <tt>statements-1</tt> is aborted and control transfers
to <tt>statements-2</tt>; control remains in <tt>statements-1</tt>,
otherwise.
If <tt>statements-1</tt> terminates, <tt>statements-2</tt> is ignored.
<p>
In an <tt>unless</tt>, a <tt>d_step</tt>, in contrast with an <tt>atomic</tt>,
is considered indivisible; i.e., enabledness of <tt>statements-2</tt> is
not checked if control in <tt>statements-1</tt> resides within the scope
of a <tt>d_step</tt>.


<h2><tt><a name="exec">Executing a Promela system</a></tt></h2>
A <em>system state</em> of a <tt><b>Promela</b></tt> system comprises the values of the
global variables, the contents of the channel buffers and for each
process instance, the values of its location counter, its local
variables and local channel buffers.
If a never claim is present, the state also includes the value of the
claim's location counter.
<p>
Initially, all global (non-initialized) variables contain the value 0
and the channel buffers are empty.
The existing process instances are the ones created through the
<tt>active</tt> modifier on the <tt>proctype</tt>
declarations together with the
<tt>init</tt> and <tt>never</tt> processes, if present.
The location counters of these instances are at their first
statements.
<p>
A system state of a <tt><b>Promela</b></tt>
system uniquely identifies the enabled
statements in every (active) process instance.
An <em>execution step</em> in a system <em>without</em> never claim,
proceeds by arbitrarily selecting one of the enabled statements and
then executing that statement, thus arriving in a new system state.
So, process instances execute asynchronously.
Note, however, that in case the selected statement was an unbuffered
send (receive), a corresponding receive (send) statement was executed
simultaneously.
<p>
If the system does have a never claim, an <em>execution step</em> is a
combined, synchronized step: executing an (enabled) statement from the
never claim together with a step from the rest of the system, as
above.
Thus, a never claim blocks execution of the system, in those
situations in which the never claim has no enabled statements (in the
current state); also see <a href="#tempclaim">tempclaim</a>.
<p>

The <em>execution sequences</em>, or <em>behaviors</em>, of a
<tt><b>Promela</b></tt> system are the maximal (possibly infinite) sequences of
execution steps, in which the first step is taken from the initial
system state and each successive step from the state produced by the
preceding step.

In particular, notice that <tt><b>Promela</b></tt>
allows starvation of processes
during an execution.
This behavior can be influenced by the analyzer command line switch
<tt>-f</tt> (the weak fairness option).
If used, process starvation cannot occur; i.e., execution
sequences along which some process instance eventually does not make a
move anymore although the instance remains continuously enabled are no
longer possible.

<h4>Atomic statements and d_steps</h4>
Atomic statements and <tt>d_step</tt>s constrain execution elsewhere in
the system, as they execute (in principle) as a single basic statement.
Accordingly, in the presence of a never claim, an execution step of the 
system combines a <em>single</em> step in the never claim with an
execution <em>sequence</em> of the atomic statement or <tt>d_step</tt>
(defined as if there were no never claim).
Note that in the case of an atomic statement, such an execution sequence 
may end in the middle of it and the above holds for
subsequent steps within the atomic statement as well.


<h2><tt><a name="anal">Analysis</a></tt></h2>
A <tt><b>Promela</b></tt> system can be <em>exhaustively</em> (but efficiently) analyzed 
for <em>correctness violations</em>: i.e., for the existence of execution 
sequences that abort through an <tt>assert</tt>; that end in an invalid
<em>end</em>-state; that avoid cycling through certain desirable, so-called
<em>progress</em> states or that cycle through undesirable, so-called
<em>acceptance</em> states; and for  executions satisfying general
(linear time) temporal properties (or claims)  defined through
<em>never-claims</em>.

<h3><tt>End-states</tt></h3>
Valid end-states are those system states in which every process
instance and the init process has either reached the end of its
defining program body or is blocked at a statement that is labeled
with a label that starts with the prefix <tt>end</tt>.
All other states are <em>invalid</em> end-states.
<p>
Strictly speaking, valid end-states should also require channels to be
empty.
Conformance with this stricter condition is obtained
through <tt><b>Spin</b></tt>'s <tt>-q</tt> option. 
<p>
When checking for <em>state properties</em>, the verifier will
complain if there is an execution that terminates in an invalid end-state.

<h3><tt><a name="ProgSt">Progress states</a></tt></h3>
A progress state is any system state in which some process instance is
at a statement labeled with a label that starts with the prefix
<tt>progress</tt>; a <em>progress label</em>.
<p>
When checking for <em>non-progress cycles</em>, the verifier will
complain if there is an execution that does not visit infinitely often a
progress state.

<h3><tt>Acceptance states</tt></h3>
An acceptance state is any system state in which some process instance
is at a statement labeled with a label that starts with the prefix
<tt>accept</tt>; an <em>acceptance label</em>.
<p>
When checking for <em>acceptance cycles</em>, the verifier will complain
if there is an execution that visits infinitely often an acceptance
state.

<h3><tt><a name="tempclaim">Temporal claims</a></tt></h3>
Temporal claims are defined by <tt><b>Promela</b></tt> <tt>never</tt> claims
(see <a href="#never">never</a>) and are used to detect behaviors that are considered
undesirable or illegal.
<p>
When checking for state properties, the verifier will complain if
there is an execution that ends in a state in which the never claim has
terminated; i.e., has reached the closing <tt>}</tt> of its body.

When checking for acceptance cycles, the verifier will complain
if there is an execution that visits infinitely often an acceptance
state.
Thus, a temporal claim can detect illegal infinite (hence cyclic)
behavior by labeling some statements in the never claim with an acceptance
label.
<p>

In such situations the never claim is said to be <em>matched</em>.
In the absence of acceptance labels, no cyclic behavior can be matched
by a temporal claim.
Also, to check a cyclic temporal claim, acceptance labels should only
occur within the claim and nowhere else in the <tt><b>Promela</b></tt> system.
<p>

A never claim is intended to monitor every execution step in the rest of
the system for illegal behavior and for this reason it executes in lock-step.
Such illegal behavior is detected if the never claim matches along a
computation.
If a claim blocks (because no statement in its body is enabled) but it
is not at its closing <tt>}</tt>, then there is no need to explore this
computation any further because it cannot lead to a violation; whence a
blocked claim terminates execution in the rest of the system so that
other executions can be explored.
<p>
Note that if a never claim exhibits non-determinism then,
according to the definition of execution sequence, the different ways
in which this non-determinism is resolved result in different executions.

<h4><a name="exclaim">Example claim</a></h4>
Let <tt>p</tt> and <tt>q</tt> be two boolean expressions and consider the
property that
<ul><i>
``along every computation, each system state in which <tt>p</tt> is true
(a <tt>p</tt>-state) is eventually followed by a <tt>q</tt>-state''
</i></ul>
The following never claim verifies whether the property holds; i.e.,
it will detect any violation of the property:
<pre>
never {
	do
	:: p -> break
	:: true		/* or equivalently: (p || !p) */
	od;
accept:
	do
	:: !q
	od
}
</pre>
The first repetition terminates only in <tt>p</tt>-states.
Such a state should eventually be followed by a <tt>q</tt>-state.
The second repetition (hence the never claim) cannot terminate, so the
never claim either eventually blocks because the computation sequence
reaches a <tt>q</tt>-state or matches because the (infinite) computation
cycles through an acceptance state.
The latter occurs precisely if there are no subsequent <tt>q</tt>-states.
Because the analyzer guarantees an exhaustive search for computations
along which the never claim is matched, a computation violating the
property is guaranteed to be detected (if there is one).
<p>
Note that replacing <tt>skip</tt> by <tt>else</tt> would check only the
<em>first</em> occurrence of a <tt>p</tt>-state along computations.
Stated differently, by giving the first repetition the
non-deterministic choice in <tt>p</tt>-states to either break or continue
and by relying on the exhaustive search mechanism of the analyzer,
every occurrence of a <tt>p</tt>-state is checked.
In fact, one can show that it is impossible to check this property
without using non-determinism as above.

<h3><tt><a name="MemTim">Memory and Time requirements</a></tt></h3>
For this, a bit more must be said about the actual analysis process.
The basic process is recursive (though its implementation is not)
and starts in the initial system state.
In each system state, the list of enabled actions is determined.
Then each action in this list is selected, it is executed and the 
procedure is recursively applied to the new system state.
If a never claim is present, the list becomes a list of action-<em>pairs</em>:
one from the never claim together with an action
(or execution sequence if an <tt>atomic</tt> or <tt>d_step</tt> is involved)
from some active process instance.
The recursion backtracks from any system state that has already been
visited or in which there is no enabled action (pair) that has not already
been selected in this state.
Thus, the basic process is a depth-first generation of all (reachable)
system states.
In reality the process is more complex because the absence of
correctness violations need be established as well.
<p>

As to the memory demands when checking for state properties, the
visited system states need to be stored in order to decide when to
backtrack, as well as the partial computation that is being extended
(the `stack' in terms of depth-first generation) in order to know where
to backtrack to.
This, together with the number of bytes needed to represent a system
state, i.e., the size of the <em>state vector</em>, determines the amount of
memory that is needed to complete an analysis.
In particular, the set of already visited system states must be kept in
main memory as this set is accessed in an, essentially, random way during
analysis.
This is the reason why the size of the system that can be analyzed is
directly determined by the amount of physical RAM.
<p>
If analysis has to establish the presence (progress) or absence (acceptance)
of cyclic computations, both the number of stored states and the size of
the `stack' at worst doubles when compared to the case of checking
state properties.
Note that checking a never claim corresponds to the analysis of a
property in one of these three classes.
Also note that adding a non-deterministic never claim to a system
will in itself increase the state space so that it is quite possible
that the memory demands increase more than twofold when searching for
behavior matching a never-claim that has an acceptance state.
<p>
Analysis time is proportional to the number of visited configurations.

<h4><a name="MemAtD">Atomic statements and <tt>d_step</tt>s</a></h4>
An atomic statement or <tt>d_step</tt> causes the
statements in its scope to execute, in principle, as a single basic
statement.
Accordingly, the number of system states is reduced, whence the memory
needed to record the visited (global) states, because no process
instance can change state other than the one in which control resides
within the atomic statement or <tt>d_step</tt>.
In addition, system states in which control resides <em>inside</em> some
<tt>d_step</tt> need not be recorded at all; not even on the stack.

<h3><tt><a name="pored">Partial order reduction</a></tt></h3>
This is an optimized search technique that decreases the memory and
time needed for an analysis by an order of magnitude in most cases;
sometimes substantially more.
It will never increase the necessary memory and, at worst, only slightly
increase the analysis time.
The reduction method is invoked by default
and the analysis results are guaranteed to be the same
as those obtained without reduction.

Generally speaking, partial order reduction works during analysis by
deciding in each system state where there is non-determinism, whether
the property that is being verified depends on the order in which execution
steps are taken. If it is independent of this order, the analyzer fixes
an ordering and ignores executions in which these steps are taken in a
different order.
Thus, the effect is as if pieces of <tt><b>Promela</b></tt> code had been enclosed
in atomic statements, except that they are <em>dynamically</em> placed.
I.e., the execution order of syntactically the same two statements can
influence the property in one system state, whereas the property can be
independent of the ordering in another.
<p>

Partial order reduction as implemented in <tt><b>Spin</b></tt> has
the most effect on loosely coupled systems that interact through
shared, global variables and/or <em>buffered</em> channels.
If a system has no shared variables and uses only unbuffered communication
channels, there will be no reduction in memory or time.

<h4>Stutter closedness</h4>
The only requirement for using partial order reduction is that a
<tt><b>Promela</b></tt> <tt>never</tt> claim must be <em>stutter-closed</em>.
This means that the property expressed by the claim must not depend on
the number of execution steps that it remains true or false.
For example, the two never claims in the <a href="#exclaim">example</a> are stutter-closed,
whereas the claim
<pre>
	never { p; p }
</pre>
is not, since it depends on the expression <tt>p</tt> remaining true for at
least one execution step (and it has to be true in the initial system state).
<p>
Any property that can be expressed in linear temporal logic without using
the `next-state' (<tt>X</tt>) operator is guaranteed to be stutter-closed.
In fact, the above never claim would correspond to the temporal logic
formula: <tt>p && X p</tt>.
<p>

In fact, independently of whether partial order reduction is used or not,
it is probably a good idea to only verify stutter closed never claims.


<h4><a name="SearchNPC">Searching for non-progress cycles</a></h4>
Non-progress cycles can be detected using the runtime <tt>-l</tt> option.
This will cause a search for acceptance cycles with the following never
claim compiled in:
<pre>
never {
	/* non-progress: <>[] np_ */
	do
	:: skip
	:: np_ -> break
	od;
accept:
	do
	:: np_
	od
}
</pre>

This never claim matches along behaviors on which from some point onwards,
the predicate <tt>np_</tt> remains <tt>true</tt>; i.e., only non-progress
states are visited.
<p>
Note that for more complex non-progress properties, the user has to supply
her own never claim and it is here that the <tt>np_</tt>-predicate is of
use.

<h4>Increasing the amount of reduction</h4>
If a system uses buffered communications, the effectiveness of partial
order reduction can be enhanced by declaring <tt>proctype</tt>s to have
exclusive access to channels (<tt>xr</tt> and <tt>xs</tt>) whenever this is
the case.
However, doing so constrains the way a channel can be accessed:
<pre>
<b>	If you declare   Other processes may only do</b>
<tt>	xr q             send actions on q
	                 nfull(q)
	xs q             receive actions on q
	                 nempty(q) </tt></pre>
Any other type of access will give an error during analysis.
In particular the functions <tt>full()</tt> and <tt>empty()</tt>, which are
included for reasons of symmetry.

<h3><tt>Bitstate hashing</tt></h3>
Bitstate hashing is used in cases where memory is insufficient to perform an exhaustive
analysis (even with partial order reduction).
It is compatible with partial order reduction.
Bit-state hashing applies to larger models but (or, rather, because) it 
does not guarantee an exhaustive analysis.
On the other hand, when set-off against classical random simulation
techniques, it is always better to use bit-state hashing because
the coverage (i.e., the number of visited stated relative to the number
of actual states) is never worse, and usually much better, than that 
achieved with random simulation.
Using this technique, the analyzer will never incorrectly flag errors;
however, it may miss errors. 
<p>
Bit-state hashing works by allowing more states to be stored in the memory, 
<tt>M</tt>, set aside for recording visited states; the memory needed to store
the stack is not reduced.
It achieves this reduction by viewing every bit in <tt>M</tt> as a bucket in
a <em>hash table</em>.
Each system state is hashed onto a fixed number of buckets (i.e., 2),
but only the fact that a bucket has become filled is recorded.
In other words, there is <em>no collision detection</em> and if two
system states hash onto the same buckets, they are deemed to be the same
states.
It is this feature that allows many more states to be stored.
E.g., if the state vector of a system is 100 bytes then bit-state
hashing, in the ideal case of a perfect hashing function, allows upto
800 times as many states to be stored and visited as would be possible
with an exhaustive analysis using the same amount of memory.
<p>
Reality is more complex.
Hash functions are not perfect, collisions will occur and get more
common the fuller the hash table becomes and each collision potentially
causes a part of the state space to remain unexplored.
<p>
The analyzer gives an indication of the quality of a bit-state search
in the form of a <em>hash factor</em>: the fraction of buckets that
were filled.  I.e., a hash-factor of 100 means that, on average, at
most 1 out of every 100 bits in <tt>M</tt> was set.
This is taken as indicating a good quality search.
<tt><b>Spin</b></tt> reports in this case
``expected coverage: >= 99.9% on avg.''.
For a hash-factor between 10 and  100, <tt><b>Spin</b></tt>
gives an expected coverage of 98% on average.
These are heuristic estimates, and the variance can be large.
E.g., experiments indicate that `98% coverage on average' can mean as low
as 84% during an actual analyzer run.
On the other hand, such coverage still is much superior over what is
achieved by a standard random simulation.
<hr>
<table cols=3>
<tr>
<td valign=top width=200>
<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>
</td>
<td valign=top width=100 align=center></td>
<td valign=top width=400 align=right>
<a href="http://spinroot.com/spin/">Spin HomePage</a></td></tr>
</table>
</html>