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

@@ -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
 

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

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