Promela Syntax

The following describes only the basic constructions of the Promela language that are used in generating Engee models or are useful in analyzing the generated code. The syntax of Promela, intended for the specification of parallel programs, is not involved in Engee and is hardly considered here.

General (lexical) information:

The identifiers in Promela satisfy the regular expression [a-zA-Z_][a-zA-Z_0-9]*;
Since spin It uses an available C language preprocessor as a preprocessor, multi-line and single-line (undocumented feature) comments of the ISO C99 standard are supported.

Structure of the source file in Promela language

The text of the program in Promela language can consist of three main sections:

Defining user-defined data types and global variables;
Process Definitions;
Operators ltl.

Definitions of user-defined data types and global variables

In Promela, definitions of user-defined data types and global variables can be interspersed, but must be placed at the beginning of the file — before the definitions of processes and operators. ltl.

Custom Data Types

The Promela code generator in Engee uses only one Promela construct designed to define custom data types. — typedef, which is used to define the types of data structures.

Syntax typedef used by Engee:

"typedef" name "{" declaration_list "}" ";"

where name — an identifier that is not keyword Promela, and grammar declaration_list it has the form:

declaration_list ::= declaration ";" { declaration ";" }

declaration ::= type_name variable_name [ "[" array_size "]" ]

type_name ::= "bool" | "byte" | "short" | "int"

variable_name ::= name

array_size ::= constant_expression

constant_expression — a constant expression with an integer value.

For example, a structural type declaration S, which includes:

32-bit field i32 signed integer type;
16-bit field i16 signed integer type;
8-bit field u8 an unsigned integer type;
1-bit field b an unsigned integer (logical) type;
Array a of 10 logical type elements.

can be described as

typedef S {
    int i32;
    short i16;
    byte u8;
    bool b;
    bool a[10];
};

With a more detailed description of the syntax typedef available on project page Promela/Spin.

Global variables

The grammar for defining a global variable in Promela looks like this:

global_variable_declaration ::=
    type_name variable_name [ "=" initializer_scalar ] ";"
|   type_name variable_name [ "[" array_size "]" ] [ "=" initializer_list ] ";"

initializer_scalar ::= constant_expression

initializer_list ::= "{" constant_expression [ "," constant_expression ]* "}"

Grammars type_name, variable_name, array_size and constant_expression described above.

Scalar variables, one-dimensional arrays, and variable structures can be defined.

For example, the following code defines a variable-an array of 5 elements of the type byte, initialized with units:

byte x[5] = {1, 1, 1, 1, 1};

If a scalar variable is not explicitly initialized, then spin sets its initial value to zero, and if it is an array or structure, fills its elements with zeros.

Defining processes

When generating a model in Promela, Engee defines a process of a single type: fsm (from "Finite State Machine").

active proctype fsm() { ... }

This means that the process fsm it will run in a single instance in the mode simulations. If the mode is used verification, then a description of the process fsm, together with the LTL specification, converted to an automaton, will be analyzed by the generated verifier.

The body of the process description consists of a sequence of operators such as definitions of local variables, assignment operators, and program flow control operators.

In Promela, operators are semantically divided into blocking and non-blocking ones, but in Promela models generated by the Engee generator, only non-blocking operators are used.

Definitions of local variables

The syntax for defining Promela local variables is completely the same as syntax definitions of global variables.

Regardless of where the local variable definition operator is placed: at the beginning of the process body or before the first use, the variable definition is performed as if it were located at the beginning of the process body.

This means that you cannot define more than one local variable with the same name. For example:

{ int a; }
{ int a; }

In this case, initialization of local variables is performed in the context where the variable is declared. That is, the code in the example:

int a = 1;
{
    a = 2;
    int b = a + 1;
}

semantically equivalent to the code:

int a = 1;
int b;
a = 2;
b = a + 1;

not the code:

int a = 1;
int b = a + 1;
a = 2;

Assignment operators

On the left side of the assignment operator, you can use the name of a scalar variable, array element, or structure.

On the right side is an arithmetic or logical expression containing variable names, logical or integer constants.

Increment operators are also supported (++) and decrement (--).

Logical expressions

When generating Promela Engee models, logical bundles can be used:

Denial — !;
Conjunction (logical And) — &&;
Disjunction (logical OR) — ||.

