proctype A(chan inn, out)
{	byte mt; /* message data */
 	bit  vr;
 S1:	mt = (mt+1)%MAX;
 	out!mt,1;
 	goto S2;
 S2:	inn?vr;
 	if
 	:: (vr == 1) -> goto S1
 	:: (vr == 0) -> goto S3
 	:: printf("MSC: AERROR1\n") -> goto S5
 	fi;
 S3:	out!mt,1;
 	goto S2;
 S4:	inn?vr;
 	if
 	:: goto S1
 	:: printf("MSC: AERROR2\n"); goto S5
 	fi;
 S5:	out!mt,0;
  	goto S4
  }
  proctype B(chan inn, out)
  {	byte mr, lmr;
  	bit ar;
  	goto S2; /* initial state */
  S1:	assert(mr == (lmr+1)%MAX);
  	lmr = mr;
  	out!1;
  	goto S2;
  S2:	inn?mr,ar;
  	if
  	:: (ar == 1) -> goto S1
  	:: (ar == 0) -> goto S3
  	:: printf("MSC: ERROR1\n"); goto S5
  	fi;
  S3:	out!1;
  	goto S2;
  S4:	inn?mr,ar;
  	if
  	:: goto S1
  	:: printf("MSC: ERROR2\n"); goto S5
  	fi;
  S5:	out!0;
  	goto S4
  }
  init {
  	chan a2b = [2] of { bit };
  	chan b2a = [2] of { byte, bit };
  	atomic {
  		run A(a2b, b2a);
  		run B(b2a, a2b)
  	}
  }