A forum for Spin users
You are not logged in.
Pages: 1
what I meant is similar to this chunck of code, I found this clarification very useful, the problem sorted out.
THANK YOU
Does Promela allow ' if ' and ' else ' to be executable at the same time??
Basically I have two processes say LH process and RH process. The LH process writes a msg on channel CH1 and the RH process reads it to make a decision about the received msg . ' if ' / ' else ' clause used to check the received msg and send the decision back to LH process on another channel CH2 , in my model I found both statements in ' if ' and ' else ' are executable at the same time !!!.
Any help to resolve this will be much appreciated - Thanks
it is working fine now, thanks
ispin does not run the Dot tool after updating line 21 in ispin.tcl file on a PC machine. The original line changed by set DOT "C:/Program\ \ Files/Graphviz/bin/dot.exe" which is the default installation on my machine and it shows this error message "ispin: cannot find C:/Program Files/Graphviz/dot.exe"
Pages: 1