Я новичок в промеле. У меня есть программа, написанная на промеле:
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)
Кто-нибудь знает, как нарисовать систему переходов для этой программы?
Вы должны вычислить все возможные чередования вашей модели promela. В вашем случае есть два активных процесса, так что это все еще выполнимо; тем не менее, вы все еще получаете изображение с 20 узлами. Для вдохновения предлагаю применить инструмент spinspider:
spinspider -p2 -vsignal[0] -vsignal[1] yourProgram.pml
В результате получится следующее изображение: Система перехода.
spinspider является частью дистрибутива JSpin, который по-прежнему можно использовать, хотя JSpin в настоящее время устарел.
