property files and a script

Former-commit-id: 7f41447df4
9 years ago · ea46ef78d0
55 changed files with 124 additions and 6 deletions
--- a/examples/multi-objective/mdp/benchmarks_numerical.sh
+++ b/examples/multi-objective/mdp/benchmarks_numerical.sh
@ -0,0 +1,64 @@
+#!/bin/sh
+
+mkdir benchmarks_numerical
+
+
+executable=../../../../prism/prism-4.3-src/bin/prism 
+options='-epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g'
+modelcommand=
+propertycommand=
+logfilepostfix='.prism.output'
+$executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_3_2$logfilepostfix 
+$executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_4_2$logfilepostfix 
+$executable $modelcommand consensus/consensus2_5_2.nm $propertycommand consensus/consensus2_5_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_5_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_3_2.nm $propertycommand consensus/consensus3_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_3_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_4_2.nm $propertycommand consensus/consensus3_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_4_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_5_2.nm $propertycommand consensus/consensus3_5_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_5_2$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf4.nm $propertycommand zeroconf/zeroconf4_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf4$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf6.nm $propertycommand zeroconf/zeroconf6_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf6$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf8.nm $propertycommand zeroconf/zeroconf8_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf8$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb2_14.nm $propertycommand zeroconf-tb/zeroconf-tb2_14_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb2_14$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb4_10.nm $propertycommand zeroconf-tb/zeroconf-tb4_10_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb4_10$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb4_14.nm $propertycommand zeroconf-tb/zeroconf-tb4_14_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb4_14$logfilepostfix 
+$executable $modelcommand team/team2obj_3.nm $propertycommand team/team2obj_3_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_3$logfilepostfix 
+$executable $modelcommand team/team3obj_3.nm $propertycommand team/team3obj_3_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_3$logfilepostfix 
+$executable $modelcommand team/team2obj_4.nm $propertycommand team/team2obj_4_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_4$logfilepostfix 
+$executable $modelcommand team/team3obj_4.nm $propertycommand team/team3obj_4_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_4$logfilepostfix 
+$executable $modelcommand team/team2obj_5.nm $propertycommand team/team2obj_5_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_5$logfilepostfix 
+$executable $modelcommand team/team3obj_5.nm $propertycommand team/team3obj_5_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_5$logfilepostfix 
+$executable $modelcommand scheduler/scheduler05.nm $propertycommand scheduler/scheduler05_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler05$logfilepostfix 
+$executable $modelcommand scheduler/scheduler25.nm $propertycommand scheduler/scheduler25_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler25$logfilepostfix 
+$executable $modelcommand scheduler/scheduler50.nm $propertycommand scheduler/scheduler50_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler50$logfilepostfix 
+$executable $modelcommand dpm/dpm100.nm $propertycommand dpm/dpm100_numerical.pctl $options | tee  benchmarks_numerical/7_dpm100$logfilepostfix 
+$executable $modelcommand dpm/dpm200.nm $propertycommand dpm/dpm200_numerical.pctl $options | tee  benchmarks_numerical/7_dpm200$logfilepostfix 
+$executable $modelcommand dpm/dpm300.nm $propertycommand dpm/dpm300_numerical.pctl $options | tee  benchmarks_numerical/7_dpm300$logfilepostfix 
+
+executable=../../../../prism/prism-4.3-src/bin/prism 
+options='-epsilon 0.000001 -paretoepsilon 0.0001 -sparse -javamaxmem 3g -gs'
+modelcommand=
+propertycommand=
+logfilepostfix='.prism-gs.output'
+$executable $modelcommand consensus/consensus2_3_2.nm $propertycommand consensus/consensus2_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_3_2$logfilepostfix 
+$executable $modelcommand consensus/consensus2_4_2.nm $propertycommand consensus/consensus2_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_4_2$logfilepostfix 
+$executable $modelcommand consensus/consensus2_5_2.nm $propertycommand consensus/consensus2_5_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus2_5_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_3_2.nm $propertycommand consensus/consensus3_3_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_3_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_4_2.nm $propertycommand consensus/consensus3_4_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_4_2$logfilepostfix 
+$executable $modelcommand consensus/consensus3_5_2.nm $propertycommand consensus/consensus3_5_2_numerical.pctl $options | tee  benchmarks_numerical/1_consensus3_5_2$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf4.nm $propertycommand zeroconf/zeroconf4_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf4$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf6.nm $propertycommand zeroconf/zeroconf6_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf6$logfilepostfix 
+$executable $modelcommand zeroconf/zeroconf8.nm $propertycommand zeroconf/zeroconf8_numerical.pctl $options | tee  benchmarks_numerical/2_zeroconf8$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb2_14.nm $propertycommand zeroconf-tb/zeroconf-tb2_14_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb2_14$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb4_10.nm $propertycommand zeroconf-tb/zeroconf-tb4_10_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb4_10$logfilepostfix 
+$executable $modelcommand zeroconf-tb/zeroconf-tb4_14.nm $propertycommand zeroconf-tb/zeroconf-tb4_14_numerical.pctl $options | tee  benchmarks_numerical/3_zeroconf-tb4_14$logfilepostfix 
+$executable $modelcommand team/team2obj_3.nm $propertycommand team/team2obj_3_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_3$logfilepostfix 
+$executable $modelcommand team/team3obj_3.nm $propertycommand team/team3obj_3_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_3$logfilepostfix 
+$executable $modelcommand team/team2obj_4.nm $propertycommand team/team2obj_4_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_4$logfilepostfix 
+$executable $modelcommand team/team3obj_4.nm $propertycommand team/team3obj_4_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_4$logfilepostfix 
+$executable $modelcommand team/team2obj_5.nm $propertycommand team/team2obj_5_numerical.pctl $options | tee  benchmarks_numerical/4_team2obj_5$logfilepostfix 
+$executable $modelcommand team/team3obj_5.nm $propertycommand team/team3obj_5_numerical.pctl $options | tee  benchmarks_numerical/5_team3obj_5$logfilepostfix 
+$executable $modelcommand scheduler/scheduler05.nm $propertycommand scheduler/scheduler05_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler05$logfilepostfix 
+$executable $modelcommand scheduler/scheduler25.nm $propertycommand scheduler/scheduler25_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler25$logfilepostfix 
+$executable $modelcommand scheduler/scheduler50.nm $propertycommand scheduler/scheduler50_numerical.pctl $options | tee  benchmarks_numerical/6_scheduler50$logfilepostfix 
+$executable $modelcommand dpm/dpm100.nm $propertycommand dpm/dpm100_numerical.pctl $options | tee  benchmarks_numerical/7_dpm100$logfilepostfix 
+$executable $modelcommand dpm/dpm200.nm $propertycommand dpm/dpm200_numerical.pctl $options | tee  benchmarks_numerical/7_dpm200$logfilepostfix 
+$executable $modelcommand dpm/dpm300.nm $propertycommand dpm/dpm300_numerical.pctl $options | tee  benchmarks_numerical/7_dpm300$logfilepostfix 
--- a/examples/multi-objective/mdp/consensus/consensus2_3_2_numerical.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus2_3_2_numerical.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], P>=0.8916673903 [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus2_3_2_pareto.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus2_3_2_pareto.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus2_4_2_numerical.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus2_4_2_numerical.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], P>=0.9882640457 [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus2_4_2_pareto.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus2_4_2_pareto.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus2_5_2_numerical.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus2_5_2_numerical.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], P>=0.9987286134 [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus2_5_2_pareto.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus2_5_2_pareto.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus3_3_2_numerical.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus3_3_2_numerical.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], P>=0.7709112445 [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus3_3_2_pareto.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus3_3_2_pareto.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus3_4_2_numerical.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus3_4_2_numerical.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], P>=0.9475183421 [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus3_4_2_pareto.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus3_4_2_pareto.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus3_5_2_numerical.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus3_5_2_numerical.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], P>=0.9879770423 [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/consensus/consensus3_5_2_pareto.pctl
+++ b/examples/multi-objective/mdp/consensus/consensus3_5_2_pareto.pctl
@ -0,0 +1 @@
+multi(Pmax=? [ F "one_proc_err" ], Pmax=? [ G "one_coin_ok" ]) 
--- a/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl
+++ b/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl
@ -0,0 +1,3 @@
+ multi(R{"power"}min=? [ C<=100 ], R{"queue"}<=70 [ C<=100 ]); 
+// Note: The property file from http://www.prismmodelchecker.org/files/atva12mo/ does not provide a threshold for the second objective.
+// We pick a threshold that intersects the pareto curve.
--- a/examples/multi-objective/mdp/dpm/dpm100_pareto.pctl
+++ b/examples/multi-objective/mdp/dpm/dpm100_pareto.pctl
@ -0,0 +1 @@
+ multi(R{"power"}min=? [ C<=100 ], R{"queue"}min=? [ C<=100 ]) 
--- a/examples/multi-objective/mdp/dpm/dpm200_numerical.pctl
+++ b/examples/multi-objective/mdp/dpm/dpm200_numerical.pctl
@ -0,0 +1,3 @@
+ multi(R{"power"}min=? [ C<=200 ], R{"queue"}<=170 [ C<=200 ]) 
+// Note: The property file from http://www.prismmodelchecker.org/files/atva12mo/ does not provide a threshold for the second objective.
+// We pick a threshold that intersects the pareto curve.
--- a/examples/multi-objective/mdp/dpm/dpm200_pareto.pctl
+++ b/examples/multi-objective/mdp/dpm/dpm200_pareto.pctl
@ -0,0 +1 @@
+ multi(R{"power"}min=? [ C<=200 ], R{"queue"}min=? [ C<=200 ]) 
--- a/examples/multi-objective/mdp/dpm/dpm300_numerical.pctl
+++ b/examples/multi-objective/mdp/dpm/dpm300_numerical.pctl
@ -0,0 +1,3 @@
+ multi(R{"power"}min=? [ C<=300 ], R{"queue"}<=270 [ C<=300 ]) 
+// Note: The property file from http://www.prismmodelchecker.org/files/atva12mo/ does not provide a threshold for the second objective.
+// We pick a threshold that intersects the pareto curve.
--- a/examples/multi-objective/mdp/dpm/dpm300_pareto.pctl
+++ b/examples/multi-objective/mdp/dpm/dpm300_pareto.pctl
@ -0,0 +1 @@
+ multi(R{"power"}min=? [ C<=300 ], R{"queue"}min=? [ C<=300 ]) 
--- a/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl
+++ b/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl
@ -0,0 +1 @@
+ multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) 
--- a/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl
+++ b/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl
@ -0,0 +1 @@
+  multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) 
--- a/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl
+++ b/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl
@ -0,0 +1 @@
+ multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) 
--- a/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl
+++ b/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl
@ -0,0 +1 @@
+  multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) 
--- a/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl
+++ b/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl
@ -0,0 +1 @@
+ multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) 
--- a/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl
+++ b/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl
@ -0,0 +1 @@
+  multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) 
--- a/examples/multi-objective/mdp/team/team2obj_3_numerical.pctl
+++ b/examples/multi-objective/mdp/team/team2obj_3_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ]) 
--- a/examples/multi-objective/mdp/team/team2obj_3_pareto.pctl
+++ b/examples/multi-objective/mdp/team/team2obj_3_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ]) 
--- a/examples/multi-objective/mdp/team/team2obj_4_numerical.pctl
+++ b/examples/multi-objective/mdp/team/team2obj_4_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ]) 
--- a/examples/multi-objective/mdp/team/team2obj_4_pareto.pctl
+++ b/examples/multi-objective/mdp/team/team2obj_4_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ]) 
--- a/examples/multi-objective/mdp/team/team2obj_5_numerical.pctl
+++ b/examples/multi-objective/mdp/team/team2obj_5_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ]) 
--- a/examples/multi-objective/mdp/team/team2obj_5_pareto.pctl
+++ b/examples/multi-objective/mdp/team/team2obj_5_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ]) 
--- a/examples/multi-objective/mdp/team/team3obj_3_numerical.pctl
+++ b/examples/multi-objective/mdp/team/team3obj_3_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.210204082 [ C ],  P>=0.5 [ F task2_completed ]) 
--- a/examples/multi-objective/mdp/team/team3obj_3_pareto.pctl
+++ b/examples/multi-objective/mdp/team/team3obj_3_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ], Pmax=? [ F task2_completed ]) 
--- a/examples/multi-objective/mdp/team/team3obj_4_numerical.pctl
+++ b/examples/multi-objective/mdp/team/team3obj_4_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.423469388 [ C ],  P>=0.5 [ F task2_completed ]) 
--- a/examples/multi-objective/mdp/team/team3obj_4_pareto.pctl
+++ b/examples/multi-objective/mdp/team/team3obj_4_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ], Pmax=? [ F task2_completed ]) 
--- a/examples/multi-objective/mdp/team/team3obj_5_numerical.pctl
+++ b/examples/multi-objective/mdp/team/team3obj_5_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}>=2.753061224 [ C ],  P>=0.5 [ F task2_completed ]) 
--- a/examples/multi-objective/mdp/team/team3obj_5_pareto.pctl
+++ b/examples/multi-objective/mdp/team/team3obj_5_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ], Pmax=? [ F task2_completed ]) 
--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm
@ -117,7 +117,7 @@ endmodule
 //-------------------------------------------------------------
 // error automaton for the environment assumption
 // do not get a reply when K probes are sent
