diff --git a/examples/multiobjective/.gitignore b/examples/multiobjective/.gitignore new file mode 100644 index 000000000..afed0735d --- /dev/null +++ b/examples/multiobjective/.gitignore @@ -0,0 +1 @@ +*.csv diff --git a/examples/multiobjective/displaypareto/.gitignore b/examples/multiobjective/displaypareto/.gitignore new file mode 100644 index 000000000..12aacb080 --- /dev/null +++ b/examples/multiobjective/displaypareto/.gitignore @@ -0,0 +1,4 @@ +*.aux +*.log +*.synctex.gz +*.pdf diff --git a/examples/multiobjective/displaypareto/displaypareto.tex b/examples/multiobjective/displaypareto/displaypareto.tex new file mode 100644 index 000000000..17d5909b8 --- /dev/null +++ b/examples/multiobjective/displaypareto/displaypareto.tex @@ -0,0 +1,20 @@ +\documentclass{article} +\usepackage{pgfplots} +\usepackage{filecontents} + +%\newcommand{\resultPath}{../mdp/consensus/results_3_3_2/} +%\newcommand{\resultPath}{../mdp/scheduler/results05/} +\newcommand{\resultPath}{../mdp/zeroconf-tb/results4_10/} + +\begin{document} + \centering +\begin{tikzpicture}[scale=1.75] +\begin{axis}[enlargelimits=false, axis background/.style={fill=red!50}] +\addplot[fill=white] table [col sep=comma] {\resultPath overapproximation.csv} -- cycle; +\addplot[fill=green] table [col sep=comma] {\resultPath underapproximation.csv} -- cycle; +\addplot[mark=o, mark options={blue, scale=1.5, thick}, only marks] table [col sep=comma] {\resultPath paretopoints.csv}; +\addplot[mark=false] table [col sep=comma] {\resultPath boundaries.csv}; +\end{axis} +\end{tikzpicture} + +\end{document} \ No newline at end of file diff --git a/examples/multiobjective/mdp/scheduler/scheduler05_pareto.pctl b/examples/multiobjective/mdp/scheduler/scheduler05_pareto.pctl index 494a78895..b95651662 100644 --- a/examples/multiobjective/mdp/scheduler/scheduler05_pareto.pctl +++ b/examples/multiobjective/mdp/scheduler/scheduler05_pareto.pctl @@ -1,4 +1,4 @@ - multi(R{"energy"}min=?[ F "tasks_complete" ], R{"time"}min=? [ F "tasks_complete" ]) + multi(R{"time"}min=?[ F "tasks_complete" ], R{"energy"}min=? [ F "tasks_complete" ]) // Original query: //multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) // Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multiobjective/mdp/scheduler/scheduler25_pareto.pctl b/examples/multiobjective/mdp/scheduler/scheduler25_pareto.pctl index a9188a837..d818ef6d2 100644 --- a/examples/multiobjective/mdp/scheduler/scheduler25_pareto.pctl +++ b/examples/multiobjective/mdp/scheduler/scheduler25_pareto.pctl @@ -1,4 +1,4 @@ - multi(R{"energy"}min=?[ F "tasks_complete" ], R{"time"}min=? [ F "tasks_complete" ]) + multi(R{"time"}min=?[ F "tasks_complete" ], R{"energy"}min=? [ F "tasks_complete" ]) // Original query: // multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) // Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/examples/multiobjective/mdp/scheduler/scheduler50_pareto.pctl b/examples/multiobjective/mdp/scheduler/scheduler50_pareto.pctl index 74bd8ba03..9cb7bf3d0 100644 --- a/examples/multiobjective/mdp/scheduler/scheduler50_pareto.pctl +++ b/examples/multiobjective/mdp/scheduler/scheduler50_pareto.pctl @@ -1,4 +1,4 @@ - multi(R{"energy"}min=?[ F "tasks_complete" ], R{"time"}min=? [ F "tasks_complete" ]) + multi(R{"time"}min=?[ F "tasks_complete" ], R{"energy"}min=? [ F "tasks_complete" ]) // Original query: // multi(R{"energy"}min=?[ C ], R{"time"}min=? [ C ]) // Note that the min values are actually infinity and prism (currently) gives wrong results for this, e.g., R{"time"}min=?[ C<=2000 ] gives a larger value than multi(R{"time"}min=?[ C ], R{"energy"}<=1.45 [ C ]) . \ No newline at end of file diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp index 22089a63d..696e8883f 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp @@ -307,9 +307,13 @@ namespace storm { } statistics << "\t Combined: " << std::setw(8) << combinedTime << std::endl; statistics << std::endl; - statistics << "Performed Refinement Steps: " << resultData.refinementSteps().size() << std::endl; - statistics << "Precision (Approximation): " << settings::getModule().getPrecision() << std::endl; - statistics << "Precision (Value Iteration): " << settings::getModule().getPrecision() << std::endl; + statistics << "Performed Refinement Steps: " << resultData.refinementSteps().size() << (resultData.getMaxStepsPerformed() ? " (computation aborted) " : "" ) << std::endl; + statistics << "Precision (Approximation): " << "Goal precision: " << settings::getModule().getPrecision(); + if(resultData.isPrecisionOfResultSet()) { + statistics << " Achieved precision: " << storm::utility::convertNumber(resultData.getPrecisionOfResult()) << ( resultData.getTargetPrecisionReached() ? "" : " (goal not achieved)"); + } + statistics << std::endl; + statistics << "Convergence precision for iterative solvers: " << settings::getModule().getPrecision() << std::endl; statistics << std::endl; statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;