From 09e52e3348c6032a4f76a31b2232f269fabf968f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Thu, 23 Jul 2009 12:52:24 +0000 Subject: [PATCH] Zeroconf model closer to benchmark one. git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@1320 bbc10eb1-c90d-0410-af57-cb519fbb1720 --- prism-examples/zeroconf/auto | 20 +++++++++---------- prism-examples/zeroconf/zeroconf.nm | 2 +- .../zeroconf/zeroconf_time_bounded.nm | 2 +- 3 files changed, 12 insertions(+), 12 deletions(-) diff --git a/prism-examples/zeroconf/auto b/prism-examples/zeroconf/auto index 835295aa..3750cdcf 100755 --- a/prism-examples/zeroconf/auto +++ b/prism-examples/zeroconf/auto @@ -1,22 +1,22 @@ #!/bin/csh # example command for minimum probabilistic reachability -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=true -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=false -prop 1 # example command for maximum probabilistic reachability -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=true -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=false -prop 1 # example command for minimum expected reachability -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=true -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=false -prop 1 # example command for maximum expected reachability -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=true -prop 1 -prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,loss=0.1,err=0,reset=false -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=true -prop 1 +prism zeroconf.nm zeroconf.pctl -const N=1000,K=4,err=0,reset=false -prop 1 # example command for time bounded reachability -prism zeroconf_time_bounded.nm zeroconf_time_bounded.pctl -const N=1000,K=1,loss=0.1,T=11,bound=10,reset=true -fixdl -prism zeroconf_time_bounded.nm zeroconf_time_bounded.pctl -const N=1000,K=1,loss=0.1,T=11,bound=10,reset=false -fixdl +prism zeroconf_time_bounded.nm zeroconf_time_bounded.pctl -const N=1000,K=1,T=11,bound=10,reset=true -fixdl +prism zeroconf_time_bounded.nm zeroconf_time_bounded.pctl -const N=1000,K=1,T=11,bound=10,reset=false -fixdl diff --git a/prism-examples/zeroconf/zeroconf.nm b/prism-examples/zeroconf/zeroconf.nm index 202de862..5f2c44d9 100644 --- a/prism-examples/zeroconf/zeroconf.nm +++ b/prism-examples/zeroconf/zeroconf.nm @@ -54,7 +54,7 @@ mdp // VARIABLES const int N; // number of abstract hosts const int K; // number of probes to send -const double loss; // probability of message loss +const double loss = 0.1; // probability of message loss // PROBABILITIES const double old = N/65024; // probability pick an ip address being used diff --git a/prism-examples/zeroconf/zeroconf_time_bounded.nm b/prism-examples/zeroconf/zeroconf_time_bounded.nm index df2ad776..4ce3bd0c 100644 --- a/prism-examples/zeroconf/zeroconf_time_bounded.nm +++ b/prism-examples/zeroconf/zeroconf_time_bounded.nm @@ -55,7 +55,7 @@ mdp // VARIABLES const int N; // number of abstract hosts const int K; // number of probes to send -const double loss; // probability of message loss +const double loss = 0.1; // probability of message loss // PROBABILITIES const double old = N/65024; // probability pick an ip address being used