-const int M; // time between sending and receiving a message
+const int M=1; // time between sending and receiving a message

 module env_error2

--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_numerical.pctl
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F time_error=1 ] , P>=0.81[ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_pareto.pctl
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F time_error=1 ] , Pmax=? [ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm
@ -117,7 +117,7 @@ endmodule
 //-------------------------------------------------------------
 // error automaton for the environment assumption
 // do not get a reply when K probes are sent
-const int M; // time between sending and receiving a message
+const int M=1; // time between sending and receiving a message

 module env_error4

--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_numerical.pctl
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F time_error=1 ] , P>=0.993141[ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_pareto.pctl
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F time_error=1 ] , Pmax=? [ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm
@ -117,7 +117,7 @@ endmodule
 //-------------------------------------------------------------
 // error automaton for the environment assumption
 // do not get a reply when K probes are sent
-const int M; // time between sending and receiving a message
+const int M=1; // time between sending and receiving a message

 module env_error4

--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_numerical.pctl
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F time_error=1 ] , P>=0.993141[ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_pareto.pctl
+++ b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F time_error=1 ] , Pmax=? [ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf/zeroconf4.nm
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf4.nm
@ -117,7 +117,7 @@ endmodule
 //-------------------------------------------------------------
 // error automaton for the environment assumption
 // do not get a reply when K probes are sent
-const int M; // time between sending and receiving a message
+const int M=1; // time between sending and receiving a message

 module env_error4

--- a/examples/multi-objective/mdp/zeroconf/zeroconf4_numerical.pctl
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf4_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.993141[ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf/zeroconf4_pareto.pctl
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf4_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F l=4 & ip=1 ] , Pmax=? [ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf/zeroconf6.nm
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf6.nm
@ -117,7 +117,7 @@ endmodule
 //-------------------------------------------------------------
 // error automaton for the environment assumption
 // do not get a reply when K probes are sent
-const int M; // time between sending and receiving a message
+const int M=1; // time between sending and receiving a message

 module env_error6

--- a/examples/multi-objective/mdp/zeroconf/zeroconf6_numerical.pctl
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf6_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.9997523901[ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf/zeroconf6_pareto.pctl
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf6_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F l=4 & ip=1 ] , Pmax=? [ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf/zeroconf8.nm
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf8.nm
@ -117,7 +117,7 @@ endmodule
 //-------------------------------------------------------------
 // error automaton for the environment assumption
 // do not get a reply when K probes are sent
-const int M; // time between sending and receiving a message
+const int M=1; // time between sending and receiving a message

 module env_error8

--- a/examples/multi-objective/mdp/zeroconf/zeroconf8_numerical.pctl
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf8_numerical.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F l=4 & ip=1 ] , P>=0.9999910613[ G (error=0) ])
--- a/examples/multi-objective/mdp/zeroconf/zeroconf8_pareto.pctl
+++ b/examples/multi-objective/mdp/zeroconf/zeroconf8_pareto.pctl
@ -0,0 +1 @@
+ multi(Pmax=? [ F l=4 & ip=1 ] , Pmax=? [ G (error=0) ])