Господа,

Необходимо взять программу из первой задачи, построить её модель на языке 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 апреля.

С уважением, Константин Савенков.