Извлечение программной документации для NuSMV

NuSMV - это один из современных верификаторов, поддерживающих символьную верификацию на основе BDD и SAT. При желании разобраться, как он устроен очень полезно иметь программную документацию. В этом проекте программная документация генерируется perl-скриптом без использования специализированных утилит. Для того, чтобы сгенерировать документацию, необходимо в корневом каталоге проекта выполнить:


helpers/extract_doc .


Генерируется документация в HTML наподобие Javadoc, содержащая объявления типов, функций, а также их краткое описание

Сборка SMV

SMV - первый верификатор, в котором был реализован алгоритм символьной верификации на основе бинарных решающих диаграмм. Проект не радует своим дружелюбием, так как готовые сборки для linux не запускаются, из исходников проект собирается, но для этого пришлось поразбираться с исходными кодами. Чтобы сэкономить время другим желающим заняться верификацией, ниже описаны шаги по сборке SMV.

Шаг первый: скачиваем и распаковываем
Необходимо скачать исходные коды smv по ссылке smv.r2.5.4.3.tar.gz и распаковать:
tar -xzf smv.r2.5.4.3.tar.gz

Шаг второй: изменяем makefile
К строке в файле makefile
DFLAGS = -DBETTERHASH -DSMV_SIGNALS -DOTHER_SIMP
необходимо добавить
-DYYMALLOC=malloc

Шаг третий: собираем проект
Запустить сборку
make

Далее можно запустить один из примеров:
./smv examples/counter.smv
На экран должно быть выведено сообщение вида
-- specification AG AF bit2.carry_out is true
-- specification AG (!bit2.carry_out) is false
-- as demonstrated by the following execution sequence
state 1.1:
bit0.carry_out = 0
bit0.value = 0
bit1.carry_out = 0
bit1.value = 0
bit2.carry_out = 0
bit2.value = 0
...