From 27ac2798c4f54d7c5ffb6c835aee10ce75db0d2f Mon Sep 17 00:00:00 2001 From: TimQu Date: Fri, 18 Aug 2017 18:26:30 +0200 Subject: [PATCH] allowing multi(...) path formulas in multiobjective model checking --- .../SparseMultiObjectivePreprocessor.cpp | 11 +++++++++++ .../multiobjective/SparseMultiObjectivePreprocessor.h | 1 + .../pcaa/SparseMdpPcaaWeightVectorChecker.cpp | 4 ++-- 3 files changed, 14 insertions(+), 2 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp index ada77e9c2..c6cfc0aa4 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp @@ -177,6 +177,8 @@ namespace storm { preprocessUntilFormula(formula.getSubformula().asUntilFormula(), opInfo, data); } else if (formula.getSubformula().isBoundedUntilFormula()){ preprocessBoundedUntilFormula(formula.getSubformula().asBoundedUntilFormula(), opInfo, data); + } else if (formula.getSubformula().isMultiObjectiveFormula()){ + preprocessMultiObjectiveSubformula(formula.getSubformula().asMultiObjectiveFormula(), opInfo, data); } else if (formula.getSubformula().isGloballyFormula()){ preprocessGloballyFormula(formula.getSubformula().asGloballyFormula(), opInfo, data); } else if (formula.getSubformula().isEventuallyFormula()){ @@ -263,6 +265,15 @@ namespace storm { } + template + void SparseMultiObjectivePreprocessor::preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { + // Check whether only bounded until formulas are contained + for (auto const& f : formula.getSubformulas()) { + STORM_LOG_THROW(f->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "MultiObjective subformulas are only allowed if they all contain bounded until formulas"); + } + data.objectives.back()->formula = std::make_shared(formula.asSharedPointer(), opInfo); + } + template void SparseMultiObjectivePreprocessor::preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data) { diff --git a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h index 505431e62..fe0cf145a 100644 --- a/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.h @@ -60,6 +60,7 @@ namespace storm { static void preprocessTimeOperatorFormula(storm::logic::TimeOperatorFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); static void preprocessUntilFormula(storm::logic::UntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, std::shared_ptr subformula = nullptr); static void preprocessBoundedUntilFormula(storm::logic::BoundedUntilFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); + static void preprocessMultiObjectiveSubformula(storm::logic::MultiObjectiveFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); static void preprocessGloballyFormula(storm::logic::GloballyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data); static void preprocessEventuallyFormula(storm::logic::EventuallyFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); static void preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp index aee1cd035..8b1fad20e 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparseMdpPcaaWeightVectorChecker.cpp @@ -29,7 +29,7 @@ namespace storm { // set the state action rewards. Also do some sanity checks on the objectives. for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { auto const& formula = *objectives[objIndex].formula; - if (!(formula.isProbabilityOperatorFormula() && formula.getSubformula().isBoundedUntilFormula())) { + if (!(formula.isProbabilityOperatorFormula() && (formula.getSubformula().isBoundedUntilFormula() || formula.getSubformula().isMultiObjectiveFormula()))) { STORM_LOG_THROW(formula.isRewardOperatorFormula() && formula.asRewardOperatorFormula().hasRewardModelName(), storm::exceptions::UnexpectedException, "Unexpected type of operator formula: " << formula); STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() || formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula()); typename SparseMdpModelType::RewardModelType const& rewModel = this->model.getRewardModel(formula.asRewardOperatorFormula().getRewardModelName()); @@ -44,7 +44,7 @@ namespace storm { // Currently, only step bounds are considered. bool containsRewardBoundedObjectives = false; for (uint_fast64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) { - if (this->objectives[objIndex].formula->getSubformula().isBoundedUntilFormula()) { + if (this->objectives[objIndex].formula->isProbabilityOperatorFormula()) { containsRewardBoundedObjectives = true; break; }