diff --git a/examples/mdp/wlan/wlan0_collide.nm b/examples/mdp/wlan/wlan0_collide.nm index 73d7699cb..1c14704e5 100644 --- a/examples/mdp/wlan/wlan0_collide.nm +++ b/examples/mdp/wlan/wlan0_collide.nm @@ -1,218 +1,219 @@ -// WLAN PROTOCOL (two stations) -// discrete time model -// gxn/jzs 20/02/02 - -mdp - -// COLLISIONS -const int COL; // maximum number of collisions - -// 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 either 2 or 3 which is modelled by a non-deterministic choice -const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice -const int TRANS_TIME_MAX; // scaling up -const int TRANS_TIME_MIN = 4; // scaling down -const int ACK_TO = 6; -const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice -const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice -// maximum constant used in timing constraints + 1 -const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; - -// CONTENTION WINDOW -// CWMIN =15 & CWMAX =16 -// this means that MAX_BACKOFF IS 2 -const int MAX_BACKOFF = 0; - -//-----------------------------------------------------------------// -// THE MEDIUM/CHANNEL - -// FORMULAE FOR THE CHANNEL -// channel is busy -// formula busy = c1>0 | c2>0; -// channel is free -// formula free = c1=0 & c2=0; - -module medium - - // number of collisions - col : [0..COL]; - - // 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,COL)); - [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); - - // 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..1]; - backoff1 : [0..15]; - - // BACKOFF COUNTER - bc1 : [0..1]; - // 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 & (c1>0 | c2>0) -> (s1'=2) & (x1'=0); - // WAIT UNTIL FREE BEFORE SETTING BACKOFF - // let time pass (no need for the clock x1 to change) - [time] s1=2 & (c1>0 | c2>0) -> (s1'=2); - // find that channel is free so check its free for DIFS before setting backoff - [] s1=2 & (c1=0 & c2=0) -> (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 & (c1>0 | c2>0) -> (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,MAX_BACKOFF)); - // 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 & (c1>0 | c2>0) -> (s1'=6) & (x1'=0); - // WAIT UNTIL FREE IN BACKOFF - // let time pass (no need for the clock x1 to change) - [time] s1=6 & (c1>0 | c2>0) -> (s1'=6); - // find that channel is free - [] s1=6 & (c1=0 & c2=0) -> (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 & (c1>0 | c2>0) -> (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 & (c1>0 | c2>0) -> (s1'=2); - // check channel and free: let time pass - [time] s1=10 & c1=0 & x1=0 & (c1=0 & c2=0) -> (x1'=min(x1+1,TIME_MAX)); - // let time pass - // following guard is always false as SIFS=1 - // [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 & (c1=0 & c2=0))) -> (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 & (c1>0 | c2>0) -> (s1'=2); - // check channel and free: let time pass - [time] s1=11 & x1=0 & (c1=0 & c2=0) -> (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 -// ---------------------------------------------------------------------------- // - -label "oneCollision" = col=1; -label "twoCollisions" = col=2; \ No newline at end of file +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =16 +// this means that MAX_BACKOFF IS 2 +const int MAX_BACKOFF = 0; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..1]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..1]; + // 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,MAX_BACKOFF)); + // 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); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlan1_collide.nm b/examples/mdp/wlan/wlan1_collide.nm new file mode 100644 index 000000000..7c4904cd9 --- /dev/null +++ b/examples/mdp/wlan/wlan1_collide.nm @@ -0,0 +1,221 @@ +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =31 +// this means that MAX_BACKOFF IS 2 +const int MAX_BACKOFF = 1; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..1]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..MAX_BACKOFF]; + // 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,MAX_BACKOFF)); + // backoff counter 1 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // 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); + // chEck channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlan2_collide.nm b/examples/mdp/wlan/wlan2_collide.nm index 839e04a59..a3fcccafa 100644 --- a/examples/mdp/wlan/wlan2_collide.nm +++ b/examples/mdp/wlan/wlan2_collide.nm @@ -1,225 +1,226 @@ -// WLAN PROTOCOL (two stations) -// discrete time model -// gxn/jzs 20/02/02 - -mdp - -// COLLISIONS -const int COL; // maximum number of collisions - -// 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 either 2 or 3 which is modelled by a non-deterministic choice -const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice -const int TRANS_TIME_MAX; // scaling up -const int TRANS_TIME_MIN = 4; // scaling down -const int ACK_TO = 6; -const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice -const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice -// maximum constant used in timing constraints + 1 -const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; - -// CONTENTION WINDOW -// CWMIN =15 & CWMAX =63 -// this means that MAX_BACKOFF IS 2 -const int MAX_BACKOFF = 2; - -//-----------------------------------------------------------------// -// THE MEDIUM/CHANNEL - -// FORMULAE FOR THE CHANNEL -// channel is (c1>0 | c2>0) -// formula busy = c1>0 | c2>0; -// channel is (c1=0 & c2=0) -// formula free = c1=0 & c2=0; - -module medium - - // number of collisions - col : [0..COL]; - - // 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,COL)); - [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); - - // 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 (c1=0 & c2=0) before setting backoff - // 3 wait for DIFS then set slot - // 4 set backoff - // 5 backoff - // 6 wait until (c1=0 & c2=0) 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..3]; - backoff1 : [0..15]; - - // BACKOFF COUNTER - bc1 : [0..MAX_BACKOFF]; - // 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 (c1>0 | c2>0) so wait until (c1=0 & c2=0) - [] s1=1 & (c1>0 | c2>0) -> (s1'=2) & (x1'=0); - // WAIT UNTIL (c1=0 & c2=0) BEFORE SETTING BACKOFF - // let time pass (no need for the clock x1 to change) - [time] s1=2 & (c1>0 | c2>0) -> (s1'=2); - // find that channel is (c1=0 & c2=0) so check its (c1=0 & c2=0) for DIFS before setting backoff - [] s1=2 & (c1=0 & c2=0) -> (s1'=3); - // WAIT FOR DIFS THEN SET BACKOFF - // let time pass - [time] s1=3 & x1 (x1'=min(x1+1,TIME_MAX)); - // found channel (c1>0 | c2>0) so wait until (c1=0 & c2=0) - [] s1=3 & (c1>0 | c2>0) -> (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,MAX_BACKOFF)); - // backoff counter 1 - [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) - + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); - // backoff counter 2 - [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) - + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) - + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) - + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); - // 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 (c1>0 | c2>0) - [] s1=5 & (c1>0 | c2>0) -> (s1'=6) & (x1'=0); - // WAIT UNTIL (c1=0 & c2=0) IN BACKOFF - // let time pass (no need for the clock x1 to change) - [time] s1=6 & (c1>0 | c2>0) -> (s1'=6); - // find that channel is (c1=0 & c2=0) - [] s1=6 & (c1=0 & c2=0) -> (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 (c1>0 | c2>0) - [] s1=7 & (c1>0 | c2>0) -> (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 (c1>0 | c2>0): go into backoff - [] s1=10 & c1=0 & x1=0 & (c1>0 | c2>0) -> (s1'=2); - // check channel and (c1=0 & c2=0): let time pass - [time] s1=10 & c1=0 & x1=0 & (c1=0 & c2=0) -> (x1'=min(x1+1,TIME_MAX)); - // let time pass - // following guard is always false as SIFS=1 - // [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 (c1=0 & c2=0)) - [send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & (c1=0 & c2=0))) -> (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 (c1>0 | c2>0): go into backoff - [] s1=11 & x1=0 & (c1>0 | c2>0) -> (s1'=2); - // check channel and (c1=0 & c2=0): let time pass - [time] s1=11 & x1=0 & (c1=0 & c2=0) -> (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 -// ---------------------------------------------------------------------------- // - -label "oneCollision" = col=1; -label "twoCollisions" = col=2; \ No newline at end of file +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =63 +// this means that MAX_BACKOFF IS 2 +const int MAX_BACKOFF = 2; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..3]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..MAX_BACKOFF]; + // 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,MAX_BACKOFF)); + // backoff counter 1 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 2 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // 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); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlan3_collide.nm b/examples/mdp/wlan/wlan3_collide.nm new file mode 100644 index 000000000..1d093e6d7 --- /dev/null +++ b/examples/mdp/wlan/wlan3_collide.nm @@ -0,0 +1,235 @@ +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =127 +// this means that MAX_BACKOFF IS 3 +const int MAX_BACKOFF = 3; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..7]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..MAX_BACKOFF]; + // 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,MAX_BACKOFF)); + // backoff counter 1 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 2 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 3 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // 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); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlan4_collide.nm b/examples/mdp/wlan/wlan4_collide.nm new file mode 100644 index 000000000..1287de1f3 --- /dev/null +++ b/examples/mdp/wlan/wlan4_collide.nm @@ -0,0 +1,252 @@ +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =255 +// this means that MAX_BACKOFF IS 4 +const int MAX_BACKOFF = 4; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..15]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..MAX_BACKOFF]; + // 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,MAX_BACKOFF)); + // backoff counter 1 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 2 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 3 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 4 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // 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); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlan5_collide.nm b/examples/mdp/wlan/wlan5_collide.nm new file mode 100644 index 000000000..e01b7cfcd --- /dev/null +++ b/examples/mdp/wlan/wlan5_collide.nm @@ -0,0 +1,286 @@ +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =511 +// this means that MAX_BACKOFF IS 5 +const int MAX_BACKOFF = 5; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..31]; + backoff1 : [0..15]; + + // BACKOFF COUNTER + bc1 : [0..MAX_BACKOFF]; + // 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,MAX_BACKOFF)); + // backoff counter 1 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 2 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 3 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 4 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 5 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=5 -> 1/32 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,MAX_BACKOFF)); + + // 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); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlan6_collide.nm b/examples/mdp/wlan/wlan6_collide.nm new file mode 100644 index 000000000..e0a098f71 --- /dev/null +++ b/examples/mdp/wlan/wlan6_collide.nm @@ -0,0 +1,351 @@ +// WLAN PROTOCOL (two stations) +// discrete time model +// gxn/jzs 20/02/02 + +mdp + +// COLLISIONS +const int COL; // maximum number of collisions + +// 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 either 2 or 3 which is modelled by a non-deterministic choice +const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +const int TRANS_TIME_MAX; // scaling up +const int TRANS_TIME_MIN = 4; // scaling down +const int ACK_TO = 6; +const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice +const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice +// maximum constant used in timing constraints + 1 +const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1; + +// CONTENTION WINDOW +// CWMIN =15 & CWMAX =1023 +// this means that MAX_BACKOFF IS 6 +const int MAX_BACKOFF = 6; + +//-----------------------------------------------------------------// +// THE MEDIUM/CHANNEL + +// FORMULAE FOR THE CHANNEL +// channel is busy +formula busy = c1>0 | c2>0; +// channel is free +formula free = c1=0 & c2=0; + +module medium + + // number of collisions + col : [0..COL]; + + // 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,COL)); + [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL)); + + // 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..MAX_BACKOFF]; + // 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,MAX_BACKOFF)); + // backoff counter 1 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 2 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 3 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 4 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // backoff counter 5 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=5 -> 1/32 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/32 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,MAX_BACKOFF)); + + // backoff counter 6 + [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=6 -> 1/64 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=16) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=17) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=18) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=19) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=20) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=21) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=22) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=23) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=24) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=25) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=26) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=27) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=28) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=29) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=30) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=31) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=32) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=33) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=34) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=35) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=36) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=37) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=38) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=39) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=40) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=41) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=42) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=43) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=44) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=45) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=46) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=47) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=48) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=49) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=50) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=51) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=52) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=53) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=54) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=55) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=56) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=57) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=58) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=59) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=60) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=61) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=62) & (bc1'=min(bc1+1,MAX_BACKOFF)) + + 1/64 : (s1'=4) & (x1'=0) & (slot1'=63) & (bc1'=min(bc1+1,MAX_BACKOFF)); + // 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); + // check channel and free: let time pass + [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX)); + // let time pass + // following guard is always false as SIFS=1 + // [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 +// ---------------------------------------------------------------------------- // + +label "twoCollisions" = col=2; +label "fourCollisions" = col=4; +label "sixCollisions" = col=6; \ No newline at end of file diff --git a/examples/mdp/wlan/wlanX_1.cexprop b/examples/mdp/wlan/wlanX_1.cexprop deleted file mode 100644 index 4c3a40fd8..000000000 --- a/examples/mdp/wlan/wlanX_1.cexprop +++ /dev/null @@ -1 +0,0 @@ -P<0.5 [ F oneCollision ] diff --git a/examples/mdp/wlan/wlanX_4.cexprop b/examples/mdp/wlan/wlanX_4.cexprop new file mode 100644 index 000000000..ad82b1457 --- /dev/null +++ b/examples/mdp/wlan/wlanX_4.cexprop @@ -0,0 +1 @@ +P<0.1 [ F fourCollisions ] diff --git a/examples/mdp/wlan/wlanX_6.cexprop b/examples/mdp/wlan/wlanX_6.cexprop new file mode 100644 index 000000000..b02357fa7 --- /dev/null +++ b/examples/mdp/wlan/wlanX_6.cexprop @@ -0,0 +1 @@ +P<0.1 [ F sixCollisions ] diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h index be446333d..9d3f5f74f 100644 --- a/src/adapters/ExplicitModelAdapter.h +++ b/src/adapters/ExplicitModelAdapter.h @@ -317,7 +317,7 @@ namespace storm { for (std::string const& action : program.getActions()) { StateType const* currentState = stateInformation.reachableStates[stateIndex]; boost::optional>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action); - + // Only process this action label, if there is at least one feasible solution. if (optionalActiveCommandLists) { std::vector> const& activeCommandList = optionalActiveCommandLists.get(); diff --git a/src/parser/prismparser/VariableState.cpp b/src/parser/prismparser/VariableState.cpp index a3d85579b..244a3f17e 100644 --- a/src/parser/prismparser/VariableState.cpp +++ b/src/parser/prismparser/VariableState.cpp @@ -175,6 +175,12 @@ namespace storm { booleanConstants_.clear(); doubleConstants_.clear(); allConstantNames_.clear(); + constantBooleanFormulas_.clear(); + booleanFormulas_.clear(); + constantIntegerFormulas_.clear(); + integerFormulas_.clear(); + constantDoubleFormulas_.clear(); + doubleFormulas_.clear(); this->firstRun = false; nextGlobalCommandIndex = 0; nextGlobalUpdateIndex = 0;