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

Не существует возможности ограничитьдоступ к локальной переменной лишь для части модуля, описывающего процесс (т.е. несуществует аналога блока или области видимости). Все переменные инициализируютсянулями (для булевой переменной это false).bool flag;int state;byte msg;/* Примеры объявлений переменных */В языке допускаются комментарии только такого вида: /* комментарий */.В Promela поддерживаются только одномерные массивы например,byte state[N]объявляет массив с именем state из N байт, к которому можно обращаться следующимобразомstate[0] = state[3] + 5 * state[3*2/n]где n является константой или переменной.

Индексом массива может являться любоевыражение, которое вычисляет целочисленное значение. При значении индекса внедиапазона 0.. N-1 результат не определен; наиболее вероятно, что это вызовет ошибку привыполнении программы (runtime error).Многомерные массивы могут быть заданы неявно с помощью конструкции typedef (см.пример алгоритма Нидхама-Шредера п.3.3).Перечислимый тип mtype (mnemonic type, мнемонический тип) может содержатьсимвольные значения переменных, которые задаются при помощи одного или несколькихобъявлений.

Фактически, это аналог перечислимого типа в других языкахпрограммирования. Все переменные, объявленные с помощью mtype, представляют собойодно множество перечислимого типа, независимо от числа объявлений. При помощи всехобъявлений типа mtype можно задать не более 255 значений:mtype = { apple, pear, orange, banana };mtype = { fruit, vegetables, cardboard };init {}mtype n = pear;printf("MSC: %en = fruit;printf("MSC: is/* инициализация переменной n значением pear */", n);/* присвоение переменной n значения fruit */%e\n ", n)Синтаксисоператораprintfподобенаналогичному оператору в C. У этого оператора двааргумента: строка и список аргументов.

В строкезадаются форматы выводимых переменных: d –целое в десятичном формате, i – беззнаковое целоезначение, с – один символ, e – константа типаmtype. Как уже отмечалось ранее для выводасообщения на диаграмме взаимодействия ХSpin строка в printf должна начинаться с пятисимволов “MSC: ”.13КаналыКаналы сообщений используются для моделирования передачи данных от одного процесса кдругому. Они объявляются локально или глобально при помощи служебного слова chan:chan qname = [16] of { short }Здесь объявлен канал qname с буфером 16, т.е. этот канал может хранить до 16 сообщенийтипа short, т.е.

в канале может находиться не более 16 непрочитанных сообщений .Для работы с каналами существуют операторы посылки и получения сообщений. Оператор“!” :qname ! exprпосылает сообщение со значением переменной expr в только что объявленный канал qname,добавляя это значение к концу очереди в канале. По умолчанию оператор выполняется, есликанал назначения не переполнен, в противном случае он блокируется. Каналы передаютсообщения в порядке FIFO: первым вошел – первым вышел.Оператор приема сообщения “?”:qname ? msgпринимает сообщение из начала буфера канала и сохраняет его в переменной msg.Выполнение опрератора приема сообщения возможно только в случае, если канал не пуст.Для передачи составных сообщений, т.е. сообщений, содержащих конечное число полей,используются каналы, объявленные подобно данному:chan pname = [16] of { byte, int, chan }В примере объявляется канал pname для сообщений, каждое из которых содержит три поля –одно восьмибитное значение (типа byte, стоящее в начале сообщения), одно 32-битноезначение (типа int) и имя канала.

Передача идентификатора (имени) канала от одногопроцесса другому возможна посредством сообщения (как в данном примере) или в качествепараметра экземпляра процесса (см. пример алгоритма выбора лидера – п.3.1). Заметим, чтоиспользование массивов как поля сообщения в явном виде не допускается.При посылке нескольких значений в одном сообщении задается список переменных череззапятуюpname ! expr1,expr2,expr3В другом процессе можно принять это сообщение, присвоив три переданные значения тремразличным переменным:pname ? var1, var2, var3Часто первое поле сообщения используется для задания типа сообщения (фактически, длясвязывания с сообщением некоторой характеристики).

Эти данные объявляются при помощитипа mtype:14/* объявляется тип сообщения: */mtype = { ack, nak, err, next, accept }/* объявляются две переменные этого типа: */mtype msgtype1, msgtype2;При использовании типа передаваемых данных mtype в объявлении каналасоответствующие поля сообщений будут всегда интерпретированы символически, а нечисленно. Например:chan tname = [4] of { mtype, int, bit };Здесь по каналу qname будут пересылаться сообщения, состоящие из трехполей: первое –типа mtype, второе – целое значение, третье – битовое значение.

Для задания операцийпосылки и получения сообщения определенного типа используется следующее обозначениеtname ! msgtype (data, b)Эта запись эквивалентна следующей альтернативной записи:tname ! msgtype, data, bНекоторые аргументы операторов как посылки, так и приема сообщений могут бытьконстантами:tname ! ack, var, 0/* По каналу tname передается сообщениеиз двух констант (ack типа mtype и 0) изначения целой переменной var */tname ? ack (data,1) /* Из канала qname читается сообщение, в которомпервым элементом должна быть константа ack типаmtype, вторым – произвольное значение типа int,которое запишется в переменную data, третьей частьюпринятого сообщения должна быть битовая константа 1*/Оператор получения сообщения при наличии констант будет выполним, только еслисообщение в начале буфера канала в соответствующих полях имеет значения заданныхконстант.

