Data types

The basic data types used in PROMELA are presented in the table below. The sizes in bits are given for a PC i386/Linux machine.

The names bit and bool are synonyms for a single bit of information. A byte is an unsigned quantity that can store a value between 0 and 255. shorts and ints are signed quantities that differ only in the range of values they can hold.

Variables can also be declared as arrays. For example, the declaration:

 int x [10];

declares an array of 10 integers that can be accessed in array subscript expressions like:

x[0] = x[1] + x[2];

But the arrays can not be enumerated on creation, so they must be initialised as follows:

<nowiki/>
 int x[3];
 x[0] = 1;
 x[1] = 2;
 x[2] = 3;

The index to an array can be any expression that determines a unique integer value. The effect of an index outside the range is undefined. Multi-dimensional arrays can be defined indirectly with the help of the typedef construct (see below).

Processes

The state of a variable or of a message channel can only be changed or inspected by processes. The behavior of a process is defined by a proctype declaration. For example, the following declares a process type A with one variable state:

<nowiki/>
 proctype A()
 {
     byte state;
     state = 3;
 }

The proctype definition only declares process behavior, it does not execute it. Initially, in the PROMELA model, just one process will be executed: a process of type init, that must be declared explicitly in every PROMELA specification.

New processes can be spawned using the run statement, which takes an argument consisting of the name of a proctype, from which a process is then instantiated. The run operator can be used in the body of the proctype definitions, not only in the initial process. This allows for dynamic creation of processes in PROMELA.

An executing process disappears when it terminates—that is, when it reaches the end of the body in the proctype definition, and all child processes that it started have terminated.

A proctype may also be active (below).

Atomic construct

By prefixing a sequence of statements enclosed in curly braces with the keyword atomic, the user can indicate that the sequence is to be executed as one indivisible unit, non-interleaved with any other processes.

<nowiki/>
 atomic
 {
     statements;
 }

Atomic sequences can be an important tool in reducing the complexity of verification models. Note that atomic sequences restrict the amount of interleaving that is allowed in a distributed system. Intractable models can be made tractable by labeling all manipulations of local variables with atomic sequences.

Message passing

Message channels are used to model the transfer of data from one process to another. They are declared either locally or globally, for instance as follows:

chan qname = [16] of {short}

This declares a buffered channel that can store up to 16 messages of type short (capacity is 16 here).

The statement:

qname ! expr;

sends the value of the expression expr to the channel with name qname, that is, it appends the value to the tail of the channel.

The statement:

qname ? msg;

receives the message, retrieves it from the head of the channel, and stores it in the variable msg. The channels pass messages in first-in-first-out order.

A rendezvous port can be declared as a message channel with the store length zero. For example, the following:

chan port = [0] of {byte}

defines a rendezvous port that can pass messages of type byte. Message interactions via such rendezvous ports are by definition synchronous, i.e. sender or receiver (the one that arrives first at the channel) will block for the contender that arrives second (receiver or sender).

When a buffered channel has been filled to its capacity (sending is "capacity" number of outputs ahead of receiving inputs), the default behavior of the channel is to become synchronous, and the sender will block on the next sending. Observe that there is no common message buffer shared between channels. Increasing complexity, as compared to using a channel as unidirectional and point to point, it is possible to share channels between multiple receivers or multiple senders, and to merge independent data-streams into a single shared channel. From this follows that a single channel may also be used for bidirectional communication.

Control flow constructs

There are three control flow constructs in PROMELA. They are the case selection, the repetition and the unconditional jump.

<nowiki/>
 if
 :: (a != b) -> option1
 :: (a == b) -> option2
 fi

<nowiki/>
 if
 :: (A == true) -> option1;
 :: (B == true) -> option2; /* May arrive here also if A==true */
 :: else -> fallthrough_option;
 fi

<nowiki/>
 if
 :: value = 3;
 :: value = 4;
 fi

<nowiki/>
 do
 :: count = count + 1
 :: a = b + 2
 :: (count == 0) -> break
 od

<nowiki/>
 do
 :: count = count + 1
 :: a = b + 2
 :: (count == 0) -> goto done
 od
 done:
 skip;

Assertions

An important language construct in PROMELA that needs a little explanation is the assert statement. Statements of the form:

assert(any_boolean_condition)

are always executable. If a boolean condition specified holds, the statement has no effect. If, however, the condition does not necessarily hold, the statement will produce an error during verifications with SPIN.

Complex data structures

A PROMELA typedef definition can be used to introduce a new name for a list of data objects of predefined or earlier defined types. The new type name can be used to declare and instantiate new data objects, which can be used in any context in an obvious way:

<nowiki/>
 typedef MyStruct
 {
     short Field1;
     byte Field2;
 };

The access to the fields declared in a typedef construction is done in the same manner as in C programming language. For example:

MyStruct x;
x.Field1 = 1;

is a valid PROMELA sequence that assigns to the field Field1 of the variable x the value 1.

Active proctypes

The active keyword can be prefixed to any proctype definition. If the keyword is present, an instance of that proctype will be active in the initial system state. Multiple instantiations of that proctype can be specified with an optional array suffix of the keyword. Example:

<nowiki/>
 active proctype A() { ... }
 active [4] proctype B() { ... }

Executability

The semantics of executability provides the basic means in Promela for modeling process synchronizations.

<nowiki/>
 mtype = {M_UP, M_DW};
 chan Chan_data_down = [0] of {mtype};
 chan Chan_data_up   = [0] of {mtype};
 proctype P1 (chan Chan_data_in, Chan_data_out)
 {
     do
     ::  Chan_data_in  ? M_UP -> skip;
     ::  Chan_data_out ! M_DW -> skip;
     od;
 };
 proctype P2 (chan Chan_data_in, Chan_data_out)
 {
     do
     ::  Chan_data_in  ? M_DW -> skip;
     ::  Chan_data_out ! M_UP -> skip;
     od;
 };
 init
 {
     atomic
     {
         run P1 (Chan_data_up, Chan_data_down);
         run P2 (Chan_data_down, Chan_data_up);
     }
 }

In the example, the two processes P1 and P2 have non-deterministic choices of (1) input from the other or (2) output to the other. Two rendezvous handshakes are possible, or executable, and one of them is chosen. This repeats forever. Therefore, this model will not deadlock.

When Spin analyzes a model like the above, it will verify the choices with a non-deterministic algorithm, where all executable choices will be explored. However, when Spin's simulator visualizes possible non-verified communication patterns, it may use a random generator to resolve the "non-deterministic" choice. Therefore, the simulator may fail to show a bad execution (in the example, there is no bad trail). This illustrates a difference between verification and simulation. In addition, it is also possible to generate executable code from Promela models using Refinement.^[3]

Keywords

The following identifiers are reserved for use as keywords.