// Modest PTA model of the bounded retransmission protocol (BRP)
// [HH09], http://www.modestchecker.net/CaseStudies/BRP/
action put, get, put_k, get_k, put_l, get_l;
action new_file;
action s_ok, s_dk, s_nok, s_restart;
action r_ok, r_inc, r_fst, r_nok, r_timeout;
exception error;

const int N = 16; // number of frames per file
const int MAX = 2; // maximum number of retransmissions per frame
const int TD = 1; // transmission delay
const int TS = 2 * TD + 1; // sender timeout
const int TR = 2 * MAX * TS + 3 * TD; // receiver timeout
const int SYNC = TR;

bool ff, lf, ab; // channel data: first/last frame, alternating bit
int(0..N) i; // sender chunk counter
bool inTransitK = false;
bool inTransitL = false;

bool first_file_done = false;
bool get_k_seen, s_ok_seen, s_nok_seen, s_dk_seen, s_restart_seen, r_ok_seen, r_timeout_seen;

// Invariant (timed) properties (from [BrpOnTime], the TA model)
bool premature_timeout, channel_k_overflow, channel_l_overflow;
// "there is at most one message in transit for each channel"
property T_1 = A[] (!(channel_k_overflow || channel_l_overflow));
// "there is at most one message in transit in total"
property T_2 = A[] (!(inTransitK && inTransitL));
// Assumption (A1): "no premature timeouts"
property T_A1 = A[] (!premature_timeout);
// Assumption (A2): "sender starts new file only after receiver reacted to failure"
// Note that receiver can only notice failure if it received at least one chunk, i.e. get_k_seen
property T_A2 = A[] (!s_restart_seen || !get_k_seen || r_timeout_seen);

// Probabilistic reachability properties (from [D'AJJL01], the RAPTURE/PRISM model)
// property A of [D'AJJL01]: "the maximum probability that eventually the sender reports 
// a certain unsuccessful transmission but the receiver got the complete file"
property P_A = Pmax(<>(s_nok_seen && r_ok_seen));
// property B of [D'AJJL01]: "the maximum probability that eventually the sender reports
// a certain successful transmission but the receiver did not get the complete file"
property P_B = Pmax(<>(s_ok_seen && !r_ok_seen));
// property 1 of [D'AJJL01]: "the maximum probability that eventually the sender
// does not report a successful transmission"
property P_1 = Pmax(<>(s_nok_seen || s_dk_seen));
// property 2 of [D'AJJL01]: "the maximum probability that eventually the sender
// reports an uncertainty on the success of the transmission"
property P_2 = Pmax(<>(s_dk_seen));
// property 3 of [D'AJJL01]: "the maximum probability that eventually the sender
// reports an unsuccessful transmission after more than 8 chunks have been sent successfully"
property P_3 = Pmax(<>(s_nok_seen && i > 8));
// property 4 of [D'AJJL01]: "the maximum probability that eventually the receiver
// does not receive any chunk and the sender tried to send a chunk"
property P_4 = Pmax(<>((s_ok_seen || s_nok_seen || s_dk_seen) && !get_k_seen));


process Sender()
{
	bool bit;
	int(0..MAX) rc;
	clock c;

	try
	{
		do {
		::	when urgent(i < N) {= i++ =};
			do
			{
				// send frame
				invariant(c <= 0) put_k {= ff = (i == 1), lf = (i == N), ab = bit, c = 0 =};
				invariant(c <= TS) alt {
				::	// receive ack
					get_l {= bit = !bit, rc = 0, c = 0 =};
					urgent break
				:: // timeout
					when(c >= TS)
					if(rc < MAX)
					{
						// retry
						{= rc++, c = 0 =}
					}
					else if(i < N)
					{
						// no retries left
						s_nok {= rc = 0, c = 0 =};
						urgent throw(error)
					}
					else
					{
						// no retries left
						s_dk {= rc = 0, c = 0 =};
						urgent throw(error)
					}
				}
			}
		::	when(i == N)
			// file transmission successfully completed
			invariant(c <= 0) s_ok {= first_file_done = true =};
			urgent break
		}
	}
	catch error
	{
		// File transfer did not succeed: wait, then restart with next file
		invariant(c <= SYNC) when(c >= SYNC)
		s_restart {= bit = false, first_file_done = true =}
	}
}

process Receiver()
{
	bool r_ff, r_lf, r_ab;
	bool bit;
	clock c;

	// receive first frame
	if(ff) { get_k {= c = 0, bit = ab, r_ff = ff, r_lf = lf, r_ab = ab =} }
	else { get_k {= c = 0, premature_timeout = true =}; stop };
	do
	{
		invariant(c <= 0)
		{
			if(r_ab != bit)
			{
				// repetition, re-ack
				put_l
			}
			else
			{
				// report frame
				if(r_lf)      { r_ok }
				else if(r_ff) { r_fst }
				else          { r_inc };
				put_l {= bit = !bit =}
			}
		};
		invariant(c <= TR)
		{
			alt {
			::	// receive next frame
				get_k {= c = 0, r_ff = ff, r_lf = lf, r_ab = ab =}
			::	// timeout
				when(c == TR)
				if(r_lf)
				{
					// we just got the last frame, though
					r_timeout; break
				}
				else
				{
					r_nok;
					// abort transfer
					r_timeout; break
				}
			}
		}
	};
	Receiver()
}

process ChannelK()
{
	clock c;

	put_k palt
	{
		:98:	{= c = 0, inTransitK = true =};
				invariant(c <= TD) alt {
				::	get_k {= inTransitK = false =}
				::	put_k {= channel_k_overflow = true =}; stop
				}
		: 2:	{==}
	};
	ChannelK()
}

process ChannelL()
{
	clock c;

	put_l palt
	{
		:99:	{= c = 0, inTransitL = true =};
				invariant(c <= TD) alt {
				::	get_l {= inTransitL = false =}
				::	put_l {= channel_l_overflow = true =}; stop
				}
		: 1:	{==}
	};
	ChannelL()
}

process Observer()
{
	alt {
	::	get_k     {= get_k_seen     = true =}
	::	s_ok      {= s_ok_seen      = true =}
	::	s_nok     {= s_nok_seen     = true =}
	::	s_dk      {= s_dk_seen      = true =}
	::	s_restart {= s_restart_seen = true =}
	::	r_ok      {= r_ok_seen      = true =}
	::	r_timeout {= r_timeout_seen = true =}
	};
	Observer()
}

par {
::	Sender()
::	Receiver()
::	ChannelK()
::	ChannelL()
::	Observer()
}