И.В. Шошмина, Ю.Г. Карпов - Введение в язык Promela и систему комплексной верификации Spin, страница 9

*/16/* отладочная печать */17printf(“MSC: %d\n,” mynumber);/* посылаем сообщение типа one с параметром18out ! one(mynumber);mynumber – номером данного процесса *//* метка end показывает, что не будет ошибкой,19end: doесли процесс в итоге остается в этом цикле вечно */20:: in?one(nr)->/* если получаем сообщение типа one с номером,то записываем номер в переменную nr и смотрим: */21if/* если процесс активен, то: */22:: Active ->23if/* если максимум еще не найден*/24:: nr != maximum ->/* то передаем сообщение типа two25out ! two(nr);с полученным номером соседа */26neighbourR = nr27:: else ->/* если же максимум найден (т.е. возникла28ситуация, когда остался 1 активный процесс )*/29assert(nr == N);/* то убедимся, что этот максимум равенколичеству процессов */30know_winner = 1; /* и отметим, что теперь известен лидер */31out ! winner,nr; /* передадим сообщение типа winnerс номером узла, который мы считаем лидером */32fi/* если же процесс не активен*/33:: else ->/* то просто пропускаем сообщения дальше*/34out ! one(nr)35fi36/* если получаем сообщение типа two,37:: in?two(nr) ->то записываем полученный номер35в переменную nr */3839404142434445464748495051525354555657585960if:: Active ->if:: neighbourR > nr && neighbourR > maximum -> /* если номероказывается новым локальным максимумом */maximum = neighbourR; /* сохраняем значение новогомаксимума */out ! one(neighbourR) /* передаем номер дальше */:: else ->/* иначе процесс становится пассивным */Active = 0fi/* если же процесс не активен*/:: else ->/* то просто пропускаем сообщения дальше*/out ! two(nr)fi/* если получили сообщение о том,:: in ? winner,nr ->что лидер выбран, то: */if/* если текущий процесс не лидер*/:: nr != mynumber ->printf(“MSC: LOST\n”);/* если же, наоборот, текущий процесс:: else ->является лидером*/printf(“MSC: LEADER\n”);/* количество лидеров увеличилось*/nr_leaders++;assert(nrleaders == 1) /* проверим, что лидеров в системе только 1*/fi;if/* если процесс уже знал о том, что лидер выбран,:: know_winnerто этот процесс его и назначил.

Значит, мы ужеобошли все кольцо и нужно заканчивать работу*//* иначе передадим сообщение о лидере дальше*/:: else -> out!winner,nrfi;breakod6162636465 }6667 init {68byte proc;69atomic {70717273747576777879 }/* если процесс активен, то сравниваем его номерс соседним активным слева илокальным максимумом */}/* инициализирующий процесс *//* одной атомарной операцией запускаем N копийпроцесса node*/proc = 1;do:: proc <= N ->run node (q[proc-1], q[proc%N], (N+I-proc)%N+1);/* каждые 2 соседних процесса связывают2 уникальных канала in и out */proc++:: proc > N ->breakodПример симуляции модели выбора лидераПроцесс с номером 5 первым посылает свой номер по каналу соседнему процессу [28 -> 34].Все остальные процессы делают то же самое, прежде чем начать принимать соседниезначения [30 -> 38; 35 -> 54; 40 -> 49; 42 -> 66].36После того, как 4-ый процесс отправил свой номер следующему (3-ему) [30 -> 38], онполучает номер от 5-го процесса (для него предыдущего) [28 -> 34].

Т.к. полученноесообщение типа one и этот номер не равен сохраненному максимуму (4-ем), то предаем этотномер в сообщении типа two следующему процессу [47 -> 65].То же самое делают и всеостальные процессы [48 -> 76; 61 > 80; 60 -> 105; 81 -> 82], т.к.максимум пока не может бытьдостигнут.Когдапроцесс4получаетсообщение типа two с номером 1[81 -> 82], он сравниваетсохраненный номер активногососеда (5, полученный из 28 -> 34)и свой максимум (4, т.к.

он еще неменялся) с полученным значением.Получается, что номер активногососеда больше в обоих случаях =>это локальный максимум =>сохраняем максимум и следующимсообщением посылаем его [104 ->106].Процесс 3, получив сообщениетипа two со значением 5 [47 -> 65],сравнивает сохраненный номерактивного соседа (4) и своймаксимум (3) с полученнымзначением.

Получается, что номерактивного соседа меньше =>процесс 3 становится пассивным идальше просто пропускает черезсебя все сообщения [104 -> 106] ->[113 -> 115].То же самое происходит и спроцессом 2 после [48 -> 76], и спроцессом 1 после [61 -> 80], и,наконец, с процессом 5 после [60 > 105].Таким образом, сообщение типаone со значением 5 возвращаетсяобратно [134 -> 135] к процессу№4, пославшему это сообщение.Процесс проверяет, что значение всообщении равно максимуму и сообщает остальным, что лидер выбран [142 -> 143].После окончания симуляции в окне Simulation Output выведены все сообщения от Spin. Вданных сообщениях для каждого шага симуляции показано, какой процесс выполнялся икакая строчка описания протокола на Promela была выполнена.В окне log (внизу основного окна программы) выводятся строчки:37.starting simulation.spin -X -p -v -g -l -s -r -n1 -j0 pan_in.at end of run.Они показывают команды, которые были синтезированы Xspin, для выполнения симуляции суказанными параметрами.Для закрытия окон симуляции нажмите кнопку Cancel на панели Simulation Output.Верификация базовых свойствЗапустите верификацию базовых свойств, нажав кнопку Run на панели Set VerificationParameters.

