Синтаксис Promela

Далее описываются только базовые конструкции языка Promela, применяющиеся при генерации из моделей Engee или полезные при анализе сгенерированного кода. Синтаксис Promela, предназначенный для спецификации параллельных программ, в Engee не задействован и здесь почти не рассматривается.

Общая (лексическая) информация:

Идентификаторы в Promela удовлетворяют регулярному выражению [a-zA-Z_][a-zA-Z_0-9]*;
Так как spin в качестве препроцессора использует доступный препроцессор языка Си, поддерживаются многострочные и однострочные (недокументированная возможность) комментарии стандарта ISO C99.

Строение исходного файла на языке Promela

Текст программы на языке Promela может состоять из трех основных разделов:

Определение пользовательских типов данных и глобальных переменных;
Определения процессов;
Операторы ltl.

Определения пользовательских типов данных и глобальных переменных

В Promela определения пользовательских типов данных и глобальных переменных могут перемежаться, но должны быть размещены в начале файла — до определений процессов и операторов ltl.

Пользовательские типы данных

Генератор кода Promela в Engee использует только одну конструкцию Promela, предназначенную для определения пользовательских типов данных — typedef, которая служит для определения типов структур данных.

Синтаксис typedef, используемый Engee:

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

где name — идентификатор, не являющийся ключевым словом Promela, а грамматика declaration_list имеет вид:

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 — константное выражение, имеющее целочисленное значение.

Например, объявление структурного типа S, включающего в себя:

32-битовое поле i32 знакового целочисленного типа;
16-битовое поле i16 знакового целочисленного типа;
8-битовое поле u8 беззнакового целочисленного типа;
1-битовое поле b беззнакового целочисленного (логического) типа;
Массив a из 10 элементов логического типа.

может быть описано как

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

С более подробным описанием синтаксиса typedef можно ознакомиться на странице проекта Promela/Spin.

Глобальные переменные

Грамматика определения глобальной переменной в Promela имеет вид:

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 ]* "}"

Грамматики type_name, variable_name, array_size и constant_expression описаны выше.

Допускается определение переменных-скаляров, одномерных массивов и переменных-структур.

Например, следующий код определяет переменную-массив из 5 элементов типа byte, инициализированный единицами:

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

Если скалярная переменная не инициализирована явно, то spin устанавливает ее начальное значение равным нулю, а если это массив или структура — заполняет ее элементы нулями.

Определение процессов

При генерации модели на языке Promela Engee определяет процесс единственного типа: fsm (от "Finite State Machine").

active proctype fsm() { ... }

Это означает, что процесс fsm будет запускаться в единственном экземпляре в режиме симуляции. Если используется режим верификации, то описание процесса fsm, совместно с LTL-спецификацией, преобразованное в автомат, будет анализироваться порожденным верификатором.

Тело описания процесса состоит из последовательности таких операторов, как определения локальных переменных, операторы присваивания и операторы управления потоком выполнения программы.

В Promela операторы семантически подразделяются на блокирующие и неблокирующие, но в Promela-моделях, порождаемых генератором Engee, используются только неблокирующие операторы.

Определения локальных переменных

Синтаксис определения локальных переменных Promela полностью совпадает с синтаксисом определения глобальных переменных.

Независимо от того, где размещен оператор определения локальной переменной: в начале тела процесса или перед первым использованием, — определение переменной выполняется так, как если бы оно было расположено в начале тела процесса.

Из этого следует, что нельзя определить более одной локальной переменной с одним и тем же именем. Например:

{ int a; }
{ int a; }

При этом инициализация локальных переменных выполняется в том контексте, где объявлена переменная. То есть код в примере:

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

семантически эквивалентен коду:

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

а не коду:

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

Операторы присваивания

В левой части оператора присваивания допускается использовать имя скалярной переменной, элемента массива или структуры.

В правой части — арифметическое или логическое выражение, содержащее имена переменных, логические или целочисленные константы.

