pareto curve output improvements

Former-commit-id: 6a7928922b

examples/multiobjective/.gitignore

@@ -0,0 +1 @@
+*.csv

examples/multiobjective/displaypareto/.gitignore

@@ -0,0 +1,4 @@
+*.aux
+*.log
+*.synctex.gz
+*.pdf

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}

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 ]) .

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 ]) .

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 ]) .

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<storm::settings::modules::MultiObjectiveSettings>().getPrecision() << std::endl;
-                statistics << "Precision (Value Iteration): " << settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision() << std::endl;
+                statistics << "Performed Refinement Steps: " << resultData.refinementSteps().size() << (resultData.getMaxStepsPerformed() ? " (computation aborted) " : "" ) << std::endl;
+                statistics << "Precision (Approximation): " << "Goal precision: " << settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision();
+                if(resultData.isPrecisionOfResultSet()) {
+                    statistics << " Achieved precision: " << storm::utility::convertNumber<double>(resultData.getPrecisionOfResult()) << ( resultData.getTargetPrecisionReached() ? "" : " (goal not achieved)");
+                }
+                statistics << std::endl;
+                statistics << "Convergence precision for iterative solvers: " << settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision() << std::endl;
                 statistics << std::endl;
                 statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;