7. Обзор средства SPIN - синтаксис, трансляция базовых конструкций в модели Крипке, страница 2

(обращения к полям структур)Присваивание всегда активно и выполняется за один переход вмодели Крипке:Iпеременная изменяется так же, как в CIуправление передаётся следующей командепоследовательности(S) Тело процесса: условиеЛюбое булево выражение может быть записано как условнаякомандаУсловная команда активна ⇔ значение выражения — trueПри выполнении условной командыIзначения всех переменных остаются неизменнымиIуправление передаётся следующей командепоследовательности(S) Тело процесса: ветвлениеif:: последовательность_команд...:: последовательность_командfiАльтернатива — это последовательность команд после “::”Голова альтернативы — это первая командаАльтернатива активна, если активна её голова(S) Тело процесса: ветвлениеif:: последовательность_команд...:: последовательность_командfiКоманда ветвления активна ⇔ активна хотя бы однаальтернативаПри выполнении активной команды ветвленияIIнедетерминированно выбирается одна из активныхальтернативкоманда ветвления заменяется на выбраннуюальтернативу, и переходы совершаются согласно этойальтернативеIIпервый переход для команды ветвления — это первыйпереход для выбранной альтернативыкогда все команды альтернативы выполнены, управлениепередаётся следующей команде(S) Тело процесса: ветвлениеif:: последовательность_команд...:: последовательность_командfiКлючевое слово else — это специальная команда, работающаятак:Iеё можно писать непосредственно после “::”, и не болеечем в одной из альтернативIкоманда else активна ⇔ все остальные альтернативынеактивныIпри выполнении команды else значения переменных неизменяютсяЗапись “->” — это синоним “;”, повышающий наглядностьзаписи альтернатив(S) Тело процесса: ветвлениеПримерМодель Крипке для этого примера выглядит так:i/0i/0i/0i/1i/0i/1i/1i/2i/2i/2i/2(S) Тело процесса: циклdo:: последовательность_команд...:: последовательность_командodКоманда цикла работает почти так же, как и командаветвленияЕдинственное отличие: после выполнения альтернативыуправление не передаётся следующей команде, а возвращаетсяв начало циклаКлючевое слово break — это всегда активная команда, неизменяющая данных и принудительно передающая управлениеинструкции, следующей за циклом(S) Тело процесса: циклПримерМодель Крипке для этого примера выглядит так:i/0i/0i/0i/2i/1i/1i/2(S) Запуск и аргументы процессовСпециальной командой можно запускать новые процессы всистеме:run тип_процесса (параметры )Эта команда всегда активнаКоманда выполняется за один переход, выполнение передаётсяследующей команде, и в системе запускается процессуказанного типаВ общем случае тип процесса имеет аргументы:Iаргументы — это список объявлений , разделённых “;”Iобъявление ::= тип список_имён_через_запятуюПараметры запускаемого процесса и аргументы в описаниипроцесса работают так же, как и передача параметров позначению при вызове функции в C/C++(S) Запуск и аргументы процессовМодель Крипке для этого примера выглядит так:i/5i/5i/2i/1i/5i/1i/1i/2(S) Локальные переменныеПомимо глобальных переменных Promela позволяет объявлятьи локальные переменные в начале текста тела процессаОбъявления локальных переменных выглядят так же, как иобъявления глобальныхЛокальные переменные создаются для каждого процесса вмомент его запускаИнициализация локальных переменных работает так же, как идля глобальных переменныхОбъявление локальной переменной не является командой(S) Каналы связиЯзык Promela позволяет объявлять каналы связи двух видов:IсинхронныеIасинхронныеАсинхронный канал способен хранить количество сообщений,не превосходящее его ёмкость (положительное целое число) иобъявляется так:chan имя_канала = [ёмкость ] of {тип_сообщений }Синхронный канал связи — это канал ёмкости 0:chan имя_канала = [0] of {тип_сообщений }(S) Каналы связиКоманда посылки сообщения в канал имеет вид<имя канала >!<выражение >Команда приёма сообщения из канала имеет вид<имя канала >?<имя переменной >или<имя канала >?<выражение >В зависимости от ёмкости канала эти команды работаютпо-разномуАсинхронный канал:Iкоманда посылки сообщения активна ⇔ канал хранитсообщений меньше, чем его ёмкостьIкоманда приёма сообщения активна ⇔ канал хранит хотябы одно сообщение и (в случае инструкции второго вида)значение сообщения совпадает со значением выражения(S) Каналы связиКоманда посылки сообщения в канал имеет вид<имя канала >!<выражение >Команда приёма сообщения из канала имеет вид<имя канала >?<имя переменной >или<имя канала >?<выражение >В зависимости от ёмкости канала эти команды работаютпо-разномуАсинхронный канал:Iпо выполнении команды посылки сообщения в каналдобавляется сообщение с тем же значением, что ивыражение в инструкцииIпо выполнении команды приёма первого вида впеременную записывается значение сообщения, посланногораньше остальныхIпо выполнении команды приёма обоих видов прочитанноесообщение удаляется из канала(S) Каналы связиКоманда посылки сообщения в канал имеет вид<имя канала >!<выражение >Команда приёма сообщения из канала имеет вид<имя канала >?<имя переменной >или<имя канала >?<выражение >В зависимости от ёмкости канала эти команды работаютпо-разномуСинхронный канал:Iкоманды посылки и приёма сообщения выполняютсяодновременно, каждая ровно в одном процессеIпосылаемое значение напрямую передаётсяпринимающему процессуIв остальном передача сообщения происходит так же, какдля асинхронных каналов(S) Каналы связиВ этой системе два процесса постепенно увеличивают значенияпеременных i, j (с переполнением) пересылая увеличенныезначения через синхронный канал связиКоманда “!” одного процесса и команда “?” другого процессавыполняются одновременно за один переход(S) Неделимые последовательностиинструкцийА что делать, если хочется выполнить последовательностькоманд за один шаг выполнения системы?Например, в протоколах доступа к критической секции частобывает важным уметь неделимо проверять и изменятьзначение переменной (семафора)Неделимость последовательности команд моделируется в языкеPROMELA так:atomic{<команды >}Как это работает:(в простом случае)1.

