О положительном результате свидетельствует текст errors: 0.
Даже для этого небольшого протокола с 5 процессами (плюс
соединяющие их каналы) множество состояний уже довольно велико.
Поэтому SPIN предоставляет определенные механизмы для того,
чтобы сделать множество состояний меньше. Это осуществляется или
за счет хранения их компактным способом (используя редукцию
частичных порядков), или путем применения хеширования (которое
избегает просмотра всего множества состояний), или комбинацией
этих способов.
Эффект применения редукции частичных порядков к рассмотренному
примеру состоит в том, что сохраняются только 3189 состояний и
5014 переходов вместо 16585 состояний и 61172 переходов, по
сравнению со случаем, когда редукция частичных порядков не
применялась.
Таким же путем могут быть верифицированы следующие свойства:
лидер всегда в конечном счете будет выбран; выбранным лидером
будет процесс с наибольшим идентификатором; если процесс выбран
лидером, то он останется лидером навсегда.
Покажем, что происходит, когда проверяется неверное свойство:
проверим G[#leaders = 1]. Оно нарушается в состоянии, когда все
экземпляры процессов создаются, так как среди них нет лидера. Если
запустить верификатор SPIN, то получим ошибку, и сгенерируется
контрпример, который сохранится в файл. Для анализа ошибки может
быть запущена управляемая симуляция, базирующаяся на
построенном контрпримере. Кратчайшая трасса, которая ведет к
ошибке, может быть сгенерирована по запросу.
Верификация с использованием утверждений
Альтернативным, а часто и более эффективным путем верификации,
являются так называемые утверждения (assertions). Утверждение –
это конструкция, аргументом которой является булево выражение.
Его исполнение не имеет побочных эффектов. Если спецификация на
языке PROMELA содержит утверждение, то SPIN проверяет, есть ли
вычисление, при котором утверждение нарушается. В этом случае
отображается ошибка.
Рассмотрим пример использования утверждений. Предположим, что
требуется проверить, действительно ли число лидеров всегда не
превышает одного. Это может быть проверено путем добавления
утверждения
assert(nr_leaders <= 1)
непосредственно в код спецификации PROMELA в момент, когда
процесс определяет, что он выиграл выборы и увеличивает