[model-checking] Подсказки по 2 заданию

Господа,

1. Естественно, сравнивать число состояний, полученных от спина, надо не с количеством достижимых состояний для программы с произвольными аргументами, а с количеством состояний в LTS для параллельной композиции процессов.

2. В ходе верификации спин применяет различные подходы к сжатию пространства состояний (редукцию частичных порядков, например). Это надо отключить -- вы же строили свои графы, не применяя этих методов.

3. Спин умеет выдавать таблицу состояний в текстовом виде. Однако это не таблица состояний для параллельной композиции! Это таблицы состояний для отдельных процессов. Тем не менее, вы можете использовать их, чтобы понять, откуда проистекает различие в числе состояний.

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