Add zeroconf benchmarks

prism/benchmark.org

@@ -102,6 +102,8 @@
    | 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 |
+   | zeroconf               | zeroconf/zeroconf.nm                       | mdp        | N, K, err, reset            |
+   | zeroconf_time_bounded  | zeroconf/zeroconf_time_bounded.nm          | mdp        | N, K, T, bound, reset       |
 
    We have to import this table into python for later reference:
 
@@ -1154,3 +1156,49 @@
    | 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 |
+
+** Zeroconf
+
+   #+BEGIN_QUOTE
+   This case study concerns the IPv4 Zeroconf Protocol [CAG02]
+
+   We consider the probabilistic timed automata models presented in [KNPS06] using
+   the integer semantics also presented in the paper.
+
+   For more information, see: http://www.prismmodelchecker.org/casestudies/zeroconf.php
+
+   =====================================================================================
+
+   PARAMETERS
+
+   - reset :: reset is true/false dependent on whether the reset/norest model is to be analysed
+   - loss :: probability of message (0.1, 0.01, 0.001 and 0)
+   - K :: number of probes (4 in standard) 1:1:8
+   - N :: number of concrete hosts, e.g. 20 or 1000 for small/large network
+   - err :: error cost from 1e+6 to 1e+12
+   - bound :: time bound from 0:50 (then set T to be 1+maximum value of bound in experiment)
+   #+END_QUOTE
+
+   Benchmarks:
+
+   We partition on part of the current state of the environment.
+
+   #+NAME: zeroconf_benchmarks
+   | Model                 | Constants                            | Partition |
+   |-----------------------+--------------------------------------+-----------|
+   | zeroconf              | N=1000,K=4,err=0,reset=true          | n,n0,n1,b |
+   | zeroconf              | N=1000,K=4,err=0,reset=false         | n,n0,n1,b |
+   | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true  | n,n0,n1,b |
+   | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b |
+
+   Results:
+
+   #+CALL: bench(zeroconf_benchmarks)
+
+   #+RESULTS:
+   | Model                 | Constants                            | Partition |      Time(s) |
+   |-----------------------+--------------------------------------+-----------+--------------|
+   | zeroconf              | N=1000,K=4,err=0,reset=true          | n,n0,n1,b |  0.061241483 |
+   | zeroconf              | N=1000,K=4,err=0,reset=false         | n,n0,n1,b | 35.664296268 |
+   | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=true  | n,n0,n1,b |  0.261397650 |
+   | zeroconf_time_bounded | N=1000,K=1,T=11,bound=10,reset=false | n,n0,n1,b |  1.259019603 |