Верификация модели leader должна пройти без ошибок, и в открывшемся окнеVerification Output выводится сообщение “errors: 0”. Закройте окно верификации.Введем искусственную ошибку в программу, добавив в строку 22 оператор assert(false).В результате строка будет выглядеть::: Active -> assert(false);Снова запустим верификацию. Теперь SPIN обнаружит ошибку, и предложит посмотретьконтрпример, ее демонстрирующий Run Guided Simulation (Запустить управляемуюсимуляцию).Если выбрать изменение установок управляемой симуляции Setup Guided Simulation, тоXSpin снова панель задания параметров симуляции, все опции в которой, кроме однойостались без изменений.

XSpin установил в Simulation style Guided Simulation вместо RandomSimulation.GuidedЕсливыбратьRunSimulation, и затем Run в окнеSimulation Output, то XSpinпокажет путь, который привел кошибке.В этот раз симуляция завершаетсяв момент, когда было достигнутонарушение в assert, а не когдавсе процессы дошли до своегоконечного состояния.После завершения симуляциизакройте все окна симуляции,нажав кнопку Cancel в Simulation Output Panel. Удалите добавленный оператор assert (т.е.строка 22 будет выглядеть следующим образом :: Active ->).Проверка LTL формулПользователь может определить свои специфичные требования к модели в SPIN, выразив ихв виде LTL формул. Обозначение темпоральных операторов в «Редакторе LTL формул» (LTLProperty Manager в меню Run):38<>q[]qw U qFqGqw U qхотя бы раз в будущем qвсегда в будущем qw до тех пор пока qгде q – атомарный предикат.По умолчанию XSpin пытается считать файл с расширением .ltl, и тем же именем, что ифайл на Promela, загруженный в основном окне.

В нашем случае будут загружены данные изleader.ltl.1. Проверим требование, что лидер должен быть только 1, т.е. что в нашей модели неможет быть выбрано два и более лидеров.39Введем новую формулу в окно Formula:[] noMoreДанной свойство означает, что выражение, заданное с помощью noMore, должно быть всегдаистинно. Можно задать, является ли выполнение данной формулы желаемым поведениемсистемы или ошибочным: в первом случае выбирается в Property holds for пункт AllExecutions, иначе - No Executions. Так как выполнение свойства является желаемым,выберите в Property holds for пункт All Executions.Атомные предикаты, подобные noMore, задаются в окне Symbol definition box.#define noMore (nr_leaders <= 1)Нажмите кнопку Generate. В окне Never Claim для заданной LTL формулы генерируетсяособый процесс never, с включенным в него ОТРИЦАНИЕМ формулы./** Formula As Typed: [] notMore* The Never Claim Below Corresponds* To The Negated Formula !([] notMore)* (formalizing violations of the original)*/never {/* !([] notMore) */T0_init:if:: (! ((notMore))) -> goto accept_all:: (1) -> goto T0_initfi;accept_all:skip}Результаты верификации будут положительные, в том смысле, что данная формулавыполняется на данной модели:40Full statespace search for:never claim+assertion violations + (if within scope of claim)acceptancecycles + (fairness disabled)invalid end states- (disabled by never claim)State-vector 200 byte, depth reached 205, errors: 097 states, stored1 states, matched98 transitions (= stored+matched)12 atomic stepshash conflicts: 0 (resolved)unreached in proctype nodeline 53, "pan.___", state 28, "out!two,nr"(1 of 49 states)unreached in proctype :init:(0 of 11 states)unreached in proctype :never:line 104, "pan.___", state 8, "-end-"(1 of 8 states)SPIN выводит достаточно много дополнительной информации (число состояний, векторглобального состояния, недостижимые участки кода и т.п.), которая необходима дляоптимизации модели.Таким образом, мы убедились, что лидер выбирается всегда только 1.

Ту же самую проверкуможно сделать и с помощью оператора assert и базовой верификации (в приведенномвыше тексте программы это уже сделано):57 assert(nrleaders == 1)Строчка идет в тексте программы сразу после добавления нового лидера, для того, чтобыSpin проверил, что добавленный лидер оказывается единственным в модели.2. Проверим, что лидер, в конце концов, будет выбран при помощи LTL формулы<>[]oneLeader,где в качестве атомного предиката задано:#define oneLeader(nr_leaders == 1).Эта формула означает, что когда-нибудь наступит момент, после которого количестволидеров всегда будет 1, т.е.

лидер будет выбран. Свойство на этой модели выполняется.3. Проверим, что номер выбранного лидера всегда будет максимальным (т.е. в даннойпрограмме равным количеству процессов).Это свойство легче всего проверить с помощью добавления оператора assert(nr == N) втом месте кода, где считается, что лидер найден (см. строчку 29 в коде), nr – номерпроцесса, которого мы начинаем считать лидером, а N – число процессов в модели. Врассматриваемой модели свойство выполняется.Немного модифицируем модель так, чтобы не все процессы участвовали в выборе. Введемглобальные переменные: election_started = 0 и first_message = 1. Если раньше унас каждый процесс в начале работы был активен и отправлял свой идентификатор в канал,то теперь все процессы в начале неактивны Active = 0 и ничего не отправляют в канал41(уберем 18-ую строчку).