Семинар 5.1. NuSMV практика
Описание файла
PDF-файл из архива "Семинар 5.1. NuSMV практика", который расположен в категории "". Всё это находится в предмете "математические методы верификации схем и программ" из 10 семестр (2 семестр магистратуры), которые можно найти в файловом архиве МГУ им. Ломоносова. Не смотря на прямую связь этого архива с МГУ им. Ломоносова, его также можно найти и в других разделах. .
Просмотр PDF-файла онлайн
Текст из PDF
Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2016Семинар 5-6NuSMV: практикаЕщё немного возможностей NuSMVIVAR <переменная > :<переменная > :...DEFINE <переменная ><переменная >...<тип >;<тип >;:= <выражение >;:= <выражение >;Переменные, описанные в блоке IVAR, входят в пространствосостояний автомата, но нельзя использовать их внутри init иnextПеременные, описанные в блоке DEFINE, — это (если коротко)макроопределения; в частности, они не входят в пространствосостоянийСимуляция присутствует в NuSMV, но так как времени наобъяснения мало, смотрите сами в документации, как ейпользоватьсяУпражнение 1: реализация модели КрипкеПроверить выполнимость свойств в модели Крипкеb∅IAGAFaIAFAGaIAFEGaIAXAXAXaIAXAXEXaIEFA(¬(a ∨ b)Ua ∧ b)aa, bУпражнение 2: моделирование программОписать параллельную композицию трёх программ, вбесконечном цикле выполняющих следующее:Iпервая программа: if(x < 10) x = x + 1;Iвторая программа: if(x > 0) x = x - 1;Iтретья программа: if(x == 10) x = 0;Начальное значение x: нольУбедиться в том, что значение x не выходит за пределыинтервала [0,10], в предположении, что1.
условный оператор атомарен2. условный оператор неатомарен; проверка условияатомарна; присваивание атомарноIв последнем случае сделать то же для интервала [-1,11]Упражнение 3: моделирование схемÿ⊕ÿ¬x0x1Убедиться, что схемой реализуется двухбитовый счётчик:(x1 x0 )t+1 = (x1 x0 )t + 1 (mod4)Упражнение 4: крестики-ноликиOXXПроверить, существует ли в этой игреIвыигрышная стратегия i-го игрокаIпроигрышная стратегия i-го игрокаIничейная стратегия i-го игрокаIне-выигрышная стратегия i-го игрокаIне-проигрышная стратегия i-го игрокаIне-ничейная стратегия i-го игрока(i ∈ {1, 2})Упражнение 5: обедающие философы“Плохая ситуация”: ни один философ больше никогда непообедаетIУбедиться, что если философы берут две вилкиодновременно, то плохой ситуации не возникнетIУбедиться, что в классической постановке можетвозникнуть плохая ситуацияУпражнение 5: обедающие философы“Плохая ситуация”: ни один философ больше никогда непообедаетIIДобавить в классическую постановку возможностьположить вилку так, чтобы плохой ситуации не возниклоПроверить для изменённой системы следующие свойства:IIкаждый философ всегда имеет возможность пообедатьесли философ взял вилку, то он обязательно когда-нибудьпообедаетУпражнение 5: обедающие философы“Плохая ситуация”: ни один философ больше никогда непообедаетЕсли это ещё не сделано,Iразделить желание философа пообедать, его обеденныеприготовления и факт принятия пищиIисключить как можно больше обеденныхнесправедливостейУпражнение 5: обедающие философы“Плохая ситуация”: ни один философ больше никогда непообедаетIУбедиться, чтоIIIфилософ не бывает вечно сытфилософ обедает только тогда, когда хочет обедатьесли философ хочет пообедать, то он рано или позднопообедаетУпражнение 6: ресторанАлиса и Боб зашли пообедать в ресторан (и собираютсяобедать бесконечно долго)Неожиданно обнаружилось, что в ресторане осталась толькоодна чистая свободная вилкаЧтобы и Алиса, и Боб могли обедать, официант взял на себяответственность выдавать и забирать вилкуТребуется1.
описать эту систему, сделав официанта как можно болеесправедливым2. убедиться, чтоIIникто не просит вилку без надобноститот, кто захотел вилку, рано или поздно её получит.