2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 50
Текст из файла (страница 50)
Мнр блоков: е) эммча; 6) пространство сосгоанвй Исходная конфнгурапнв на рнс. 8.4 будет предсмшаенв тмс те[о[-вотнпм, чр [ц-г, сргг[-о, сто[о[-г, альт[и-нотнтна, стт[г]-э. Всжможные переходы между состояннямн прогриммнрукпоя так 1. Выбирается случайный блок [, стоящнй сверху(т. е. если срц]-нстнщо), н этот блок сннмастся (чр[ссчс нц [» нотнтно). 2.
Выбраннмй блок либо кладется на стол (сот[и-нотяхно), лнбо выбнраегся другой блок В отлнчнмй от с [2[-г[, мпорыЙ стонт сверку (срц[ нотнгна), н напето помещается бяок и (срц[ ь ов вйц )). Прог рацн Прог гура[ меня Прог волос ложе Одна чески нспос реша В нас ко.
С эуют (гю е стоян слою женн томас шем этом класс Ргорй прнш орган СЬ с) "[[ ла вмм и ется, га исг гое. й вск)сс мсщя В.З. И йи) Вольв стн де (ля~ в н т чр шнг юды Проверяемое условие задвигая квк совпадение текущей и целевой конфнгу- РаЦИИ, т. Е. СОВПаДЕНИЕМ МаССИВОВ чры И т чр П, а таКжЕ асье(1 И т аснпС. Программа в цикле сначала ироверяст, совпалн ли текущая и целевая конфигурации, и если нет, то случайно делает один из возможных переходов — изменяет текущее состояние (конфигурацию) на соседнее. Программа на языке Рпппе!а для решения этой задачи приведена в Руко.
водстве по язы«у Рюше)а и использованию системы верификации Яр(п, приложенному к этой книге. Одна нз главных трудностей проблемы планирования — та, что для прайтнческих залач пространство поиска огромно. Эта трудность преодолевается использованием символьного аягорнтма тобе( сйесЫпй на основе бинарных решыощих диаграмм, который мы будем изучать в следующих главах. В настоящее время тобе) спссЫпй используется в планировании оцень широко. Современные системы планирования, ссновшшые на этих идеях, используют мощные схемы, объединяющие методы символьной верификации (см.
гл. 10) и классические методы эвристического поиска в пространстве состояний. Па основе идей любе( сйесЫпй разработаны алгоритмы решения слшкных проблем построения планов. удовлагворжоших требованивм, выраженным произвольнымн формулами темпоральной логики. Примером с автоматической генерацией подобного плана является приведенная в следующем разделе задача о фермере, волке, козе и капусте. По исследованиям в этом направлении проводится несколько ежегодных конференций, разработаны мощные системы планирования, интегрировавшие любе( сйесЫпй с классическими методами эвристического поиска (ВОПР(ап, С1КСРч МВР, Ргор(ап идр.).
Существует множество успешных примеров практического применения этого подхода к задачам планирования. В частности, в заявлении организационного комитета Мшкдународного семинара чрйшшпй Ыв Моде! СйесЫпй 'Ы" говорится: "В настоящее время тоде) сйесеиб яапытся одной из наиболее "горячит" тгм ин(эорнатиаа Идея зоключоетсл е том, что модель системы проеерягтсл но вытмненнг для нее логичгслнч тргбоеоннй Изначально эта идем была штмьзоеана для проверки корректности стем н компьютгриык протою.юе. Недавно элю ят идея была применена дяя задач планирования в области наг)кственнога иитгялекта с замечательным рсиелам н прилепа и созданию мощи ык систем планированы~.
гно), грху 8.3. Логические головоломки и тОбЕ! СпЕСЫИЯ Большое число логических голоашипюк состоит в поиске последовательности действий, которве приводит некоторую систему нз эадвнмого соспжння в г в некоторое требуемое состояние. Такие головоломки можно считать частным случаам проблемы планирования. Рассмотрим несколько примеров. Китайские кольца (СЫпеэе г!пйз) — з!о старинная механическая пшаволомка, которая состоит в том, что заданы Н колец, соединенных друг с другом и надетых на горпюнтальную вытяну!ую проволочную петлю. К каждому кольцу прикреплен стержень (рис. 8.5, а). Цель головоломки — построщь план действий, в результате которых все кольца будут сняты а петли.
Для решения задачи нужно учесть следующее. Первое кольцо всегда можно спать с легли или надеть на нее (рис. 8.5, б). Любое кольцо можно снять или напеть на петлю. талька если блившйшее предыдущее находится нв петле, а все кольца до этого предыдущего уже сняты (рис. 8.5, е). Используем для решения головоломки систему верификации Бр!и. Будем рассматривать эту систему колец как дискретную динамическую систему..
Мы мпвюм описать все возможные изменения состояний анстемы, ее начальное и целевое состояния, н проверить выполнение у системы свойства: целевое состояние ледостихиио. Баян это условие неверно, то система верификации выдаст опровержение — конзрпример, который и будет искомым планом действий. Состояние системы "Китайские кольца" определим юж набор значений буле- ВЫХ ПЕРеменных хнхз,..«х„, ГДЕ х, — Састояние /-ГО СЛеВа колы!а (х! Лне — надето, х! Ра/ве — снято), л — число колец. Начальное соаюяние — все значения х, равны !гив, целевое состояние — вае значения х, равны /а/зв.
Переходы в кюкцом состоянии определяются так: если все т„хз,...,хв, Уа/Рв (зги кольца аняты), а хь =вне (2.е кольцо надето), то значение переменной хз,! можно изменить на противоположное(т. е. кольцо 2+1 можно либо снять, либо надеть). Прмеряеиое свойство: АО(х! н хз ч хз ч хв г хз) — на всех пущх во всех состояниях всегда хотя бы одно кольцо остапе!ел, т. е. никакая последовательносп, действий НЕ приведет к целевому аостоянию, в котором все кольца сняты. Основной фрагмент программы ранения этой проблемы на языке Рвоте)а для 5 колец выглядит так: Ьсс1 х1, х2, хз, хв, хэ Свив! /' вначале всв вальса вв!мвм */ аа :: сгвв -+ в1 х1 /* вврвсв вовьао и!ива все! лв свввв/вввввь*/ ! ! х1 -+ х2 вз. /«если 1 ввавва, ю 2 !таво свесь/ввлввь «/ !!-впщвз -+ хэ хэ /' з-сввга, 2- вя, вс З новее с в /ввзют */ првмщ !!-в11 :: в1в :: х11 Оа Систе! (8 шм 11111 -! аы Лагнч голов< еще в в шко сти, т фирм> сйесй! ражие Проб! что ф! каз) г лять ! что б с ком! Хотя шени! сструк МОДЕР саста: време будев Тают блем рекал релра тура конус сама ется! имехеяил алщвлнт лмпег ЛОВО- ' дру.
ронть Южно ь илн тле. а 4 рас" ,. Мы НОЕ И зе сохации ганом булесльца ю со!ня з, н все о), то сльцо Ытео: ~гя бы гриве- йа для х144 х2ыхз -+ х4 х4 /* если 1-е х 2-я-сеяти,х З-хяхеео, то 4 ноево схяяь/хятть*/ 4144 «244 хзаах4 -4 хз а5 /* 5-е мжхс снять/хялееь */ хгьь хзш «зы хшх х5 -+ ьхеях /* Останов, ясе «ольхе схяги '/ сс Система Брш вмдест контрпример — искомый путь к целевому состовнню нз 18 шагов: 11111 -+ 01111 -+ 01011ы 11011 -ь 10011 -ь 00011 -+ 00010 -+ 11010 -+ 01010 -Я 01110 -ь 11110 -ь 00110 -+ 00100-411100-401100-401000-+11000-~00000 Логические головоломки, связанные с переправамн через реку. Такие головоломки имеют более чем тысячелетнюю историю.
Они были известны еше в Древнем Египта. В наше время подобные мшачн встречаются не только в школьных математических кружках, но и при приеме на работу (а частности, такие ъщачи задавались на собеседояаиияХ ПРн найме сотрудников в фирму ЯМайкроссфт"). Мы рассмотрим здесь решение с помощью тобе) сйесуйпй двух из ншц некоторые другие формулировки приведены как упражнения к этой главе. Проблема "фермер, волк, каза и капуста".
Зта головоломка состоит в том, что фермер должен переправить через реку с левого берега на правый волка, козу и мешок капусты. Кроме фермера, который только один н мажет управлять лодкой, лодка мажет вмдержать дополнительно что-то одно — либо волка, либо козу, либо мешок капусты. Решение проблемы осложняется тем, что без присмотра фермера келия козу оставлять с валком, а капусту— С Ксэсй. Хотя среда, в которой принимаются решения, совсем не дискретныг, дяя решения этой проблемы некио построить абстрактную дискретную модель— структуру Кринке, и исследошпь на ней возможные нуги. Зта абстрактная модель не будет учитывать ни времени нахождения системы в каком-либо состоянии (например, пока фермер отдыхает после очередной переправы), ни времени переправы.
Переходы, представляющие собой переправы, в модели будем считать неделимыми (рис. 8.6). Такая абстракция не учитывает проблем с затвскнванием в лодку козы, проблем с течением реки и т. п. Дла решение задачи эти факторы не важны, переходы в модели неделимы с точки зрелая лробымыг ссстаяяеянл илана переправы. Таким образом, абстрактная дискретная модель переходов (структура Кринке) яшшется адекватной системе обьекгов <(84)гмер, волк, коза, халустаэ и ее динамике для решения задачи планирования переправы, хотя сама система с козой, голодным волком, течением реки и т.
п. вовсе не являсшя дмскретиой. ))веа Л ))Леман Рис. Э.б. а) Голоеоломка "К!ланские юлька"; б) первое юные всепа можно снять либо нелсть; в) если а — ! колец саатм, а а — нет, то и ь ! калью мсино снктьлибо налета Рпе. 8.8. Проблема переправм через реву фермора, волва, возм и вапуотм /леев в Состоянием среды будем считать состояние всех чепарех действующих объектов. Введем булавы переменные; / описывает состояние фермера, и— состояние волка, й — состояние козы и с — состояние капусты. Их значения: г" = /сйе — фермер на левом берегу, /'= лтм — фермер на правом берегу; то же длв волке, козы и капусты. Таким образом, состояние (/'=ггие,и /л/зе,й=1а/зе,с ггие) говорит о том, по фермер с капустой уже находятся на правом берегу, а волк с коюй ждуг на левом. Будем такое состовнне обозначать (/, щ у,с).
Началыюе состояние — все на левом берау, целевое состояние — все на правом берегу. Переходм струкгуры Крипке определявгг возможные изменения сосюяний системы, т. е. переправы через реку. Этн переправы характернзукися тем, что только фермер мвквт управлвть лодкой. Поэтому, например, из сосюяння (/. и, у,с) можно перейти только в два состояния: в состояние (-г/, и, й,с) (фермер, который находился на правом берегу, переехал на левый берег один) или в состояние (-т/, щ у, с) гфермер переехал на левмй берег с капустой, которая нвходилвсь на том же берегу, что н онй В отличие от предыдущей задачи, на искомый путь здесь должно быль наложено ограничение. Его можно вырвмпь формулой (й и и) д (л и с) и» (й и / )— если коза находится на том хм берегу, чго н волк или капуста, то фер.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
