gistfile1.txt

/* alternating bit - version with message loss */

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

chan	sender  =[1] of { byte };
chan	receiver=[1] of { byte };

proctype Sender()
{	byte any;
again:
	do
	:: receiver!msg1;
   sent1:
		if
		:: sender?ack1 -> 
            progress1: break
		:: sender?any /* lost */
		:: timeout    /* retransmit */
		fi
	od;
	do
	:: receiver!msg0;
   sent2:
		if
		:: sender?ack0 -> 
            progress2: break
		:: sender?any /* lost */
		:: timeout    /* retransmit */
		fi
	od;
	goto again
}

proctype Receiver()
{	byte any;
again:
	do
	:: receiver?msg1 -> sender!ack1; 
                       progress3: break
	:: receiver?msg0 -> sender!ack0
	:: receiver?any /* lost */
	od;
P0:
	do
	:: receiver?msg0 -> sender!ack0; 
                       progress4: break
	:: receiver?msg1 -> sender!ack1
	:: receiver?any /* lost */
	od;
P1:
	goto again
}

init { atomic { run Sender(); run Receiver() } }

ltl l1 { always(Sender@sent1 implies eventually Receiver@progress3) }
ltl l2 { (!Receiver@progress3) W Sender@sent1}