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

Fixed a bug: formulas are now handled (more) correctly. Added some WLAN examples. 

Former-commit-id: 4b87ffc99f
tempestpy_adaptions
dehnert 11 years ago
parent
310a840ad5
commit
a52419652d
12 changed files with 1799 additions and 445 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. 437
      examples/mdp/wlan/wlan0_collide.nm
  2. 221
      examples/mdp/wlan/wlan1_collide.nm
  3. 451
      examples/mdp/wlan/wlan2_collide.nm
  4. 235
      examples/mdp/wlan/wlan3_collide.nm
  5. 252
      examples/mdp/wlan/wlan4_collide.nm
  6. 286
      examples/mdp/wlan/wlan5_collide.nm
  7. 351
      examples/mdp/wlan/wlan6_collide.nm
  8. 1
      examples/mdp/wlan/wlanX_1.cexprop
  9. 1
      examples/mdp/wlan/wlanX_4.cexprop
  10. 1
      examples/mdp/wlan/wlanX_6.cexprop
  11. 2
      src/adapters/ExplicitModelAdapter.h
  12. 6
      src/parser/prismparser/VariableState.cpp

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

@ -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<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;
// 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 & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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 & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

221
examples/mdp/wlan/wlan1_collide.nm
View File

@ -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<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

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

@ -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<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;
// 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<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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 & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

235
examples/mdp/wlan/wlan3_collide.nm
View File

@ -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<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

252
examples/mdp/wlan/wlan4_collide.nm
View File

@ -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<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

286
examples/mdp/wlan/wlan5_collide.nm
View File

@ -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<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

351
examples/mdp/wlan/wlan6_collide.nm
View File

@ -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<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// ready to transmit
[] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
// found channel busy so wait until free
[] s1=1 & busy -> (s1'=2) & (x1'=0);
// WAIT UNTIL FREE BEFORE SETTING BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=2 & busy -> (s1'=2);
// find that channel is free so check its free for DIFS before setting backoff
[] s1=2 & free -> (s1'=3);
// WAIT FOR DIFS THEN SET BACKOFF
// let time pass
[time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// found channel busy so wait until free
[] s1=3 & busy -> (s1'=2) & (x1'=0);
// start backoff first uniformly choose slot
// backoff counter 0
[] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,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<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
// decrement backoff
[] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
// finish backoff
[] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
// found channel busy
[] s1=5 & busy -> (s1'=6) & (x1'=0);
// WAIT UNTIL FREE IN BACKOFF
// let time pass (no need for the clock x1 to change)
[time] s1=6 & busy -> (s1'=6);
// find that channel is free
[] s1=6 & free -> (s1'=7);
// WAIT FOR DIFS THEN RESUME BACKOFF
// let time pass
[time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
// resume backoff (start again from previous backoff)
[] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
// found channel busy
[] s1=7 & busy -> (s1'=6) & (x1'=0);
// VULNERABLE
// let time pass
[time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
// move to transmit
[send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
// TRANSMIT
// let time pass
[time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
// finish transmission successful
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
// finish transmission garbled
[finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
// WAIT FOR SIFS THEN WAIT FOR ACK
// WAIT FOR SIFS i.e. c1=0
// check channel and busy: go into backoff
[] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
// 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<SIFS -> (x1'=min(x1+1,TIME_MAX));
// ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
[send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
// WAIT FOR ACK i.e. c1=1
// let time pass
[time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
// get acknowledgement so packet sent correctly and move to done
[finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
// WAIT FOR ACK_TO
// check channel and busy: go into backoff
[] s1=11 & x1=0 & busy -> (s1'=2);
// check channel and free: let time pass
[time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
// let time pass
[time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
// no acknowledgement (go to backoff waiting DIFS first)
[] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
// DONE
[time] s1=12 -> (s1'=12);
endmodule
// ---------------------------------------------------------------------------- //
// STATION 2 (rename STATION 1)
module
station2=station1[x1=x2,
s1=s2,
s2=s1,
c1=c2,
c2=c1,
slot1=slot2,
backoff1=backoff2,
bc1=bc2,
send1=send2,
finish1=finish2]
endmodule
// ---------------------------------------------------------------------------- //
label "twoCollisions" = col=2;
label "fourCollisions" = col=4;
label "sixCollisions" = col=6;

1
examples/mdp/wlan/wlanX_1.cexprop
View File

@ -1 +0,0 @@
P<0.5 [ F oneCollision ]

1
examples/mdp/wlan/wlanX_4.cexprop
View File

@ -0,0 +1 @@
P<0.1 [ F fourCollisions ]

1
examples/mdp/wlan/wlanX_6.cexprop
View File

@ -0,0 +1 @@
P<0.1 [ F sixCollisions ]

2
src/adapters/ExplicitModelAdapter.h
View File

@ -317,7 +317,7 @@ namespace storm {
for (std::string const& action : program.getActions()) {
StateType const* currentState = stateInformation.reachableStates[stateIndex];
boost::optional<std::vector<std::list<storm::ir::Command>>> optionalActiveCommandLists = getActiveCommandsByAction(program, currentState, action);
// Only process this action label, if there is at least one feasible solution.
if (optionalActiveCommandLists) {
std::vector<std::list<storm::ir::Command>> const& activeCommandList = optionalActiveCommandLists.get();

6
src/parser/prismparser/VariableState.cpp
View File

@ -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;

Write Preview
Loading…
Cancel
Save