INTRODUCTION
Six parts of the Promela language are discussed in separate sections of this manual. A seventh section gives a brief motivation for things that are intentionally outside the language. The sections are:

• 1. Meta Terms (translated by preprocessors into vanilla Promela)
• 2. Declarators (for defining process, channel, and data objects)
• 3. Control Flow Constructors (separators, compound statements, jumps, labels, etc.)
• 4. Basic Statements (such as send, receive, assignment, etc.)
• 5. Predefined Functions and Operators (such as len, run, nempty, etc.)
• 6. Grammar Rules and Lexical Units.
• 7. Omissions (such as floating point, probabilities, etc.)

References to terms defined in this manual are in bold, with the corresponding section number in parentheses, e.g. send(4), len(5).

In the tradition of the well-known Unix manuals, each manual page that follows this introduction contains some or all of the following defining elements.

• NAME
  A one sentence synopsis of the construct and its main purpose.
• SYNTAX
  In the syntax rules text is reproduced as it is typed. Optional terms are enclosed in (non-quoted) square brackets. The Kleene star * is used to indicate zero or more repetitions of an optional term. When the special symbols '[', ']', '*', appear as literals, they are quoted. For instance, in

  chan name = '[' const ']' of { typename [ , typename ] * }
  

  the first two square brackets are literals, and the last two enclose an optional part of the definition.

All terms set in italic , such as name , const, and typename , refer to the grammar rules from Section 6.

• EXECUTABILITY
  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 Semantics below. If the executability clause is described as True , no conditions other than the implied conditions apply.
• EFFECT
  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 None , no effect other than the implicit change in local state is defined. See also the description under Semantics below.
• DESCRIPTION
  Describes in informal terms what the purpose and use is of the language element being defined.
• EXAMPLES
  Gives some typical applications of the construct.
• NOTES
  Adds some additional notes about special circumstances or cautions.
• SEE ALSO
  Gives references to other parts of this reference manual that may provide additional explanations.

SEMANTICS
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 proctype declarations. Similarly, the domains of values that variables can hold are derived from variable type declarations.

The semantics engine executes the model in a step by step manner. In each step, one executable 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 executability clause, as described in this manual. For the selected statement, the effect 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.

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.

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 sets , identifiers , integers , and Booleans .

• (S.1) A variable is a tuple {name,scope,domain,inival,curval}
  where
  • name is an identifier that is unique within scope ,
  • scope is defined by an integer (see below).
  • domain is a finite set of integer s.
  • inival , the initial value, is an integer within domain , and
  • curval , the current value, is an integer within domain .

In the remainder of this section we refer to the elements of a tuple with a dot notation. For instance, if v is a variable, then v.scope is its scope.

The scope of a variable either identifies all active processes (for globally declared variables) or one specific active process. For the purposes of this definition, we can assume that a non-negative integer identifies the pid (S.4) of one active process, and an arbitrary negative integer identifies all active processes. The type of a variable determines its domain . For instance, a variable of type bit (see datatypes(2)) has domain {0,1}.

• (S.2) A message is an ordered set of variables (S.1).
• (S.3) A channel is a tuple {ch_id,nslots,contents}
  where
  • ch_id is an integer (see below),
  • nslots is an integer , and
  • contents is an ordered set of messages (S.2) with maximum cardinality nslots .

A non-negative ch_id will be used to identify an active channel , while a negative number will identify a channel template from which more channels of the same type may be instantiated. Note that the definition of a channel does not contain a scope , 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 Promela, i.e., every channel is in principle accessible to every active process, by knowledge of the identifying ch_id .

• (S.4) A process is a tuple {pid,lvars,lstates,initial,curstate,trans}
  where
  • pid is an integer (see below),
  • lvars is a finite set of variables (S.1), each with scope=pid ,
  • lstates is a finite set of integers (see below),
  • initial and curstate are elements of set lstates , and
  • trans is transition relation (S.5) defined on lstates .
  For the purpose of definition S.4, we can assume that a non-negative value of pid identifies an active process , while a negative value for the pid field identifies a process template from which extra active processes of the same type may be instantiated. In the initial state of a newly instantiated process (see active(3), run(5)) curstate=initial , and all elements of lvars have curval=inival .

