// WLAN PROTOCOL (two stations)
// discrete time model
// gxn/jzs 20/02/02

mdp

// TIMING CONSTRAINTS
// we have used the FHSS parameters
// then scaled by the value of ASLOTTIME
const int ASLOTTIME = 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 TRANS_TIME_MAX = 315; // scaling up
const int TRANS_TIME_MIN = 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
const int TIME_MAX = 315; // maximum constant used in timing constraints + 1
const int BOFF = 6; // max backoff (since contention window is [15,1023])

// THE MEDIUM/CHANNEL

formula busy = c1>0 | c2>0; // channel is busy
formula free = c1=0 & c2=0; // channel is free

module medium
	
	col : [0..8]; // number of collisions
	// medium status 
	c1 : [0..2];
	c2 : [0..2];
	// ci corresponds to messages associated with station i
	// 0 nothing being sent
	// 1 being sent correctly
	// 2 being sent garbled	  
	
	// begin sending message and nothing else currently being sent
	[send1] c1=0 & c2=0 -> (c1'=1);
	[send2] c2=0 & c1=0 -> (c2'=1);
	// begin sending message and  something is already being sent
	// in this case both messages become garbled
	[send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & col'=min(col+1,8);
	[send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & col'=min(col+1,8);
	// finish sending message
	[finish1] c1>0 -> (c1'=0);
	[finish2] c2>0 -> (c2'=0);
	
endmodule

// STATION 1
module station1
	// clock for station 1
	x1 : [0..TIME_MAX];
	
	// local state
	s1 : [1..12];
	// 1 sense
	// 2 wait until free before setting backoff
	// 3 wait for DIFS then set slot
	// 4 set backoff 
	// 5 backoff
	// 6 wait until free in backoff
	// 7 wait for DIFS then resume backoff
	// 8 vulnerable 
	// 9 transmit
	// 11 wait for SIFS and then ACK
	// 10 wait for ACT_TO 
	// 12 done
	// BACKOFF
	// separate into slots
	slot1 : [0..63]; 
	backoff1 : [0..15];
	
	// BACKOFF COUNTER
	bc1 : [0..BOFF];
	// SENSE
	// let time pass
	[time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
	// ready to transmit
	[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
	// found channel busy so wait until free
	[] s1=1 & busy -> (s1'=2) & (x1'=0);
	// WAIT UNTIL FREE BEFORE SETTING BACKOFF
	// let time pass (no need for the clock x1 to change)
	[time] s1=2 & busy -> (s1'=2);
	// find that channel is free so check its free for DIFS before setting backoff
	[] s1=2 & free -> (s1'=3);
	// WAIT FOR DIFS THEN SET BACKOFF
	// let time pass
	[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
	// found channel busy so wait until free
	[] s1=3 & busy -> (s1'=2) & (x1'=0);
	// start backoff  first uniformly choose slot
	// backoff counter 0
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 ->
		   (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF));
	// backoff counter 1
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 ->
		   1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF))
		+ 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,BOFF));
	// backoff counter 2
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 ->
		   1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF))
		+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,BOFF))
		+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,BOFF))
		+ 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,BOFF));
	// backoff counter 3
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 ->
		   1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,BOFF))
		+ 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,BOFF));
	// backoff counter 4
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 ->
		   1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,BOFF))
		+ 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,BOFF));
	// backoff counter 5
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=5 ->
		   1/32 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,BOFF))
		+ 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,BOFF));
	// backoff counter 6
	[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=6 ->
		   1/64 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=32) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=33) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=34) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=35) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=36) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=37) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=38) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=39) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=40) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=41) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=42) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=43) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=44) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=45) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=46) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=47) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=48) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=49) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=50) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=51) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=52) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=53) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=54) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=55) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=56) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=57) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=58) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=59) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=60) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=61) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=62) & (bc1'=min(bc1+1,BOFF))
		+ 1/64 : (s1'=4) & (x1'=0) & (slot1'=63) & (bc1'=min(bc1+1,BOFF));
	// SET BACKOFF (no time can pass)
	// chosen slot now set backoff
	[] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0)
		    + 1/16 : (s1'=5) & (backoff1'=1)
		    + 1/16 : (s1'=5) & (backoff1'=2)
		    + 1/16 : (s1'=5) & (backoff1'=3)
		    + 1/16 : (s1'=5) & (backoff1'=4)
		    + 1/16 : (s1'=5) & (backoff1'=5)
		    + 1/16 : (s1'=5) & (backoff1'=6)
		    + 1/16 : (s1'=5) & (backoff1'=7)
		    + 1/16 : (s1'=5) & (backoff1'=8)
		    + 1/16 : (s1'=5) & (backoff1'=9)
		    + 1/16 : (s1'=5) & (backoff1'=10)
		    + 1/16 : (s1'=5) & (backoff1'=11)
		    + 1/16 : (s1'=5) & (backoff1'=12)
		    + 1/16 : (s1'=5) & (backoff1'=13)
		    + 1/16 : (s1'=5) & (backoff1'=14)
		    + 1/16 : (s1'=5) & (backoff1'=15);
	// BACKOFF
	// let time pass
	[time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
	// decrement backoff
	[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);	
	[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 ->
			(s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);	
	// finish backoff 
	[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
	// found channel busy
	[] s1=5 & busy -> (s1'=6) & (x1'=0);
	// WAIT UNTIL FREE IN BACKOFF
	// let time pass (no need for the clock x1 to change)
	[time] s1=6 & busy -> (s1'=6);
	// find that channel is free
	[] s1=6 & free -> (s1'=7);
	
	// WAIT FOR DIFS THEN RESUME BACKOFF
	// let time pass
	[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
	// resume backoff (start again from previous backoff)
	[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
	// found channel busy
	[] s1=7 & busy -> (s1'=6) & (x1'=0);
	
	// VULNERABLE
	// let time pass
	[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
	// move to transmit
	[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
	// TRANSMIT
	// let time pass
	[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
	// finish transmission successful	
	[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
	// finish transmission garbled
	[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
	// WAIT FOR SIFS THEN WAIT FOR ACK
	
	// WAIT FOR SIFS i.e. c1=0
	// check channel and busy: go into backoff
	[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
	// chack channel and free: let time pass
	[time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
	// let time pass
	[time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX));
	// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
	[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
	
	// WAIT FOR ACK i.e. c1=1
	// let time pass
	[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
	// get acknowledgement so packet sent correctly and move to done
	[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
	
	// WAIT FOR ACK_TO
	// check channel and busy: go into backoff
	[] s1=11 & x1=0 & busy -> (s1'=2);
	// check channel and free: let time pass
	[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
	// let time pass
	[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
	// no acknowledgement (go to backoff waiting DIFS first)
	[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
		
	// DONE
	[time] s1=12 -> (s1'=12);
	
endmodule

// STATION 2 (rename STATION 1)
module station2=station1[x1=x2, 
                  s1=s2,
                  s2=s1,
                  c1=c2,
                  c2=c1, 
                  slot1=slot2, 
                  backoff1=backoff2, 
                  bc1=bc2, 
                  send1=send2, 
                  finish1=finish2] 
endmodule

// reward structure for expected number of collisions
rewards "collisions"
	[send1] c1=0 & c2>0 : 1; // station one starts transmitting and station two is already transmitting
	[send2] c2=0 & c1>0 : 1; // station two starts transmitting and station one is already transmitting
endrewards

// reward structure for expected time
// recall one time unit equals ASLOT(=50μs)
rewards "time"
	[time] true : 50;
endrewards

// reward strcuture for expected cost
// cost (per time unit) is set to:
// 1 in locations where the channel is free,
// 10 in locations where the channel is in use and a message is being sent correctly
// 1000 in locations where a station is sending a garbled message
// 2000 in locations where both stations are sending garbled messages
rewards	"cost"
	[time] c1=0 & c2=0 : 50;
	[time] c1=1 & c2=0 : 50*10;
	[time] c1=0 & c2=1 : 50*10;
	[time] c1=1 & c2=1 : 50*20;
	[time] c1=0 & c2=2 & bc1=0 & bc2=0 : 50*10;
	[time] c1=2 & c2=0 & bc1=0 & bc2=0 : 50*10;
	[time] c1=2 & c2=2 & bc1=0 & bc2=0 : 50*20;
	[time] c1=0 & c2=2 & (bc1>0 | bc2>0) : 50*1000;
	[time] c1=2 & c2=0 & (bc1>0 | bc2>0) : 50*1000;
	[time] c1=2 & c2=2 & (bc1>0 | bc2>0) : 50*2000;
endrewards