Как нарисовать систему перехода в promela?

Question

Я новичок в promela. У меня есть программирование, которое написано в promela:

bit signal [2]; 
active [2] proctype proc() { 
l1: signal[_pid]=1; 
l2: !signal[1-_pid] -> 
l3: signal[_pid]=0; 
} 
#define sig0 (signal[0]==0) 
#define sig1 (signal[0]==1) 

Кто-нибудь знает, как нарисовать систему перехода для этой программы?

Answer 1

Вы должны вычислить все возможные перемежения вашей модели promela. В вашем случае есть два активных процесса, поэтому это все равно выполнимо; однако вы все равно получаете изображение с 20 узлами. Для того, чтобы получить вдохновение, я бы предложил применить spinspider инструмент:

spinspider -p2 -vsignal[0] -vsignal[1] yourProgram.pml 

Результат является следующее изображение: Transition System

spinspider является частью JSpin distribution, который должен быть еще можно использовать, хотя JSpin является устаревшим Теперь.