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

разделяющей местность на квадраты небольшого одинакового размера. 
Территорию леса определим в виде набора горизонтальных рядов 
квадратов: для каждого горизонтального ряда, имеющего свой номер 
внутри некоторого отрезка вертикальной оси координат, задаются номера 
начального и конечного квадрата в ряду. 
В штаб МЧС сообщаются координаты квадратов, определяющих 
границу пожара. 
Внутри каждого квадрата допускается не более одного дрона. Дрон 
может двигаться по вертикали или горизонтали на соседние квадраты.
В начальный момент все дроны находятся по вертикальной оси ниже 
обследуемого участка леса. Каждый дрон последовательно обследует по три 
ряда, на которых не должно быть других дронов. Находясь в тройке рядов 
внутри обследуемого участка леса, дрон последовательно просматривает 
соседние квадраты внутри тройки рядов на наличие в них пожара. 
Обнаружив пожар при прохождении участка без пожара, дрон сообщает 
координаты граничных квадратов в МЧС. Далее дрон зависает на границе 
пожара, взводит таймер и по кругу обследует шестерку квадратов на 
предмет появления или исчезновения в них пожара, и если граница пожара 
сместилась, передает изменения в МЧС. По истечению времени по таймеру 
дрон продолжает движение по трем рядам, проходя через зону сплошного 
огня. При выходе на границу огня, сообщает об этом в МЧС, зависая на 
этом месте для определения изменения границы огня, взводит таймер. 
Далее дрон продолжает движение по тройке рядов. 
Выйдя на границу обследуемого участка леса, дрон ищет тройку 
необследованных рядов и приступает к их сканированию. Дроны завершают 
работу после обследования всей территории участка леса. 
Построить модель процесса определения границы пожара в лесу в 
виде автоматной программы с реализацией в Event-B. Необходимо избежать 
столкновения дронов при переходе дрона к началу тройки рядов и 
обеспечить полноту обследования территории леса. 

---

8 
Задача 17 
Имеются следующая модификация предыдущей задачи определения 
границы пожара в лесу стаей дронов. Дрон, находящийся в тройке рядов 
внутри обследуемого участка, способен видеть также восемь соседних 
квадратов по вертикали, горизонтали и диагонали. Такому дрону нет 
необходимости проводить круговой облет соседних квадратов. При 
обнаружении границы пожара, дрон взводит таймер и зависает на одном 
месте.
Все дроны, вышедшие за границы обследуемого участка леса и 
движущиеся к новой тройке рядов, перемещаются с одного квадрата на 
другой синхронно, то есть одновременно. Действует то же самое 
ограничение: в одном квадрате не могут находиться два дрона. Тем не 
менее, дрон может зайти в квадрат, занимаемый другим, но при условии, 
что другой дрон выйдет с него на том же такте. На каждом такте все дроны 
вне обследуемого участка леса обязаны двигаться. Исключение составляет 
случай, когда поступательное движение к цели оказывается 
заблокированным – такому дрону разрешено остаться на месте. 
-Задача 18 
Построить модель Протокола Вопрос-ответ. В протоколе два узла: 
спрашивающий и отвечающий. Спрашивающий последовательно 
генерирует вопросы и посылает их отвечающему по надежному каналу 
связи. На каждый поступающий вопрос отвечающий формирует ответ и 
пересылает его спрашивающему по другому надежному каналу.
Каждый вопрос снабжается номером. Нумерация вопросов с единицы. 
Каждый следующий вопрос имеет номер, на единицу больший, чем номер 
предыдущего вопроса. Каждый ответ на вопрос снабжается тем же 
номером, что и вопрос. 
Необходимо построить автоматную программу протокола и 
переписать ее в виде спецификации Event-B. Канал в Event-B реализуется в 
виде очереди. Доказать что номера полученных ответов являются 
начальным отрезком набора номеров посланных вопросов. 
Структура данных – очередь реализуется либо через функцию, либо 
через импорт стандартной теории Queue.

---

