Spinroot

eugen

Member

Registered: 2011-11-28

Posts: 16

ispin error while displaying automata

I have ispin 1.0.5 and spin 6.1.0. While trying to display the automaton for the receiver process of the following model I get the following error.

mtype = {msg0, msg1, ack0, ack1};

chan snd = [1] of {mtype};
chan rcv = [1] of {mtype};


active proctype lossy () {
  mtype drop;

  do
    :: snd?drop;
drop_snd:
       skip

    :: rcv?drop;
drop_rcv:
       skip
  od
}

active proctype sender () {
again:
  do
	:: snd!msg1; /* send message with bit=1 */
	   if
	     :: rcv?ack1 -> break/* receive acknowledge with bit=1 */
	     :: rcv?ack0 -> skip /* retransmission */
	     :: timeout -> skip /* retransmission */
	   fi
  od;
  do
    :: snd!msg0; /* send message with bit=0 */
       if
	 :: rcv?ack0 -> break/* receive acknowledge with bit=1 */
	 :: rcv?ack1 -> skip /* retransmission */
	 :: timeout -> skip /* retransmission */
       fi
  od;
  goto again
}

active proctype receiver () {
again:
  do /* expected bit is 1 */
    :: snd?msg1 -> /* receive msg1 from sender */
       rcv!ack1; /* acknowledge with ack1 */
       break /* alternate expected bit */
       
    :: snd?msg0 -> /* receive msg0 from sender */
       rcv!ack0; /* acknowledge with ack0 */
  od;
  
  do /* expected bit is 0 */
    :: snd?msg0 -> /* receive msg0 from sender */
       rcv!ack0; /* acknowledge with ack0 */
       break /* alternate expected bit */
       
    :: snd?msg1 -> /* receive msg1 from sender */
       rcv!ack1 /* acknowledge with ack1 */
  od;
  goto again
}

unexpected "," outside function argument list
in expression "50 * 1, height="
unexpected "," outside function argument list
in expression "50 * 1, height="
    (parsing expression "50 * 1, height=")
    invoked from within
"expr 50 * $mf"
    (procedure "find_field" line 10)
    invoked from within
"find_field "width="  $line"
    (procedure "display_graph" line 129)
    invoked from within
"display_graph p_receiver"
    (command bound to event)

spinroot

forum

Registered: 2010-11-18

Posts: 700

Website

Re: ispin error while displaying automata

I'll check it out