diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp index 75a2c0008..97bac76ec 100644 --- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp +++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp @@ -34,6 +34,7 @@ namespace storm { template std::unique_ptr SparseMdpMultiObjectiveModelChecker::checkMultiObjectiveFormula(CheckTask 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 result; #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp index b1af9b9ab..837141a1d 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp @@ -1,5 +1,7 @@ #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h" +#include + #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 std::unique_ptr SparseMultiObjectivePostprocessor::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 std::unique_ptr SparseMultiObjectivePostprocessor::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(new ExplicitQualitativeCheckResult(initState, resultData.getThresholdsAreAchievable())); } template typename std::unique_ptr SparseMultiObjectivePostprocessor::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() * optimizingObjective.toOriginalValueTransformationFactor + optimizingObjective.toOriginalValueTransformationOffset; + STORM_LOG_WARN_COND(resultData.getTargetPrecisionReached(), "The target precision for numerical queries has not been reached."); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(initState, resultForOriginalModel)); + } else { + STORM_LOG_ERROR_COND(resultData.isThresholdsAreAchievableSet(), "Could not find out whether the thresholds are achievable."); + return std::unique_ptr(new ExplicitQualitativeCheckResult(initState, false)); + } } template typename std::unique_ptr SparseMultiObjectivePostprocessor::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(new ExplicitQualitativeCheckResult(initState, false)); } #ifdef STORM_HAVE_CARL diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h index 28f196b39..ae2015b48 100644 --- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h +++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h @@ -10,8 +10,6 @@ namespace storm { namespace modelchecker { - - namespace helper { template