We will refer to the elements of set lstates as the local states of a process (S.4). The integer values suffice to uniquely identify each state within the set, but hold no more information.

• (S.5) A transition relation is a finite set of tuples {tr_id,source,target,cond,effect,prty,rv}
  where
  • tr_id is a non-negative integer ,
  • source and target are local states (i.e., integer s),
  • cond is a Boolean condition(4) on the global system state (S.6),
  • effect is a function that modifies the global system state (S.6),
  • prty and rv are integer s.

The elements prty and rv are used in cond and effect definitions to enforce the semantics of, respectively, the unless(3) construct, and of synchronous message passing operations, see send(4).

• (S.6) A global system state is a tuple of the form {gvars,procs,chans,exclusive,handshake,timeout,else,stutter}
  where
  • gvars is a finite set of global variables (S.1), each with scope=-1 ,
  • procs is a finite set of active processes (S.4), each with pid!=-1 ,
  • chans is a finite set of channels (S.3), each with ch_id!=-1 ,
  • exclusive , and handshake are integer s, and
  • timeout , else , and stutter are Boolean s.
• In the initial system state all elements of procs are in their initial state (see S.4), all elements of gvars have curval=inival (see S.1), all elements of chans have contents={} (i.e., the empty set) (see S.3), exclusive and handshake are zero, and timeout and else are False . The initial value of stutter is also False . (It can be set to True only by the verifier, when it replaces the default check for safety properties with a check for liveness properties.)

The definitions S.1 to S.6 capture the minimal information that is needed to define the semantics of the Promela 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 Promela constructs that is independent of the Spin tool.

OPERATIONAL MODEL, SEMANTICS ENGINE
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.

Let E be a set of pairs { p,t }, with p a process, and t a transition. Let executable(s) be a function, yet to be defined, that returns a set of such pairs, one for each executable transitions in system state s . The semantics engine then performs as follows.

  1 while ((E = executable(s)) != {})
  2 {
  3 	for some {p,t} from E
  4 	{	s' = apply(t.effect, s)
  5 
  6 		if (handshake == 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 			handshake = 0
 20 	}	}	
 21 }
 22 while (stutter) { s = s }	/* the 'stutter' extension */

To verify liveness properties with Spin, we must be able to treat finite executions as special cases of infinite executions. The standard way of doing so is to define a stutter extension of finite executions, where the final state is repeated ad infinitum. The semantics engine above uses the system variable stutter 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.

The function apply() applies the effect of the selected transition to the system state, possibly modifying system and local variables, the contents of channels, or even the values of exclusive and handshake , as defined in the effect clauses from atomic(3), and send(4), 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. send(4)). On line 11 the transitions that have now become executable are selected. The definition of the function executable() 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 E . 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).

The main part of the semantics definition is in the definition of what precisely constitutes an executable transition. One part will be clear: in the current system state the executability clause t.cond must be satisfied. But there is more.

The following specification of the function executable() resolves these issues. To avoid confusion, the state variables timeout and else are set in bold. These two variables are the only two that can be modified within this function, as part of the selection process.

  1 Set
  2 executable(State s)
  3 {	new Set E
  4 	new Set e
  5 
  6 	E = {}
  7 	timeout = False
  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 = {};  else = False
 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) == True)
 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 (else == False)
 26				{	else = True
 27					goto OneProc
 28				} # or else lower the priority
 29 	}	}	}
 30 
 31 	if (E == {} and exclusive != 0)
 32 	{	exclusive = 0
 33 		goto AllProcs
 34 	}
 35 	if (E == {} and timeout == False)
 36 	{	timeout = True
 37 		goto AllProcs
 38 	}
 39 
 40 	return E	# defining the set of executable transitions
 41 }

