6 - Практические приёмы абстракции. Свойства линейного времени. Спецификация и верификация свойств при помощи Spin (1161370), страница 3
Текст из файла (страница 3)
Выигрывает процессс максимальнымномером.2. Должен быть толькоодин победитель.3. Оператор отправкисообщения недостижим.out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr); assert(false)fi:: in?winner,nr -> assert(nr == N) ;if:: nr != mynumber:: else -> nr_leaders++; assert(nr_leaders == 1)fi;if:: know_winner:: else -> out!winner,nrfi;breakod312Циклыбездействия• Свойство:– Программа эффективноработает, покаувеличиваетсязначение переменнойmaximum.• Проверяем:> ./spin -a leader2.pml> gcc -DNP -o pan pan.c> ./pan -l...(циклов бездействия ненайдено)out!one(mynumber);do:: in?one(nr) ->if:: Active ->if:: nr != maximum ->out!two(nr);neighbourR = nr:: else ->know_winner = 1;out!winner,nr;fi:: else ->out!one(nr)fi:: in?two(nr) ->if:: Active ->if:: neighbourR > nr && neighbourR > maximum ->progress:maximum = neighbourR;out!one(neighbourR):: else ->Active = 0fi:: else ->out!two(nr)fi:: in?winner,nr;if:: nr != mynumber:: else -> nr_leaders++fi;if:: know_winner:: else -> out!winner,nrfi;breakodСпасибо за внимание!Вопросы?.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
