You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

251 lines
11 KiB

  1. // WLAN PROTOCOL (two stations)
  2. // discrete time model
  3. // gxn/jzs 20/02/02
  4. mdp
  5. // COLLISIONS
  6. const int COL; // maximum number of collisions
  7. // TIMING CONSTRAINTS
  8. // we have used the FHSS parameters
  9. // then scaled by the value of ASLOTTIME
  10. const int ASLOTTIME = 1;
  11. const int DIFS = 3; // due to scaling can be either 2 or 3 which is modelled by a non-deterministic choice
  12. const int VULN = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
  13. const int TRANS_TIME_MAX; // scaling up
  14. const int TRANS_TIME_MIN = 4; // scaling down
  15. const int ACK_TO = 6;
  16. const int ACK = 4; // due to scaling can be either 3 or 4 which is modelled by a non-deterministic choice
  17. const int SIFS = 1; // due to scaling can be either 0 or 1 which is modelled by a non-deterministic choice
  18. // maximum constant used in timing constraints + 1
  19. const int TIME_MAX = max(ACK_TO,TRANS_TIME_MAX)+1;
  20. // CONTENTION WINDOW
  21. // CWMIN =15 & CWMAX =255
  22. // this means that MAX_BACKOFF IS 4
  23. const int MAX_BACKOFF = 4;
  24. //-----------------------------------------------------------------//
  25. // THE MEDIUM/CHANNEL
  26. // FORMULAE FOR THE CHANNEL
  27. // channel is busy
  28. formula busy = c1>0 | c2>0;
  29. // channel is free
  30. formula free = c1=0 & c2=0;
  31. module medium
  32. // number of collisions
  33. col : [0..COL];
  34. // medium status
  35. c1 : [0..2];
  36. c2 : [0..2];
  37. // ci corresponds to messages associated with station i
  38. // 0 nothing being sent
  39. // 1 being sent correctly
  40. // 2 being sent garbled
  41. // begin sending message and nothing else currently being sent
  42. [send1] c1=0 & c2=0 -> (c1'=1);
  43. [send2] c2=0 & c1=0 -> (c2'=1);
  44. // begin sending message and something is already being sent
  45. // in this case both messages become garbled
  46. [send1] c1=0 & c2>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
  47. [send2] c2=0 & c1>0 -> (c1'=2) & (c2'=2) & (col'=min(col+1,COL));
  48. // finish sending message
  49. [finish1] c1>0 -> (c1'=0);
  50. [finish2] c2>0 -> (c2'=0);
  51. endmodule
  52. //-----------------------------------------------------------------//
  53. // STATION 1
  54. module station1
  55. // clock for station 1
  56. x1 : [0..TIME_MAX];
  57. // local state
  58. s1 : [1..12];
  59. // 1 sense
  60. // 2 wait until free before setting backoff
  61. // 3 wait for DIFS then set slot
  62. // 4 set backoff
  63. // 5 backoff
  64. // 6 wait until free in backoff
  65. // 7 wait for DIFS then resume backoff
  66. // 8 vulnerable
  67. // 9 transmit
  68. // 11 wait for SIFS and then ACK
  69. // 10 wait for ACT_TO
  70. // 12 done
  71. // BACKOFF
  72. // separate into slots
  73. slot1 : [0..15];
  74. backoff1 : [0..15];
  75. // BACKOFF COUNTER
  76. bc1 : [0..MAX_BACKOFF];
  77. // SENSE
  78. // let time pass
  79. [time] s1=1 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
  80. // ready to transmit
  81. [] s1=1 & (x1=DIFS | x1=DIFS-1) -> (s1'=8) & (x1'=0);
  82. // found channel busy so wait until free
  83. [] s1=1 & busy -> (s1'=2) & (x1'=0);
  84. // WAIT UNTIL FREE BEFORE SETTING BACKOFF
  85. // let time pass (no need for the clock x1 to change)
  86. [time] s1=2 & busy -> (s1'=2);
  87. // find that channel is free so check its free for DIFS before setting backoff
  88. [] s1=2 & free -> (s1'=3);
  89. // WAIT FOR DIFS THEN SET BACKOFF
  90. // let time pass
  91. [time] s1=3 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
  92. // found channel busy so wait until free
  93. [] s1=3 & busy -> (s1'=2) & (x1'=0);
  94. // start backoff first uniformly choose slot
  95. // backoff counter 0
  96. [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=0 -> (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF));
  97. // backoff counter 1
  98. [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=1 -> 1/2 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF))
  99. + 1/2 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF));
  100. // backoff counter 2
  101. [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=2 -> 1/4 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF))
  102. + 1/4 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF))
  103. + 1/4 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF))
  104. + 1/4 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF));
  105. // backoff counter 3
  106. [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=3 -> 1/8 : (s1'=4) & (x1'=0) & (slot1'=0) & (bc1'=min(bc1+1,MAX_BACKOFF))
  107. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=1) & (bc1'=min(bc1+1,MAX_BACKOFF))
  108. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=2) & (bc1'=min(bc1+1,MAX_BACKOFF))
  109. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=3) & (bc1'=min(bc1+1,MAX_BACKOFF))
  110. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=4) & (bc1'=min(bc1+1,MAX_BACKOFF))
  111. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=5) & (bc1'=min(bc1+1,MAX_BACKOFF))
  112. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=6) & (bc1'=min(bc1+1,MAX_BACKOFF))
  113. + 1/8 : (s1'=4) & (x1'=0) & (slot1'=7) & (bc1'=min(bc1+1,MAX_BACKOFF));
  114. // backoff counter 4
  115. [] s1=3 & (x1=DIFS | x1=DIFS-1) & bc1=4 -> 1/16 : (s1'=4) & (x1'=0) & (slot1'=0 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  116. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=1 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  117. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=2 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  118. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=3 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  119. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=4 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  120. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=5 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  121. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=6 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  122. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=7 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  123. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=8 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  124. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=9 ) & (bc1'=min(bc1+1,MAX_BACKOFF))
  125. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=10) & (bc1'=min(bc1+1,MAX_BACKOFF))
  126. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=11) & (bc1'=min(bc1+1,MAX_BACKOFF))
  127. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=12) & (bc1'=min(bc1+1,MAX_BACKOFF))
  128. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=13) & (bc1'=min(bc1+1,MAX_BACKOFF))
  129. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=14) & (bc1'=min(bc1+1,MAX_BACKOFF))
  130. + 1/16 : (s1'=4) & (x1'=0) & (slot1'=15) & (bc1'=min(bc1+1,MAX_BACKOFF));
  131. // SET BACKOFF (no time can pass)
  132. // chosen slot now set backoff
  133. [] s1=4 -> 1/16 : (s1'=5) & (backoff1'=0 )
  134. + 1/16 : (s1'=5) & (backoff1'=1 )
  135. + 1/16 : (s1'=5) & (backoff1'=2 )
  136. + 1/16 : (s1'=5) & (backoff1'=3 )
  137. + 1/16 : (s1'=5) & (backoff1'=4 )
  138. + 1/16 : (s1'=5) & (backoff1'=5 )
  139. + 1/16 : (s1'=5) & (backoff1'=6 )
  140. + 1/16 : (s1'=5) & (backoff1'=7 )
  141. + 1/16 : (s1'=5) & (backoff1'=8 )
  142. + 1/16 : (s1'=5) & (backoff1'=9 )
  143. + 1/16 : (s1'=5) & (backoff1'=10)
  144. + 1/16 : (s1'=5) & (backoff1'=11)
  145. + 1/16 : (s1'=5) & (backoff1'=12)
  146. + 1/16 : (s1'=5) & (backoff1'=13)
  147. + 1/16 : (s1'=5) & (backoff1'=14)
  148. + 1/16 : (s1'=5) & (backoff1'=15);
  149. // BACKOFF
  150. // let time pass
  151. [time] s1=5 & x1<ASLOTTIME & free -> (x1'=min(x1+1,TIME_MAX));
  152. // decrement backoff
  153. [] s1=5 & x1=ASLOTTIME & backoff1>0 -> (s1'=5) & (x1'=0) & (backoff1'=backoff1-1);
  154. [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1>0 -> (s1'=5) & (x1'=0) & (backoff1'=15) & (slot1'=slot1-1);
  155. // finish backoff
  156. [] s1=5 & x1=ASLOTTIME & backoff1=0 & slot1=0 -> (s1'=8) & (x1'=0);
  157. // found channel busy
  158. [] s1=5 & busy -> (s1'=6) & (x1'=0);
  159. // WAIT UNTIL FREE IN BACKOFF
  160. // let time pass (no need for the clock x1 to change)
  161. [time] s1=6 & busy -> (s1'=6);
  162. // find that channel is free
  163. [] s1=6 & free -> (s1'=7);
  164. // WAIT FOR DIFS THEN RESUME BACKOFF
  165. // let time pass
  166. [time] s1=7 & x1<DIFS & free -> (x1'=min(x1+1,TIME_MAX));
  167. // resume backoff (start again from previous backoff)
  168. [] s1=7 & (x1=DIFS | x1=DIFS-1) -> (s1'=5) & (x1'=0);
  169. // found channel busy
  170. [] s1=7 & busy -> (s1'=6) & (x1'=0);
  171. // VULNERABLE
  172. // let time pass
  173. [time] s1=8 & x1<VULN -> (x1'=min(x1+1,TIME_MAX));
  174. // move to transmit
  175. [send1] s1=8 & (x1=VULN | x1=VULN-1) -> (s1'=9) & (x1'=0);
  176. // TRANSMIT
  177. // let time pass
  178. [time] s1=9 & x1<TRANS_TIME_MAX -> (x1'=min(x1+1,TIME_MAX));
  179. // finish transmission successful
  180. [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=1 -> (s1'=10) & (x1'=0);
  181. // finish transmission garbled
  182. [finish1] s1=9 & x1>=TRANS_TIME_MIN & c1=2 -> (s1'=11) & (x1'=0);
  183. // WAIT FOR SIFS THEN WAIT FOR ACK
  184. // WAIT FOR SIFS i.e. c1=0
  185. // check channel and busy: go into backoff
  186. [] s1=10 & c1=0 & x1=0 & busy -> (s1'=2);
  187. // check channel and free: let time pass
  188. [time] s1=10 & c1=0 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
  189. // let time pass
  190. // following guard is always false as SIFS=1
  191. // [time] s1=10 & c1=0 & x1>0 & x1<SIFS -> (x1'=min(x1+1,TIME_MAX));
  192. // ack is sent after SIFS (since SIFS-1=0 add condition that channel is free)
  193. [send1] s1=10 & c1=0 & (x1=SIFS | (x1=SIFS-1 & free)) -> (s1'=10) & (x1'=0);
  194. // WAIT FOR ACK i.e. c1=1
  195. // let time pass
  196. [time] s1=10 & c1=1 & x1<ACK -> (x1'=min(x1+1,TIME_MAX));
  197. // get acknowledgement so packet sent correctly and move to done
  198. [finish1] s1=10 & c1=1 & (x1=ACK | x1=ACK-1) -> (s1'=12) & (x1'=0) & (bc1'=0);
  199. // WAIT FOR ACK_TO
  200. // check channel and busy: go into backoff
  201. [] s1=11 & x1=0 & busy -> (s1'=2);
  202. // check channel and free: let time pass
  203. [time] s1=11 & x1=0 & free -> (x1'=min(x1+1,TIME_MAX));
  204. // let time pass
  205. [time] s1=11 & x1>0 & x1<ACK_TO -> (x1'=min(x1+1,TIME_MAX));
  206. // no acknowledgement (go to backoff waiting DIFS first)
  207. [] s1=11 & x1=ACK_TO -> (s1'=3) & (x1'=0);
  208. // DONE
  209. [time] s1=12 -> (s1'=12);
  210. endmodule
  211. // ---------------------------------------------------------------------------- //
  212. // STATION 2 (rename STATION 1)
  213. module
  214. station2=station1[x1=x2,
  215. s1=s2,
  216. s2=s1,
  217. c1=c2,
  218. c2=c1,
  219. slot1=slot2,
  220. backoff1=backoff2,
  221. bc1=bc2,
  222. send1=send2,
  223. finish1=finish2]
  224. endmodule
  225. // ---------------------------------------------------------------------------- //
  226. label "twoCollisions" = col=2;
  227. label "fourCollisions" = col=4;
  228. label "sixCollisions" = col=6;