byte prod_n=0;

chan Sin =[0] of {int};
chan Sout =[0] of {int};
chan toK =[0] of {int};
chan fromK =[0] of {int};
chan toL =[0] of {int};
chan fromL =[0] of {int};
chan timeisout =[0] of {int};
chan Rout =[0] of {int};
chan shake =[0] of {int};
chan shakePC =[0] of {int};
bit error;

active proctype Producer() {
byte result=0;
byte n=0;

ready: if
:: prod_n = 1; goto start_send;
:: prod_n = 2; goto start_send;
:: prod_n = 3; goto start_send;
:: prod_n = 4; goto start_send;
:: prod_n = 5; goto start_send;
:: prod_n = 6; goto start_send;
:: prod_n = 7; goto start_send;
:: prod_n = 8; goto start_send;
:: prod_n = 9; goto start_send;
:: prod_n = 10; goto start_send;
:: prod_n = 11; goto start_send;
:: prod_n = 12; goto start_send;
:: prod_n = 13; goto start_send;
:: prod_n = 14; goto start_send;
:: prod_n = 15; goto start_send;
:: prod_n = 16; goto start_send;
:: prod_n = 17; goto start_send;
:: prod_n = 18; goto start_send;
:: prod_n = 19; goto start_send;
:: prod_n = 20; goto start_send;
fi;
start_send: if
:: Sin!prod_n; goto wait_result;
fi;
wait_result: if
:: Sout?result; goto check;
fi;
check: if
::  atomic {result==1;shakePC!0;}  goto ready;
:: result==2 || result==3; goto start_send;
fi;
}

active proctype Consumer() {
byte m=0;
byte n=0;

ready: if
::  atomic {Rout?m;n = n+1;}  goto get_msg;
fi;
get_msg: if
:: (m==4) || (m==5); goto ready;
::  atomic {m==2;n = 0;}  goto ready;
:: m==1; goto check;
fi;
check: if
::  atomic {n==prod_n;shakePC?0;}  goto ready;
:: n!=prod_n; goto st_error;
fi;
st_error: error=1; }

active proctype Sender() {
byte ab=0;
byte n=0;
byte e=0;
byte counter=0;

idle: if
::  atomic {Sin?n;e = 1;}  goto next_frame;
fi;
next_frame: if
:: counter = 0; goto send;
fi;
wait_ack: if
::  atomic {fromL?0;ab = 1-ab;}  goto success;
::  atomic {counter==30;timeisout?0;}  goto q_error;
::  atomic {counter<30;timeisout?0;counter = counter+1;}  goto send;
fi;
send: if
::  atomic {e==1 && e==n;toK!(4+2+ab);}  goto wait_ack;
::  atomic {e>1 && e==n;toK!(2+ab);}  goto wait_ack;
::  atomic {e==1 && e<n;toK!(4+ab);}  goto wait_ack;
::  atomic {e>1 && e<n;toK!ab;}  goto wait_ack;
fi;
success: if
::  atomic {e<n;e = e+1;}  goto next_frame;
::  atomic {e==n;Sout!1;}  goto ret;
fi;
q_error: if
::  atomic {e<n;Sout!2;}  goto ret;
::  atomic {e==n;Sout!3;}  goto ret;
fi;
ret: if
:: shake!0; goto idle;
fi;
}

active proctype Receiver() {
byte value=0;
byte exp_ab=0;

new_file: if
:: fromK?value; goto first_safe;
:: shake?0; goto new_file;
fi;
idle: if
:: fromK?value; goto frame_received;
:: (value&2)==2; goto ret;
:: Rout!2; goto ret;
fi;
frame_received: if
::  atomic {(value&1)==exp_ab && (value&2)==2;Rout!1;}  goto frame_reported;
::  atomic {((value&1)==exp_ab) && ((value&2)==0) && ((value&4)==0);Rout!5;}  goto frame_reported;
::  atomic {((value&1)==exp_ab) && ((value&2)==0) && ((value&4)==4);Rout!4;}  goto frame_reported;
::  atomic {exp_ab!=(value&1);toL!0;}  goto idle;
fi;
frame_reported: if
::  atomic {toL!0;exp_ab = 1-exp_ab;}  goto idle;
fi;
first_safe: if
:: exp_ab = (value&1); goto frame_received;
fi;
ret: if
:: shake?0; goto new_file;
fi;
}

active proctype K() {
byte value=0;

ready: if
:: toK?value; goto got_msg;
fi;
got_msg: if
:: timeisout!0; goto ready;
:: fromK!value; goto ready;
fi;
}

active proctype L() {
ready: if
:: toL?0; goto got_msg;
fi;
got_msg: if
:: fromL!0; goto ready;
:: timeisout!0; goto ready;
fi;
}

never
{
again:
  if
  :: true; goto again;
  :: error;
  fi;
}