diff --git a/prism/benchmark.org b/prism/benchmark.org index c58a203191dbeef5dbf8b30821a5ef39d762f914..9e65375e411f1f15a7c7adc995933f6a08c36917 100644 --- a/prism/benchmark.org +++ b/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 |