2. Model Checking. Вериф. парал. и распределенных программных систем. Карпов (2010) (1185529), страница 58
Текст из файла (страница 58)
Мноамстае О-путей легко интер"регирозать как ксиъкиатнаную нормальную форму функции 1'. Пример 9.4 Функция У'(а. Ь„с), В(ВУ юпорой прелстааяена на рнс. ОЭг монет быль записана а дизьюнктианой нормальной форме(ДПФ) так: г аЬча Ьс.
Следо- г г Ю г г г г г т г г 1 г г Гаева в Буяс пред пода постр опера видна запив опера Рекур функц выпал пим и [л- ввюльиа, фуикцвя ср првиимает значение 1 иа шмдующих наборах перемен- иыхг и = 1, Ь =1 (при любых значеипшг переменной с ) и а = 1, Ь = О, с = 1.
Превериа того, ввлветсв ли фуикцвв выпеливьюй, вевыиолввзюй влв абщезиачвмей. Такая проверка дая булевой функции, представленной в форме В00, осущеспмжтся элементарно. В00 невыполнимой функции мцгержит единственную вершину, помеченную О; В00 общезпачимой функции содермит единственную вершину, помеченную!; В00 выполнимой функции аодермпт аершипу, помеченную 1 (риа. 9.10). Проверка экввввлевтвеств двух булевьп фуиицвй, Проверка эквивалент- ности двух булевых функций, предапшяеииых в В00, сводится к проверке июмарфиости двух биварпых решающих дишрамм (при одном цорядке перемеииых), поскольку В00 — шишпическое представление фувкцип. рвв 9,1О.
Прелсшыеиш иеяыпояпвмай (е), абмезпачпмой (а) в аыпелпамай (в) функций цястг ну г мрш пил С Бина! эги В В би~ ломе рую! еем ! где рг О-р бр Опера лующг 1. Есл юмеи- 1. 6 нлн виной акции функзнмой шеигверке рядке Булевы внерацнв иад ВРР. Булевы операции над дмэчнмми функциями, представленными в ВРР, выполвпотся очень просто. Операция Д„.ь— подстановка булеза значения Ь вместо переменной .г в функции у, выполняетса перенаправлением всех ребер диаграммы, входящих в кюкдую вершину г, помеченную х, в вершину, в которую направлено выходное Ь-ребро вершины т (см. рис.
9.3). Операция отришшня саоднтся к изменению значь ний 0 на 1 н 1 на 0 в терминальных вершинах диаграммы (рис. 9.11). Бинарные логические операции над лвумя ВРО выполншотся просто, если зтн ВРР построены в соответствии с одним и тем хю порядком переменных. В бинарной решающей диаграмме лля любой промемугочной вершины т, помеченной переменной х, подграф, который начинается с вершины, в каторую идет О-ребро, назовем Ьзн(т), а тот граф, в которую идет 1-ребро, наюасм Ь!яЬ(г!. Зтн графы в общем случае пересекмогся.
Кмкдый из них представлжт частичную функцию при различных значениях х. Алгормгм построения ВРР, являющейся результатом применения бинарной булевой операции к двум заданным ВР0, основан на следующих соотношениях. Очевидное равенство, которое представляет разявкение Шеннона: гт !у'х=Огйепр'~ >е(шзт! запишем так (считая гт = у" Э я, где Э вЂ” обозначение произвольной буланой операции): У"ЭБ=Кх=бтйеп[УЭБ)~ ее(ге[~Э8)! ~=Кх =ОгйенИ! е Эб! с)я(ш[у !, Эд! ~).
Рекурсивное применение мого саотношенив позвошжт построить ВРР функции !'Эя по диаграммам функций у и й. Рнс.9.12 покшывает, как еыпслняетея произвольная бинарная булеяа операция иад двумя ВРР с одним и тем ме порядком переменных. Обозначим подграф с вершиной т, помеченной переменной х, так: [х-+.е ) где рс н р, — подграфы, в шпорые из вершины т мдуг, соошетственно, О-ребро н 1-ребро. Операции над дивграммамн выполняются рекурсивно в соотмтствии со следующими правиламн. 1.
Если в вершинах диаграмм одна и тв ме переменная х, то: [ р,р 1Э[ — бс.бг1-[ 6ЬЭбе)4((Э9 Я' Имен Поел ннмв форм с \ с с \ \ с \ \ с Ъ с с с с с сс Рвв Р.11. Разулащт врвменанве онерацнв отрщмнне л Вувтвущ, врелстанленщщ а 1ИтП ткн Слово ~ н1 Мнив (О, 1„ 2. Если переменные х н у в вершиивхднягрвмм резные н «<у, то: [ р р[Р[у есий[=[ (р Э[у ее,рз[)(ЛР[у бейзел именно зто повязано нв рнс. 9д 2. Паоле выполнения операций результнрукнивя структура макет быль нв мяннмвльив.
Применение алгоритма йегйнт приводит результат к требуемой форме В00. ,Я ««у Рис. 9Л2. Рсвлизвшм йпирим«булевмх оправив ивл лвуме фуи«пнямя, ярелсвзашюншв в В00 ТЕОРЕМА й.й Сложность выполнения бинарных булевых оперений нвд двумя фунюшвмн г н д, предстввленныии в форме В00, пслиномивяыа: 0([Д«~ ф). мииимиввини булевьзх функций, нренствалепиьп в ВРР. набор Фушаий [О, й йс[ являя«ел базисом булевых Функций. Иннин сяоввмн, любвя буле- Оен ва функция может быть предствшюна с помощью суперпозицин функций из этого мншксствв. Например, функции базиса Буля (отрицание, дизьюнкция н конъюнкция) представятся так: 13 отрицание х: ту' х сйсн О сйс! !3 дизьюнкция х г у: (У'хгйси!сйсу ОЗ конькекцня лл у: Кхгьеиусйсб Бинарная решающая дишрамма — это такое представление булевой функции в этом базисе, в котором все се эквивалентные булевы подвыршкения присутствуют один раз.
Например, ВРР на рис. 9.7 можно записать твк: у=л-~х, Г4сй У» =ф.хз Пэснбсгзс! »»з = К хз гйел»»г с!зс О уэ !Ух»гйс 1еаг О ~ход фуикц г'(»н л „х ) 1. .»щ гз'.г» сопгас»сшукп различным вершинам граф Таким сбреем, ВРВ является минимавьным графическим представлением булевой функции в базисе (О, 1, йс) при фиксированной упорядоченности переменных. Клшсическвя проблема построения минимальной ДНФ булевой функции, представленной в ВРР, решается очень проси.
Сначала из ВРР можно построить все имплнкаиты функции, перебрав все пути из корня в терминальную вершину. помеченную 1. Например, функция Г, представленная В00 на рис. 9.19, имеет следукицне две импликанты; аЬ, с Ьс. Имею этн импливвнты, можно далее нсцользовать классические методы минимизации.
Для нашего примера легко получштся миннмвльнвя скобочная форма функции: а(Ь о с) . Современные алгоритмы двухуровневой минимизации используют ВЕОУ, что позвояяст существенно повысить эффективность минимизации по сравнению с классическими алгоритмами (39). Одна нз первых работ, в которых нсследоваюя эффект от применения ВОР дла минимизасмн логических функций, называлась "Прорыв с двухуровневой милнмштгш» лсгичеттм схс»»" (32).
Прц р О.б Рргсмотрим пример минимизации болев сложной функции от 4 переменных: лг»тзлзл»»л»лэ яул» о лРт зз т» ох»хзхз т» ч ( ~!хэ"»хзх») ий лп ция и !кции ~исут- $ вер. рафа еиием гкции, но по. ~ В00 ~мылитт. Для якции: цзуют цацки рабат. ~ логи- <ыых: с \ Ъ с \ с Ъ Поеч (рне. и ар мина Мин носи раош ВПП минн наем ченн Поет послФ рно. е прим занан мепи Построим дяя этой функции В00 из ее двоичного решмощего дерева (рис. 9.13). Из этого рисунка видно, что функция имеет две нмпяюшнты: х,хз н х~ тзхзхс.
Просим склеивание н вынос за скобки даст для этой функшш миннмавьиую сксбочиую форму г = А~ (гз о хзх4). Миинмизаннп иеиалпостью оиределениыя булевык функций. Неполностью определенные булевы функции могут быть представлены с помощью расширений В00. Одно из таких расширений, МВ0 (модифицированные В00), предложено в работе [й5). В этой работе также излшкены алгоритмы минимизации неполностью определанных булевых функций перенаправлением тек ребер графа МВ0, которые ведут в терминальную вершину, помеченную Х (боп'1 аие). Рис.
9.14 пшмзмввст пример такой минимизации. Пестроевие ВРВ. Построение ВР0 булевой функции можно вмполнить после построения ее двоичного решающего персея, как это показано на рнс. 9.2 и 9.13. Но если функция представлена в формульной записи, моною применить простой алгоритм трансляции, выполняя сннтвкаичсскнй анализ заданной формулы (т. е. выделяя се элементарные подформулы) и исповыуя мстолы атрнбутной трвнсшщни.
.«и:.о ',т 5- . 41меаа Прим П р Е= Г с лля по с И По ап ются е При а5 ла х 5 КОРНЕ5 Семан блемы Так, о петерс .чы -о Р=А5 тт Рбм„ВИ, Фин. Прщмр миннмнтащв пастпамт опреледеинеп фущтщи В соо: щ5и, т, натив опера аоскот ЕА1.К~ Ф рч В сне 55 Хб подфо На ри .55 — те ние) т ритма на рис Пример й.б Построим ВОЮ для булевой функции )г слвлукнцего вндш У=Ум(-а~х) лля порыва переменных х < у с я.
В соответствии с основной идеей сшпвкснчески-ориентированной транашции, такое построение должно выполняться в два этапа. Нв первом по грамматике языка логических формул, учитывмошей приоритеты логических операций, строится синтаксическое дерево формулы гт с помощью обычного восходящего алгоритма снгпвксического анализа, например, алгоритма (.А(.К(1) (159). Синтаксическое дерево представлвст собой структуру подформул дюной формулы. Оно повпаио нв рис.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
