// Modest MDP model of the bounded exponential backoff procedure (BEB)
// [BFHH11]
action tick, tack, tock;

const int K = 4; // maximum value for backoff
const int N = 3; // number of tries before giving up
const int H = 3; // number of hosts (must correspond to the number of Host() instantiations in the global composition)

int(0..2) cr; // count how many hosts attempt to seize the line in a slot (zero, one, many)
bool line_seized;
bool gave_up;

property LineSeized = Pmax(<> line_seized); // some host managed to seize the line before any other gave up
property GaveUp = Pmax(<> gave_up); // some host gave up before any other managed to seize the line (does not work with POR)

process Clock()
{
	tick; tack; tau {= cr = 0 =}; tock; Clock()
}

process Host()
{
	int(0..N) na;     // nr_attempts 0..N
	int(0..K) ev = 2; // exp_val 0..K
	int(0..K) wt;     // slots_to_wait 0..K

	do
	{
		if(wt > 0)
		{
			// wait this slot
			tick {= wt-- =}
		}
		else
		{
			tau {= cr = min(2, cr + 1) =}; // attempt to seize the line
			tick;
			if(cr == 1)
			{
				// someone managed to seize the line
				tau {= line_seized = true =}; stop
			}
			else if(na >= N)
			{
				// maximum number of attempts exceeded
				tau {= gave_up = true =}; stop
			}
			else
			{
				// backoff
				tau {= na++, wt = DiscreteUniform(0, max(0, ev - 1)), ev = min(2 * ev, K) =} 
			}
		};
		tack; tock
	}
}

par
{
::	Clock()
::	Host()
::	Host()
::	Host()
}