Редактирование: ВПнМ, примеры задач/Задача 4
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
Текущая версия | Ваш текст | ||
Строка 507: | Строка 507: | ||
</pre> | </pre> | ||
- | == Дополнительные материалы для выполнения задания == | + | === Дополнительные материалы для выполнения задания === |
- | === Скрипт для генерации файлов, необходимых в задании, на основании моделей === | + | ==== Скрипт для генерации файлов, необходимых в задании, на основании моделей ==== |
Данный скрипт генерирует файлы assert_out.txt, ver_out.txt, nonprogress_out.txt, safety_out.txt, spec.ltl на основании моделей (model.prm, new_model.prm, model_assert.prm) и формулы (формула должна находиться в formulae.ltl или передаваться в качестве параметра). | Данный скрипт генерирует файлы assert_out.txt, ver_out.txt, nonprogress_out.txt, safety_out.txt, spec.ltl на основании моделей (model.prm, new_model.prm, model_assert.prm) и формулы (формула должна находиться в formulae.ltl или передаваться в качестве параметра). | ||
Строка 534: | Строка 534: | ||
./pan -a -A > ltl_check.txt</pre> | ./pan -a -A > ltl_check.txt</pre> | ||
- | === Скрипт для генерации дистрибутива === | + | ==== Скрипт для генерации дистрибутива ==== |
Данный скрипт помещает файлы, необходимые для отправки, в поддиректорию distr/. Если раскомментировать последнюю строку, то дополнительно будет создан архив, содержащий все эти файлы. | Данный скрипт помещает файлы, необходимые для отправки, в поддиректорию distr/. Если раскомментировать последнюю строку, то дополнительно будет создан архив, содержащий все эти файлы. | ||