// 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 (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 (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 (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 (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 (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 (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 (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 (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 (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