Add wlan benchmarks

prism/benchmark.org

@@ -43,7 +43,7 @@
 
    #+NAME: models
    | Name                   | Model file                                 | Model type | Constants                   |
-   |------------------------+--------------------------------------------+------------+-----------------------|
+   |------------------------+--------------------------------------------+------------+-----------------------------|
    | brp                    | brp/brp.pm                                 | dtmc       | N, MAX                      |
    | cell                   | cell/cell.sm                               | ctmc       | N                           |
    | cluster                | cluster/cluster.sm                         | ctmc       | N, T                        |
@@ -99,6 +99,9 @@
    | herman                 | self-stabilisation/herman/hermanN.pm       | dtmc       | N, K, k                     |
    | israeli-jalfon         | self-stabilisation/israeli-jalfon/ijN.nm   | mdp        | N, K, k                     |
    | tandem                 | tandem/tandem.sm                           | ctmc       | T, c                        |
+   | wlan                   | wlan/wlanK.nm                              | mdp        | TRANS_TIME_MAX, k, K        |
+   | wlan_collide           | wlan/wlanK_collide.nm                      | mdp        | COL, TRANS_TIME_MAX, k, K   |
+   | wlan_time_bounded      | wlan/wlanK_time_bounded.nm                 | mdp        | TRANS_TIME_MAX, DEADLINE, K |
 
    We have to import this table into python for later reference:
 
@@ -1104,3 +1107,50 @@
    | tandem | T=1,c=63  | sc        |  0.454109282 |
    | tandem | T=1,c=127 | sc        |  2.150405680 |
    | tandem | T=1,c=255 | sc        | 10.081655538 |
+
+** WLAN
+
+   #+BEGIN_QUOTE
+   This case study concerns the IEEE 802.11 Wireless LAN
+
+   We consider the scenario where two stations trying to send packets simultaneously.
+
+   The PRISM model is taken from [KNS02a] using the integer semantics given in [KNS06]. In the model one time unit
+   corresponds to 50μs and to ensure integer bounds, where neccessary, scaling lower bound constraints down and
+   upper bound constraints up to sensure a sound abstraction.
+
+   For more information on the probabilistic timed automata see: http://www.prismmodelchecker.org/casestudies/wlan.php
+   #+END_QUOTE
+
+   Benchmarks:
+
+   We initially partition on the state of the medium: Are messages being sent
+   and are they transmitted correctly or garbled.
+
+   #+NAME: wlan_benchmarks
+   | Model             | Constants                          | Partition |
+   |-------------------+------------------------------------+-----------|
+   | wlan              | TRANS_TIME_MAX=10,k=2,K=0          | c1,c2     |
+   | wlan              | TRANS_TIME_MAX=10,k=2,K=1          | c1,c2     |
+   | wlan              | TRANS_TIME_MAX=10,k=2,K=2          | c1,c2     |
+   | wlan_collide      | COL=2,TRANS_TIME_MAX=10,k=2,K=0    | c1,c2     |
+   | wlan_collide      | COL=2,TRANS_TIME_MAX=10,k=2,K=2    | c1,c2     |
+   | wlan_collide      | COL=2,TRANS_TIME_MAX=10,k=2,K=3    | c1,c2     |
+   | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2     |
+   | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2     |
+
+   Results:
+
+   #+CALL: bench(wlan_benchmarks)
+
+   #+RESULTS:
+   | Model             | Constants                          | Partition |      Time(s) |
+   |-------------------+------------------------------------+-----------+--------------|
+   | wlan              | TRANS_TIME_MAX=10,k=2,K=0          | c1,c2     |  2.454806027 |
+   | wlan              | TRANS_TIME_MAX=10,k=2,K=1          | c1,c2     |  2.501042125 |
+   | wlan              | TRANS_TIME_MAX=10,k=2,K=2          | c1,c2     |  2.495283789 |
+   | wlan_collide      | COL=2,TRANS_TIME_MAX=10,k=2,K=0    | c1,c2     |  2.523926107 |
+   | wlan_collide      | COL=2,TRANS_TIME_MAX=10,k=2,K=2    | c1,c2     |  2.534154258 |
+   | wlan_collide      | COL=2,TRANS_TIME_MAX=10,k=2,K=3    | c1,c2     |  2.611946316 |
+   | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=0 | c1,c2     | 25.584948198 |
+   | wlan_time_bounded | TRANS_TIME_MAX=10,DEADLINE=100,K=1 | c1,c2     | 67.281157195 |