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

если на предыдущем шаге выполнилась непоследняяинструкция последовательности, то выполняетсяследующая по порядку инструкция3. после выполнения последней инструкции происходитпереход к следующей после условного оператораинструкцииPROMELA: примерbool a;active proctype P() {L1: if:: L2: a = !a; L3: a = !a;:: L4: a = !a;fiL5:}!aL1aL3aL5!aL5PROMELA: условная инструкцияБулево выражение может выступать в роли (условной)инструкцииУсловная инструкция работает так:Iесли значение инструкции — true, то происходит переходк следующей инструкцииIесли значение инструкции — false, то эта инструкция неможет быть выполненаЯзык PROMELA содержит особую условную инструкцию else:Iона может быть только первой инструкциейпоследовательности в условном операторе и операторециклаIelse = true тогда и только тогда, когда никакая другаяинструкция не может быть выполненаЯзык PROMELA разрешает писать “->” вместо “;”Правило хорошего тона — ставить -> вместо ; после условныхинструкцийPROMELA: примерbool a;active proctype P() {L1: do:: L2: a -> L3: a = !a;:: L4: else -> L5: a = !a;od}!aL1aL3!aL5aL1PROMELA: композиция процессовВ общем случае в модели PROMELA в каждый моментвремени может быть запущено более одного процессаЗапущенные процессы работают асинхронно, и шаг работысистемы выглядит следующим образом:Iнедетерминированно выбирается процесс, в котором можетвыполниться какая-либо инструкцияIэтот процесс выполняет одну инструкциюPROMELA: запуск процессаПроцесс может быть запущен двумя способами:I active [N] proctype ...IIN процессов запускаются в начале работы системы (часть[N] может быть опущена, и тогда запускается одинпроцесс)run <тип процесса >()Iэто инструкция, по выполнении которой в системудобавляется один новый процесс заданного типа,находящийся в начальном состоянии управленияPROMELA: примерint a;active [2] proctype P() {L1: a++;L2:}0L1 L11L1 L21L2 L12L2 L2PROMELA: примерbool a;active proctype P() {L1: run Q(); L2:}proctype Q() {L1: a = !a; L2:}0P@L10P@L2Q@L11P@L2Q@L2PROMELA: локальные переменныеВ теле процесса можно объявлять локальные переменные также, как вне тела всех процессов объявляются глобальныеЛокальная переменная может быть объявлена (иинициализирована) в любом месте внешнейпоследовательности тела процессаОбъявление локальной переменной не считаетсяинструкциейДоступ к локальной переменной может быть получен из любойинструкции, принадлежащей идущим далее по текстуэлементам последовательностиИнициализация локальной переменной происходит призапуске процесса, поэтому рекомендуется объявлять вселокальные переменные в начале описания тела процессаPROMELA: примерactive [2] proctype mosquito() {bool buzzing;do:: buzzing = !buzzing;od}00011011PROMELA: каналы связиВ языке PROMELA есть ещё один тип переменных, неупомянутый ранее и никак не соотносящийся с типами в C++:каналы связи chanКанал, объявленный среди глобальных переменных, какправило инициализируется:chan <имя > = [N] of {<тип >}Так заводится канал ёмкости N, по которому пересылаютсясообщения заданного типаЁмкость канала — это максимальное количество сообщений,которые может хранить каналPROMELA: посылка и приём сообщенийИнструкция посылки сообщения в канал имеет вид<имя канала >!<выражение >Инструкция приёма сообщения из канала имеет вид<имя канала >?<имя переменной >или<имя канала >?<выражение >В зависимости от ёмкости каналы разбиваются на два классаЕсли ёмкость положительна, то канал асинхронный:Iинструкция посылки сообщения может быть выполненатогда и только тогда, когда канал хранит сообщенийменьше, чем его ёмкостьIинструкция приёма сообщения может быть выполненатогда и только тогда, когда канал хранит хотя бы односообщение и (в случае инструкции второго вида) значениесообщения совпадает со значением выраженияPROMELA: посылка и приём сообщенийИнструкция посылки сообщения в канал имеет вид<имя канала >!<выражение >Инструкция приёма сообщения из канала имеет вид<имя канала >?<имя переменной >или<имя канала >?<выражение >В зависимости от ёмкости каналы разбиваются на два классаЕсли ёмкость положительна, то канал асинхронный:Iпо выполнении инструкции посылки сообщения в каналдобавляется сообщение с тем же значением, что ивыражение в инструкцииIпо выполнении инструкции приёма первого вида впеременную записывается значение сообщения, посланногораньше остальныхIпо выполнении инструкции приёма обоих видовпрочитанное сообщение удаляется из каналаPROMELA: посылка и приём сообщенийИнструкция посылки сообщения в канал имеет вид<имя канала >!<выражение >Инструкция приёма сообщения из канала имеет вид<имя канала >?<имя переменной >или<имя канала >?<выражение >В зависимости от ёмкости каналы разбиваются на два классаЕсли канал имеет ёмкость 0, то он синхронный:Iинструкции посылки и приёма сообщения выполняютсяодновременно, каждая ровно в одном процессеIпосылаемое значение напрямую передаётсяпринимающему процессуIв остальном передача сообщения происходит так же, какдля асинхронных каналовPROMELA: примерchan buzz = [0] of {bool}active proctype mosquito() {do ::buzz!false; ::buzz!true; od}active proctype me() {bool found;do ::buzz?found; ::found->KILLING:break; odKILLED:}011KILLING1KILLEDPROMELA: LTL-требованияltl <имя требования > {<тело требования >}Тело требования — это LTL-формула в таком синтаксисе:I[] пишется вместо GI<> пишется вместо FIU используется как обычноIможно использовать булевы выраженияIв качестве булевой переменной можно использовать записьP@L: хотя бы один экземпляр процесса типа P находится всостоянии управления с меткой LIнастоятельно не рекомендуется использовать XPROMELA: примерbool near, dead, hunted;mtype = {ping}; chan c = [0] of {mtype};active proctype mosquito() { do:: !near -> near = true; c!ping;:: near && !hunted && !dead -> near = false;od }active proctype bird() { do:: 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)}Как выглядит модель Крипке для этой системы?Что означают требования?PROMELA: примерbool near, dead, hunted;mtype = {ping}; chan c = [0] of {mtype};active proctype mosquito() { do:: !near -> near = true; c!ping;:: near && !hunted && !dead -> near = false;od }active proctype bird() { do:: 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)}Обязательно ли включать в SPIN режим верификации свойствживости, или достаточно режима для свойств безопасности?Какие из требований выполнены для системы?PROMELA: неделимые последовательностиинструкцийА что делать, если хочется выполнить последовательностьинструкций за один шаг выполнения системы?Например, в протоколах доступа к критической секции частобывает важным уметь неделимо проверять и изменятьзначение переменной (семафора)Неделимость последовательности действий моделируется вязыке PROMELA так:atomic{<последовательность >}Как это работает:(в простом случае)1 если сейчас выполнилась инструкция из блока atomic и наследующем шаге есть возможность выполнить инструкциюиз этого же блока, то эта инструкция обязательновыполняетсяPROMELA: неделимые последовательностиинструкцийА что делать, если хочется выполнить последовательностьинструкций за один шаг выполнения системы?Например, в протоколах доступа к критической секции частобывает важным уметь неделимо проверять и изменятьзначение переменной (семафора)Неделимость последовательности действий моделируется вязыке PROMELA так:atomic{<последовательность >}Как это работает:(в простом случае)2 если сейчас выполнилась инструкция из блока atomic, нони одна инструкция из этого блока больше не можетвыполниться, то выполнение системы происходитобычным образомPROMELA: неделимые последовательностиинструкцийА что делать, если хочется выполнить последовательностьинструкций за один шаг выполнения системы?Например, в протоколах доступа к критической секции частобывает важным уметь неделимо проверять и изменятьзначение переменной (семафора)Неделимость последовательности действий моделируется вязыке PROMELA так:atomic{<последовательность >}Как это работает:(в простом случае)3 если при выполнении обычным образом вдругвыполнилась ещё одна инструкция из блока atomic, тодальнейшее выполнение опять происходит согласнопунктам 1, 2PROMELA: пример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)}А теперь как работает система, и какие требования для неёвыполнены?PROMELA: аргументы процессаПри описании типа процесса можно задавать списокаргументов:proctype P(<аргументы >) ...В списке аргументов перечисляются переменные с явнымуказанием их типов (как аргументы функции) безинициализацииПеременные одного типа перечисляются через запятую с однимуказанием типа; аргументы разных типов разделены точкой сзапятой (как в обычном объявлении переменных)При вызове процесса явно указываются значения всехаргументов (как при вызове функции)В теле процесса аргументы используются так же, как илокальные переменные (как при передаче параметров позначению)Для синхронизации процессов через значения переменныхаргументы процессов не подходят: текущее значениеаргумента видно только внутри процессаPROMELA: примерint a;active proctype P() {run Q(1); run Q(2);}proctype Q(int x) {a = x;}0P@10 P@2Q(1)@11 P@2Q(1)@22 P@3Q(1)@1Q(2)@20 P@3Q(1)@1Q(2)@11 P@3Q(1)@2Q(2)@11 P@3Q(1)@2Q(2)@22 P@3Q(1)@2Q(2)@2.