diff --git a/src/storm/modelchecker/multiobjective/Objective.h b/src/storm/modelchecker/multiobjective/Objective.h index 6e7040fac..09faaf075 100644 --- a/src/storm/modelchecker/multiobjective/Objective.h +++ b/src/storm/modelchecker/multiobjective/Objective.h @@ -31,6 +31,8 @@ namespace storm { // Lower and upper time/step bouds boost::optional lowerTimeBound, upperTimeBound; + boost::optional lowerResultBound, upperResultBound; + void printToStream(std::ostream& out) const { out << originalFormula->toString(); out << " \t"; @@ -39,7 +41,7 @@ namespace storm { out << " \t"; out << "intern bound: "; if (bound){ - out << bound; + out << *bound; } else { out << " -none- "; } @@ -55,7 +57,23 @@ namespace storm { out << " -none- "; } out << " \t"; - out << "intern reward model: " << *rewardModelName; + out << "intern reward model: "; + if (rewardModelName) { + out << *rewardModelName; + } else { + out << " -none- "; + } + out << " \t"; + out << "result bounds: "; + if (lowerResultBound && upperResultBound) { + out << "[" << *lowerResultBound << ", " << *upperResultBound << "]"; + } else if (lowerResultBound) { + out << ">=" << *lowerResultBound; + } else if (upperResultBound) { + out << "<=" << *upperResultBound; + } else { + out << " -none- "; + } } }; } diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index e85b41de6..bb93e0eaf 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -44,16 +44,19 @@ namespace storm { } } + // Incorporate the required memory into the state space storm::storage::SparseModelMemoryProduct product = data.memory->product(originalModel); std::shared_ptr preprocessedModel = std::dynamic_pointer_cast(product.build()); auto backwardTransitions = preprocessedModel->getBackwardTransitions(); + // compute the end components of the model (if required) bool endComponentAnalysisRequired = false; for (auto& task : data.tasks) { endComponentAnalysisRequired = endComponentAnalysisRequired || task->requiresEndComponentAnalysis(); } if (endComponentAnalysisRequired) { + // TODO STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "End component analysis required but currently not implemented."); } @@ -61,41 +64,8 @@ namespace storm { task->perform(*preprocessedModel); } - ReturnType result(originalFormula, originalModel); - for (auto& obj : data.objectives) { - result.objectives.push_back(std::move(*obj)); - } - result.preprocessedModel = std::move(preprocessedModel); - result.queryType = ReturnType::QueryType::Achievability; - - auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions); - auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions); - - std::set relevantRewardModels; - for (auto const& obj : result.objectives) { - relevantRewardModels.insert(*obj.rewardModelName); - } - - // Build a subsystem that discards states that yield infinite reward for all schedulers. - // We can also merge the states that will have reward zero anyway. - storm::storage::BitVector zeroRewardStates = ~minMaxNonZeroRewardStates.second; - storm::transformer::GoalStateMerger merger(*result.preprocessedModel); - typename storm::transformer::GoalStateMerger::ReturnType mergerResult = merger.mergeTargetAndSinkStates(finiteRewardStates, zeroRewardStates, storm::storage::BitVector(finiteRewardStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); - - result.preprocessedModel = mergerResult.model; - result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % finiteRewardStates; - if (mergerResult.targetState) { - storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); - targetStateAsVector.set(*mergerResult.targetState, true); - result.possibleECChoices = storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector); - result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); - // There is an additional state in the result - result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); - } - assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates()); - - - return result; + // Build the actual result + return buildResult(originalModel, originalFormula, data, preprocessedModel, backwardTransitions); } template @@ -139,8 +109,6 @@ namespace storm { break; } } - - } template @@ -189,6 +157,10 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data) { + // Probabilities are between zero and one + data.objectives.back()->lowerResultBound = storm::utility::zero(); + data.objectives.back()->upperResultBound = storm::utility::one(); + if (formula.getSubformula().isUntilFormula()){ preprocessUntilFormula(formula.getSubformula().asUntilFormula(), data); } else if (formula.getSubformula().isBoundedUntilFormula()){ @@ -217,6 +189,8 @@ namespace storm { rewardModelName = data.originalModel.getRewardModels().begin()->first; } + data.objectives.back()->lowerResultBound = storm::utility::zero(); + if (formula.getSubformula().isEventuallyFormula()){ preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data, rewardModelName); } else if (formula.getSubformula().isCumulativeRewardFormula()) { @@ -233,6 +207,8 @@ namespace storm { // Time formulas are only supported for Markov automata STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton), storm::exceptions::InvalidPropertyException, "Time operator formulas are only supported for Markov automata."); + data.objectives.back()->lowerResultBound = storm::utility::zero(); + if (formula.getSubformula().isEventuallyFormula()){ preprocessEventuallyFormula(formula.getSubformula().asEventuallyFormula(), data); } else { @@ -344,6 +320,8 @@ namespace storm { data.objectives.back()->upperTimeBound = storm::logic::TimeBound(formula.isBoundStrict(), formula.getBound()); } + assert(optionalRewardModelName.is_initialized()); + data.objectives.back()->rewardModelName = *optionalRewardModelName; } @@ -354,6 +332,68 @@ namespace storm { data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); } + template + typename SparseMultiObjectivePreprocessor::ReturnType SparseMultiObjectivePreprocessor::buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr const& preprocessedModel, storm::storage::SparseMatrix const& backwardTransitions) { + + ReturnType result(originalFormula, originalModel); + + result.preprocessedModel = preprocessedModel; + + for (auto& obj : data.objectives) { + result.objectives.push_back(std::move(*obj)); + } + + result.queryType = getQueryType(result.objectives); + + auto minMaxNonZeroRewardStates = getStatesWithNonZeroRewardMinMax(result, backwardTransitions); + auto finiteRewardStates = ensureRewardFiniteness(result, data.finiteRewardCheckObjectives, minMaxNonZeroRewardStates.first, backwardTransitions); + + std::set relevantRewardModels; + for (auto const& obj : result.objectives) { + relevantRewardModels.insert(*obj.rewardModelName); + } + + // Build a subsystem that discards states that yield infinite reward for all schedulers. + // We can also merge the states that will have reward zero anyway. + storm::storage::BitVector zeroRewardStates = ~minMaxNonZeroRewardStates.second; + storm::storage::BitVector maybeStates = finiteRewardStates & ~zeroRewardStates; + storm::transformer::GoalStateMerger merger(*result.preprocessedModel); + typename storm::transformer::GoalStateMerger::ReturnType mergerResult = merger.mergeTargetAndSinkStates(maybeStates, zeroRewardStates, storm::storage::BitVector(maybeStates.size(), false), std::vector(relevantRewardModels.begin(), relevantRewardModels.end())); + + result.preprocessedModel = mergerResult.model; + result.possibleBottomStates = (~minMaxNonZeroRewardStates.first) % maybeStates; + if (mergerResult.targetState) { + storm::storage::BitVector targetStateAsVector(result.preprocessedModel->getNumberOfStates(), false); + targetStateAsVector.set(*mergerResult.targetState, true); + result.possibleECChoices = result.preprocessedModel->getTransitionMatrix().getRowIndicesOfRowGroups(storm::utility::graph::performProb0E(*result.preprocessedModel, result.preprocessedModel->getBackwardTransitions(), storm::storage::BitVector(targetStateAsVector.size(), true), targetStateAsVector)); + result.possibleECChoices.set(result.preprocessedModel->getTransitionMatrix().getRowGroupIndices()[*mergerResult.targetState], true); + // There is an additional state in the result + result.possibleBottomStates.resize(result.possibleBottomStates.size() + 1, true); + } + assert(result.possibleBottomStates.size() == result.preprocessedModel->getNumberOfStates()); + + return result; + } + + template + typename SparseMultiObjectivePreprocessor::ReturnType::QueryType SparseMultiObjectivePreprocessor::getQueryType(std::vector> const& objectives) { + uint_fast64_t numOfObjectivesWithThreshold = 0; + for (auto& obj : objectives) { + if (obj.bound) { + ++numOfObjectivesWithThreshold; + } + } + if (numOfObjectivesWithThreshold == objectives.size()) { + return ReturnType::QueryType::Achievability; + } else if (numOfObjectivesWithThreshold + 1 == objectives.size()) { + // Note: We do not want to consider a Pareto query when the total number of objectives is one. + return ReturnType::QueryType::Quantitative; + } else if (numOfObjectivesWithThreshold == 0) { + return ReturnType::QueryType::Pareto; + } else { + STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "Invalid Multi-objective query: The numer of qualitative objectives should be either 0 (Pareto query), 1 (quantitative query), or #objectives (achievability query)."); + } + } template std::pair SparseMultiObjectivePreprocessor::getStatesWithNonZeroRewardMinMax(ReturnType& result, storm::storage::SparseMatrix const& backwardTransitions) { diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 8e4dd26eb..318433575 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -65,6 +65,17 @@ namespace storm { static void preprocessTotalRewardFormula(PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. + /*! + * Builds the result from preprocessing + */ + static ReturnType buildResult(SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula, PreprocessorData& data, std::shared_ptr const& preprocessedModel, storm::storage::SparseMatrix const& backwardTransitions); + + /*! + * Returns the query type + */ + static typename ReturnType::QueryType getQueryType(std::vector> const& objectives); + + /*! * Computes the set of states that have a non-zero reward w.r.t. all objectives, assuming that the objectives are all minimizing and maximizing, respectively. */ diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h index 96de2956c..8143447ed 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorReturnType.h @@ -6,6 +6,7 @@ #include "storm/logic/Formulas.h" #include "storm/modelchecker/multiobjective/Objective.h" +#include "storm/storage/BitVector.h" #include "storm/exceptions/UnexpectedException.h" @@ -16,7 +17,7 @@ namespace storm { template struct SparseMultiObjectivePreprocessorReturnType { - enum class QueryType { Achievability }; + enum class QueryType { Achievability, Quantitative, Pareto }; storm::logic::MultiObjectiveFormula const& originalFormula; SparseModelType const& originalModel;