From ad7f800ac0f2f5bc1f21d74b56f961300ab73acd Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 16 Oct 2013 11:13:22 +0200 Subject: [PATCH] Added examples from MILP-paper. Former-commit-id: 6c8f918ed5c087ccc981cbdd970f16e87f2442f6 --- examples/mdp/csma/csma2_2.nm | 130 ++++++++++++++ examples/mdp/csma/csma2_4.nm | 128 ++++++++++++++ examples/mdp/firewire/impl/firewire.nm | 170 +++++++++++++++++++ examples/mdp/wlan/wlan0_collide.nm | 218 ++++++++++++++++++++++++ examples/mdp/wlan/wlan2_collide.nm | 225 +++++++++++++++++++++++++ 5 files changed, 871 insertions(+) create mode 100644 examples/mdp/csma/csma2_2.nm create mode 100644 examples/mdp/csma/csma2_4.nm create mode 100644 examples/mdp/firewire/impl/firewire.nm create mode 100644 examples/mdp/wlan/wlan0_collide.nm create mode 100644 examples/mdp/wlan/wlan2_collide.nm diff --git a/examples/mdp/csma/csma2_2.nm b/examples/mdp/csma/csma2_2.nm new file mode 100644 index 000000000..18ec5c897 --- /dev/null +++ b/examples/mdp/csma/csma2_2.nm @@ -0,0 +1,130 @@ +// CSMA/CD protocol - probabilistic version of kronos model (3 stations) +// gxn/dxp 04/12/01 + +mdp + +// note made changes since cannot have strict inequalities +// in digital clocks approach and suppose a station only sends one message + +// simplified parameters scaled +const int sigma=1; // time for messages to propagate along the bus +const int lambda=30; // time to send a message + +// actual parameters +const int N = 2; // number of processes +const int K = 2; // exponential backoff limit +const int slot = 2*sigma; // length of slot +// const int M = floor(pow(2, K))-1 ; // max number of slots to wait +const int M = 3 ; // max number of slots to wait +//const int lambda=782; +//const int sigma=26; + +// formula min_backoff_after_success = min(s1=4?cd1:K+1,s2=4?cd2:K+1); +// formula min_collisions = min(cd1,cd2); +// formula max_collisions = max(cd1,cd2); + +//---------------------------------------------------------------------------------------------------------------------------- +// the bus +module bus + + b : [0..2]; + // b=0 - idle + // b=1 - active + // b=2 - collision + + // clocks of bus + y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) + y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) + + // a sender sends (ok - no other message being sent) + [send1] (b=0) -> (b'=1); + [send2] (b=0) -> (b'=1); + + // a sender sends (bus busy - collision) + [send1] (b=1|b=2) & (y1 (b'=2); + [send2] (b=1|b=2) & (y1 (b'=2); + + // finish sending + [end1] (b=1) -> (b'=0) & (y1'=0); + [end2] (b=1) -> (b'=0) & (y1'=0); + + // bus busy + [busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); + [busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); + + // collision detected + [cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); + + // time passage + [time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 + [time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 + [time] (b=2) & (y2 (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- +// model of first sender +module station1 + + // LOCAL STATE + s1 : [0..5]; + // s1=0 - initial state + // s1=1 - transmit + // s1=2 - collision (set backoff) + // s1=3 - wait (bus busy) + // s1=4 - successfully sent + + // LOCAL CLOCK + x1 : [0..max(lambda,slot)]; + + // BACKOFF COUNTER (number of slots to wait) + bc1 : [0..M]; + + // COLLISION COUNTER + cd1 : [0..K]; + + // start sending + [send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending + [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff + + // transmitting + [time] (s1=1) & (x1 (x1'=min(x1+1,lambda)); // let time pass + [end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished + [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) + [cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important + + // set backoff (no time can pass in this state) + // probability depends on which transmission this is (cd1) + [] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; + [] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; + + // wait until backoff counter reaches 0 then send again + [time] (s1=3) & (x1 (x1'=x1+1); // let time pass (in slot) + [time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) + [send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) + [busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) + + // once finished nothing matters + [time] (s1>=4) -> (x1'=0); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward structure for expected time +rewards "time" + [time] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- + +// labels/formulae +label "all_delivered" = s1=4&s2=4; +label "one_delivered" = s1=4|s2=4; +label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); + diff --git a/examples/mdp/csma/csma2_4.nm b/examples/mdp/csma/csma2_4.nm new file mode 100644 index 000000000..ddc1f3281 --- /dev/null +++ b/examples/mdp/csma/csma2_4.nm @@ -0,0 +1,128 @@ +// CSMA/CD protocol - probabilistic version of kronos model (3 stations) +// gxn/dxp 04/12/01 + +mdp + +// note made changes since cannot have strict inequalities +// in digital clocks approach and suppose a station only sends one message + +// simplified parameters scaled +const int sigma=1; // time for messages to propagate along the bus +const int lambda=30; // time to send a message + +// actual parameters +const int N = 2; // number of processes +const int K = 4; // exponential backoff limit +const int slot = 2*sigma; // length of slot +const int M = 15 ; // max number of slots to wait +//const int lambda=782; +//const int sigma=26; + + +//---------------------------------------------------------------------------------------------------------------------------- +// the bus +module bus + + b : [0..2]; + // b=0 - idle + // b=1 - active + // b=2 - collision + + // clocks of bus + y1 : [0..sigma+1]; // time since first send (used find time until channel sensed busy) + y2 : [0..sigma+1]; // time since second send (used to find time until collision detected) + + // a sender sends (ok - no other message being sent) + [send1] (b=0) -> (b'=1); + [send2] (b=0) -> (b'=1); + + // a sender sends (bus busy - collision) + [send1] (b=1|b=2) & (y1 (b'=2); + [send2] (b=1|b=2) & (y1 (b'=2); + + // finish sending + [end1] (b=1) -> (b'=0) & (y1'=0); + [end2] (b=1) -> (b'=0) & (y1'=0); + + // bus busy + [busy1] (b=1|b=2) & (y1>=sigma) -> (b'=b); + [busy2] (b=1|b=2) & (y1>=sigma) -> (b'=b); + + // collision detected + [cd] (b=2) & (y2<=sigma) -> (b'=0) & (y1'=0) & (y2'=0); + + // time passage + [time] (b=0) -> (y1'=0); // value of y1/y2 does not matter in state 0 + [time] (b=1) -> (y1'=min(y1+1,sigma+1)); // no invariant in state 1 + [time] (b=2) & (y2 (y1'=min(y1+1,sigma+1)) & (y2'=min(y2+1,sigma+1)); // invariant in state 2 (time until collision detected) + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- +// model of first sender +module station1 + + // LOCAL STATE + s1 : [0..5]; + // s1=0 - initial state + // s1=1 - transmit + // s1=2 - collision (set backoff) + // s1=3 - wait (bus busy) + // s1=4 - successfully sent + + // LOCAL CLOCK + x1 : [0..max(lambda,slot)]; + + // BACKOFF COUNTER (number of slots to wait) + bc1 : [0..M]; + + // COLLISION COUNTER + cd1 : [0..K]; + + // start sending + [send1] (s1=0) -> (s1'=1) & (x1'=0); // start sending + [busy1] (s1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // detects channel is busy so go into backoff + + // transmitting + [time] (s1=1) & (x1 (x1'=min(x1+1,lambda)); // let time pass + [end1] (s1=1) & (x1=lambda) -> (s1'=4) & (x1'=0); // finished + [cd] (s1=1) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // collision detected (increment backoff counter) + [cd] !(s1=1) -> (s1'=s1); // add loop for collision detection when not important + + // set backoff (no time can pass in this state) + // probability depends on which transmission this is (cd1) + [] s1=2 & cd1=1 -> 1/2 : (s1'=3) & (bc1'=0) + 1/2 : (s1'=3) & (bc1'=1) ; + [] s1=2 & cd1=2 -> 1/4 : (s1'=3) & (bc1'=0) + 1/4 : (s1'=3) & (bc1'=1) + 1/4 : (s1'=3) & (bc1'=2) + 1/4 : (s1'=3) & (bc1'=3) ; + [] s1=2 & cd1=3 -> 1/8 : (s1'=3) & (bc1'=0) + 1/8 : (s1'=3) & (bc1'=1) + 1/8 : (s1'=3) & (bc1'=2) + 1/8 : (s1'=3) & (bc1'=3) + 1/8 : (s1'=3) & (bc1'=4) + 1/8 : (s1'=3) & (bc1'=5) + 1/8 : (s1'=3) & (bc1'=6) + 1/8 : (s1'=3) & (bc1'=7) ; + [] s1=2 & cd1=4 -> 1/16 : (s1'=3) & (bc1'=0) + 1/16 : (s1'=3) & (bc1'=1) + 1/16 : (s1'=3) & (bc1'=2) + 1/16 : (s1'=3) & (bc1'=3) + 1/16 : (s1'=3) & (bc1'=4) + 1/16 : (s1'=3) & (bc1'=5) + 1/16 : (s1'=3) & (bc1'=6) + 1/16 : (s1'=3) & (bc1'=7) + 1/16 : (s1'=3) & (bc1'=8) + 1/16 : (s1'=3) & (bc1'=9) + 1/16 : (s1'=3) & (bc1'=10) + 1/16 : (s1'=3) & (bc1'=11) + 1/16 : (s1'=3) & (bc1'=12) + 1/16 : (s1'=3) & (bc1'=13) + 1/16 : (s1'=3) & (bc1'=14) + 1/16 : (s1'=3) & (bc1'=15) ; + + // wait until backoff counter reaches 0 then send again + [time] (s1=3) & (x1 (x1'=x1+1); // let time pass (in slot) + [time] (s1=3) & (x1=slot) & (bc1>0) -> (x1'=1) & (bc1'=bc1-1); // let time pass (move slots) + [send1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=1) & (x1'=0); // finished backoff (bus appears free) + [busy1] (s1=3) & (x1=slot) & (bc1=0) -> (s1'=2) & (x1'=0) & (cd1'=min(K,cd1+1)); // finished backoff (bus busy) + + // once finished nothing matters + [time] (s1>=4) -> (x1'=0); + +endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// construct further stations through renaming +module station2=station1[s1=s2,x1=x2,cd1=cd2,bc1=bc2,send1=send2,busy1=busy2,end1=end2] endmodule + +//---------------------------------------------------------------------------------------------------------------------------- + +// reward structure for expected time +rewards "time" + [time] true : 1; +endrewards + +//---------------------------------------------------------------------------------------------------------------------------- + +// labels/formulae +label "all_delivered" = s1=4&s2=4; +label "one_delivered" = s1=4|s2=4; +label "collision_max_backoff" = (cd1=K & s1=1 & b=2)|(cd2=K & s2=1 & b=2); + diff --git a/examples/mdp/firewire/impl/firewire.nm b/examples/mdp/firewire/impl/firewire.nm new file mode 100644 index 000000000..26fa210b4 --- /dev/null +++ b/examples/mdp/firewire/impl/firewire.nm @@ -0,0 +1,170 @@ +// firewire protocol with integer semantics +// dxp/gxn 14/06/01 + +// CLOCKS +// x1 (x2) clock for node1 (node2) +// y1 and y2 (z1 and z2) clocks for wire12 (wire21) +mdp + +// maximum and minimum delays +// fast +const int rc_fast_max = 85; +const int rc_fast_min = 76; +// slow +const int rc_slow_max = 167; +const int rc_slow_min = 159; +// delay caused by the wire length +const int delay; +// probability of choosing fast +const double fast; +const double slow=1-fast; + +module wire12 + + // local state + w12 : [0..9]; + // 0 - empty + // 1 - rec_req + // 2 - rec_req_ack + // 3 - rec_ack + // 4 - rec_ack_idle + // 5 - rec_idle + // 6 - rec_idle_req + // 7 - rec_ack_req + // 8 - rec_req_idle + // 9 - rec_idle_ack + + // clock for wire12 + y1 : [0..delay+1]; + y2 : [0..delay+1]; + + // empty + // do not need y1 and y2 to increase as always reset when this state is left + // similarly can reset y1 and y2 when we re-enter this state + [snd_req12] w12=0 -> (w12'=1) & (y1'=0) & (y2'=0); + [snd_ack12] w12=0 -> (w12'=3) & (y1'=0) & (y2'=0); + [snd_idle12] w12=0 -> (w12'=5) & (y1'=0) & (y2'=0); + [time] w12=0 -> (w12'=w12); + // rec_req + [snd_req12] w12=1 -> (w12'=1); + [rec_req12] w12=1 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_ack12] w12=1 -> (w12'=2) & (y2'=0); + [snd_idle12] w12=1 -> (w12'=8) & (y2'=0); + [time] w12=1 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_ack + [snd_ack12] w12=2 -> (w12'=2); + [rec_req12] w12=2 -> (w12'=3); + [time] w12=2 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack + [snd_ack12] w12=3 -> (w12'=3); + [rec_ack12] w12=3 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_idle12] w12=3 -> (w12'=4) & (y2'=0); + [snd_req12] w12=3 -> (w12'=7) & (y2'=0); + [time] w12=3 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_idle + [snd_idle12] w12=4 -> (w12'=4); + [rec_ack12] w12=4 -> (w12'=5); + [time] w12=4 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle + [snd_idle12] w12=5 -> (w12'=5); + [rec_idle12] w12=5 -> (w12'=0) & (y1'=0) & (y2'=0); + [snd_req12] w12=5 -> (w12'=6) & (y2'=0); + [snd_ack12] w12=5 -> (w12'=9) & (y2'=0); + [time] w12=5 & y2 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_req + [snd_req12] w12=6 -> (w12'=6); + [rec_idle12] w12=6 -> (w12'=1); + [time] w12=6 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_ack_req + [snd_req12] w12=7 -> (w12'=7); + [rec_ack12] w12=7 -> (w12'=1); + [time] w12=7 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_req_idle + [snd_idle12] w12=8 -> (w12'=8); + [rec_req12] w12=8 -> (w12'=5); + [time] w12=8 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + // rec_idle_ack + [snd_ack12] w12=9 -> (w12'=9); + [rec_idle12] w12=9 -> (w12'=3); + [time] w12=9 & y1 (y1'=min(y1+1,delay+1)) & (y2'=min(y2+1,delay+1)); + +endmodule + +module node1 + + // clock for node1 + x1 : [0..168]; + + // local state + s1 : [0..8]; + // 0 - root contention + // 1 - rec_idle + // 2 - rec_req_fast + // 3 - rec_req_slow + // 4 - rec_idle_fast + // 5 - rec_idle_slow + // 6 - snd_req + // 7- almost_root + // 8 - almost_child + + // added resets to x1 when not considered again until after rest + // removed root and child (using almost root and almost child) + + // root contention immediate state) + [snd_idle12] s1=0 -> fast : (s1'=2) & (x1'=0) + slow : (s1'=3) & (x1'=0); + [rec_idle21] s1=0 -> (s1'=1); + // rec_idle immediate state) + [snd_idle12] s1=1 -> fast : (s1'=4) & (x1'=0) + slow : (s1'=5) & (x1'=0); + [rec_req21] s1=1 -> (s1'=0); + // rec_req_fast + [rec_idle21] s1=2 -> (s1'=4); + [snd_ack12] s1=2 & x1>=rc_fast_min -> (s1'=7) & (x1'=0); + [time] s1=2 & x1 (x1'=min(x1+1,168)); + // rec_req_slow + [rec_idle21] s1=3 -> (s1'=5); + [snd_ack12] s1=3 & x1>=rc_slow_min -> (s1'=7) & (x1'=0); + [time] s1=3 & x1 (x1'=min(x1+1,168)); + // rec_idle_fast + [rec_req21] s1=4 -> (s1'=2); + [snd_req12] s1=4 & x1>=rc_fast_min -> (s1'=6) & (x1'=0); + [time] s1=4 & x1 (x1'=min(x1+1,168)); + // rec_idle_slow + [rec_req21] s1=5 -> (s1'=3); + [snd_req12] s1=5 & x1>=rc_slow_min -> (s1'=6) & (x1'=0); + [time] s1=5 & x1 (x1'=min(x1+1,168)); + // snd_req + // do not use x1 until reset (in state 0 or in state 1) so do not need to increase x1 + // also can set x1 to 0 upon entering this state + [rec_req21] s1=6 -> (s1'=0); + [rec_ack21] s1=6 -> (s1'=8); + [time] s1=6 -> (s1'=s1); + // almost root (immediate) + // loop in final states to remove deadlock + [] s1=7 & s2=8 -> (s1'=s1); + [] s1=8 & s2=7 -> (s1'=s1); + [time] s1=7 -> (s1'=s1); + [time] s1=8 -> (s1'=s1); + +endmodule + +// construct remaining automata through renaming +module wire21=wire12[w12=w21, y1=z1, y2=z2, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21, + rec_req12=rec_req21, rec_idle12=rec_idle21, rec_ack12=rec_ack21] +endmodule +module node2=node1[s1=s2, s2=s1, x1=x2, + rec_req21=rec_req12, rec_idle21=rec_idle12, rec_ack21=rec_ack12, + snd_req12=snd_req21, snd_idle12=snd_idle21, snd_ack12=snd_ack21] +endmodule + +// reward structures +// time +rewards "time" + [time] true : 1; +endrewards +// time nodes sending +rewards "time_sending" + [time] (w12>0 | w21>0) : 1; +endrewards + +label "elected" = ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)); \ No newline at end of file diff --git a/examples/mdp/wlan/wlan0_collide.nm b/examples/mdp/wlan/wlan0_collide.nm new file mode 100644 index 000000000..73d7699cb --- /dev/null +++ b/examples/mdp/wlan/wlan0_collide.nm @@ -0,0 +1,218 @@ +// 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 diff --git a/examples/mdp/wlan/wlan2_collide.nm b/examples/mdp/wlan/wlan2_collide.nm new file mode 100644 index 000000000..839e04a59 --- /dev/null +++ b/examples/mdp/wlan/wlan2_collide.nm @@ -0,0 +1,225 @@ +// 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