Можно ли распечатать пространство состояний с помощью SPIN?

Я хотел бы, чтобы SPIN распечатывал вычисленное пространство состояний, чтобы я мог сделать его визуализацию, а затем вручную исследовать его. Это возможно?

Я уже проверил такие флаги, как -DCHECK и -DVERBOSE, но думаю, что это не то, что я ищу...


visualization state-space promela spin
person Dmitry Korolev    schedule 07.05.2013    source источник
comment
Если вы никогда не использовали его, похоже, что этот вариант Spin имеет встроенную поддержку видов визуализации, которые могут вас заинтересовать: code.google.com/p/erigone   -  person Gian    schedule 07.05.2013
comment
Я хочу сделать визуализацию сам по некоторым причинам, поэтому встроенные инструменты для меня не лучший вариант.   -  person Dmitry Korolev    schedule 07.05.2013
comment
Вы ищете все пространство состояний или только вектор состояния в конкретной точке выполнения? Вас интересуют состояния в векторе состояний, которые являются внутренними для SPIN, такие как управляющее состояние (например, программный счетчик) для каждого proctype или только глобальное и локальное состояние, которое вы определяете?   -  person GoZoner    schedule 10.05.2013
comment
@GoZoner Ищу все пространство состояний, содержащее только переменные из вектора состояния, т.е. без внутренних. На данный момент я использую метод, аналогичный тому, что реализован в SpinSpider.   -  person Dmitry Korolev    schedule 13.05.2013

Ответы (1)


arrow_upward
0
arrow_downward

Нет, в настоящее время нет графического вывода искомого пространства состояний в spin. График программы можно построить с помощью graphviz dot, как описано здесь.

person Ioannis Filippidis    schedule 16.09.2014