From 1bb535fc64c788eb012c5c8d976e35051d4af6ab Mon Sep 17 00:00:00 2001
From: Hans-Peter Deifel <hpd@hpdeifel.de>
Date: Fri, 24 Aug 2018 09:53:17 +0200
Subject: [PATCH] Add zeroconf benchmarks
---
prism/benchmark.org | 48 +++++++++++++++++++++++++++++++++++++++++++++
1 file changed, 48 insertions(+)
diff --git a/prism/benchmark.org b/prism/benchmark.org
index c58a203..9e65375 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 |
--
GitLab