Поддерживаются также операторы инкремента (++) и декремента (--).

Логические выражения

При генерации моделей Promela Engee могут использоваться логические связки:

Отрицание — !;
Конъюнкция (логическое И) — &&;
Дизъюнкция (логическое ИЛИ) — ||.

Кроме того, могут использоваться операторы сравнения ==, !=, <, <=, > и >=.

Аргументами логических операторов могут быть выражения целочисленного или логического типов.

Арифметические выражения

В Promela-генераторе кода Engee реализованы следующие целочисленные арифметические операции: унарные + и -, сложение, вычитание, умножение и деление по модулю (%).

Так как в качестве исходных выражений генератор кода использует выражения на языке Julia, где результат деления является типом Float, а вычисления с плавающей точкой в Promela не поддерживаются, оператор деления / в генераторе кода Promela-моделей не реализован.

Операторы управления потоком выполнения

Генератор кода Promela может использовать три вида синтаксиса управляющих операторов: условный оператор if и два оператора цикла do и for.

Условный оператор `if`

В Promela оператор if является разновидностью недетерминированного условного оператора Эдсгера Дейкстры:

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 ";" }

Где statement — любой оператор Promela, а boolean_expression — логическое выражение.

Генератор кода Promela-моделей не использует возможности недетерминированного программирования оператора if, поэтому каждый такой оператор выглядит так:

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

Если альтернативное действие отсутствует, то оно заменяется пустым оператором skip.

Ветка else необходима даже при отсутствии альтернативного действия, так как в противном случае модель может заблокироваться.

Например, оператор

if
:: false -> ...
fi

эквивалентен вечному ожиданию.

Оператор цикла `do`

В Promela оператор do является разновидностью еще одного недетерминированного оператора — оператора цикла Эдсгера Дейкстры со сходным синтаксисом:

do_operator ::= "do" guarded_command_set "od"

где guarded_command_set описан выше.

Генератор кода Promela-моделей использует детерминированный вариант цикла do, который может иметь две ветки:

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

Он эквивалентен циклу while:

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

Или одну ветку:

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

что соответствует бесконечному циклу.

Оператор цикла `for`

Генератор кода Promela использует один из трех вариантов синтаксиса for:

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

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

где variable_name — имя локальной или глобальной переменной, а integer_expression — выражение с целочисленным или логическим типом значения.

Например, семантика оператора следующая:

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

Здесь выражения a и b вычисляются один раз перед циклом, и если a <= b, переменная i последовательно принимает значения от a до b включительно.

Если a > b, то цикл не выполняется.

Оператор безусловного перехода `goto`

В Promela поддерживаются метки с синтаксисом:

label_definition ::= label ":"

и оператор безусловного перехода:

goto_operator ::= "goto" label ";"

где label — имя метки, любой допустимый идентификатор, кроме ключевых слов.

Некоторые имена меток имеют особое значение для spin: это метки с префиксами accept, end и progress. Генератор моделей Promela в Engee не использует такие метки, и рекомендуется избегать их без необходимости.

Инварианты (assertions)

Помимо механизма LTL-спецификаций, язык Promela позволяет выполнять верификацию с помощью оператора assert(<логическая_формула>) (подробнее см. assert).

Его семантика аналогична языкам Си/Си++: если условие оператора ложно, выполнение или верификация завершается с ошибкой.

Оператор assert удобен тем, что проверяется всегда — независимо от режима (симуляция или верификация) и выбранного оператора ltl.

Ключевые слова Promela

Список зарезервированных слов, которые нельзя использовать в качестве идентификаторов:

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

Блок операторов `ltl`

Исходный текст на языке Promela может завершаться блоком, состоящим из операторов ltl.

Синтаксис оператора ltl:

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

где name — имя спецификации (формулы LTL), а ltl_formula — сама спецификация логики линейного времени LTL.

Более подробное описание работы со спецификациями см. в главах Вставка спецификаций и Генерация и запуск верификатора.