Господа (и дамы),

Ниже находится текст четвёртого, последнего задания. Перешлите его, пожалуйста, тем вашим коллегам, которые не удосужились подписаться на рассылку.

Срок высылки решённого задания -- 25 апреля.

Понедельник 28 апреля с 9 утра в аудитории 758 -- зачёт по практикуму для студентов групп кафедры АСВК. Те, кто не прислал какие-то задачи или недоволен полученной оценкой за практикум (она к этому моменту будет выставлена), сможет попытаться поправить эту ситуацию на зачёте. У студентов других групп такая попытка будет на экзамене.

На последней лекции будет консультация к экзамену. Список экзаменационных вопросов к этому моменту будет разослан.

На майских праздниках меня здесь не будет. С 12 по 25 мая я буду в командировке. Соответственно, если вы не получите свою оценку по практикуму на зачёте (это касается студентов АСВК), то к сессии вы допущены не будете, и помочь вам никто не сможет. Оценка за практикум идёт в диплом. Соответственно, думайте сами. Особенно это касается господ Ермакова, Салия, Волкова, Крупа, Попова, Семёнова, Баранова, Любицкого, Петрова и госпожи Полежаевой.

Экзамен будет после 25 мая. В экзаменационный день будет разбит на две части: приём экзамена у тех, у кого нет проблем по практикуму и у тех, у кого есть проблемы.

---- Легенда 4 задания --------

Для данной вам программы и её модели, построенной в ходе решения третьей задачи:

1. Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt. 2. В модели не должно быть недостижимого кода (unreachable code). 3. Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt 4. В модели не должно быть циклов бездействия (non-progress cycles), за исключением: 4.1) цикла, связанного с бесконечным выполнением моделируемой функции 4.2) циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml. 5. Сформулированное в третьей задаче свойство описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. Спецификацию приложить в файле с именем spec.ltl.

a. В случае, если модель пришлось изменить: * описать в теле письма, почему спецификация не выполняется на исходной модели; * описать в теле письма, как изменилась модель и почему; * описать в теле письма, почему новая модель адекватна; * приложить контрпример, выданный pan, в файле counterexample.txt; * приложить исходную и изменённую модели в файлах model.prm и new_model.prm; * приложить вывод pan в файле ver_out.txt.

b. В случае, если спецификация не выполняется на модели: * приложить контрпример, выданный pan, в файле counterexample.txt; * построить по контрпримеру Spin контрпример на исходной программе; * убедиться в том, что контрпример на исходной программе выполняется; * приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных. * приложить вывод pan в файле ver_out.txt.

c. В случае, если изменения в модели не потребовались и спецификация выполняется: * приложить модель в файле model.prm; * приложить вывод pan в файле ver_out.txt.

Во всех случаях письмо должно удовлетворять требованиям: * письмо написано в формате plain/text без html; * в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и utf8 (желательно в кодировке koi8-r). * к письму должна прилагаться формулировка третьей задачи с файле с именем task3.txt ------------------------------------