если сейчас выполнилась команда из блока atomic и наследующем шаге есть возможность выполнить команду изэтого же блока, то эта команда обязательно выполняется(S) Неделимые последовательностиинструкцийА что делать, если хочется выполнить последовательностькоманд за один шаг выполнения системы?Например, в протоколах доступа к критической секции частобывает важным уметь неделимо проверять и изменятьзначение переменной (семафора)Неделимость последовательности команд моделируется в языкеPROMELA так:atomic{<команды >}Как это работает:(в простом случае)2.

если сейчас выполнилась команда из блока atomic, но ниодна команда из этого блока больше не можетвыполниться, то выполнение системы происходитобычным образом(S) Неделимые последовательностиинструкцийА что делать, если хочется выполнить последовательностькоманд за один шаг выполнения системы?Например, в протоколах доступа к критической секции частобывает важным уметь неделимо проверять и изменятьзначение переменной (семафора)Неделимость последовательности команд моделируется в языкеPROMELA так:atomic{<команды >}Как это работает:(в простом случае)3.

если при выполнении обычным образом вдругвыполнилась ещё одна команда из блока atomic, тодальнейшее выполнение опять происходит согласнопунктам 1, 2(S) Неделимые последовательностиинструкцийМодель Крипке для этого примера выглядит так:i/5i/5i/2i/1i/5i/1i/2(S) Пример для размышленийbool near, dead, hunted;mtype = {ping}; chan c = [0] of {ping};active proctype mosquito() { do:: !near -> atomic{near = true; c!ping;}:: near && !hunted && !dead -> near = false;od }active proctype bird() { do:: atomic{c?ping -> hunted = true;}:: hunted && near -> dead = true; hunted = false;:: hunted && !near -> hunted = false;od }ltl inevitable_death {<>(near && <> dead)}ltl cannot_fly_away {[](near -> <> dead)}ltl reliable_hunt {[](hunting -> <> dead)}Как это работает, и какие свойства выполнены?Конец семинара 7.