4 - Среда верификации SPIN. Описание моделей на языке Promela (1161368), страница 2

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 2)

зачениям полейсообщения;– значения consti ограничивают допустимые значенияполей;– выполним, если заданный канал не пуст и первоесообщение в канале соответствует всем константнымзначениям в операторе приёма сообщения.Отправка и приём сообщений• пример:#define ack 5chan ch = [N] of {int, bit};другой вариант:bit seqno;ch!ack,0;ch!ack(0);ch?ack,seqnoch?ack(seqno)Асинхронная передача сообщений• асинхронные сообщения буферизуются дляпоследующего приёма, пока канал не полон,• отправитель блокируется, когда канал полон,• получатель блокируется, когда канал пуст.q!m1q!m2q!m3m3m2q?m1m1q?m2q?m3Синхронная передача сообщений• ёмкость канала равна 0:chan ch = [0] of {mtype};• передача сообщений методом «рандеву»;• не хранит сообщения;• отправитель блокируется в ожидании получателя, инаоборот;• отправка и приём выполняются атомарно.q!m1q?m1q!m2q?m2q!m3q?m3Пример: моделируем семафорmtype = { P, V };chan sema = [0] of { mtype };active proctype semaphore(){L:sema!P -> sema?V; goto L}active [5] proctype user(){L:/*non-critical*/sema?P ->/*critical*/sema!V;goto L;}?V!PДругие операции с каналами• len(q) – возвращает число сообщений вканале,• empty(q) – возвращает true, если q пуст,• full(q) – возвращает true, если q полон,• nempty(q) – вместо !empty(q) (вцелях оптимизации),• nfull(q) – вместо !full(q) (в целяхоптимизации).Операции со скобками• q?[n,m,p]есть ли в канале подходящее сообщение?– булево выражение без побочных эффектов,– равно true, только когда q?m,n,p выполнимо, однако невлияет на значения n,m,p и не меняет содержимое канала q;• q?<n,m,p>широковещательный канал– выполнимо тогда же, когда и q?n,m,p; влияет на значенияn,m,p так же, как и q?n,m,p, однако не меняет содержимое q;• q?n(m,p)отделяем тип сообщения от параметров– вариант записи оператора приёма сообщения (т.е.

q?n,m,p),– может использоваться для отделения переменной от констант.Область видимости объявленияканала• имя канала может быть локальным или глобальным, ноканал сам по себе – всегда глобальный объект.chan x = [3] of { chan };active proctype A(){ chan a;x?a;a!x}active proctype B(){ chan b = [2] of { chan };x!b;b?x;0}глобальная переменная, видна A и Bнеинициализированный локальный каналполучаем идентификатор канала от процесса Bиспользуем егоинициализированный локальный каналотправляем процессу А идентификатор каналазначение x не изменилосьесли B умрёт, канал b исчезнет!Особые случаи:упорядоченная отправка, случайный приём• q!!n,m,p– аналогично q!n,m,p, но сообщение n,m,pпомещается в канал сразу за первым сообщением, меньшимn,m,p;• q??n,m,p– аналогично q?n,m,p, но из канала можетбыть выбрано любое сообщение (не обязательно первое).init{chan q = [3] of {int};int x;q!!5;q!!2;q?x->printf(“%d\n”,x);q?x->printf(“%d\n”,x)}> ./spin sorted.pml251 process created>Основные типы данных PromelaТипbitboolbytechanmtypepidshortintunsigned 0..2n-1Диапазон0..1false..true0..2551..2551..2551..255-215..215-1-231..231-1Пример объявленияbit turn = 1;bool flag = true;byte cnt;chan q;mtype msg;pid p;short s = 100;int x = 1;unsigned u : 3;3 бита,0..7• по умолчанию все объекты (и локальные, и глобальные)инициализируются нулём;• все переменные должны быть объявлены до первогоиспользования;• переменная может быть объявлена где угодно.Основные типы данных PromelaВ Promela нет действительных чисел, чисел сплавающей точкой и указателей.

