Задачи на формальную спецификацию

section { 
type PROC = enum(0, 1); 
PROC turn = 0; 
type FLAGS = array(PROC, bool); 
FLAGS flag = {false, false}; 
} 
Два процесса, с номерами 0 и 1, одновременно пытаются попасть в 
критическую секцию, представленную ниже управляющим состоянием cs. 
Переменная turn определяет номер процесса, которому предоставляется 
возможность войти в критическую секцию. Доступ также регулируется 
флагами для каждого процесса: массив flag. Вначале доступ по флагу 
закрыт. Процесс, желающий попасть в критическую секцию, вначале 
присваивает свой флаг в истину. Однако очередь предоставляет другому 
процессу. Полная программа представлена ниже. 
M1 
S 
R 
a 
b 
c 
d 
r 
M2 
u 
s 

---

6 
process Peterson(PROC a) { 
pp: PROC b = (a + 1) mod 2; 
p0: flag[a] = true; 
p1: turn = b;
p2: if (flag[b]) #p3 else #cs; 
p3: if (turn = b) #p2 else #cs; 
cs: skip; 
p4: flag[a] = false; #p0 
} 
process main  {Peterson(0) || Peterson(1)} 
При кодировании в Event-B применяется switch-технология. Вводится тип: 
type State = enum(pp, p0, p1, p2, p3, cs, p4); 
Для событий, кодирующих сегменты кода, предлагается использовать 
параметр a. 
Необходимо доказать, что в критической секции в любой момент 
времени может находиться не более одного процесса. 
-Задача 14 
Стая дронов ищет пропавшую в лесу девочку. Обследуется 
односвязный участок леса. Территория леса снабжена квадратной сеткой, 
разделяющей местность на квадраты небольшого одинакового размера. 
Территорию леса определим в виде набора горизонтальных рядов 
квадратов: для каждого горизонтального ряда, имеющего свой номер 
внутри некоторого отрезка вертикальной оси координат, задаются номера 
начального и конечного квадрата в ряду. 
Внутри каждого квадрата допускается не более одного дрона. Дрон 
может двигаться по вертикали или горизонтали на соседние квадраты.
В начальный момент все дроны находятся на горизонтальной оси 
ниже обследуемого участка леса. Дроны размещаются по горизонтальным 
рядам не более одного дрона на ряд. Находясь внутри ряда, дрон 
последовательно обследует каждый квадрат, проводя съемку местности 
квадрата. При обнаружении объекта, похожего на девочку, дрон посылает в 
штаб МЧС координаты квадрата и результаты съемки. Каждый дрон, когда 
он оказывается вне обследуемого участка леса, движется к одному из 
концов свободного необследованного горизонтального ряда. 
Дроны завершают работу после обследования всей территории 
участка леса, либо по сигналу от МЧС. 
Построить модель процесса поиска девочки в лесу в виде автоматной 
программы с реализацией в Event-B. Необходимо избежать столкновения 
дронов и обеспечить полноту обследования территории леса. 

---

7 
-Задача 15 
Имеются следующая модификация предыдущей задачи поиска 
пропавшей девочки стаей дронов. Перемещение дронов с одного квадрата 
на другой реализуется синхронно, то есть одновременно. Действует то же 
самое ограничение: в одном квадрате не могут находиться два дрона. Тем 
не менее, дрон может зайти в квадрат, занимаемый другим, но при условии, 
что другой дрон выйдет с него на том же такте. На каждом такте все дроны 
обязаны двигаться. Исключение составляет случай, когда поступательное 
движение к цели оказывается заблокированным – такому дрону разрешено 
остаться на месте. 
Задача 16 
Стая дронов определяет границу пожара в лесу. Обследуется 
односвязный участок леса. Территория леса снабжена квадратной сеткой,