9 
-Задача 19 
Построить модель Системы бронирования времени в теннисном клубе 
на трех теннисных кортах. Два корта грунтовые. Третий корт имеет 
покрытие хард. Игрок – член теннисного клуба может забронировать любое 
свободное время в пределах текущей недели для игры в теннис на одном из 
кортов. 
Время на каждом корте квантуется по полчаса, начиная с 8-00 утра до 
22-00 вечера. Член теннисного клуба может забронировать только один 
отрезок времени, содержащий от одного до трех смежных квантов. По 
истечении забронированного времени он может забронировать другой 
участок свободного времени до конца текущей недели. Он может также 
отказаться от забронированного участка времени, и тогда имеет 
возможность заказать для игры другое время и на другом корте. 
Указанные ограничения не распространяются на администратора 
теннисного клуба. Он может в любое время бронировать несколько разных 
свободных участков произвольной длины на разных кортах для турнира, 
ремонта, аренды, игры или группового времени. По завершении недели 
администратор создает новое расписание на следующую неделю, которое 
становится доступным членам клуба в понедельник. 
Во время дождя и определенное время после него корты непригодны 
для игры. После слабого дождя грунтовые корты сохнут 4 часа, после 
сильного дождя – 20 часов. Хард высыхает через два часа после слабого 
дождя и через 6 часов после сильного дождя. Необходимо учитывать, что 
дождь возможен в любое время, в том числе ночью. 
Бронирование времени реализуется в рамках сессии члена клуба с 
Системой бронирования. Член клуба сообщает Системе корт, день и 
отрезок времени для игры. Система проверяет, что указанный отрезок 
времени не занят другими, и либо подтверждает бронирование, либо 
отказывает в бронировании с указанием причины (один из квантов занят, 
дождь или его последствия, повторное бронирование). В случае 
бронирования Система корректирует расписание на кортах. 
Необходимо построить автоматную программу Системы 
бронирования и переписать ее в виде спецификации Event-B. Доказать, что 
все указанные ограничения реализуются в данной Системе. 
-Задача 20 
Беспилотному вездеходу требуется доставить груз из точки А в точку 
Б при наличии на местности крутых гор, недоступных для вездехода. 
Доступность определяется предикатом R. Точка (x, y) является доступной, 
если предикат R(x, y) истинен. Вездеход снабжен лазерным фонарем 
сверхвысокой дальности. Лазерный фонарь может быть направлен в любом 
направлении, показывая ближайшую точку, недоступную по этому 
направлению для прохождения вездеходом. Лазерный фонарь, 
направленный на точку Б, указывает на эту точку при отсутствии 
препятствий. Требуется построить автоматную программу движения 
вездехода для успешной доставки груза в точку Б. Далее программа должна 
быть переписана в виде спецификации на Event-B. Доказывается 
корректность действий вездехода. Из стандартной библиотеки необходимо 
загрузить теорию типа real. 

---

1
0 
-Задача 21 
Имеются следующая модификация предыдущей задачи доставки груза 
беспилотным вездеходом. Местность представлена сеткой целочисленных 
координат. Движение реализуется по целочисленным координатам. 
Допустимо движение в любом направлении при условии, что сумма 
изменений по двум координатам не должна превышать 10. 
-Задача 22 
В сложной гористой местности при наличии множества обширных 
сквозных пещер квадрокоптеру требуется доставить груз из точки А в точку 
Б. Квадрокоптер обладает панорамным зрением в пределах некоторого угла 
в направлении своего движения. Квадрокоптер перемещается шагами. В 
конце каждого шага квадрокоптер останавливается, зависая в одной точке, 
сканирует ближайшую местность и получает семь разных показаний вида 
(r, θ, φ), где r – расстояние до ближайшей преграды в направлении: θ – 
зенитный угол и φ – азимутальный угол в сферической системе координат 
(см. https://ru.wikipedia.org/wiki/
Сферическая_система_координат). Если в 
некотором показании преграда отсутствует, то r = maxR – предельно 
большое число. Далее, на основе семи показаний квадрокоптер изменяет 
направление своего движения и определяет новую целевую точку для 
следующего шага. Требуется построить автоматную программу движения 
квадрокоптера для успешной доставки груза в точку Б. Далее программа 
должна быть переписана в виде спецификации на Event-B. Доказывается 
корректность действий квадрокоптера. Из стандартной библиотеки 
необходимо загрузить теорию типа real. 
Задача 23 
Имеются следующая модификация предыдущей задачи доставки груза 
квадрокоптером. Местность представлена сеткой целочисленных 
координат. Движение реализуется по целочисленным координатам. Каждое 
из семи показаний при сканировании местности квадрокоптером имеет вид 
(x, y, z), где x, y и z – целочисленные координаты ближайшего 
препятствия. Если преграда отсутствует, то все координаты равны maxR – 
предельно большому числу. 
-Задача 24 
Имеются следующие дополнения в задаче управления движением на 
перекрестке. Имеется постоянно включенный таймер, увеличивающий свое 
показание на единицу через каждую секунду. 20 сек. – время для 
пересечения магистрали пешеходами. 60 сек. – время переключения 
светофора от зеленого к красному для автомобилей. В начале пешеходного 
перехода есть кнопка, которую может нажать пешеход, чтобы 
информировать о намерении перейти магистраль. Требуется построить 
контроллер управления светофорами с учетом показаний таймера и кнопки.