Этот языкпредназначен для описания взаимодействияобъектов, а не для описания вычислений.Массивы и пользовательские типыданныхОдномерные массивы:byte a[27];bit flags[4] = 1;• все элементы массива инициализируются одним значением,• индексы нумеруются с 0.Пользовательские типы данных:typedef record {short f1;byte f2 = 4;}record rr;ff.f1 = 5;ключевое словоимя пользовательского типапо умолчанию 0объявление переменнойнового типассылка на элемент структурыЕщё один способ объявлениямассивовtypedef array {byte b[4];}array a[4];a[3].b[2] = 1;или#define ab(x,y) a[x].b[y]ab(x,y) = ab(2,3) + ab(3,2);Перед разбором все модели прогоняются через препроцессор С(поддерживаются #define, #if, #ifdef, #ifndef, #include)Вычисление выражений• Значение всех выражений вычисляется в наиболеешироком диапазоне (int);• В присваиваниях и передаче сообщений значенияприводятся к целевому типу после вычисления.mtype = {foo, bar};active proctype tryme(){ byte x;short y = 1024;chan a,b;mtype p;axxp}====a + b;257;y;y/8ОшибкаПредупреждение –потеря данныхПредупреждение –потеря данныхСообщения об ошибке не будетОбласть видимости объектов данных• Только два уровня видимости:– глобальный (данные видны всем активнымпользователям),– локальный (данные видны только одному процессу)• подобластей (напр.

для блоков) нет,• локальная переменная видна везде в теле процесса.active proctype main(){ int x, y;{int y, z;x++; y++; z++};Ошибка, повторное объявление yprintf(“y=%d, z=%d\n”, y, z);}Переменная z всё ещё видна!Поток управления процесса• 5 способов задать поток управления:– последовательная композиция (“;”), метки, goto,– структуризация (макросы и inline),– атомарные последовательности (atomic, d_step),– недетерминированный выбор и итерации (if..fi,do..od),– escape-последовательности ({...}unless{...}).Макросы – препроцессор cpp• Используется для включения файлов иразворачивания макросов,• Варианты использования:– константы#define MAXQ 2chan q=[MAXQ] of {mtype,chan};(альтернатива: spin –DMAXQ=2 …)#define RESET(a)\– макросыatomic {a[0] = 0; a[1] = 0}– условный код#define LOSSY 1...#ifdef LOSSYactive proctype D()#endif#if 0COMMENTS#endifМакросы – препроцессор cpp• Минусы:– имена макросов не видны в парсере,– имена макросов не видны при моделировании,• Варианты:– использовать mtype для определения констант,– использовать другой препроцессор (ключ -P),• inline-определения.inline-определения• среднее между макросом и процедурой,• именованный фрагмент кода с параметрами,• не функция – не возвращает значения.#define swap(a,b) tmp = a;\a = b;\b = tmp#endifinline swap(a,b){tmp = a;a = b;b = tmp}Недетерминированный выборif::guard1 -> stmnt1.1;stmnt1.2;stmnt1.3;::guard2 -> stmnt2.1;stmnt2.2;stmnt2.3;::::guardn -> stmntn.1;stmntn.2;stmntn.3;fi• оператор if выполним, если выполним хотя бы один изстражей,• если выполнимо более одного стража, то для выполнениявыбирается один из них недетерминированным образом,• если ни один из стражей не выполним, выполнениеоператора if блокируется,• в качестве стража может быть использован любойоператор.Ещё по if/*ищем максимум среди x и y*/if:: x >= y -> m = x:: x <= y -> m = yfi/*случайный выбор числа 0..3*/if:: n = 0:: n = 1:: n = 2:: n = 3fiif::::::::fi(n%2 != 0)(n >= 0)(n%3 == 0)else /* ->-> n-> n-> nskip= 0= n-2= 3*/выполняется, только если невыполняется ни один изстражейLTSВыражение elseCif(x <= y)x = y – x;y++;Promelaif::(x <= y) -> x = y – x:: elsefi;y++• в отличие от С, если else отсутствует, товыполнение блокируется,• т.е.

все варианты выполнения оператора ifдолжны быть явно выписаны.Специальные выражения ипеременные• else – true, если ни один операторпроцесса не выполним,• timeout – true, если ни один оператормодели не выполним,• _ – переменная, доступная только позаписи, значение не сохраняет,• _pid – номер текущего процесса,• _nr_pr – число активных процессов.Оператор dodo::guard1 -> stmnt1.1;stmnt1.2;stmnt1.3;::guard2 -> stmnt2.1;stmnt2.2;stmnt2.3;::::guardn -> stmntn.1;stmntn.2;stmntn.3;do• в качестве стража может быть использованлюбой оператор,• фактически, это оператор if, выполняемый вцикле• из цикла можно выйти только при помощиbreak и goto.Оператор do• Ждём, пока не наступит момент (a==b)do::(a == b) -> break;::else -> skipodL:if::( a== b) -> skipelse goto Lfi(a == b)• все три фрагмента эквивалентныСпасибо за внимание!• Вопросы?.

Характеристики

Список файлов лекций