вторник, 22 декабря 2009 г.

Сборка верификатора dspin

Верификатор dspin был разработан на основе верификатора spin. Основная идея, положенная в основу верификатора, состояла в расширении языка Promela различными конструкциями, облегчающими построение моделей при верификации программ.

При сборке версии dspin-3.2.0+0.5 возникает предупреждение об ожидаемом конфликте сдвига/вывода. Причина этого предупреждения в том, что в коде грамматики spin.y объявлен конфликт, который на самом деле отсутствует. Для устранения нужно закомментировать конструкцию %expect 1.

Другая проблема стандартной сборки - не работает часть тестов. Эта проблема связана с тем, что в файлах тестов используется версия 3.2.0+0.4, которая не совпадает с фактической 3.2.0+0.5. Эту проблему можно легко решить с помощью sed.

В результате рассмотренных правок получен работающий дистрибутив dspin.