[model-checking] Комментарии ко второму заданию

Дорогие студенты,

Несколько комментариев ко второму заданию.

1. Я совершенно забыл написать, из чего складываются баллы за него: * LTS отдельных процессов - 10 * программа, строящая LTS - 25 * абстрактная LTS (состояние - значение h) - 20 * модель на promela - 25 * обоснование разницы в количестве состояний - 20 ИТОГО: 100 баллов

2. О том, как понять, какое пространство состояний строит SPIN и чем оно отличается от пространства состояний, которое строит ваша программа было рассказано на последней лекции (см. слайды про ключи SPIN)

3. При построении LTS для состояния, включающего только значение h, размечать состояния счетчиком операторов не нужно.

Ну и давайте продлим сроки сдачи до 28 марта.

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