В противном случае он будет блокирован. Например, приведенный выше операторполучения сообщения будет невыполним, если в начале буфера находится сообщение<ack,15,0 >.Если оператор окажется невыполнимым, то процесс, пытающийся его выполнить, будетприостановлен, пока оператор не станет выполнимым. Таким образом, можно моделироватькоммуникацию «точка-точка» нескольких процессов, связанных одним каналом.Рассмотрим упрощенную реализацию протокола альтернирующего бита (Bartlett, Scantleburyи Wilkinson [1]):mtype = { msg, ack };chanchan/*объявляем два возможных типа сообщения */to_sndr = [2] of { mtype, bit };to_rcvr = [2] of { mtype, bit };active proctype Sender(){again: to_rcvr!msg,1;to_sndr?ack,1;/*объявляем канал отправителя *//*объявляем канал получателя *//* процесс отправителя *//* отправляем сообщение, помеченное битом 1 *//* получаем подтверждение, помеченное битом 1 */15to_rcvr!msg,0;to_sndr?ack,0;goto again/* отправляем сообщение, помеченное битом 0 *//* получаем подтверждение, помеченное битом 0 */}active proctype Receiver(){again: to_rcvr?msg,1;to_sndr!ack,1;to_rcvr?msg,0;to_sndr!ack,0;goto again}/* процесс получателя *//* получаем сообщение, помеченное битом 1 *//* отправляем подтверждение, помеченное битом 1 *//* получаем сообщение, помеченное битом 0 *//* отправляем подтверждение, помеченное битом 0 */В алгоритме альтернирующего бита процесс-отправитель попеременно отправляетсообщения, помеченные то битом 1, то битом 0, и ожидает соответствующие подтверждения.Процесс-получатель получает сообщения, помеченные то битом 1, то битом 0, и отсылаетпроцессу-отправителю на них подтверждения.

В полной версии протокола сообщения могутбыть потеряны, но здесь потери канала не моделируются. Бесконечный цикл реализован вэтой модели при помощи оператора перехода goto и локальной метки again в каждомпроцессе.В языке Promela для каналов определено несколько функций (len, empty, nempty, full,nfull). Например, предопределенная функция len(qname) возвращает количествосообщений, хранящихся в канале qname в текущий момент времени. Если len используетсякак оператор по правую сторону присваивания, то он будет невыполимым, если канал пуст,т.к. он возвращает нулевой результат, который по определениюозначает, что оператор временно невыполним. Следующий примерпоказывает, как отправить сообщение msgtype в случае, если каналqname не переполнен:(len(qname) < MAX) -> qname ! msgtypeЗдесь если доступ к каналу qname разделяется несколькимипроцессами, то выполнение второго оператора необязательно будетпроисходить сразу после выполнения первого оператора проверки.Например, это случится, если другой процесс пошлет сообщение вканал qname (и число сообщений в нем станет равно MAX) сразупосле того, как данный процесс определит, что канал не полон.Взаимодействие рандевуРанее мы рассматривали только асинхронные взаимодействиямежду процессами через канал сообщений, декларируемый какchan qname = [N] of { byte }где N является положительной константой, которая определяетразмер буфера.

Установив размер буфера, равным 0:chan port = [0] of { byte }определим рандеву-канал (который в данном примере можетпередавать однобайтное сообщения). Поскольку буфер рандевуканала равен нулю, то такой канал может передавать, но не может16хранить сообщения. Взаимодействия процессов по рандеву-каналам по определениюсинхронны. Рассмотрим следующий пример.#define msgtype 1chan name = [0] of { byte, byte };proctype A(){name ! msgtype(4);name ! msgtype(1)}proctype B(){byte state;name ? msgtype(state)}init{atomic { run A(); run B() }}Канал name объявлен здесь как глобальный рандеву-канал.

Два процесса синхронновыполнят свои первые операторы: подтверждение связи («рукопожатие») по сообщениюmsgtype и передачу значения 4 в локальную переменную state. Второй оператор посылкив процессе A невыполним, потому что отсутствует соответствующая операция приемасообщения в процессе B.Если бы канал name был определен с ненулевым размером буфера, поведение было быотличным. Допустим, что размер буфера равен 2, тогда процесс типа A может закончить своевыполнение даже до того, как процесс В начнет работу. Если назначить размер буфера,равным 1, то последовательность событий будет следующей. Процесс типа A можетзакончить свое первое действие посылки, но он блокируется на втором действии, потому чтотеперь канал полон.

Процесс типа B читает первое сообщение и завершается. В этой точке Aстановится опять выполнимым и завершается, оставляя свое последнее сообщение в канале.Взаимодействия рандеву бинарные: только два процесса, отправитель и получатель, могутбыть синхронизированы при рандеву «рукопожатии». Ниже будет рассмотрен примерспособа использования рандеву-канала для построения семафора –п.1.3.Правило выполнимостиPromela основывается на семантике выполнимости, которая обеспечивает базовые средства вязыке для моделирования синхронизации процессов. В зависимости от состояния системы,любой оператор в модели Spin или выполним, или блокирован. Определены четыре основныхтипа операторов в Promela: оператор вывода переменных printf, оператор присваивания,операторы ввода/вывода (при передаче данных по каналам) и операторы-выражения.