// if parameter B is defined then the channel can loose at most B messages in a row

channel K_in, K_out, L_in, L_out;


default(Strategy, 0) // 0 = naive, 1 = abp, 2 = brp, 3 = simple

channel send, receive;

process channel_K {
byte v ifdef(`B',`, lost=0'); // msg_lost only for property
state ready,tr, data_lost;
init ready;
trans
 ready -> tr { sync K_in?v; },
 tr -> ready { ifdef(`B',`guard lost < B; effect lost = lost + 1;') }, //loose msg
 tr -> ready { sync K_out!v;  ifdef(`B',` effect lost = 0;') };
}

process channel_L {
byte v   ifdef(`B',`, lost=0'); // msg_lost only for property
state ready,tr, dataOK;
init ready;
trans
 ready -> tr { sync L_in?v; },
 tr -> ready { ifdef(`B',`guard lost < B; effect lost = lost + 1;') }, // loose msg
 tr -> ready { sync L_out!v;  ifdef(`B',`effect lost = 0;') };
}

process Producer {
state ready, produce0, produce1;
init ready;
trans
 ready -> produce0 {},
 ready -> produce1 {},
 produce0 -> ready { sync send!0; },
 produce1 -> ready { sync send!1; };
}

process Consumer {
byte value;
state ready, got_msg, consume0, consume1;
init ready;
trans
 ready -> got_msg  {sync receive?value; },
 got_msg -> consume0 { guard value==0; },
 got_msg -> consume1 { guard value==1; },
 consume0 -> ready {},
 consume1 -> ready {};
}

define(naive, `
process Sender {
byte value;
state ready, sending;
init ready;
trans
 ready -> sending { sync send?value; },
 sending -> ready { sync K_in!value;};
}

process Receiver {
byte value;
state wait_msg, got_msg;
init wait_msg;
trans
 wait_msg -> got_msg {sync K_out?value;},
 got_msg -> wait_msg {sync receive!value;};
}
')

define(abp, `
process Sender {
byte value, sab=0, ack;
state ready, sending, wait_ack;
init ready;
trans
 ready -> sending {sync send?value;},
 sending -> sending {sync K_in!value;},
 sending -> wait_ack {sync L_out?ack;},
 wait_ack -> sending { guard ack != sab;},
 wait_ack -> ready { guard ack == sab; effect sab = 1-sab;};
}

process Receiver {
byte value, ifdef(`ERROR', `rab=0', `rab=1');
state wait_msg, got_msg;
init wait_msg;
trans
 wait_msg -> wait_msg { sync L_in!rab;},
 wait_msg -> got_msg { sync K_out?value;},
 got_msg -> wait_msg { sync receive!value; effect rab=1-rab;};
}
')

define(brp,`
default(MAX,3)

process Sender {
byte value, sab, retry;
state ready, sending, wait_ack, failed;
init ready;
trans
 ready -> sending {sync send?value; effect sab = 1 -sab; },
 sending -> wait_ack {sync K_in!`(value*2+sab)'; effect retry = 1;},
 wait_ack -> wait_ack {guard retry < MAX; sync K_in!`(value*2+sab)'; effect retry = retry+1;},
 wait_ack -> ready {sync L_out?value; },
 wait_ack -> failed { guard retry == MAX;};
}

process Receiver {
byte value, rab=1;
state waiting, got_msg, send_ack;
init waiting;
trans
 waiting -> got_msg {sync K_out?value;},
 got_msg -> waiting {guard value % 2 != rab;},
 got_msg -> send_ack {guard value % 2 == rab; sync receive!`(value/2)';},
 send_ack -> waiting {sync L_in!0; effect rab= 1-rab;};
}
')

define(simple,`
process Sender {
byte value;
state ready, sending, wait_ack;
init ready;
trans
 ready -> sending { sync send?value; },
 sending -> wait_ack { sync K_in!value;},
 wait_ack -> sending {},
 wait_ack -> ready { sync L_out?value;};
}


process Receiver {
byte value;
state wait_msg, got_msg, send_ack;
init wait_msg;
trans
 wait_msg -> got_msg {sync K_out?value;},
 ifelse(V, `1', `got_msg -> send_ack {sync receive!value;},
 send_ack -> wait_msg {sync L_in!0;};',
 `wait_msg -> wait_msg {sync L_in!0; },
 got_msg -> wait_msg {sync receive!value;};')
 
}
')

ifelse(Strategy, 0, `naive', Strategy, 1, `abp', Strategy, 2, `brp', `simple')

system async;