И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin (1161239), страница 13
Текст из файла (страница 13)
Когдавилка лежит на столе (она свободна), то ожидается запрос либо от левого, либо от правогофилософа на ее использование. Когда один из философов взял вилку, то посоответствующему каналу ожидается сигнал о возвращении вилки.proctype fork(chan left_phil, right_phil){byte cur_state_fork = 0;/* F0. Вилка свободна */end:do::( cur_state_fork == 0) ->if::right_phil ? msgtype ->cur_state_fork = 2;::left_phil ? msgtype ->cur_state_fork = 1;/* Если вилка свободна *//* Правый философ запросил вилку *//* F2.
Вилка у правого философа *//* Левый философ запросил вилку *//* F1. Вилка у левого философа */57::skip;fi::( cur_state_fork == 1) ->left_phil ? msgtype ->cur_state_fork = 0;::( cur_state_fork == 2) ->right_phil ? msgtype ->cur_state_fork = 0;od}/* Левый философ возвращает вилку *//* F0. Вилка свободна *//* Правый философ возвращает вилку *//* F0. Вилка свободна */Запуск процессов-вилок и процессов-философов происходит в процессе init. Рассмотримнумерацию процессов и каналов. Даны N процессов-философов с номерами от 1 до N(аналогично для вилок), N каналов для левых (аналогично для правых) по отношению кфилософам вилок с номерами от 0 до N-1.•Припишем процессу-философу номер proc.•l_fork – канал для взаимодействия философа proc с левой вилкой получит номерproc-1.•r_fork – каналу для взаимодействия философа proc с правой вилкой назначимномер proc.•Процессу, соответствующему правой вилке этого философа, назначим номер proc.Согласно предложенной нумерации получим номера и названия каналов для взаимодействиявилки с левым и правым философом: r_fork с номером proc для левого по отношению квилке философа и l_fork с номером proc для правого по отношению к вилке философа.Запуск начинается с процессов с номером 1.init {byteproc;proc = 1;get_in_stuck = 0;do:: proc <= N->/* запуск процесса-философа №proc с левым каналом №(proc-1) и правым каналом №proc */run phil (l_fork[proc-1], r_fork[proc%N], proc);/* запуск процесса-вилки №proc с каналом для левого философа №procи каналом для левогофилософа №proc */run fork (r_fork[proc%N], l_fork[proc%N], proc);proc++;}:: proc > N ->breakodОбнаружение состояния общего голоданияСитуация общего голодания, которую необходимо обнаружить, проявляется во взаимнойблокировке процессов – ни один из процессов-философов не может продолжить работу,ожидая поступления вилки.
Свойство взаимной или системной блокировки (system deadlock)58относится к базовым верифицируемым Spin и проверяется автоматически при поискенекорректных конечных состояний. Для этого необходимо убедиться, что в окне ВаsicVerification Options установлен флаг Invalid Endstates. В выводе результатов верификациипоявится сообщение, свидетельствующее об обнаружении пакетом системной блокировки:Full statespace search for:never claimassertion violationscycle checksinvalid end states- (not selected)- (disabled by -A flag)- (disabled by -DSAFETY)+Контрпример, обнаруженный верификатором, демонстрирует, как один за другим философытянутся за левыми вилками, до тех пор пока не приходят к ситуации, когда каждый философждет правой вилки.3.5Мир блоковМир блоков – это искусственная среда планирования действий, которая вследствие своейясности и простоты была одним из наиболее часто приводимых в литературе попланированию в искусственном интеллекте в 1960х.Среда состоит из кубиков (блоков), стоящих на столе по отдельности или в несколькихвертикальных башнях.
Взаимное расположение кубиков можно считать состоянием среды.Целью является построение заданной конфигурации – одной или нескольких башен. Толькоодин кубик, на котором ничего не стояло, может быть перемещен за один шаг: он можетбыть либо поставлен на стол, либо помещен сверху на какую-нибудь башню.59Описание модели на языке PromelaПостроим модель на языке Promela, описывающую все возможные конфигурации идопустимые их изменения для любого заданного числа блоков и любого их расположения.Число блоков определим параметром N, блок будет идентифицироваться уникальнымномером от 0 до N-1.
Конфигурацию будем задавать двумя массивами длины N: up[i]определяет номер блока, стоящего над i-м, down[i] определяет номер блока, стоящего подi-м. Специальная константа NOTHING определяет, что над или под блоком ничего не стоит.Целевая конфигурация определяется подобными массивами Tup и Tdown.Исходная конфигурация на рисунке будет представлена так: up[0]=NOTHING, up[1]=2,up[2]=0, down[0]=2, down[1]=NOTHING, down[2]=2. Возможные переходы междусостояниями программируются так:a) выбираетсяслучайный блок i, стоящий сверху (над нимup[i]==NOTHING), и этот блок снимается (up[down[i]] = NOTHING);ничегонет,b) выбранный блок либо кладется на стол (down[i]=NOTHING), либо выбираетсядругой блок j, который стоит наверху (up[j]==NOTHING), и на него помещаетсяблок i (up[j]=i; down[i] = j). Блок j отличен от i (j≠i),.Проверяемое условие задается как совпадение текущей и целевой конфигурации, т.е.совпадением массивов up[] и Tup[], а также down[] и Tdown[].
Программа в цикле сначалапроверяет, совпали ли текущая и целевая конфигурации, и если нет – то случайно делаетодин из возможных переходов – изменяет текущее состояние (конфигурацию) на соседнее.#define N 3#define NOTHING 255#define N-1 2/* массивы текущего состояния */byte up[N];byte down[N];/* массивы целевого состояния */byte Tup[N];byte Tdown[N];byte i, j, k;bool equal = false,findi = true,findj = false,/* число кубиков *//* номер над i –м кубиком *//* номер под i –м кубиком *//* номер над i –м кубиком *//* номер под i –м кубиком *//* номера кубиков *//* определяем снимаемый кубик i *//* определяем кубик j, на который ставим i */60checkconf = false;/* проверяем полученную конфигурацию */active proctype cube_world(){/* начальное состояние*/up[0] = NOTHING;up[1] = 2;up[2] = 0;down[0] = 2;down[1] = NOTHING;down[2] = 1;/* целевое состояние */Tup[0] = 1;Tup[1] = 2;Tup[2] = NOTHING;Tdown[0] = NOTHING;Tdown[1] = 0;Tdown[2] = 1;i = 0;j = 0;/* основной цикл */do:: findi ->/* случайный выбор i */if :: (up[i] == NOTHING) -> findj = true; findi = false;if :: ( down[i] != NOTHING ) ->up[ down[i] ] = NOTHING;/* i-й сняли */:: else -> skip;fi;:: (i < N-1) -> i ++:: (i > 0)-> i -fi:: findj && ( down[i] != NOTHING) -> /* */down[i] = NOTHING;/* i-й положили на стол */printf("MSC: [%d] to table \n", i);findj = false;checkconf = true;:: findj -> /* случайно выберем j и i-й поставим на j-й */if :: ( i != j ) && ( up[j] == NOTHING ) ->up[j] = i; down[i] = j;/* i-й кубик ставим на j-й */printf("MSC: [%d] to [%d] \n", i, j);findj = false;checkconf = true;:: (j < N-1) -> j ++:: (j > 0)-> j -fi:: checkconf -> /* проверка, достигли ли целевого состояния */equal = true; k = 0;do :: ( k < N ) ->equal=equal && (up[k]==Tup[k]) && (down[k]==Tdown[k]);k++:: ( !equal ) -> break:: ( k == N ) -> breakod;if :: (equal) -> break /* целевое состояние найдено */:: else -> checkconf = false; findi = truefiod;61}printf("MSC: movement finished \n")Поиск решения задачи средствами SpinЗадав начальное и целевое состояния, попробуем найти решение (последовательностьдопустимых переходов) средствами верификации.
Для этого поставим задачу перед Spin: несуществует ни одного пути такого, что выполняется LTL-формула: FG (equal == true), т.е.не существует ни одного пути, на котором возможно прийти к целевому состоянию изданного начального.Spin находит контрпример, предлагая решение данной задачи.Поскольку модель допускает несколько решений, то Spin находит одну извозможных последовательностей переходов – совсем неоптимальную.Изобразим для наглядности решение, предложенное верификатором, какпоследовательность перемещения кубиков.62Приложение 1. Параметры симуляцииВыберите в меню Run пункт Set Simulation Parameters.
Откроется диалоговое окно SimulationOptions.В данном окне на панели Display Mode задается, какие окна необходимо выводить присимуляции.• MSC Panel – панель диаграммы взаимодействия. Для данного окна можно задать, какбудут отображаться надписи на диаграмме.o Step Number Labels – на диаграмме указываются номера шагов симуляции.o Source Text Labels – на диаграмме указываются строчки исходного кода.Ghj• Time Sequence Panel. Данная панель показывает, какие действия выполняет каждыйпроцесс в определенный момент времени.o Interleaved Steps – в каждый момент времени на диаграмме выводится номерпроцесса, который выполняется, и строка кода, которая выполняется в этомпроцессе.o One Window per Process – для каждого процесса открывается окно, содержащееописание процесса на языке Promela.
Во время симуляции подсвечиваетсястрока, которая в данный момент времени выполняется.o One Trace per Process – для каждого процесса открывается окно. Во времясимуляции выводится номер строки, которая в данный момент временивыполняется.• Data Values Panel – панель для просмотра значений данных.o Track Buffered Channels – просмотр значений каналов с буфером.o Track Global Variables – просмотр значения глобальных переменных.o Track Local Variables – просмотр значения локальных переменных.63o Display vars marked ‘show’ in MSC – просмотр изменения значения переменнойна MSC диаграмме.
Для отображения переменной необходимо передобъявлением этой переменной поставить префикс show (например, написатьshow byte cnt вместо byte cnt).• Execution Bar Panel – панель просмотра процента выполненных шагов каждымпроцессом в зависимости от общего числа выполненных шагов.• На панеле Simulation Style устанавливается тип симуляции. Возможны 3 видасимуляции:o Random - все недетерминированные решения определяются случайнымобразом.o Guided – симуляция для сгенерированного верификатором ошибочного пути.Данная симуляция используется для отладки ошибки, найденнойверификатором.o Steps Skipped – число первых шагов, которые пропускаются.o Interactive –пользователя.всенедетерминированныерешениязапрашиваютсяу64Приложение 2.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
