Господа,
Необходимо взять программу из первой задачи, построить её модель на
языке Promela и, запустив верификацию в среде SPIN, получить точное
значение числа состояний этой модели для значений входных параметров
(f.a=1,f.b=2,f.c=3,f.d=4).
Обоснуйте, почему количество состояний, подсчитанное при помощи
системы Spin, отличается от полученного вручную при выполнении первого
задания.
Результаты -- текстовой файл (src.txt) с исходной программой,
текстовой файл с расширением task2.pml с моделью, текстовой файл log.txt
с тем, что выдал верификатор при запуске модели, текстовой файл
states.txt с 1)
фразой «Согласно верификатору, у модели – N достижимых состояний», где N
-- число состояний, выданных верификатором, 2) фразой «При выполнении
первого задания количество достижимых состояний было оценено как M», где
М – число, данное в решении первой задачи и 3) обоснованием отличия N от M.
О том, как среди вывода верификатора распознать число состояний
модели, можно прочитать в руководстве к системе Spin.
Последний срок сдачи задания -- 13 апреля.
С уважением,
Константин Савенков.
