From 722cb3109c99615d79930844b01f91dbb5da6f2b Mon Sep 17 00:00:00 2001 From: dehnert Date: Tue, 22 Aug 2017 11:12:08 +0200 Subject: [PATCH] dd quotient extraction of reward models in dd bisimulation --- .../csl/helper/SparseCtmcCslHelper.cpp | 4 +- src/storm/models/sparse/Ctmc.cpp | 7 ++++ src/storm/models/sparse/Ctmc.h | 2 + .../models/sparse/DeterministicModel.cpp | 7 ---- src/storm/models/sparse/DeterministicModel.h | 2 - src/storm/models/sparse/Dtmc.cpp | 6 +++ src/storm/models/sparse/Dtmc.h | 1 + .../models/sparse/StandardRewardModel.cpp | 41 ++++++++++++------- src/storm/models/sparse/StandardRewardModel.h | 10 +++-- .../dd/bisimulation/MdpPartitionRefiner.cpp | 7 +++- .../dd/bisimulation/MdpPartitionRefiner.h | 2 + .../dd/bisimulation/PartitionRefiner.cpp | 33 +++++++++++++++ .../dd/bisimulation/PartitionRefiner.h | 9 ++++ .../dd/bisimulation/QuotientExtractor.cpp | 23 +++++++++-- 14 files changed, 120 insertions(+), 34 deletions(-) diff --git a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp index e0cd132ee..b574cabd1 100644 --- a/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp +++ b/src/storm/modelchecker/csl/helper/SparseCtmcCslHelper.cpp @@ -264,7 +264,7 @@ namespace storm { storm::storage::SparseMatrix uniformizedMatrix = computeUniformizedMatrix(rateMatrix, storm::storage::BitVector(numberOfStates, true), uniformizationRate, exitRateVector); // Compute the total state reward vector. - std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector, false); + std::vector totalRewardVector = rewardModel.getTotalRewardVector(rateMatrix, exitRateVector); // Finally, compute the transient probabilities. return computeTransientProbabilities(uniformizedMatrix, nullptr, timeBound, uniformizationRate, totalRewardVector, linearEquationSolverFactory); @@ -359,7 +359,7 @@ namespace storm { // Only compute the result if the model has a state-based reward model. STORM_LOG_THROW(!rewardModel.empty(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula."); - return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector, true), exitRateVector, linearEquationSolverFactory); + return computeLongRunAverageRewards(probabilityMatrix, rewardModel.getTotalRewardVector(probabilityMatrix, *exitRateVector), exitRateVector, linearEquationSolverFactory); } template diff --git a/src/storm/models/sparse/Ctmc.cpp b/src/storm/models/sparse/Ctmc.cpp index bdfb406bb..9b36ded21 100644 --- a/src/storm/models/sparse/Ctmc.cpp +++ b/src/storm/models/sparse/Ctmc.cpp @@ -72,6 +72,13 @@ namespace storm { return exitRates; } + template + void Ctmc::reduceToStateBasedRewards() { + for (auto& rewardModel : this->getRewardModels()) { + rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true, &exitRates); + } + } + template class Ctmc; #ifdef STORM_HAVE_CARL diff --git a/src/storm/models/sparse/Ctmc.h b/src/storm/models/sparse/Ctmc.h index c6afaac16..ed5a46329 100644 --- a/src/storm/models/sparse/Ctmc.h +++ b/src/storm/models/sparse/Ctmc.h @@ -62,6 +62,8 @@ namespace storm { */ std::vector& getExitRateVector(); + virtual void reduceToStateBasedRewards() override; + private: /*! * Computes the exit rate vector based on the given rate matrix. diff --git a/src/storm/models/sparse/DeterministicModel.cpp b/src/storm/models/sparse/DeterministicModel.cpp index 27c923bfa..5e2b85fe4 100644 --- a/src/storm/models/sparse/DeterministicModel.cpp +++ b/src/storm/models/sparse/DeterministicModel.cpp @@ -59,13 +59,6 @@ namespace storm { } } - template - void DeterministicModel::reduceToStateBasedRewards() { - for (auto& rewardModel : this->getRewardModels()) { - rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true); - } - } - template class DeterministicModel; #ifdef STORM_HAVE_CARL template class DeterministicModel; diff --git a/src/storm/models/sparse/DeterministicModel.h b/src/storm/models/sparse/DeterministicModel.h index f2dd82e12..13486ef5c 100644 --- a/src/storm/models/sparse/DeterministicModel.h +++ b/src/storm/models/sparse/DeterministicModel.h @@ -29,8 +29,6 @@ namespace storm { DeterministicModel(DeterministicModel&& other) = default; DeterministicModel& operator=(DeterministicModel&& model) = default; - - virtual void reduceToStateBasedRewards() override; virtual void writeDotToStream(std::ostream& outStream, bool includeLabeling = true, storm::storage::BitVector const* subsystem = nullptr, std::vector const* firstValue = nullptr, std::vector const* secondValue = nullptr, std::vector const* stateColoring = nullptr, std::vector const* colors = nullptr, std::vector* scheduler = nullptr, bool finalizeOutput = true) const override; }; diff --git a/src/storm/models/sparse/Dtmc.cpp b/src/storm/models/sparse/Dtmc.cpp index 2fa945420..29b31babe 100644 --- a/src/storm/models/sparse/Dtmc.cpp +++ b/src/storm/models/sparse/Dtmc.cpp @@ -35,6 +35,12 @@ namespace storm { // Intentionally left empty } + template + void Dtmc::reduceToStateBasedRewards() { + for (auto& rewardModel : this->getRewardModels()) { + rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), true); + } + } template class Dtmc; diff --git a/src/storm/models/sparse/Dtmc.h b/src/storm/models/sparse/Dtmc.h index ecc3ecba8..6809b686c 100644 --- a/src/storm/models/sparse/Dtmc.h +++ b/src/storm/models/sparse/Dtmc.h @@ -50,6 +50,7 @@ namespace storm { Dtmc(Dtmc&& dtmc) = default; Dtmc& operator=(Dtmc&& dtmc) = default; + virtual void reduceToStateBasedRewards() override; }; diff --git a/src/storm/models/sparse/StandardRewardModel.cpp b/src/storm/models/sparse/StandardRewardModel.cpp index 721608047..4385c46e1 100644 --- a/src/storm/models/sparse/StandardRewardModel.cpp +++ b/src/storm/models/sparse/StandardRewardModel.cpp @@ -165,7 +165,7 @@ namespace storm { template template - void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards) { + void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights) { if (this->hasTransitionRewards()) { if (this->hasStateActionRewards()) { storm::utility::vector::addVectors(this->getStateActionRewardVector(), transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()), this->getStateActionRewardVector()); @@ -177,10 +177,21 @@ namespace storm { if (reduceToStateRewards && this->hasStateActionRewards()) { STORM_LOG_THROW(transitionMatrix.getRowGroupCount() == this->getStateActionRewardVector().size(), storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible if the size of the action reward vector equals the number of states."); - if (this->hasStateRewards()) { - storm::utility::vector::addVectors(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector()); + if (weights) { + if (this->hasStateRewards()) { + storm::utility::vector::applyPointwise(this->getStateActionRewardVector(), *weights, this->getStateRewardVector(), + [] (ValueType const& sar, MatrixValueType const& w, ValueType const& sr) -> ValueType { + return sr + w * sar; }); + } else { + this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector); + storm::utility::vector::applyPointwise(this->optionalStateRewardVector.get(), *weights, this->optionalStateRewardVector.get(), [] (ValueType const& r, MatrixValueType const& w) { return w * r; } ); + } } else { - this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector); + if (this->hasStateRewards()) { + storm::utility::vector::addVectors(this->getStateActionRewardVector(), this->getStateRewardVector(), this->getStateRewardVector()); + } else { + this->optionalStateRewardVector = std::move(this->optionalStateActionRewardVector); + } } this->optionalStateActionRewardVector = boost::none; } @@ -201,7 +212,7 @@ namespace storm { template template - std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const { + std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const { std::vector result; if (this->hasTransitionRewards()) { result = transitionMatrix.getPointwiseProductRowSumVector(this->getTransitionRewardMatrix()); @@ -382,13 +393,13 @@ namespace storm { // Explicitly instantiate the class. template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template double StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, double const& stateRewardWeight, double const& actionRewardWeight) const; - template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); template class StandardRewardModel; @@ -396,9 +407,9 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; - template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, float const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, float const & newValue); template class StandardRewardModel; @@ -407,12 +418,12 @@ namespace storm { #ifdef STORM_HAVE_CARL template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::RationalNumber StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalNumber const& stateRewardWeight, storm::RationalNumber const& actionRewardWeight) const; - template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalNumber const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalNumber const & newValue); template class StandardRewardModel; @@ -420,13 +431,13 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template storm::storage::BitVector StandardRewardModel::getStatesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template storm::storage::BitVector StandardRewardModel::getChoicesWithZeroReward(storm::storage::SparseMatrix const& transitionMatrix) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template storm::RationalFunction StandardRewardModel::getTotalStateActionReward(uint_fast64_t stateIndex, uint_fast64_t choiceIndex, storm::storage::SparseMatrix const& transitionMatrix, storm::RationalFunction const& stateRewardWeight, storm::RationalFunction const& actionRewardWeight) const; - template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::RationalFunction const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::RationalFunction const & newValue); template class StandardRewardModel; @@ -434,13 +445,13 @@ namespace storm { template std::vector StandardRewardModel::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix const& transitionMatrix, storm::storage::BitVector const& filter) const; template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix) const; - template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + template std::vector StandardRewardModel::getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; template std::vector StandardRewardModel::getTotalActionRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& stateRewardWeights) const; template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, double const & newValue); template void StandardRewardModel::setStateActionReward(uint_fast64_t choiceIndex, storm::Interval const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, double const & newValue); template void StandardRewardModel::setStateReward(uint_fast64_t state, storm::Interval const & newValue); - template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards); + template void StandardRewardModel::reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards, std::vector const* weights); template class StandardRewardModel; template std::ostream& operator<<(std::ostream& out, StandardRewardModel const& rewardModel); #endif diff --git a/src/storm/models/sparse/StandardRewardModel.h b/src/storm/models/sparse/StandardRewardModel.h index c58f38312..410d9f448 100644 --- a/src/storm/models/sparse/StandardRewardModel.h +++ b/src/storm/models/sparse/StandardRewardModel.h @@ -191,9 +191,13 @@ namespace storm { * but not all reward-based properties. * * @param transitionMatrix The transition matrix that is used to weight the rewards in the reward matrix. + * @param reduceToStateRewards If set, the state-action rewards and the state rewards are summed so the + * model only has a state reward vector left. + * @param weights If given and if the reduction to state rewards only is enabled, this vector is used to + * weight the state-action and transition rewards */ template - void reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards = false); + void reduceToStateBasedRewards(storm::storage::SparseMatrix const& transitionMatrix, bool reduceToStateRewards = false, std::vector const* weights = nullptr); /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and @@ -211,12 +215,10 @@ namespace storm { * * @param transitionMatrix The matrix that is used to weight the values of the transition reward matrix. * @param weights A vector used for scaling the entries of transition and/or state-action rewards (if present). - * @param scaleTransAndActions If true both transition rewards and state-action rewards are scaled by the - * weights. Otherwise, only the state-action rewards are scaled. * @return The full state-action reward vector. */ template - std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights, bool scaleTransAndActions) const; + std::vector getTotalRewardVector(storm::storage::SparseMatrix const& transitionMatrix, std::vector const& weights) const; /*! * Creates a vector representing the complete reward vector based on the state-, state-action- and diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp index d26cc4111..5ce9fc504 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp @@ -21,7 +21,7 @@ namespace storm { // For this, we use the signature computer/refiner of this class. STORM_LOG_TRACE("Refining choice partition."); - Partition newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, choicePartition, this->statePartition, mode); + Partition newChoicePartition = this->internalRefine(this->signatureComputer, this->signatureRefiner, this->choicePartition, this->statePartition, mode); if (newChoicePartition == choicePartition) { this->status = Status::FixedPoint; @@ -48,6 +48,11 @@ namespace storm { return choicePartition; } + template + bool MdpPartitionRefiner::refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards) { + Partition newChoicePartition = this->signatureRefiner.refine(this->choicePartition, Signature(stateActionRewards)); + } + template class MdpPartitionRefiner; template class MdpPartitionRefiner; diff --git a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h index c513386ee..e5511e939 100644 --- a/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h @@ -32,6 +32,8 @@ namespace storm { Partition const& getChoicePartition() const; private: + virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards) override; + // The choice partition in the refinement process. Partition choicePartition; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp index cd064343f..422f4175b 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.cpp @@ -2,6 +2,9 @@ #include "storm/models/symbolic/StandardRewardModel.h" +#include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" + namespace storm { namespace dd { namespace bisimulation { @@ -69,6 +72,36 @@ namespace storm { } } + template + bool PartitionRefiner::refineWrtRewardModel(storm::models::symbolic::Model const& model, storm::models::symbolic::StandardRewardModel const& rewardModel) { + STORM_LOG_THROW(rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards."); + bool result = false; + if (rewardModel.hasStateActionRewards()) { + result |= refineWrtStateActionRewards(model, rewardModel.getStateActionRewardVector()); + } + if (rewardModel.hasStateRewards()) { + result |= refineWrtStateRewards(model, rewardModel.getStateActionRewardVector()); + } + return result; + } + + template + bool PartitionRefiner::refineWrtStateRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateRewards) { + Partition newPartition = signatureRefiner.refine(statePartition, Signature(stateRewards)); + if (newPartition == statePartition) { + return false; + } else { + this->statePartition = newPartition; + return true; + } + } + + template + bool PartitionRefiner::refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards) { + // By default, we treat state-action rewards just like state-rewards, which works for DTMCs and CTMCs. + return refineWrtStateRewards(model, stateActionRewards); + } + template Partition const& PartitionRefiner::getStatePartition() const { return statePartition; diff --git a/src/storm/storage/dd/bisimulation/PartitionRefiner.h b/src/storm/storage/dd/bisimulation/PartitionRefiner.h index 870c1f429..d8236d6e8 100644 --- a/src/storm/storage/dd/bisimulation/PartitionRefiner.h +++ b/src/storm/storage/dd/bisimulation/PartitionRefiner.h @@ -32,6 +32,12 @@ namespace storm { */ virtual bool refine(SignatureMode const& mode = SignatureMode::Eager); + /*! + * Refines the partition wrt. to the reward model. + * @return True iff the partition is stable and no refinement was actually performed. + */ + bool refineWrtRewardModel(storm::models::symbolic::Model const& model, storm::models::symbolic::StandardRewardModel const& rewardModel); + /*! * Retrieves the current state partition in the refinement process. */ @@ -45,6 +51,9 @@ namespace storm { protected: Partition internalRefine(SignatureComputer& stateSignatureComputer, SignatureRefiner& signatureRefiner, Partition const& oldPartition, Partition const& targetPartition, SignatureMode const& mode = SignatureMode::Eager); + virtual bool refineWrtStateRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateRewards); + virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model const& model, storm::dd::Add const& stateActionRewards); + // The current status. Status status; diff --git a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp index 77a99303e..c28b328e3 100644 --- a/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp +++ b/src/storm/storage/dd/bisimulation/QuotientExtractor.cpp @@ -838,12 +838,29 @@ namespace storm { storm::dd::Bdd quotientTransitionMatrixBdd = quotientTransitionMatrix.notZero(); storm::dd::Bdd deadlockStates = !quotientTransitionMatrixBdd.existsAbstract(blockPrimeVariableSet) && reachableStates; + std::unordered_map> quotientRewardModels; + for (auto const& rewardModelName : preservationInformation.getRewardModelNames()) { + auto const& rewardModel = model.getRewardModel(rewardModelName); + + boost::optional> quotientStateRewards; + if (rewardModel.hasStateRewards()) { + quotientStateRewards = rewardModel.getStateRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()); + } + + boost::optional> quotientStateActionRewards; + if (rewardModel.hasStateActionRewards()) { + quotientStateActionRewards = rewardModel.getStateActionRewardVector().multiplyMatrix(partitionAsAdd, model.getRowVariables()); + } + + quotientRewardModels.emplace(rewardModelName, storm::models::symbolic::StandardRewardModel(quotientStateRewards, quotientStateActionRewards, boost::none)); + } + if (modelType == storm::models::ModelType::Dtmc) { - return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); + return std::shared_ptr>(new storm::models::symbolic::Dtmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels)); } else if (modelType == storm::models::ModelType::Ctmc) { - return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, {})); + return std::shared_ptr>(new storm::models::symbolic::Ctmc(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, preservedLabelBdds, quotientRewardModels)); } else if (modelType == storm::models::ModelType::Mdp) { - return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, {})); + return std::shared_ptr>(new storm::models::symbolic::Mdp(model.getManager().asSharedPointer(), reachableStates, initialStates, deadlockStates, quotientTransitionMatrix, blockVariableSet, blockPrimeVariableSet, blockMetaVariablePairs, model.getNondeterminismVariables(), preservedLabelBdds, quotientRewardModels)); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Unsupported quotient type."); }