creation of check results for numerical and achievability queries

Former-commit-id: 3c628996d4

src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp

@@ -34,6 +34,7 @@ namespace storm {
         
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) {
+            STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
             std::unique_ptr<CheckResult> result;
             
 #ifdef STORM_HAVE_CARL

src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp

@@ -1,5 +1,7 @@
  #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h"
 
+#include <memory>
+
 #include "src/adapters/CarlAdapter.h"
 #include "src/models/sparse/Mdp.h"
 #include "src/models/sparse/StandardRewardModel.h"
@@ -17,7 +19,8 @@ namespace storm {
             
             template<typename SparseModelType, typename RationalNumberType>
             typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-                STORM_LOG_ASSERT(preprocessor.
+                STORM_LOG_ASSERT(preprocessorData.originalModel.getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
+                STORM_LOG_WARN_COND(!resultData.getMaxStepsPerformed(), "Multi-objective model checking has been aborted since the maximum number of refinement steps has been performed. The results are most likely incorrect.");
                 switch(preprocessorData.queryType) {
                     case PreprocessorData::QueryType::Achievability:
                         return postprocessAchievabilityQuery(preprocessorData, resultData);
@@ -34,18 +37,32 @@ namespace storm {
             
             template<typename SparseModelType, typename RationalNumberType>
             typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-            
+                STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");
+                uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, resultData.getThresholdsAreAchievable()));
             }
             
             template<typename SparseModelType, typename RationalNumberType>
             typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-            
+                uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
+                if(resultData.isThresholdsAreAchievableSet() && resultData.getThresholdsAreAchievable()) {
+                    STORM_LOG_ASSERT(resultData.isNumericalResultSet(), "Postprocessing for numerical query invoked, but no numerical result is given");
+                    STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Postprocessing for numerical query invoked, but no index of optimizing objective is specified");
+                    ObjectiveInformation optimizingObjective = preprocessorData.objectives[*preprocessorData.indexOfOptimizingObjective];
+                    ValueType resultForOriginalModel = resultData.template getNumericalResult<ValueType>() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset;
+                    STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached.");
+                    return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(initState, resultForOriginalModel));
+                } else {
+                    STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable.");
+                    return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
+                }
             }
             
             template<typename SparseModelType, typename RationalNumberType>
             typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-            
-                std::cout << "Postprocessing pareto queries not yet implemented";
+                STORM_LOG_ERROR("Postprocessing pareto queries not yet implemented");
+                uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
             }
             
 #ifdef STORM_HAVE_CARL

src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h

@@ -10,8 +10,6 @@
 
 namespace storm {
     namespace modelchecker {
-        
-
         namespace helper {
             
             template <class SparseModelType>