diff --git a/src/storm/api/bisimulation.h b/src/storm/api/bisimulation.h index 825b8e4c8..aaaa67618 100644 --- a/src/storm/api/bisimulation.h +++ b/src/storm/api/bisimulation.h @@ -43,6 +43,7 @@ namespace storm { STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Bisimulation minimization is currently only available for DTMCs, CTMCs and MDPs."); + // Try to get rid of non state-rewards to easy bisimulation computation. model->reduceToStateBasedRewards(); if (model->isOfType(storm::models::ModelType::Dtmc)) { @@ -60,6 +61,9 @@ namespace storm { STORM_LOG_THROW(model->isOfType(storm::models::ModelType::Dtmc) || model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Symbolic bisimulation minimization is currently only available for DTMCs and CTMCs."); STORM_LOG_THROW(bisimulationType == storm::storage::BisimulationType::Strong, storm::exceptions::NotSupportedException, "Currently only strong bisimulation is supported."); + // Try to get rid of non state-rewards to easy bisimulation computation. + model->reduceToStateBasedRewards(); + storm::dd::BisimulationDecomposition decomposition(*model, formulas, bisimulationType); decomposition.compute(mode); return decomposition.getQuotient(); diff --git a/src/storm/models/ModelBase.h b/src/storm/models/ModelBase.h index e6fb3f52f..614ebdcd5 100644 --- a/src/storm/models/ModelBase.h +++ b/src/storm/models/ModelBase.h @@ -122,6 +122,14 @@ namespace storm { */ virtual bool isExact() const; + /*! + * Converts the transition rewards of all reward models to state-based rewards. For deterministic models, + * this reduces the rewards to state rewards only. For nondeterminstic models, the reward models will + * contain state rewards and state-action rewards. Note that this transformation does not preserve all + * properties, but it preserves expected rewards. + */ + virtual void reduceToStateBasedRewards() = 0; + private: // The type of the model. ModelType modelType; diff --git a/src/storm/models/sparse/Model.h b/src/storm/models/sparse/Model.h index 1ae4f1619..5e52a9e12 100644 --- a/src/storm/models/sparse/Model.h +++ b/src/storm/models/sparse/Model.h @@ -292,16 +292,7 @@ namespace storm { * @return The choice origins, if they're saved. */ boost::optional>& getOptionalChoiceOrigins(); - - - /*! - * Converts the transition rewards of all reward models to state-based rewards. For deterministic models, - * this reduces the rewards to state rewards only. For nondeterminstic models, the reward models will - * contain state rewards and state-action rewards. Note that this transformation does not preserve all - * properties, but it preserves expected rewards. - */ - virtual void reduceToStateBasedRewards() = 0; - + /*! * Prints information about the model to the specified stream. * diff --git a/src/storm/models/symbolic/DeterministicModel.cpp b/src/storm/models/symbolic/DeterministicModel.cpp index 3555dcaff..5eba1bbc9 100644 --- a/src/storm/models/symbolic/DeterministicModel.cpp +++ b/src/storm/models/symbolic/DeterministicModel.cpp @@ -45,6 +45,13 @@ namespace storm { // Intentionally left empty. } + template + void DeterministicModel::reduceToStateBasedRewards() { + for (auto& rewardModel : this->getRewardModels()) { + rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), true); + } + } + // Explicitly instantiate the template class. template class DeterministicModel; template class DeterministicModel; diff --git a/src/storm/models/symbolic/DeterministicModel.h b/src/storm/models/symbolic/DeterministicModel.h index 83d25fe0d..a8fde85b4 100644 --- a/src/storm/models/symbolic/DeterministicModel.h +++ b/src/storm/models/symbolic/DeterministicModel.h @@ -80,6 +80,8 @@ namespace storm { std::vector> const& rowColumnMetaVariablePairs, std::map> labelToBddMap = std::map>(), std::unordered_map const& rewardModels = std::unordered_map()); + + virtual void reduceToStateBasedRewards() override; }; } // namespace symbolic diff --git a/src/storm/models/symbolic/Model.cpp b/src/storm/models/symbolic/Model.cpp index 686a1e9e5..505241dbc 100644 --- a/src/storm/models/symbolic/Model.cpp +++ b/src/storm/models/symbolic/Model.cpp @@ -255,11 +255,16 @@ namespace storm { return !this->rewardModels.empty(); } + template + std::unordered_map::RewardModelType>& Model::getRewardModels() { + return this->rewardModels; + } + template std::unordered_map::RewardModelType> const& Model::getRewardModels() const { return this->rewardModels; } - + template void Model::printModelInformationToStream(std::ostream& out) const { this->printModelInformationHeaderToStream(out); diff --git a/src/storm/models/symbolic/Model.h b/src/storm/models/symbolic/Model.h index 1f0aee439..89e447640 100644 --- a/src/storm/models/symbolic/Model.h +++ b/src/storm/models/symbolic/Model.h @@ -298,6 +298,7 @@ namespace storm { */ bool hasRewardModel() const; + std::unordered_map& getRewardModels(); std::unordered_map const& getRewardModels() const; /*! diff --git a/src/storm/models/symbolic/NondeterministicModel.cpp b/src/storm/models/symbolic/NondeterministicModel.cpp index 6545e27c0..25cea032d 100644 --- a/src/storm/models/symbolic/NondeterministicModel.cpp +++ b/src/storm/models/symbolic/NondeterministicModel.cpp @@ -90,6 +90,13 @@ namespace storm { out << ", nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)"; } + template + void NondeterministicModel::reduceToStateBasedRewards() { + for (auto& rewardModel : this->getRewardModels()) { + rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), false); + } + } + template void NondeterministicModel::createIllegalMask() { // Prepare the mask of illegal nondeterministic choices. diff --git a/src/storm/models/symbolic/NondeterministicModel.h b/src/storm/models/symbolic/NondeterministicModel.h index ecbc2af94..c75874644 100644 --- a/src/storm/models/symbolic/NondeterministicModel.h +++ b/src/storm/models/symbolic/NondeterministicModel.h @@ -124,6 +124,8 @@ namespace storm { virtual void printModelInformationToStream(std::ostream& out) const override; + virtual void reduceToStateBasedRewards() override; + protected: virtual void printDdVariableInformationToStream(std::ostream& out) const override; diff --git a/src/storm/models/symbolic/StandardRewardModel.cpp b/src/storm/models/symbolic/StandardRewardModel.cpp index a91040069..8fe296308 100644 --- a/src/storm/models/symbolic/StandardRewardModel.cpp +++ b/src/storm/models/symbolic/StandardRewardModel.cpp @@ -6,6 +6,8 @@ #include "storm/adapters/RationalFunctionAdapter.h" +#include "storm/exceptions/InvalidOperationException.h" + namespace storm { namespace models { namespace symbolic { @@ -157,6 +159,28 @@ namespace storm { return StandardRewardModel(modifiedStateRewardVector, this->optionalStateActionRewardVector, this->optionalTransitionRewardMatrix); } + template + void StandardRewardModel::reduceToStateBasedRewards(storm::dd::Add const& transitionMatrix, std::set const& rowVariables, std::set const& columnVariables, bool reduceToStateRewards) { + if (this->hasTransitionRewards()) { + if (this->hasStateActionRewards()) { + this->optionalStateActionRewardVector.get() += transitionMatrix.multiplyMatrix(this->getTransitionRewardMatrix(), columnVariables); + this->optionalTransitionRewardMatrix = boost::none; + } else { + this->optionalStateActionRewardVector = transitionMatrix.multiplyMatrix(this->getTransitionRewardMatrix(), columnVariables); + } + } + + if (reduceToStateRewards && this->hasStateActionRewards()) { + STORM_LOG_THROW(this->getStateActionRewardVector().getContainedMetaVariables() == rowVariables, storm::exceptions::InvalidOperationException, "The reduction to state rewards is only possible if the state-action rewards do not depend on nondeterminism variables."); + if (this->hasStateRewards()) { + this->optionalStateRewardVector = this->optionalStateRewardVector.get() + this->getStateActionRewardVector(); + } else { + this->optionalStateRewardVector = this->getStateActionRewardVector(); + } + this->optionalStateActionRewardVector = boost::none; + } + } + template class StandardRewardModel; template class StandardRewardModel; diff --git a/src/storm/models/symbolic/StandardRewardModel.h b/src/storm/models/symbolic/StandardRewardModel.h index a4e9fb573..a7ab321f4 100644 --- a/src/storm/models/symbolic/StandardRewardModel.h +++ b/src/storm/models/symbolic/StandardRewardModel.h @@ -189,6 +189,16 @@ namespace storm { */ StandardRewardModel divideStateRewardVector(storm::dd::Add const& divisor) const; + /*! + * Reduces the transition-based rewards to state-action rewards by taking the average of each row. If + * the corresponding flag is set, the state-action rewards and the state rewards are summed so the model + * only has a state reward vector left. Note that this transformation only preserves expected rewards, + * but not all reward-based properties. + * + * @param transitionMatrix The transition matrix that is used to weight the rewards in the reward matrix. + */ + void reduceToStateBasedRewards(storm::dd::Add const& transitionMatrix, std::set const& rowVariables, std::set const& columnVariables, bool reduceToStateRewards); + private: // The state reward vector. boost::optional> optionalStateRewardVector;