8-9. SPIN - практические задания по проверке LTL-спецификаций

Математические методыверификации схем ипрограммЛекторы:Захаров Владимир АнатольевичПодымов Владислав Васильевичe-mail рассказчика:valdus@yandex.ruОсень 2017Семинар 8–9Spin(практика)Упражнение 1: реализация модели КрипкеПроверить выполнимость свойств в модели Крипкеba, cIG(a → b ∨ c)IGFaIFGaIGF¬c → F(a ∧ b)IGF¬c → G(¬bUa ∧ b)∅a, bУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Процесс может сколь угодно долго находиться в критическойи некритической секциях (CRITICAL и NONCRITICAL соответственно)Переменная free не изменяется процессом, находящимся в этихсекцияхУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Инструкция в каждой отдельной строке выполняется атомарноИнструкция block(free) блокирует процесс, пока не станет истинным условие freeУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Выяснить,Iмогут ли процессы одновременно находиться в своихкритических секцияхIвозможна ли блокировка обоих процессов сразу,Iверно ли, что, выйдя из некритической секции, процессрано или поздно достигнет критическойУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Добавить в модель справедливость: процесс не может бесконечно долго находиться в критической секцииИзменить модель так, чтобы пара инструкций block(free);free = false; выполнялась атомарно: если block(free) неблокирует процесс, то немедленно выполнить free = falseУпражнение 2: доступ в критическую секциюДва процесса с разделяемой булевой переменнойbool free = true;исполняют одну и ту же программу:while(true) {NONCRITICALblock(free);free = false;CRITICALfree = true;}Внимательно посмотреть на флаг “слабая справедливость” в настройках верификацииУпражнение 3: передача сообщенийСистема состоит из одного клиента, одного сервера идвунаправленного канала связи между нимиКлиент и сервер описываются левым и правым автоматамисоответственно:request!request?response?response!Запись m! означает, что при выполнении перехода сообщение mпосылается в канал, запись m? — что сообщение m принимаетсяиз каналаУпражнение 3: передача сообщенийСистема состоит из одного клиента, одного сервера идвунаправленного канала связи между нимиКлиент и сервер описываются левым и правым автоматамисоответственно:request!request?response?response!Выяснить,Iверно ли, что если клиент посылает сообщение request,то он обязательно примет сообщение responseIвозможна ли ситуация, в которой и клиент, и серверожидают приёма сообщенийРассмотреть два варианта устройства канала:IсинхронныйIасинхронный ёмкости 1Упражнение 4: синхронные системыПо комнате летает два комараВ начальный момент времени оба комара не жужжатЕсли комар не жужжит, в следующий момент времени онначинает жужжатьЕсли комар жужжит, в следующий момент времени онперестаёт жужжатьЖужжание комара описывается булевой переменнойОписать систему жужжания двух комаров с такимтребованием: в каждый момент времени либо оба комаражужжат, либо оба комара не жужжатУпражнение 5: переправаВолк, коза, капуста и лодочник с лодкой стоят на левом берегуреки и хотят переправиться на правыйТолько лодочник может грестиЛодка вмещает только двоих, включая лодочникаНельзя оставлять волка с козой, а также козу с капустой наодном берегу без присмотра лодочникаМогут ли все переправиться на правый берег?Упражнение 6: распределённые алгоритмыТри процесса соединены друг с другом в кольцооднонаправленными асинхронными каналами связи ёмкости 1:P2P1P3Каждый процесс имеет булеву переменную b, имеющую произвольное значение в начале работы системы, и ровно два разаделает следующее:Iпосылает в канал значение bIпринимает из канала значение, и если принято true, тозаписывает true в переменную bУпражнение 6: распределённые алгоритмыТри процесса соединены друг с другом в кольцооднонаправленными асинхронными каналами связи ёмкости 1:P2P1P3Убедиться, чтоIкаждый процесс рано или поздно выполнит всю своюпоследовательность действийI(каждый процесс в конце работы хранит значение true) ⇔(хотя бы один процесс в начале работы хранил значениеtrue)I(каждый процесс в конце работы хранит значение false)⇔ (ни один процесс в начале работы не хранил значениеtrue).