// Modest model of IEEE 802.11 Wireless LAN
action send, send1, send2;
action finish, finish1, finish2;
action success, success1, success2;
action bck, bck1, bck2;
action coll1, coll2;

const int BCMAX = 2;

// Parameters for the physical layer
const int ASLOT = 1;
const int DIFS = 3; // due to scaling can be non-deterministically either 2 or 3
const int VULN = 1; // due to scaling can be non-deterministically either 0 or 1
const int TTMAX = 315; // scaling up // 25 for deadlines & expected
const int TTMIN = 4; // scaling down
const int ACK_TO = 6; 
const int ACK = 4; // due to scaling can be non-deterministically either 3 or 4
const int SIFS = 1; // due to scaling can be non-deterministically either 0 or 1

// packet status
// 0: nothing sent
// 1: sending correctly
// 2: sending garbled
int c1 limit [0..2]; // first station's packet
int c2 limit [0..2]; // second station's packet


// Properties
bool success1_seen, success2_seen, bck1_seen, bck2_seen;

// Probabilistic reachability
// Use TTMAX = 315 and uncomment lines 156, 202 and 203
const int K = 2;
// "with probability 1, eventually both stations have sent their packet correctly"
property P_1 = P(<> success1_seen && success2_seen) >= 1.0;
// "the maximum probability that either station's backoff counter reaches K"
property P_max = Pmax(<> bck1_seen || bck2_seen);

// Time-bounded probabilistic reachability
// Use TTMAX = 25 and comment out lines 156, 202 and 203
const int DEADLINE = 100;
// "the minimum probability of both stations correctly
//  delivering their packets within time DEADLINE"
property D_and = Pmin(<> success1_seen && success2_seen && time <= DEADLINE);
// "the minimum probability of either station correctly
//  delivering its packet within time DEADLINE"
property D_or = Pmin(<> (success1_seen || success2_seen) && time <= DEADLINE);
// "the minimum probability of station 1 correctly
//  delivering its packet within time DEADLINE"
property D_1 = Pmin(<> success1_seen && time <= DEADLINE);

// Expected reachability
// Use TTMAX = 25 and comment out lines 156, 202 and 203
// "the maximum expected time until both stations correctly deliver their packets"
property E_and = Xmax(time | success1_seen && success2_seen);
// "the maximum expected time until either station correctly delivers its packet"
property E_or = Xmax(time | success1_seen || success2_seen);
// "the maximum expected time until station 1 correctly delivers its packet"
property E_1 = Xmax(time | success1_seen);


process Channel()
{
	do {
		:: finish1 {= c1 = 0 =}
		:: finish2 {= c2 = 0 =}
		:: send1 {= c1 = min(c2 + 1, 2), c2 = min(c2 + c2, 2) =}
		:: send2 {= c1 = min(c1 + c1, 2), c2 = min(c1 + 1, 2) =}
	}
}

process Sender(int id limit [1..2])
{
	clock x;
	int status limit [0..2];
	int bc limit [0..BCMAX];
	int backoff limit [0..(int)pow(2, BCMAX + 4) - 1];
	
	process SENSE()
	{
		invariant(x <= DIFS)
		alt {
			:: when(x == DIFS || x == DIFS - 1) {= x = 0 =};
				VULN()
			:: when(c1 + c2 > 0) urgent(c1 + c2 > 0) {= x = 0 =};
				WAIT_FREE()
		}
	}
	
	process VULN()
	{
		invariant(x <= VULN)
		when(x == VULN || x == VULN - 1) send {= x = 0 =};
		TRANSMIT()
	}
	
	process TRANSMIT()
	{
		invariant(x <= TTMAX)
		alt {
			:: when(id == 1 && x >= TTMIN) finish {= x = 0, status = c1 =};
				TEST_CHAN()
			:: when(id == 2 && x >= TTMIN) finish {= x = 0, status = c2 =};
				TEST_CHAN()
		}
	}
	
	process TEST_CHAN()
	{
		urgent
		alt {
			:: when(c1 + c2 > 0) tau;
				WAIT_FREE()
			:: when(c1 + c2 == 0 && status == 2) tau;
				NO_ACK()
			:: when(c1 + c2 == 0 && status == 1) tau;
				SEND_ACK()
		}
	}
	
	process SEND_ACK()
	{
		invariant(x <= SIFS)
		when(x == SIFS || x == SIFS - 1) send {= x = 0 =};
		ACK()
	}
	
	process ACK()
	{
		invariant(x <= ACK)
		when(x == ACK || x == ACK - 1) finish {= x = 0 =};
		urgent success // DONE
	}
	
	process NO_ACK()
	{
		invariant(x <= ACK_TO)
		when(x == ACK_TO) {= x = 0 =};
		WAIT_DIFS()
	}
		
	process WAIT_FREE()
	{
		when(c1 + c2 == 0) urgent(c1 + c2 == 0) {= x = 0 =};
		WAIT_DIFS()
	}

	process WAIT_DIFS()
	{
		invariant(x <= DIFS)
		alt {
			:: when((x == DIFS || x == DIFS - 1))
			   {= backoff = DiscreteUniform(0, (int)pow(2, bc + 4) - 1),
			      bc = min(bc + 1, BCMAX), x = 0 =};
			   // The following line is only for the simple probabilistic reachability properties
			   urgent alt { :: when(bc == K) bck :: when(bc != K) tau };
			   BACKOFF()
			:: when(c1 + c2 > 0) urgent(c1 + c2 > 0) {= x = 0 =};
				WAIT_FREE()
		}
	}
	
	process BACKOFF()
	{
		invariant(x <= ASLOT)
		alt {
			:: when(x == ASLOT && backoff == 0) {= x = 0 =};
				VULN()
			:: when(x == ASLOT && backoff > 0) {= backoff = backoff - 1, x = 0 =};
				BACKOFF()
			:: when(c1 + c2 > 0) urgent(c1 + c2 > 0) {= x = 0 =};
				WAIT_FREEII()
		}
	}
	
	process WAIT_FREEII()
	{
		when(c1 + c2 == 0) urgent(c1 + c2 == 0) {= x = 0 =};
		WAIT_DIFSII()
	}
	
	process WAIT_DIFSII()
	{
		invariant(x <= DIFS)
		alt {
			:: when(x == DIFS || x == DIFS - 1) {= x = 0 =};
				BACKOFF()
			:: when(c1 + c2 > 0) urgent(c1 + c2 > 0) tau;
				WAIT_FREEII()
		}
	}
	
	SENSE()
}

process Observer()
{
	do {
		:: success1 {= success1_seen = true =}
		:: success2 {= success2_seen = true =}
		// The following two lines are only for the simple probabilistic reachability properties
		:: bck1 {= bck1_seen = true =}
		:: bck2 {= bck2_seen = true =}
	}
}


par {
	:: Channel()
	:: relabel {send, finish, success, bck}
		by {send1, finish1, success1, bck1} Sender(1)
	:: relabel {send, finish, success, bck}
		by {send2, finish2, success2, bck2} Sender(2)
	:: Observer()
}