From e898391e4448fa7074859c79341a66496f70b52b Mon Sep 17 00:00:00 2001 From: TimQu Date: Wed, 9 Sep 2020 15:28:42 +0200 Subject: [PATCH] Implemented stripping away of reward accumulations in multi-objective preprocessing. --- .../SparseMultiObjectivePreprocessor.cpp | 77 ++++++++++++++----- .../SparseMultiObjectivePreprocessor.h | 4 +- 2 files changed, 61 insertions(+), 20 deletions(-) diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp index a62389f3b..35d7aeb11 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp @@ -348,9 +348,9 @@ namespace storm { } else if (formula.getSubformula().isCumulativeRewardFormula()) { preprocessCumulativeRewardFormula(formula.getSubformula().asCumulativeRewardFormula(), opInfo, data, rewardModelName); } else if (formula.getSubformula().isTotalRewardFormula()) { - preprocessTotalRewardFormula(opInfo, data, rewardModelName); + preprocessTotalRewardFormula(formula.getSubformula().asTotalRewardFormula(), opInfo, data, rewardModelName); } else if (formula.getSubformula().isLongRunAverageRewardFormula()) { - preprocessLongRunAverageRewardFormula(opInfo, data, rewardModelName); + preprocessLongRunAverageRewardFormula(formula.getSubformula().asLongRunAverageRewardFormula(), opInfo, data, rewardModelName); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The subformula of " << formula << " is not supported."); } @@ -498,7 +498,8 @@ namespace storm { if (formula.isReachabilityRewardFormula()) { // build stateAction reward vector that only gives reward for states that are reachable from init assert(optionalRewardModelName.is_initialized()); - typename SparseModelType::RewardModelType objectiveRewards = data.model->getRewardModel(optionalRewardModelName.get()); + auto objectiveRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(optionalRewardModelName.get()), data.model->isDiscreteTimeModel(), formula).extract(); + // get rid of potential transition rewards objectiveRewards.reduceToStateBasedRewards(data.model->getTransitionMatrix(), false); if (objectiveRewards.hasStateRewards()) { storm::utility::vector::setVectorValues(objectiveRewards.getStateRewardVector(), reachableFromGoal, storm::utility::zero()); @@ -540,7 +541,7 @@ namespace storm { } else { data.objectives.back()->formula = std::make_shared(formula.asSharedPointer(), optionalRewardModelName.get(), opInfo); } - } else if (formula.isReachabilityTimeFormula() && data.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + } else if (formula.isReachabilityTimeFormula()) { // Reduce to reachability rewards so that time formulas do not have to be treated seperately later. std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); std::shared_ptr newSubformula = formula.getSubformula().asSharedPointer(); @@ -551,8 +552,14 @@ namespace storm { } auto newFormula = std::make_shared(newSubformula, storm::logic::FormulaContext::Reward); data.objectives.back()->formula = std::make_shared(newFormula, rewardModelName, opInfo); - std::vector timeRewards(data.model->getNumberOfStates(), storm::utility::zero()); - storm::utility::vector::setVectorValues(timeRewards, dynamic_cast const&>(*data.model).getMarkovianStates(), storm::utility::one()); + std::vector timeRewards; + if (data.model->isOfType(storm::models::ModelType::MarkovAutomaton)) { + timeRewards.assign(data.model->getNumberOfStates(), storm::utility::zero()); + storm::utility::vector::setVectorValues(timeRewards, dynamic_cast const&>(*data.model).getMarkovianStates(), storm::utility::one()); + } else { + timeRewards.assign(data.model->getNumberOfStates(), storm::utility::one()); + + } data.model->addRewardModel(rewardModelName, typename SparseModelType::RewardModelType(std::move(timeRewards))); } else { STORM_LOG_THROW(false, storm::exceptions::InvalidPropertyException, "The formula " << formula << " neither considers reachability probabilities nor reachability rewards " << (data.model->isOfType(storm::models::ModelType::MarkovAutomaton) ? "nor reachability time" : "") << ". This is not supported."); @@ -564,34 +571,68 @@ namespace storm { template void SparseMultiObjectivePreprocessor::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { STORM_LOG_THROW(data.model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type."); + std::string rewardModelName = optionalRewardModelName.get(); + // Strip away potential RewardAccumulations in the formula itself but also in reward bounds + auto filteredRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(rewardModelName), data.model->isDiscreteTimeModel(), formula); + if (filteredRewards.isDifferentFromUnfilteredModel()) { + std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + data.model->addRewardModel(rewardModelName, std::move(filteredRewards.extract())); + } - auto cumulativeRewardFormula = std::make_shared(formula); - data.objectives.back()->formula = std::make_shared(cumulativeRewardFormula, *optionalRewardModelName, opInfo); + std::vector newTimeBoundReferences; bool onlyRewardBounds = true; - for (uint64_t i = 0; i < cumulativeRewardFormula->getDimension(); ++i) { - if (!cumulativeRewardFormula->getTimeBoundReference(i).isRewardBound()) { + for (uint64_t i = 0; i < formula.getDimension(); ++i) { + auto oldTbr = formula.getTimeBoundReference(i); + if (oldTbr.isRewardBound()) { onlyRewardBounds = false; - break; + if (oldTbr.hasRewardAccumulation()) { + auto filteredBoundRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(oldTbr.getRewardName()), oldTbr.getRewardAccumulation(), data.model->isDiscreteTimeModel()); + if (filteredBoundRewards.isDifferentFromUnfilteredModel()) { + std::string freshRewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()) + std::string("_" + std::to_string(i)); + data.model->addRewardModel(freshRewardModelName, std::move(filteredBoundRewards.extract())); + newTimeBoundReferences.emplace_back(freshRewardModelName); + } else { + // Strip away the reward accumulation + newTimeBoundReferences.emplace_back(oldTbr.getRewardName()); + } + } else { + newTimeBoundReferences.push_back(oldTbr); + } + } else { + newTimeBoundReferences.push_back(oldTbr); } } + + auto newFormula = std::make_shared(formula.getBounds(), newTimeBoundReferences); + data.objectives.back()->formula = std::make_shared(newFormula, rewardModelName, opInfo); + if (onlyRewardBounds) { data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); } } template - void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + void SparseMultiObjectivePreprocessor::preprocessTotalRewardFormula(storm::logic::TotalRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { - auto totalRewardFormula = std::make_shared(); - data.objectives.back()->formula = std::make_shared(totalRewardFormula, *optionalRewardModelName, opInfo); + std::string rewardModelName = optionalRewardModelName.get(); + auto filteredRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(rewardModelName), data.model->isDiscreteTimeModel(), formula); + if (filteredRewards.isDifferentFromUnfilteredModel()) { + std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + data.model->addRewardModel(rewardModelName, filteredRewards.extract()); + } + data.objectives.back()->formula = std::make_shared(formula.stripRewardAccumulation(), rewardModelName, opInfo); data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true); } template - void SparseMultiObjectivePreprocessor::preprocessLongRunAverageRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { - - auto longRunAverageRewardFormula = std::make_shared(); - data.objectives.back()->formula = std::make_shared(longRunAverageRewardFormula, *optionalRewardModelName, opInfo); + void SparseMultiObjectivePreprocessor::preprocessLongRunAverageRewardFormula(storm::logic::LongRunAverageRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName) { + std::string rewardModelName = optionalRewardModelName.get(); + auto filteredRewards = storm::utility::createFilteredRewardModel(data.model->getRewardModel(rewardModelName), data.model->isDiscreteTimeModel(), formula); + if (filteredRewards.isDifferentFromUnfilteredModel()) { + std::string rewardModelName = data.rewardModelNamePrefix + std::to_string(data.objectives.size()); + data.model->addRewardModel(rewardModelName, std::move(filteredRewards.extract())); + } + data.objectives.back()->formula = std::make_shared(formula.stripRewardAccumulation(), rewardModelName, opInfo); } template diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h index 7141bc80a..91a45b87a 100644 --- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h +++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h @@ -75,8 +75,8 @@ namespace storm { 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); - static void preprocessTotalRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The total reward formula itself does not need to be provided as it is unique. - static void preprocessLongRunAverageRewardFormula(storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); // The long run average reward formula itself does not need to be provided as it is unique. + static void preprocessTotalRewardFormula(storm::logic::TotalRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); + static void preprocessLongRunAverageRewardFormula(storm::logic::LongRunAverageRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional const& optionalRewardModelName = boost::none); /*! * Builds the result from preprocessing