From ea46ef78d0db4a5baa6f8f9178d592cc781a8cbb Mon Sep 17 00:00:00 2001 From: TimQu Date: Sun, 12 Jun 2016 17:08:12 +0200 Subject: [PATCH] property files and a script Former-commit-id: 7f41447df479282dd43c6d7e7a1ed2183df6145b --- .../mdp/benchmarks_numerical.sh | 64 +++++++++++++++++++ .../consensus/consensus2_3_2_numerical.pctl | 1 + .../mdp/consensus/consensus2_3_2_pareto.pctl | 1 + .../consensus/consensus2_4_2_numerical.pctl | 1 + .../mdp/consensus/consensus2_4_2_pareto.pctl | 1 + .../consensus/consensus2_5_2_numerical.pctl | 1 + .../mdp/consensus/consensus2_5_2_pareto.pctl | 1 + .../consensus/consensus3_3_2_numerical.pctl | 1 + .../mdp/consensus/consensus3_3_2_pareto.pctl | 1 + .../consensus/consensus3_4_2_numerical.pctl | 1 + .../mdp/consensus/consensus3_4_2_pareto.pctl | 1 + .../consensus/consensus3_5_2_numerical.pctl | 1 + .../mdp/consensus/consensus3_5_2_pareto.pctl | 1 + .../mdp/dpm/dpm100_numerical.pctl | 3 + .../mdp/dpm/dpm100_pareto.pctl | 1 + .../mdp/dpm/dpm200_numerical.pctl | 3 + .../mdp/dpm/dpm200_pareto.pctl | 1 + .../mdp/dpm/dpm300_numerical.pctl | 3 + .../mdp/dpm/dpm300_pareto.pctl | 1 + .../mdp/scheduler/scheduler05_numerical.pctl | 1 + .../mdp/scheduler/scheduler05_pareto.pctl | 1 + .../mdp/scheduler/scheduler25_numerical.pctl | 1 + .../mdp/scheduler/scheduler25_pareto.pctl | 1 + .../mdp/scheduler/scheduler50_numerical.pctl | 1 + .../mdp/scheduler/scheduler50_pareto.pctl | 1 + .../mdp/team/team2obj_3_numerical.pctl | 1 + .../mdp/team/team2obj_3_pareto.pctl | 1 + .../mdp/team/team2obj_4_numerical.pctl | 1 + .../mdp/team/team2obj_4_pareto.pctl | 1 + .../mdp/team/team2obj_5_numerical.pctl | 1 + .../mdp/team/team2obj_5_pareto.pctl | 1 + .../mdp/team/team3obj_3_numerical.pctl | 1 + .../mdp/team/team3obj_3_pareto.pctl | 1 + .../mdp/team/team3obj_4_numerical.pctl | 1 + .../mdp/team/team3obj_4_pareto.pctl | 1 + .../mdp/team/team3obj_5_numerical.pctl | 1 + .../mdp/team/team3obj_5_pareto.pctl | 1 + .../mdp/zeroconf-tb/zeroconf-tb2_14.nm | 2 +- .../zeroconf-tb2_14_numerical.pctl | 1 + .../zeroconf-tb/zeroconf-tb2_14_pareto.pctl | 1 + .../mdp/zeroconf-tb/zeroconf-tb4_10.nm | 2 +- .../zeroconf-tb4_10_numerical.pctl | 1 + .../zeroconf-tb/zeroconf-tb4_10_pareto.pctl | 1 + .../mdp/zeroconf-tb/zeroconf-tb4_14.nm | 2 +- .../zeroconf-tb4_14_numerical.pctl | 1 + .../zeroconf-tb/zeroconf-tb4_14_pareto.pctl | 1 + .../multi-objective/mdp/zeroconf/zeroconf4.nm | 2 +- .../mdp/zeroconf/zeroconf4_numerical.pctl | 1 + .../mdp/zeroconf/zeroconf4_pareto.pctl | 1 + .../multi-objective/mdp/zeroconf/zeroconf6.nm | 2 +- .../mdp/zeroconf/zeroconf6_numerical.pctl | 1 + .../mdp/zeroconf/zeroconf6_pareto.pctl | 1 + .../multi-objective/mdp/zeroconf/zeroconf8.nm | 2 +- .../mdp/zeroconf/zeroconf8_numerical.pctl | 1 + .../mdp/zeroconf/zeroconf8_pareto.pctl | 1 + 55 files changed, 124 insertions(+), 6 deletions(-) create mode 100755 examples/multi-objective/mdp/benchmarks_numerical.sh create mode 100644 examples/multi-objective/mdp/consensus/consensus2_3_2_numerical.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus2_3_2_pareto.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus2_4_2_numerical.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus2_4_2_pareto.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus2_5_2_numerical.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus2_5_2_pareto.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus3_3_2_numerical.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus3_3_2_pareto.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus3_4_2_numerical.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus3_4_2_pareto.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus3_5_2_numerical.pctl create mode 100644 examples/multi-objective/mdp/consensus/consensus3_5_2_pareto.pctl create mode 100644 examples/multi-objective/mdp/dpm/dpm100_numerical.pctl create mode 100644 examples/multi-objective/mdp/dpm/dpm100_pareto.pctl create mode 100644 examples/multi-objective/mdp/dpm/dpm200_numerical.pctl create mode 100644 examples/multi-objective/mdp/dpm/dpm200_pareto.pctl create mode 100644 examples/multi-objective/mdp/dpm/dpm300_numerical.pctl create mode 100644 examples/multi-objective/mdp/dpm/dpm300_pareto.pctl create mode 100644 examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl create mode 100644 examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl create mode 100644 examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl create mode 100644 examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl create mode 100644 examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl create mode 100644 examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl create mode 100644 examples/multi-objective/mdp/team/team2obj_3_numerical.pctl create mode 100644 examples/multi-objective/mdp/team/team2obj_3_pareto.pctl create mode 100644 examples/multi-objective/mdp/team/team2obj_4_numerical.pctl create mode 100644 examples/multi-objective/mdp/team/team2obj_4_pareto.pctl create mode 100644 examples/multi-objective/mdp/team/team2obj_5_numerical.pctl create mode 100644 examples/multi-objective/mdp/team/team2obj_5_pareto.pctl create mode 100644 examples/multi-objective/mdp/team/team3obj_3_numerical.pctl create mode 100644 examples/multi-objective/mdp/team/team3obj_3_pareto.pctl create mode 100644 examples/multi-objective/mdp/team/team3obj_4_numerical.pctl create mode 100644 examples/multi-objective/mdp/team/team3obj_4_pareto.pctl create mode 100644 examples/multi-objective/mdp/team/team3obj_5_numerical.pctl create mode 100644 examples/multi-objective/mdp/team/team3obj_5_pareto.pctl create mode 100644 examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_numerical.pctl create mode 100644 examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_pareto.pctl create mode 100644 examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_numerical.pctl create mode 100644 examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_pareto.pctl create mode 100644 examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_numerical.pctl create mode 100644 examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_pareto.pctl create mode 100644 examples/multi-objective/mdp/zeroconf/zeroconf4_numerical.pctl create mode 100644 examples/multi-objective/mdp/zeroconf/zeroconf4_pareto.pctl create mode 100644 examples/multi-objective/mdp/zeroconf/zeroconf6_numerical.pctl create mode 100644 examples/multi-objective/mdp/zeroconf/zeroconf6_pareto.pctl create mode 100644 examples/multi-objective/mdp/zeroconf/zeroconf8_numerical.pctl create mode 100644 examples/multi-objective/mdp/zeroconf/zeroconf8_pareto.pctl diff --git a/examples/multi-objective/mdp/benchmarks_numerical.sh b/examples/multi-objective/mdp/benchmarks_numerical.sh new file mode 100755 index 000000000..5c80dcb85 --- /dev/null +++ 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 diff --git a/examples/multi-objective/mdp/consensus/consensus2_3_2_numerical.pctl b/examples/multi-objective/mdp/consensus/consensus2_3_2_numerical.pctl new file mode 100644 index 000000000..f7bb97443 --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus2_3_2_pareto.pctl b/examples/multi-objective/mdp/consensus/consensus2_3_2_pareto.pctl new file mode 100644 index 000000000..7cd298d8e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus2_4_2_numerical.pctl b/examples/multi-objective/mdp/consensus/consensus2_4_2_numerical.pctl new file mode 100644 index 000000000..62c7737ac --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus2_4_2_pareto.pctl b/examples/multi-objective/mdp/consensus/consensus2_4_2_pareto.pctl new file mode 100644 index 000000000..7cd298d8e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus2_5_2_numerical.pctl b/examples/multi-objective/mdp/consensus/consensus2_5_2_numerical.pctl new file mode 100644 index 000000000..3b52e011e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus2_5_2_pareto.pctl b/examples/multi-objective/mdp/consensus/consensus2_5_2_pareto.pctl new file mode 100644 index 000000000..7cd298d8e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus3_3_2_numerical.pctl b/examples/multi-objective/mdp/consensus/consensus3_3_2_numerical.pctl new file mode 100644 index 000000000..4e4f8e3f7 --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus3_3_2_pareto.pctl b/examples/multi-objective/mdp/consensus/consensus3_3_2_pareto.pctl new file mode 100644 index 000000000..7cd298d8e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus3_4_2_numerical.pctl b/examples/multi-objective/mdp/consensus/consensus3_4_2_numerical.pctl new file mode 100644 index 000000000..31768966d --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus3_4_2_pareto.pctl b/examples/multi-objective/mdp/consensus/consensus3_4_2_pareto.pctl new file mode 100644 index 000000000..7cd298d8e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus3_5_2_numerical.pctl b/examples/multi-objective/mdp/consensus/consensus3_5_2_numerical.pctl new file mode 100644 index 000000000..6a3113398 --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/consensus/consensus3_5_2_pareto.pctl b/examples/multi-objective/mdp/consensus/consensus3_5_2_pareto.pctl new file mode 100644 index 000000000..7cd298d8e --- /dev/null +++ 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" ]) diff --git a/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl b/examples/multi-objective/mdp/dpm/dpm100_numerical.pctl new file mode 100644 index 000000000..f081396c7 --- /dev/null +++ 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. \ No newline at end of file diff --git a/examples/multi-objective/mdp/dpm/dpm100_pareto.pctl b/examples/multi-objective/mdp/dpm/dpm100_pareto.pctl new file mode 100644 index 000000000..19e3cd685 --- /dev/null +++ b/examples/multi-objective/mdp/dpm/dpm100_pareto.pctl @@ -0,0 +1 @@ + multi(R{"power"}min=? [ C<=100 ], R{"queue"}min=? [ C<=100 ]) diff --git a/examples/multi-objective/mdp/dpm/dpm200_numerical.pctl b/examples/multi-objective/mdp/dpm/dpm200_numerical.pctl new file mode 100644 index 000000000..916821715 --- /dev/null +++ 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. \ No newline at end of file diff --git a/examples/multi-objective/mdp/dpm/dpm200_pareto.pctl b/examples/multi-objective/mdp/dpm/dpm200_pareto.pctl new file mode 100644 index 000000000..f03284f83 --- /dev/null +++ b/examples/multi-objective/mdp/dpm/dpm200_pareto.pctl @@ -0,0 +1 @@ + multi(R{"power"}min=? [ C<=200 ], R{"queue"}min=? [ C<=200 ]) diff --git a/examples/multi-objective/mdp/dpm/dpm300_numerical.pctl b/examples/multi-objective/mdp/dpm/dpm300_numerical.pctl new file mode 100644 index 000000000..a75851347 --- /dev/null +++ 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. \ No newline at end of file diff --git a/examples/multi-objective/mdp/dpm/dpm300_pareto.pctl b/examples/multi-objective/mdp/dpm/dpm300_pareto.pctl new file mode 100644 index 000000000..bde0f5eb0 --- /dev/null +++ b/examples/multi-objective/mdp/dpm/dpm300_pareto.pctl @@ -0,0 +1 @@ + multi(R{"power"}min=? [ C<=300 ], R{"queue"}min=? [ C<=300 ]) diff --git a/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl b/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl new file mode 100644 index 000000000..09581f07f --- /dev/null +++ b/examples/multi-objective/mdp/scheduler/scheduler05_numerical.pctl @@ -0,0 +1 @@ + multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl b/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl new file mode 100644 index 000000000..36ce7ae23 --- /dev/null +++ b/examples/multi-objective/mdp/scheduler/scheduler05_pareto.pctl @@ -0,0 +1 @@ + multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) diff --git a/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl b/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl new file mode 100644 index 000000000..09581f07f --- /dev/null +++ b/examples/multi-objective/mdp/scheduler/scheduler25_numerical.pctl @@ -0,0 +1 @@ + multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl b/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl new file mode 100644 index 000000000..36ce7ae23 --- /dev/null +++ b/examples/multi-objective/mdp/scheduler/scheduler25_pareto.pctl @@ -0,0 +1 @@ + multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) diff --git a/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl b/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl new file mode 100644 index 000000000..09581f07f --- /dev/null +++ b/examples/multi-objective/mdp/scheduler/scheduler50_numerical.pctl @@ -0,0 +1 @@ + multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) \ No newline at end of file diff --git a/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl b/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl new file mode 100644 index 000000000..36ce7ae23 --- /dev/null +++ b/examples/multi-objective/mdp/scheduler/scheduler50_pareto.pctl @@ -0,0 +1 @@ + multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) diff --git a/examples/multi-objective/mdp/team/team2obj_3_numerical.pctl b/examples/multi-objective/mdp/team/team2obj_3_numerical.pctl new file mode 100644 index 000000000..f6a4553cb --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team2obj_3_pareto.pctl b/examples/multi-objective/mdp/team/team2obj_3_pareto.pctl new file mode 100644 index 000000000..636cd1772 --- /dev/null +++ b/examples/multi-objective/mdp/team/team2obj_3_pareto.pctl @@ -0,0 +1 @@ + multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ]) diff --git a/examples/multi-objective/mdp/team/team2obj_4_numerical.pctl b/examples/multi-objective/mdp/team/team2obj_4_numerical.pctl new file mode 100644 index 000000000..9cb290800 --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team2obj_4_pareto.pctl b/examples/multi-objective/mdp/team/team2obj_4_pareto.pctl new file mode 100644 index 000000000..636cd1772 --- /dev/null +++ b/examples/multi-objective/mdp/team/team2obj_4_pareto.pctl @@ -0,0 +1 @@ + multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ]) diff --git a/examples/multi-objective/mdp/team/team2obj_5_numerical.pctl b/examples/multi-objective/mdp/team/team2obj_5_numerical.pctl new file mode 100644 index 000000000..027c6ef09 --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team2obj_5_pareto.pctl b/examples/multi-objective/mdp/team/team2obj_5_pareto.pctl new file mode 100644 index 000000000..636cd1772 --- /dev/null +++ b/examples/multi-objective/mdp/team/team2obj_5_pareto.pctl @@ -0,0 +1 @@ + multi(Pmax=? [ F task1_completed ], R{"w_1_total"}max=? [ C ]) diff --git a/examples/multi-objective/mdp/team/team3obj_3_numerical.pctl b/examples/multi-objective/mdp/team/team3obj_3_numerical.pctl new file mode 100644 index 000000000..4a02276ce --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team3obj_3_pareto.pctl b/examples/multi-objective/mdp/team/team3obj_3_pareto.pctl new file mode 100644 index 000000000..8343ec77e --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team3obj_4_numerical.pctl b/examples/multi-objective/mdp/team/team3obj_4_numerical.pctl new file mode 100644 index 000000000..3712e6d0d --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team3obj_4_pareto.pctl b/examples/multi-objective/mdp/team/team3obj_4_pareto.pctl new file mode 100644 index 000000000..8343ec77e --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team3obj_5_numerical.pctl b/examples/multi-objective/mdp/team/team3obj_5_numerical.pctl new file mode 100644 index 000000000..541c02e9c --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/team/team3obj_5_pareto.pctl b/examples/multi-objective/mdp/team/team3obj_5_pareto.pctl new file mode 100644 index 000000000..8343ec77e --- /dev/null +++ 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 ]) diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14.nm index 30dfd9e08..98e49695d 100644 --- 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 diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_numerical.pctl b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_numerical.pctl new file mode 100644 index 000000000..e8119cae5 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_pareto.pctl b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb2_14_pareto.pctl new file mode 100644 index 000000000..db9996245 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10.nm index 05c500235..daa91773c 100644 --- 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 diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_numerical.pctl b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_numerical.pctl new file mode 100644 index 000000000..84762f3cc --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_pareto.pctl b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_10_pareto.pctl new file mode 100644 index 000000000..db9996245 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14.nm index b91ec7995..83b540290 100644 --- 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 diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_numerical.pctl b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_numerical.pctl new file mode 100644 index 000000000..84762f3cc --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_pareto.pctl b/examples/multi-objective/mdp/zeroconf-tb/zeroconf-tb4_14_pareto.pctl new file mode 100644 index 000000000..db9996245 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf4.nm b/examples/multi-objective/mdp/zeroconf/zeroconf4.nm index 1c3bafd53..18f9109e7 100644 --- 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 diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf4_numerical.pctl b/examples/multi-objective/mdp/zeroconf/zeroconf4_numerical.pctl new file mode 100644 index 000000000..646a77159 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf4_pareto.pctl b/examples/multi-objective/mdp/zeroconf/zeroconf4_pareto.pctl new file mode 100644 index 000000000..694c19e14 --- /dev/null +++ b/examples/multi-objective/mdp/zeroconf/zeroconf4_pareto.pctl @@ -0,0 +1 @@ + multi(Pmax=? [ F l=4 & ip=1 ] , Pmax=? [ G (error=0) ]) diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf6.nm b/examples/multi-objective/mdp/zeroconf/zeroconf6.nm index cde22a032..571e154de 100644 --- 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 diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf6_numerical.pctl b/examples/multi-objective/mdp/zeroconf/zeroconf6_numerical.pctl new file mode 100644 index 000000000..016da75a6 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf6_pareto.pctl b/examples/multi-objective/mdp/zeroconf/zeroconf6_pareto.pctl new file mode 100644 index 000000000..694c19e14 --- /dev/null +++ b/examples/multi-objective/mdp/zeroconf/zeroconf6_pareto.pctl @@ -0,0 +1 @@ + multi(Pmax=? [ F l=4 & ip=1 ] , Pmax=? [ G (error=0) ]) diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf8.nm b/examples/multi-objective/mdp/zeroconf/zeroconf8.nm index e843a8c12..c43363f84 100644 --- 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 diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf8_numerical.pctl b/examples/multi-objective/mdp/zeroconf/zeroconf8_numerical.pctl new file mode 100644 index 000000000..61b79cd13 --- /dev/null +++ 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) ]) diff --git a/examples/multi-objective/mdp/zeroconf/zeroconf8_pareto.pctl b/examples/multi-objective/mdp/zeroconf/zeroconf8_pareto.pctl new file mode 100644 index 000000000..694c19e14 --- /dev/null +++ b/examples/multi-objective/mdp/zeroconf/zeroconf8_pareto.pctl @@ -0,0 +1 @@ + multi(Pmax=? [ F l=4 & ip=1 ] , Pmax=? [ G (error=0) ])