• The test on line 10-11 checks the value of the system variable exclusive . 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 atomic sequence (see atomic(3)) will set exclusive to the value of the p.pid , 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).
• 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 between processes. Priorities are defined in Promela with the unless construct, see unless(3).
• 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.
• 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.
• The test on line 19, finally, checks if the executability condition for the transition itself is satisfied.

If no transitions are found to be executable with the default value False for system variable else, the transitions of the current process are checked again, this time with else equal to True (line 26-27). If no transitions are executable in any process, the value of system variable timeout is changed to True and the entire selection process is repeated (line 32-35). The new value of timeout 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 Promela prohibits the use of both else and timeout within a single condition statement.

Note that the semantics engine does not establish the validity or invalidity of correctness requirements.

INTERPRETING PROMELA SEMANTICS
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 Promela 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 Promela proper by preprocessors. Section 2 defines the Promela syntax for declaration of variables, processes, and channels. Section 3 defines how Promela's control-flow constructs correspond to the underlying transition relations. An if 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 if , do , break , or goto ; it merely deals with local states and transitions.

Some Promela 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 Promela constructs basic statements . Section 4 defines the transition elements for each basic statement in the language. Sections 5 and 6 of this manual, finally, define the remaining Promela syntax rules for the elements of a basic statement.

THREE EXAMPLES
Consider the following Promela system.

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 }

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 }

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 }

• The definition of unless(3) 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.
• 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.
• The effect clause of the rendezvous send operation, send(4), states that the value of handshake will be set the value of ch_id for the channel used. Lines 17-18 in the semantics engine then imply that no statement can now be executed unless it has the rv 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.

We are now ready to resolve the semantics questions for each of the three cases.

In the first example , according to the priority rule enforced by the unless operator, two statements will be executable in the initial state: x!0 and y!0 . Either one could be selected for execution. If the first is executed, we enter a rendezvous offer, with handshake set to the ch_id of channel x . In the intermediate global state s' then reached (line 11-18 in the main execution loop of the semantics engine), only one statement can be added to set E' , namely x?0 . The final successor state will have handshake == 0 and both processes in their final state. Alternatively, y!0 could be selected for execution, with an analogous result.

In the second example , only one statement is executable in the initial system state: y!0 , and only the corresponding handshake can take place.

In the third example , the first two statements considered, at the highest priority, are both unexecutable. One priority level lower, though, two statements become executable: x!0 and y!0 , and the resulting two system executions are again analogous to those from the first example.

NOTES ON VERIFICATION
The addition of a verification option does not affect the semantics of a Promela 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 never claim. The reason is that these language elements have no formal semantics within the model: they cannot be used to define any part of the behavior of a model.

Assertions, special labels, and never claims are used for making meta statements about the semantics of a model. The verifier determines how such meta statements are to be interpreted.

When the verifier checks for safety properties, it is interested in cases where an assert 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 stutter, used in the definition of the semantics engine on line 22, is set to False in this case, and any mechanism can be in principle used to generate the executions of the system, in search of the violations.

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 progress states, or infinitely many traversals of user-defined accept states. The predefined system variable stutter, used in the definition of the semantics engine on line 22, is set to True 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.

THE NEVER CLAIM
For purposes of verification it is not necessary that indeed all finite or infinite executions that comply with the formal semantics are also generated. In fact, the verifier Spin 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 never claim comes in: the never claim does not define new semantics, but is used to identify that part of the existing semantics that violates an independently stated correctness criterion.

The interpretation of the never claim by the verifier in the context of the semantics engine is as follows. Note that the purpose of the claim is to suppress 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.

  1 while ((E = executable(s)) != {})
 *2 {	if (check_fails()) Stop;
  3 	for some {p,t} from E
  \&. . .
 21 }
*22 while (stutter) { s = s; if (check_fails()) Stop; }

With or without a constraint provided by a never 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 Promela semantics definition given here.