Семинар 4. NuSMV_ композиция автоматов_ проверка CTL-формул, страница 2

“IVAR”)Iесли значение выражения — множество элементов того жетипа, что и v, то это работает как “TRANS v in e”ASSIGN-выражение с next работает точно так жеASSIGN-выражение с init работает почти так же:эквивалентная конструкция содержит “INIT” вместо “TRANS”, иключевое слово “init” снимаетсяСинхронная и асинхронная композицииСистема, описанная на языке NuSMV, обычно состоит изнескольких модулей, работающих параллельноА какие виды параллельного выполнения систем вы знаете?NuSMV поддерживает два вида параллельной композициимодулей: синхронную и асинхроннуюСинхронная композиция:Iвсе модули, участвующие в композиции, одновременносовершают один переход, и это объявляется переходомкомпозицииАсинхронная композиция:Iпроизвольно выбирается один из модулей композицииIвыбранный модуль совершает переход, остальные модулине совершают переходаIполучившееся изменение состояния системы объявляетсярезультатом выполнения перехода композицииСинтаксис NuSMV: экземпляры модулейМодуль может быть использован в качестве типа переменнойв другом модулеОба типа композиции описываются похожим образомMODULE sVAR inst1 : m1; inst2 : m1; inst3 : m2;В модуле s синхронно запущены два экземпляра модуля m1 иодин экземпляр модуля m2inst1, inst2, inst3 — имена этих экземпляровMODULE aVAR inst1 : process m1; inst2 : process m1;В модуле a асинхронно запущены два экземпляра модуля m1Синтаксис NuSMV: экземпляры модулейПримерMODULE roomVAR m1 : process mosquito; m2 : process mosquito;MODULE mosquitoVAR buzzing : boolean;ASSIGN next(buzzing) := !buzzing;Так запущенные комары жужжат асинхронно:m1.b∅m1.b, m2.bm2.bСинтаксис NuSMV: экземпляры модулейПримерMODULE roomVAR m1 : mosquito; m2 : mosquito;MODULE mosquitoVAR buzzing : boolean;ASSIGN next(buzzing) := !buzzing;Так запущенные комары жужжат синхронно:m1.b∅m1.b, m2.bm2.bСинтаксис NuSMV: доступ к локальнымпеременнымЕсли в модуле M запущен экземпляр модуля m, то в модуле Mможно использовать значения всех переменных этогоэкземпляраДоступ к значениям переменных происходит так же, как доступк значениям полей структуры в C:MODULE MVAR x : m; b : boolean;ASSIGN next(b) := !x.b xor b;MODULE mVAR b : boolean;ASSIGN next(b) := !b;А как эта система работает?Синтаксис NuSMV: аргументы модуляЧтобы экземпляр модуля мог использовать значенияпеременных, описанных вовне, в его определении можнодописать аргументы:MODULE m(a1, a2, a3) .

