И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin, страница 5

Еслипроцесс достиг точки кода, где содержится невыполнимый оператор, то процессблокируется. Он может стать снова выполнимым, если ДРУГОЙ активный процессвыполнит действия, позволяющие оператору, блокированному в данном процессе,выполняться далее.Благодаря правилу выполнимости, запись многих операций в Promela упрощается.Например, вместо того, чтобы писать цикл активного ожидания:while (a != b) ->skip/* ожидать до тех пор, пока не выполнится условие a==b */где skip является пустым (нулевым) оператором, в Promela достаточно написать выражение:17(a == b)Это пример “пассивного” ожидания, когда процесс приостанавливается до выполненияусловия (в данном случае - равенства а и b).Рассмотрим следующую модель, в которой два процесса разделяют доступ к глобальнойпеременной state.byte state = 1;active proctype A(){byte tmp;(state==1) -> tmp = state; tmp = tmp+1; state = tmp}active proctype B(){byte tmp;(state==1) -> tmp = state; tmp = tmp-1; state = tmp}Процессы ожидают выполнения условия (state == 1).

Если каждый из процессов пройдетэто условие до того, как другой изменит значение state, выполнив оператор state = tmp,то оба процесса завершатся, хотя итоговое значение глобальной переменной state будетнепредсказуемо. В результате работы этой программы после ее завершения переменнаяstate может иметь любое значение: 0, 1 или 2. Если же один из процессов успеет изменитьзначение переменной state до проверки условия другим процессом, то другой процессзаблокируется.ВыраженияДля построения выражений в языке Promela используются операторы, схожие с операторамиязыка С.

В порядке приоритетов они приведены в таблице 2. Как обычно, в случае сомненийо порядке выполнения операторов и для большей ясности рекомендуется использоватькруглые скобки.В ыражения в Promela рассматриваются как утверждения, т.е. проверяются на истинностьложность в любом контексте.

Выражение выполнимо тогда и только тогда, когда его булевозначение истинно (true), что эквивалентно любому ненулевому значению целочисленнойпеременной.Табл. 2. Допустимые операторы предшествования в выражениях на языке Promela(по старшинству от старших к младшим).Операторы() []! ++ -* / %+ << >>< <= > >=== !=&^|&&Направлениедействияслева направосправа налевослева направослева направослева направослева направослева направослева направослева направослева направослева направоКомментарийскобки, скобки массивовотрицание, увеличение на 1, уменьшение на 1умножение деление модульприбавить, отнятьсдвиг влево, сдвиг вправооператоры отношенийравенство, неравенствопобитовое Ипобитовое исключающее ИЛИпобитовое ИЛИлогическое И18||-> :=слева направосправа налевосправа налевологическое ИЛИоператоры условийприсваиваниеОператор присваиванияvariable = expressionне рассматривается как выражение, так же, как и оператор печати.

Эти операторы всегдавыполнимы. При выполнении оператора присваивания в Promela сначала оцениваетсявыражение, стоящее справа (сначала инициализируются значения переменных выражения,если это не было сделано ранее, потом к ним применяются соответствующие операторы изтабл. 2). После оценки полученный результат выражения, в случае необходимости,обрезается до значения того типа, которому принадлежит переменная variable, ипеременная variable получает это значение.Использование инкремента и декремента в Promela отличается от их использования в С: онимогут быть только постфиксными (т.е. можно записать a++, но нельзя ++а) и могутиспользоваться только в выражении, но не в операторе присваивания.Входные/выходные операторы выполняются только в случае наличия возможности отправкии получения сообщения, иначе процесс, выполняющий соответствующий оператор,блокируется (см.

п.1.2, каналы). В некоторых случаях требуется протестировать возможностьоперации отправки или получения, не выполняя ее. Для этого входные/выходные операторы,фактически, трансформируются в обычные выражения взятием аргумента оператора вквадратные скобки. Таким образом, при использовании квадратных скобок вовходных/выходных операторах сам оператор не выполняется, а лишь вычисляется егозначение как выражения, например:qname ? [ack, var, 0]Смысл этого логического выражения состоит в проверке того, что очередным сообщением вканале с именем qname является структура, состоящая из мнемонического значения ack,некоторого значения переменной var и значения 0.

Если утверждение выполнимо, товозвращается единица, иначе возвращается нуль.Похожие на это условные выражения C-подобного вида(qname ? var == 0)/* синтаксическая ошибка */(a > b && qname ! 123)/* синтаксическая ошибка */илив Promela недопустимы, поскольку они не могут быть вычислены без побочных эффектов(попытки выполнить операции ввода/вывода вместо того, чтобы просто проверить, чтоочередное сообщение содержит 0 в первом случае или может быть послано – во втором).Кроме того, сами операторы отправки и получения данных не являются выражениями.Для вывода значений переменных или текста используется оператор printf. По своемудействию на состояние системы printf подобен пустому оператору skip. Оба этихоператора используются в моделях, когда необходимо осуществить всегда выполнимый шаг.Вывод текста printf производится только в режиме симуляции Spin, поскольку являетсяпобочным действием оператора.191.3Составные операторыВ части 1.2 были рассмотрены базовые операторы, существующие в Promela.

