Я хотел бы распечатать все состояния при проверке моей модели. Мы получаем файл следа, когда происходит нарушение утверждения, но я хочу видеть состояния, даже если нарушения утверждения отсутствуют. Как я могу это сделать?
Как распечатать все состояния в Promela/SPIN
comment
Какова мотивация для этого? Чтобы подтвердить, что модель «попадает» в определенные точки?
- person GoZoner schedule 03.07.2014
Ответы (1)
Один из вариантов — скомпилировать pan с gcc флагом -DVERBOSE и просмотреть все подробности проверки. Конечно, запуск займет некоторое время и будет выдавать избыточный вывод, но вы будете видеть все состояния по мере их посещения (формат не очень удобен для чтения, но может быть достаточным для ваших целей).
Другой вариант просмотра графов состояний отдельных процессов —
./pan -D | dot -Tps | ps2pdf - pan.pdf
Это создаст многостраничный PDF-файл, где каждая страница представляет собой процесс (включая претензию never).
person
Ioannis Filippidis
schedule
08.07.2014
Вторая часть ответа (график для каждого процесса), вероятно, не то, что хотел ОП.
- person d8d0d65b3f7cf42; 05.11.2015
