Редактирование: ВПнМ, примеры задач/Задача 4
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 3: | Строка 3: | ||
# Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt. | # Проверить свойство отсутствия тупиков (invalid end-states). Тупиков в модели быть не должно. Вывод pan по проверке свойства приложить в файле с именем safety_out.txt. | ||
+ | |||
# В модели не должно быть недостижимого кода (unreachable code). | # В модели не должно быть недостижимого кода (unreachable code). | ||
+ | |||
# Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt | # Сформулированное в третьей задаче свойство описать в модели с помощью assertions, проверить с помощью Spin. Возможно потребуется ввести дополнительные переменные. Модель с assertions приложить в файле с именем model_assert.prm. Вывод pan по проверке приложить в файле с именем assert_out.txt | ||
+ | |||
# В модели не должно быть циклов бездействия (non-progress cycles), за исключением: | # В модели не должно быть циклов бездействия (non-progress cycles), за исключением: | ||
+ | |||
## цикла, связанного с бесконечным выполнением моделируемой функции | ## цикла, связанного с бесконечным выполнением моделируемой функции | ||
+ | |||
## циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml. | ## циклов, соответствующих циклам моделируемой функции, которые после абстракции предикатов стали бесконечными. Иными словами, конструкции, добавленные вами в модель (например, дназначенниые для моделирования случайных данных) не должны вносить в модель бесконечных циклов. Вывод верификатора для проверки отсутствия циклов бездействия приложить в файле с именем nonprogress_out.txt. Метки progress, предназначенные для того, чтобы верификатор не обращал внимания на бесконечные циклы, перечисленные в пунктах 3.1 и 3.2, должны быть расставлены в модели model_assert.pml. | ||
+ | |||
# Сформулированное в третьей задаче свойство описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. Спецификацию приложить в файле с именем spec.ltl. | # Сформулированное в третьей задаче свойство описать с помощью логики линейного времени в формате Spin, проверить с помощью Spin. Спецификацию приложить в файле с именем spec.ltl. | ||
+ | |||
+ | |||
a. В случае, если модель пришлось изменить: | a. В случае, если модель пришлось изменить: | ||
+ | |||
* описать в теле письма, почему спецификация не выполняется на исходной модели; | * описать в теле письма, почему спецификация не выполняется на исходной модели; | ||
+ | |||
* описать в теле письма, как изменилась модель и почему; | * описать в теле письма, как изменилась модель и почему; | ||
+ | |||
* описать в теле письма, почему новая модель адекватна; | * описать в теле письма, почему новая модель адекватна; | ||
+ | |||
* приложить контрпример, выданный pan, в файле counterexample.txt; | * приложить контрпример, выданный pan, в файле counterexample.txt; | ||
+ | |||
* приложить исходную и изменённую модели в файлах model.prm и new_model.prm; | * приложить исходную и изменённую модели в файлах model.prm и new_model.prm; | ||
+ | |||
* приложить вывод pan в файле ver_out.txt. | * приложить вывод pan в файле ver_out.txt. | ||
+ | |||
+ | |||
b. В случае, если спецификация не выполняется на модели: | b. В случае, если спецификация не выполняется на модели: | ||
+ | |||
* приложить контрпример, выданный pan, в файле counterexample.txt; | * приложить контрпример, выданный pan, в файле counterexample.txt; | ||
+ | |||
* построить по контрпримеру Spin контрпример на исходной программе; | * построить по контрпримеру Spin контрпример на исходной программе; | ||
+ | |||
* убедиться в том, что контрпример на исходной программе выполняется; | * убедиться в том, что контрпример на исходной программе выполняется; | ||
+ | |||
* приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных. | * приложить контрпример на исходной программе в файле prog_counterexample.txt. Контрпример должен быть описан в виде последовательности номеров строк исходной программы и значений переменных. | ||
+ | |||
* приложить вывод pan в файле ver_out.txt. | * приложить вывод pan в файле ver_out.txt. | ||
+ | |||
+ | |||
c. В случае, если изменения в модели не потребовались и спецификация выполняется: | c. В случае, если изменения в модели не потребовались и спецификация выполняется: | ||
+ | |||
* приложить модель в файле model.prm; | * приложить модель в файле model.prm; | ||
+ | |||
* приложить вывод pan в файле ver_out.txt. | * приложить вывод pan в файле ver_out.txt. | ||
+ | |||
+ | |||
Во всех случаях письмо должно удовлетворять требованиям: | Во всех случаях письмо должно удовлетворять требованиям: | ||
+ | |||
* письмо написано в формате plain/text без html; | * письмо написано в формате plain/text без html; | ||
+ | |||
* в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и utf8 (желательно в кодировке koi8-r). | * в письме допускаются только текстовые вложения в кодировках cp1251, koi8-r и utf8 (желательно в кодировке koi8-r). | ||
+ | |||
* к письму должна прилагаться формулировка третьей задачи с файле с именем task3.txt | * к письму должна прилагаться формулировка третьей задачи с файле с именем task3.txt | ||