In addition, comparison operators can be used. ==, !=, <, ⇐, > and >=.

Arguments to logical operators can be expressions of integer or logical types.

Arithmetic expressions

The following integer arithmetic operations are implemented in the Promela code generator Engee: unary + and - addition, subtraction, multiplication and division modulo (%).

Since the code generator uses expressions in the Julia language as source expressions, where the result of division is a type Float, and floating-point calculations are not supported in Promela, the division operator / the Promela model code generator is not implemented.

Execution Flow Control Statements

The Promela code generator can use three types of control operator syntax: conditional operator if and two loop operators do and for.

Conditional operator `if`

In Promela, the operator if it is a type of non-deterministic link:https://en.wikipedia.org/wiki/Guarded_Command_Languagethe [conditional operator] of Edsger Dijkstra:

if_operator ::= "if" guarded_command_set "fi"

guarded_command_set ::= guarded_command { guarded_command }

guarded_command ::= guard "->" guarded_list

guard ::= boolean_expression | "else"

guarded_list ::= statement ";" { statement ";" }

Where statement — any Promela operator, and boolean_expression — logical expression.

The code generator of Promela models does not use the capabilities of non-deterministic operator programming if therefore , each such operator looks like this:

if
:: <условие> -> <действие>
:: else -> <альтернативное_действие>
fi

If there is no alternative action, it is replaced by an empty operator. skip.

A branch else It is necessary even in the absence of an alternative action, as otherwise the model may be blocked.

For example, the operator

if
:: false -> ...
fi

it is equivalent to eternal waiting.

The loop operator `do`

In Promela, the operator do It is a variation of another non-deterministic operator. — link:https://en.wikipedia.org/wiki/Guarded_Command_LanguageEdsger Dijkstra’s [loop operator] with a similar syntax:

do_operator ::= "do" guarded_command_set "od"

where guarded_command_set described above.

The code generator of Promela models uses a deterministic version of the loop do, which can have two branches:

do
:: <условие> -> <действие>
:: else -> break;
od

It is equivalent to a loop while:

while (<условие>) {
    <действие>;
}

Or one branch:

do
:: true -> <действие>
od

which corresponds to an infinite loop.

The loop operator `for`

The Promela code generator uses one of three syntax options for:

for_operator ::= "for" "(" variable_name ":" integer_expression ".." integer_expression ")" "{" statement_list "}"

statement_list ::= statement ";" { statement ";" }

where variable_name — the name of a local or global variable, and integer_expression — an expression with an integer or boolean value type.

For example, the semantics of the operator is as follows:

for (i : a .. b) {
    x = x + i;
}

Here are the expressions a and b are calculated once before the loop, and if a ⇐ b, a variable i consistently accepts values from a before b inclusive.

If a > b, then the loop is not executed.

The unconditional transition operator `goto`

Promela supports labels with syntax:

label_definition ::= label ":"

and the unconditional transition operator:

goto_operator ::= "goto" label ";"

where label — the name of the label, any valid identifier, except keywords.

Some label names have a special meaning for spin: these are labels with prefixes accept, end and progress. The Promela model generator in Engee does not use such labels, and it is recommended to avoid them unnecessarily.

Invariants (assertions)

In addition to the LTL specification mechanism, the Promela language allows verification using the operator assert(<logical formula>) (for more information, see assert).

Its semantics are similar to the C/C++ languages: if the operator condition is false, execution or verification fails.

Operator assert it is convenient because it is always checked, regardless of the mode (simulation or verification) and the selected operator ltl.

Promela Keywords

A list of reserved words that cannot be used as identifiers:

active

assert

atomic

unsigned

bool

break

byte

chan

d_step

else

empty

enabled

eval

false

full

goto

hidden

init

mtype

nempty

never

nfull

pc_value

priority

proctype

provided

select

short

show

skip

timeout

trace

true

typedef

unless

Operator Block `ltl`

The source text in Promela may end with a block consisting of the operators ltl.

Operator syntax ltl:

ltl_operator ::= "ltl" name "{" ltl_formula "}"

where name — name of the specification (LTL formulas), and ltl_formula — by yourself LTL Linear Time Logic specification.

For a more detailed description of working with specifications, see the chapters Insert specifications and Generation and launch of the verifier.