// Modest model for the IEEE 802.3 CSMA/CD protocol
action send, send1, send2;
action end, end1, end2;
action busy, busy1, busy2;
action cd;

const int RED = 2; // reduction factor
const int PD = (int)(26 / RED); // signal propagation delay
const int TD = (int)(808 / RED); // packet transmission delay
const int ST = 2 * PD; // backoff time slot length
const int BCMAX = 1; // 1 or 2

// Properties
bool end1_seen, end2_seen;

// Probabilistic reachability
// "with probability 1, eventually both stations send their packet correctly"
property P_1 = P(<> end1_seen && end2_seen) >= 1.0;

// Probabilistic time-bounded reachability
// "the minimum/maximum probability of both stations
// correctly delivering their packets by the deadline D"
const int D = (int)(1800 / RED);
property D_max = Pmax(<> end1_seen && end2_seen && time <= D);
property D_min = Pmin(<> end1_seen && end2_seen && time <= D);

// Expected reachability
// "the minimum/maximum expected time until
//  both stations correctly deliver their packets"
property E_min = Xmin(time | end1_seen && end2_seen);
property E_max = Xmax(time | end1_seen && end2_seen);

process Medium()
{
	clock c;
	
	do {
		:: alt { :: send1 {= c=0 =} :: send2 {= c=0 =} };
			do {
				:: alt { :: end1 {= c=0 =} :: end2 {= c=0 =} }; // transfer finished
					urgent break
				:: when(c <= PD)
					alt { :: send1 {= c=0 =} :: send2 {= c=0 =} }; // collision
					invariant(c <= PD) cd {= c=0 =}; // collision detection
					urgent break
				:: when(c >= PD)
					alt { :: busy1 :: busy2 } // carrier is sensed busy
			}
	}
}

process Station()
{
	clock c;
	int bc limit [0..BCMAX];
	int backoff limit [0..(int)pow(2, BCMAX + 1) - 1];
	
	urgent send {= c=0 =};
	do {
		:: invariant(c <= TD) alt {
			:: when(c == TD) end {= c=0 =};
				urgent break
			:: cd {= c=0, bc=min(bc + 1, BCMAX) =};
				do {
					:: urgent {= backoff=DiscreteUniform(0, (int)pow(2, bc + 1) - 1) =};
						invariant(c <= backoff * ST) when(c == backoff * ST) alt {
							:: send {= c=0 =}; urgent break
							:: busy {= c=0, bc=min(bc + 1, BCMAX) =}
						}
				}
			}
	}
}

process Observer()
{
	do {
		:: end1 {= end1_seen = true =}
		:: end2 {= end2_seen = true =}
	}
}


par {
	:: Medium()
	:: relabel { send, end, busy } by { send1, end1, busy1 } Station()
	:: relabel { send, end, busy } by { send2, end2, busy2 } Station()
	:: Observer()
}