sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Added examples from MILP-paper. 

Former-commit-id: 6c8f918ed5
tempestpy_adaptions
dehnert 11 years ago
parent
c31dbc85a7
commit
ad7f800ac0
5 changed files with 871 additions and 0 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 130
      examples/mdp/csma/csma2_2.nm
  2. 128
      examples/mdp/csma/csma2_4.nm
  3. 170
      examples/mdp/firewire/impl/firewire.nm
  4. 218
      examples/mdp/wlan/wlan0_collide.nm
  5. 225
      examples/mdp/wlan/wlan2_collide.nm

130
examples/mdp/csma/csma2_2.nm
View File

@ -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<sigma) -> (b'=2);
[send2] (b=1|b=2) & (y1<sigma) -> (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<sigma) -> (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<lambda) -> (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<slot) -> (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);

128
examples/mdp/csma/csma2_4.nm
View File

@ -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<sigma) -> (b'=2);
[send2] (b=1|b=2) & (y1<sigma) -> (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<sigma) -> (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<lambda) -> (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<slot) -> (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);

170
examples/mdp/firewire/impl/firewire.nm
View File

@ -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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<delay -> (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<rc_fast_max -> (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<rc_slow_max -> (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<rc_fast_max -> (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<rc_slow_max -> (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));

218
examples/mdp/wlan/wlan0_collide.nm
View File

@ -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<DIFS & (c1=0 & c2=0) -> (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<DIFS & (c1=0 & c2=0) -> (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<ASLOTTIME & (c1=0 & c2=0) -> (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<DIFS & (c1=0 & c2=0) -> (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<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & (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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & (c1=0 & c2=0))) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & (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<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "oneCollision" = col=1;
label "twoCollisions" = col=2;

225
examples/mdp/wlan/wlan2_collide.nm
View File

@ -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<DIFS & (c1=0 & c2=0) -> (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<DIFS & (c1=0 & c2=0) -> (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<ASLOTTIME & (c1=0 & c2=0) -> (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<DIFS & (c1=0 & c2=0) -> (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<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and (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<SIFS -> (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<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and (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<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "oneCollision" = col=1;
label "twoCollisions" = col=2;
Write Preview
Loading…
Cancel
Save