added reduction to state-based rewards to symbolic (reward) models

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<DdType, ValueType> decomposition(*model, formulas, bisimulationType);
             decomposition.compute(mode);
             return decomposition.getQuotient();

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;

src/storm/models/sparse/Model.h

@@ -292,16 +292,7 @@ namespace storm {
                  * @return The choice origins, if they're saved.
                  */
                 boost::optional<std::shared_ptr<storm::storage::sparse::ChoiceOrigins>>&  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.
                  *

src/storm/models/symbolic/DeterministicModel.cpp

@@ -45,6 +45,13 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            void DeterministicModel<Type, ValueType>::reduceToStateBasedRewards() {
+                for (auto& rewardModel : this->getRewardModels()) {
+                    rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), true);
+                }
+            }
+            
             // Explicitly instantiate the template class.
             template class DeterministicModel<storm::dd::DdType::CUDD>;
             template class DeterministicModel<storm::dd::DdType::Sylvan>;

src/storm/models/symbolic/DeterministicModel.h

@@ -80,6 +80,8 @@ namespace storm {
                                    std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
                                    std::map<std::string, storm::dd::Bdd<Type>> labelToBddMap = std::map<std::string, storm::dd::Bdd<Type>>(),
                                    std::unordered_map<std::string, RewardModelType> const& rewardModels = std::unordered_map<std::string, RewardModelType>());
+                
+                virtual void reduceToStateBasedRewards() override;
             };
             
         } // namespace symbolic

src/storm/models/symbolic/Model.cpp

@@ -255,11 +255,16 @@ namespace storm {
                 return !this->rewardModels.empty();
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            std::unordered_map<std::string, typename Model<Type, ValueType>::RewardModelType>& Model<Type, ValueType>::getRewardModels() {
+                return this->rewardModels;
+            }
+
             template<storm::dd::DdType Type, typename ValueType>
             std::unordered_map<std::string, typename Model<Type, ValueType>::RewardModelType> const& Model<Type, ValueType>::getRewardModels() const {
                 return this->rewardModels;
             }
-            
+
             template<storm::dd::DdType Type, typename ValueType>
             void Model<Type, ValueType>::printModelInformationToStream(std::ostream& out) const {
                 this->printModelInformationHeaderToStream(out);

src/storm/models/symbolic/Model.h

@@ -298,6 +298,7 @@ namespace storm {
                  */
                 bool hasRewardModel() const;
 
+                std::unordered_map<std::string, RewardModelType>& getRewardModels();
                 std::unordered_map<std::string, RewardModelType> const& getRewardModels() const;
                 
                 /*!

src/storm/models/symbolic/NondeterministicModel.cpp

@@ -90,6 +90,13 @@ namespace storm {
                 out << ", nondeterminism: " << this->getNondeterminismVariables().size() << " meta variables (" << nondeterminismVariableCount << " DD variables)";
             }
             
+            template<storm::dd::DdType Type, typename ValueType>
+            void NondeterministicModel<Type, ValueType>::reduceToStateBasedRewards() {
+                for (auto& rewardModel : this->getRewardModels()) {
+                    rewardModel.second.reduceToStateBasedRewards(this->getTransitionMatrix(), this->getRowVariables(), this->getColumnVariables(), false);
+                }
+            }
+            
             template<storm::dd::DdType Type, typename ValueType>
             void NondeterministicModel<Type, ValueType>::createIllegalMask() {
                 // Prepare the mask of illegal nondeterministic choices.

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;

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<Type, ValueType>(modifiedStateRewardVector, this->optionalStateActionRewardVector, this->optionalTransitionRewardMatrix);
             }
             
+            template <storm::dd::DdType Type, typename ValueType>
+            void StandardRewardModel<Type, ValueType>::reduceToStateBasedRewards(storm::dd::Add<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> 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<storm::dd::DdType::CUDD, double>;
             template class StandardRewardModel<storm::dd::DdType::Sylvan, double>;
 

src/storm/models/symbolic/StandardRewardModel.h

@@ -189,6 +189,16 @@ namespace storm {
                  */
                 StandardRewardModel<Type, ValueType> divideStateRewardVector(storm::dd::Add<Type, ValueType> 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<Type, ValueType> const& transitionMatrix, std::set<storm::expressions::Variable> const& rowVariables, std::set<storm::expressions::Variable> const& columnVariables, bool reduceToStateRewards);
+                
             private:
                 // The state reward vector.
                 boost::optional<storm::dd::Add<Type, ValueType>> optionalStateRewardVector;