. .Значения аргументов могут использоваться в модуле так же,как и остальные переменные (но без init и next)При определении экземпляра модуля на местах всехаргументов прописываются выражения:VARb1 : boolean;x : m(TRUE, b1, y.b);y : m(b1 & x.b, x.b, b1);Синтаксис NuSMV: главный модульКак NuSMV поймёт, какой из модулей главный: описывает тусамую систему, которую мы хотим исследовать?Правило очень простое:Iглавный модуль обязан называться mainIглавный модуль обязан не содержать аргументовСемантика модуля без аргументов — (в чистом виде, безвсяких оговорок) модель КрипкеВ модели Крипке можно проверить выполнимостьCTL-формулыNuSMV умеет это делать (и даже больше, но сейчасдостаточно этого)Синтаксис NuSMV: CTL-спецификацииВ главном модуле можно явно написать набор CTL-формул,выполнимость которых мы хотим проверитьСинтаксис очень простой:Iописание спецификации — тоже часть тела модуляIспецификация предваряется словом CTLSPECIспецификация — это выражение, дополненное связкамиAF, EF, AG, EG, AX, EX, A[...U...], E[...U...]Iнетемпоральные выражения, стоящие непосредственно подтемпоральными операторами, должны иметь булев типПримерMODULE roomVAR m1 : mosquito; m2 : mosquitoCTLSPEC EF AG !(m1.buzzing & m2.buzzing)Да когда же эти комары помрут наконец?Полноценный примерMODULE mainVAR b : bird(s.location = NEAR); s : swarm;CTLSPEC AG AF (b.satiety = FED);MODULE bird(food)VAR satiety : {FED, HUNGRY};ASSIGN next(satiety) := casesatiety = HUNGRY & food : FED;TRUE : HUNGRY;esac;MODULE swarmVAR location : {NEAR, FAR};Верно ли, что сколько бы бессмертная птица ни прожила, онаобязательно перекусит насекомыми ещё раз?Синтаксис NuSMV: справедливостьNuSMV поддерживает два способа задания справедливостиОба способа являются элементами тела модуляПервый способ: JUSTICE <выражение >Рассматриваются только такие поведения системы, в которыхвыражение в экземпляре модуля становится истиннымбесконечно частоВторой способ: COMPASSION(<выражение >, <выражение >)Рассматриваются только такие поведения системы, длякоторых верно: если выражение в первом аргументе становитсяистинным бесконечно часто, то и выражение во второмаргументе будет становиться истинным бесконечно частоДополнительная возможность:Для упрощения написания систем в каждом экземпляре,вызванном с помощью слова process, предопределенапеременная running, истинная тогда и только тогда, когдапроцесс выбран при асинхронном переходеПолноценный пример, дополненныйMODULE mainVAR b : bird(s.location = NEAR); s : swarm;CTLSPEC AG AF (b.satiety = FED);MODULE bird(food)VAR satiety : {FED, HUNGRY};ASSIGN next(satiety) := casesatiety = HUNGRY & food : FED;TRUE : HUNGRY;esac;MODULE swarmVAR location : {NEAR, FAR};JUCTICE location = NEAR;А теперь всё нормально?Насколько “справедлива” такая справедливость?Полноценный пример, исправленныйMODULE mainVAR b : bird(s.location = NEAR); s : swarm;CTLSPEC AG AF (b.satiety = FED);MODULE bird(food)VAR satiety : {FED, HUNGRY};ASSIGN next(satiety) := casesatiety = HUNGRY & food : FED;TRUE : HUNGRY;esac;MODULE swarmVAR location : {NEAR, FAR};ASSIGN next(location) := location = NEAR ? FAR : NEAR;А теперь где подвох?Полноценный пример, дважды исправленныйMODULE mainVAR b : process bird(s.location = NEAR);s : process swarm;CTLSPEC AG AF (b.satiety = FED);MODULE bird(food)VAR satiety : {FED, HUNGRY};ASSIGN next(satiety) := casesatiety = HUNGRY & food : FED;TRUE : HUNGRY;esac;MODULE swarmVAR location : {NEAR, FAR};ASSIGN next(location) := location = NEAR ? FAR : NEAR;А теперь птица наконец-таки покормится?А должна?А можно ли придумать “разумную” справедливость, прикоторой всё заработает как надо?Полноценный пример, трижды исправленныйMODULE mainVAR b : process bird(s.location = NEAR);s : process swarm(b.satiety = HUNGRY);CTLSPEC AG AF (b.satiety = FED);MODULE bird(food)VAR satiety : {FED, HUNGRY};ASSIGN next(satiety) := casesatiety = HUNGRY & food : FED;TRUE : HUNGRY;esac;MODULE swarm(hunting)VAR location : {NEAR, FAR};ASSIGN next(location) :=location = NEAR & !hunting ? FAR : NEAR;А так лучше?Полноценный пример, трижды исправленныйи дополненныйMODULE mainVAR b : process bird(s.location = NEAR);s : process swarm(b.satiety = HUNGRY);CTLSPEC AG AF (b.satiety = FED);MODULE bird(food)VAR satiety : {FED, HUNGRY};ASSIGN next(satiety) := casesatiety = HUNGRY & food : FED;TRUE : HUNGRY;esac;JUSTICE running;MODULE swarm(hunting)VAR location : {NEAR, FAR};ASSIGN next(location) :=location = NEAR & !hunting ? FAR : NEAR;JUSTICE running;А такое описание лучше всех предыдущих?Небольшое замечаниеРазработчики NuSMV объявили ключевое слово process,переменную running и асинхронное исполнение в целомустаревшими особенностями, которые использовать нехорошоВзамен они предлагают самим моделировать асинхронноеисполнение компонентов системы, первоначально имея толькосинхронное исполнениеА как это сделать?Но так как в NuSMV версии 2.6.0 асинхронное исполнение всёещё есть, то будем его использоватьЗаключение: как запускать NuSMVmy.smv.