Кроме них вatomic,языкеопределенысоставныеоператоры:последовательностивидадетерминированные шаги, структура выбора и структура повторения.Блок atomicПоследовательность операторов, заключенных в фигурные скобки, перед которой стоитключевое слово atomic,, представляет блок кода, который должен выполняться как одиннеделимый модуль, не чередующийся с другими процессами. Действие atomic подобноиспользованию семафора. Выполнение последовательности операторов внутри atomicявляется неделимым “с точки зрения” других процессов: другие процессы “видят”разделяемые глобальные переменные и каналы, используемые в этом блоке, либо до, либопосле выполнения всей последовательности операторов внутри блока atomic.

В случае есликакой-либо оператор внутри atomic не является выполнимым, вся последовательностьоператоров не выполняется. Модифицируем пример с разделяемым использованием общейдля двух процессов переменной state.byte state = 1;active proctype A(){atomic {(state==1) -> state = state+1}}active proctype B(){atomic {(state==1) -> state = state-1}}Использование блока atomic позволяет здесь предотвратить доступ конкурирующегопроцесса к глобальной переменной. При запуске этой модели может бытьнедетерминировано выбран либо процесс А, либо процесс В для того, чтобы выполнить всеоператоры блока atomic.

Если начал выполняться процесс А, то он завершится, после чегозапустится процесс В, который, однако, будет приостановлен на проверке условия (state== 1). Аналогично, если начал выполняться процесс В, то он завершится, после чегопроцесс А будет приостановлен на проверке такого же условия. Итоговое значениепеременной state будет либо 0, либо 2, в зависимости от того, какой из двух процессоввыполнится.Блоки аtomic являются важным инструментом понижения сложности моделей верификации– уменьшения числа глобальных состояний строящейся Spin’ом формальной моделипереходов: блоки atomic ограничивают количество чередований (интерливинга).Однако, надо понимать, что интерливинг реально возникает в распределенных системах ипорождает неопределенность в выполнении параллельных процессов, избавление от которойможет являться нежелательным эффектом при верификации систем, если В РЕАЛИЗАЦИИвсе операторы блока atomic, выполняются не неделимо и эффект от различного ихчередования реально различен.20Выбор по условиюОператор if несколько отличен от обычных условных операторов современных языковпрограммирования.

В простом нижеследующем примере можно использовать относительныезначения двух переменных a и b для выбора между двумя опциями:if:: (a != b) -> option1:: (a == b) -> option2fiСтруктура выбора if содержит как минимум две последовательности операторов, каждаяпредваряется двойным двоеточием. Выполняется только одна последовательность из спискавозможных (выполнимых). Последовательность выполнима, если ее первый операторвыполним. Первый оператор называется защитой (guard) или условием.Если выполнимыми оказываются несколько операторов, недетерминировано выбираетсякакой-либо один.

При этом порядок перечисления альтернатив выбора несущественен, он нина что не влияет. Если все условия невыполнимы, то процесс будет заблокирован, пока хотябы одно из них не сможет быть выбранным. Ограничения на типы выражений, которыемогут быть использованы в качестве защиты, отсутствуют. Следующий пример используетвходные операторы.#define a 1#define b 2chan ch = [1] of { byte };proctype A(){ch ! a}proctype B(){ch ! b}proctype C(){if:: ch ? a -> option1:: ch ? b -> option2fi}init{atomic { run A(); run B(); run C() }}В примере определены три процесса и один канал ch. Первая опция в структуре выборапроцесса типа C является выполнимой, если канал содержит сообщение-константу a (aявляется константой со значением 1).

Вторая опция будет выполнимой, если канал содержитсообщение b (b также является константой). Какой из операторов будет выполнен, зависитот относительных скоростей процессов, которые неизвестны.Процесс в следующем примере либо увеличивает, либо уменьшает значение переменнойcount:21byte count;proctype counter(){if:: count = count + 1:: count = count – 1fi}Поскольку оба выражения в примере всегда выполнимы, то выбор между ними полностьюнедетерминирован, он не зависит от начального значения переменной count.ЦиклЛогическим расширением структуры выбора является структура повторения (цикл).Модифицируем представленный выше пример таким образом, чтобы получить циклическуюпрограмму, которая произвольно меняет значение переменной, увеличивая или уменьшаяего:byte count;active proctype counter(){do:: count = count + 1:: count = count - 1:: (count == 0) -> breakod}Аналогично предыдущему оператору if, в операторе do для текущего выполнения можетбыть выбрана только одна опция.

После того, как выполнение выбранной опции завершится,управление передается на начало оператора цикла: выполнение структуры повторяется.Обычный способ выхода из цикла – с помощью оператора break. Можно считать break неоператором, а указанием на то, что цикл завершается, и управление должно быть переданооператору, следующему за ключевым словом od. В примере цикл будет прерван, когдаcount будет нулем. В данном примере цикла два других оператора всегда будутвыполнимыми, поэтому выбор условия для выхода будет недетерминированным даже призначении count, равном 0.Для того чтобы гарантировать завершение цикла в случае, когда счетчик станет равнымнулю, необходимо изменить модель следующим образом.active proctype counter(){do:: (count != 0) ->if:: count = count + 1:: count = count - 1fi:: (count == 0) -> breakod}В структурах выбора и повторений бывает полезно специальное условие else.