diff --git a/prism/benchmark.org b/prism/benchmark.org
index 1110d317f8106c5b2e82bb93372b90f22ea0c709..c58a203191dbeef5dbf8b30821a5ef39d762f914 100644
--- a/prism/benchmark.org
+++ b/prism/benchmark.org
@@ -42,63 +42,66 @@
used to parameterise benchmarks.
#+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 |
- | coin2 | consensus/coin2.nm | mdp | K, k |
- | coin4 | consensus/coin4.nm | mdp | K, k |
- | csma2_2 | csma/csma2_2.nm | mdp | k |
- | csma2_4 | csma/csma2_4.nm | mdp | k |
- | csma2_6 | csma/csma2_6.nm | mdp | k |
- | csma3_2 | csma/csma3_2.nm | mdp | k |
- | csma3_4 | csma/csma3_4.nm | mdp | k |
- | csma4_2 | csma/csma4_2.nm | mdp | k |
- | dice | dice/dice.pm | dtmc | |
- | two_dice_knuth | dice/two_dice_knuth.pm | dtmc | |
- | two_dice | dice/two_dice.nm | mdp | |
- | dining_crypt3 | dining_crypt/dining_crypt3.nm | mdp | k |
- | dining_crypt4 | dining_crypt/dining_crypt4.nm | mdp | k |
- | dining_crypt5 | dining_crypt/dining_crypt5.nm | mdp | k |
- | dining_crypt6 | dining_crypt/dining_crypt6.nm | mdp | k |
- | dining_crypt7 | dining_crypt/dining_crypt7.nm | mdp | k |
- | embedded | embedded/embedded.sm | ctmc | MAX_COUNT, T |
- | firewire_abst_firewire | firewire/abst/firewire.nm | mdp | delay, fast |
- | firewire_abst_deadline | firewire/abst/deadline.nm | mdp | deadline, delay, fast |
- | firewire_impl_firewire | firewire/impl/firewire.nm | mdp | delay, fast |
- | firewire_impl_deadline | firewire/impl/deadline.nm | mdp | deadline, delay, fast |
- | fms | fms/fms.sm | ctmc | n |
- | kanban | kanban/kanban.sm | ctmc | t |
- | leader_sync_3_2 | leader/synchronous/leader3_2.pm | dtmc | L |
- | leader_sync_3_3 | leader/synchronous/leader3_3.pm | dtmc | L |
- | leader_sync_3_4 | leader/synchronous/leader3_4.pm | dtmc | L |
- | leader_sync_4_2 | leader/synchronous/leader4_2.pm | dtmc | L |
- | leader_sync_4_3 | leader/synchronous/leader4_3.pm | dtmc | L |
- | leader_sync_4_4 | leader/synchronous/leader4_4.pm | dtmc | L |
- | leader_sync_5_2 | leader/synchronous/leader5_2.pm | dtmc | L |
- | leader_sync_5_3 | leader/synchronous/leader5_3.pm | dtmc | L |
- | leader_sync_5_4 | leader/synchronous/leader5_4.pm | dtmc | L |
- | leader_async3 | leader/asynchronous/leader3.nm | mdp | K |
- | leader_async4 | leader/asynchronous/leader4.nm | mdp | K |
- | leader_async5 | leader/asynchronous/leader5.nm | mdp | K |
- | nacl | molecules/nacl.sm | ctmc | N1, N2, T, i |
- | knacl | molecules/knacl.sm | ctmc | N1, N2, N3, T, i |
- | mc | molecules/mc.sm | ctmc | N1, N2, T, i |
- | mutual3 | mutual/mutual3.nm | mdp | |
- | mutual4 | mutual/mutual4.nm | mdp | |
- | mutual5 | mutual/mutual5.nm | mdp | |
- | mutual8 | mutual/mutual8.nm | mdp | |
- | mutual10 | mutual/mutual10.nm | mdp | |
- | peer2peer | peer2peer/peer2peerN_K.sm | ctmc | N, K, T |
- | phil_original | phil/original/philN.nm | mdp | N |
- | phil_nofair | phil/nofair/phil-nofairN.nm | mdp | K |
- | poll | polling/pollN.sm | ctmc | T |
- | rabin | rabin/rabinN.nm | mdp | N |
- | beauquier | self-stabilisation/beauquier/beauquierN.nm | mdp | N, K, k |
- | 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 |
+ | 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 |
+ | coin2 | consensus/coin2.nm | mdp | K, k |
+ | coin4 | consensus/coin4.nm | mdp | K, k |
+ | csma2_2 | csma/csma2_2.nm | mdp | k |
+ | csma2_4 | csma/csma2_4.nm | mdp | k |
+ | csma2_6 | csma/csma2_6.nm | mdp | k |
+ | csma3_2 | csma/csma3_2.nm | mdp | k |
+ | csma3_4 | csma/csma3_4.nm | mdp | k |
+ | csma4_2 | csma/csma4_2.nm | mdp | k |
+ | dice | dice/dice.pm | dtmc | |
+ | two_dice_knuth | dice/two_dice_knuth.pm | dtmc | |
+ | two_dice | dice/two_dice.nm | mdp | |
+ | dining_crypt3 | dining_crypt/dining_crypt3.nm | mdp | k |
+ | dining_crypt4 | dining_crypt/dining_crypt4.nm | mdp | k |
+ | dining_crypt5 | dining_crypt/dining_crypt5.nm | mdp | k |
+ | dining_crypt6 | dining_crypt/dining_crypt6.nm | mdp | k |
+ | dining_crypt7 | dining_crypt/dining_crypt7.nm | mdp | k |
+ | embedded | embedded/embedded.sm | ctmc | MAX_COUNT, T |
+ | firewire_abst_firewire | firewire/abst/firewire.nm | mdp | delay, fast |
+ | firewire_abst_deadline | firewire/abst/deadline.nm | mdp | deadline, delay, fast |
+ | firewire_impl_firewire | firewire/impl/firewire.nm | mdp | delay, fast |
+ | firewire_impl_deadline | firewire/impl/deadline.nm | mdp | deadline, delay, fast |
+ | fms | fms/fms.sm | ctmc | n |
+ | kanban | kanban/kanban.sm | ctmc | t |
+ | leader_sync_3_2 | leader/synchronous/leader3_2.pm | dtmc | L |
+ | leader_sync_3_3 | leader/synchronous/leader3_3.pm | dtmc | L |
+ | leader_sync_3_4 | leader/synchronous/leader3_4.pm | dtmc | L |
+ | leader_sync_4_2 | leader/synchronous/leader4_2.pm | dtmc | L |
+ | leader_sync_4_3 | leader/synchronous/leader4_3.pm | dtmc | L |
+ | leader_sync_4_4 | leader/synchronous/leader4_4.pm | dtmc | L |
+ | leader_sync_5_2 | leader/synchronous/leader5_2.pm | dtmc | L |
+ | leader_sync_5_3 | leader/synchronous/leader5_3.pm | dtmc | L |
+ | leader_sync_5_4 | leader/synchronous/leader5_4.pm | dtmc | L |
+ | leader_async3 | leader/asynchronous/leader3.nm | mdp | K |
+ | leader_async4 | leader/asynchronous/leader4.nm | mdp | K |
+ | leader_async5 | leader/asynchronous/leader5.nm | mdp | K |
+ | nacl | molecules/nacl.sm | ctmc | N1, N2, T, i |
+ | knacl | molecules/knacl.sm | ctmc | N1, N2, N3, T, i |
+ | mc | molecules/mc.sm | ctmc | N1, N2, T, i |
+ | mutual3 | mutual/mutual3.nm | mdp | |
+ | mutual4 | mutual/mutual4.nm | mdp | |
+ | mutual5 | mutual/mutual5.nm | mdp | |
+ | mutual8 | mutual/mutual8.nm | mdp | |
+ | mutual10 | mutual/mutual10.nm | mdp | |
+ | peer2peer | peer2peer/peer2peerN_K.sm | ctmc | N, K, T |
+ | phil_original | phil/original/philN.nm | mdp | N |
+ | phil_nofair | phil/nofair/phil-nofairN.nm | mdp | K |
+ | poll | polling/pollN.sm | ctmc | T |
+ | rabin | rabin/rabinN.nm | mdp | N |
+ | beauquier | self-stabilisation/beauquier/beauquierN.nm | mdp | N, K, k |
+ | 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 |