[model-checking] Второе задание

Добрый день,

Детальная легенда на второе задание:

Необходимо взять программу, присланную вам в качестве первой задачи, построить её модель на языке Promela и, запустив верификацию в среде SPIN, получить точное значение числа состояний этой модели.

Результаты -- текстовой файл с исходной программой, текстовой файл с расширением .pml с моделью, текстовой файл log с тем, что выдал верификатор при запуске модели, а также фраза "согласно верификатору, у модели -- N достижимых состояний", где N -- число состояний, выданных верификатором.

О том, как среди вывода верификатора распознать число состояний модели, вы можете прочитать в руководстве к системе Spin.

Результаты необходимо прислать ПО ПОЧТЕ.

Срок сдачи задания -- до 14 марта включительно,