fixed some issues with reward preservation in dd-based bisimulation

src/storm/builder/DdPrismModelBuilder.cpp

@@ -1240,7 +1240,7 @@ namespace storm {
                         }
                         stateActionRewardDd *= stateActionDd.get();
                     } else if (generationInfo.program.getModelType() == storm::prism::Program::ModelType::DTMC || generationInfo.program.getModelType() == storm::prism::Program::ModelType::CTMC) {
-                        // For CTMCs, we need to multiply the entries with the exit rate of the corresponding action.
+                        // For DTMCs and CTMC, we need to multiply the entries with the multiplicity/exit rate of the corresponding action.
                         stateActionRewardDd *= actionDd.transitionsDd.sumAbstract(generationInfo.columnMetaVariables);
                     }
                     

src/storm/storage/dd/BisimulationDecomposition.cpp

@@ -29,17 +29,17 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
-            // Intentionally left empty.
+            this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, storm::storage::BisimulationType const& bisimulationType) : model(model), preservationInformation(model, formulas, bisimulationType), refiner(createRefiner(model, Partition<DdType, ValueType>::create(model, bisimulationType, preservationInformation))) {
-            // Intentionally left empty.
+            this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
         BisimulationDecomposition<DdType, ValueType>::BisimulationDecomposition(storm::models::symbolic::Model<DdType, ValueType> const& model, Partition<DdType, ValueType> const& initialPartition, bisimulation::PreservationInformation<DdType, ValueType> const& preservationInformation) : model(model), preservationInformation(preservationInformation), refiner(createRefiner(model, initialPartition)) {
-            STORM_LOG_THROW(!model.hasRewardModel(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support preserving rewards.");
+            this->refineWrtRewardModels();
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
@@ -79,6 +79,14 @@ namespace storm {
             return quotient;
         }
         
+        template <storm::dd::DdType DdType, typename ValueType>
+        void BisimulationDecomposition<DdType, ValueType>::refineWrtRewardModels() {
+            for (auto const& rewardModelName : this->preservationInformation.getRewardModelNames()) {
+                auto const& rewardModel = this->model.getRewardModel(rewardModelName);
+                refiner->refineWrtRewardModel(rewardModel);
+            }
+        }
+        
         template class BisimulationDecomposition<storm::dd::DdType::CUDD, double>;
 
         template class BisimulationDecomposition<storm::dd::DdType::Sylvan, double>;

src/storm/storage/dd/BisimulationDecomposition.h

@@ -50,6 +50,8 @@ namespace storm {
             std::shared_ptr<storm::models::Model<ValueType>> getQuotient() const;
             
         private:
+            void refineWrtRewardModels();
+            
             // The model for which to compute the bisimulation decomposition.
             storm::models::symbolic::Model<DdType, ValueType> const& model;
             

src/storm/storage/dd/Dd.cpp

@@ -78,7 +78,7 @@ namespace storm {
         template<DdType LibraryType>
         std::set<storm::expressions::Variable> Dd<LibraryType>::subtractMetaVariables(storm::dd::Dd<LibraryType> const& first, storm::dd::Dd<LibraryType> const& second) {
             bool includesAllMetaVariables = std::includes(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end());
-            STORM_LOG_THROW(includesAllMetaVariables, storm::exceptions::InvalidArgumentException, "Cannot subtract meta variables that are not contained in the DD.");
+            STORM_LOG_WARN_COND(includesAllMetaVariables, "Subtracting from meta variables that are not contained in the DD.");
             std::set<storm::expressions::Variable> metaVariables;
             std::set_difference(first.getContainedMetaVariables().begin(), first.getContainedMetaVariables().end(), second.getContainedMetaVariables().begin(), second.getContainedMetaVariables().end(), std::inserter(metaVariables, metaVariables.begin()));
             return metaVariables;

src/storm/storage/dd/bisimulation/MdpPartitionRefiner.cpp

@@ -49,8 +49,14 @@ namespace storm {
             }
             
             template<storm::dd::DdType DdType, typename ValueType>
-            bool MdpPartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
+            bool MdpPartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
                 Partition<DdType, ValueType> newChoicePartition = this->signatureRefiner.refine(this->choicePartition, Signature<DdType, ValueType>(stateActionRewards));
+                if (newChoicePartition == this->choicePartition) {
+                    return false;
+                } else {
+                    this->choicePartition = newChoicePartition;
+                    return true;
+                }
             }
             
             template class MdpPartitionRefiner<storm::dd::DdType::CUDD, double>;

src/storm/storage/dd/bisimulation/MdpPartitionRefiner.h

@@ -32,7 +32,7 @@ namespace storm {
                 Partition<DdType, ValueType> const& getChoicePartition() const;
                 
             private:
-                virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards) override;
+                virtual bool refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) override;
                 
                 // The choice partition in the refinement process.
                 Partition<DdType, ValueType> choicePartition;

src/storm/storage/dd/bisimulation/PartitionRefiner.cpp

@@ -73,20 +73,22 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            bool PartitionRefiner<DdType, ValueType>::refineWrtRewardModel(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel) {
-                STORM_LOG_THROW(rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards.");
+            bool PartitionRefiner<DdType, ValueType>::refineWrtRewardModel(storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel) {
+                STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Symbolic bisimulation currently does not support transition rewards.");
+                STORM_LOG_TRACE("Refining with respect to reward model.");
                 bool result = false;
-                if (rewardModel.hasStateActionRewards()) {
-                    result |= refineWrtStateActionRewards(model, rewardModel.getStateActionRewardVector());
-                }
                 if (rewardModel.hasStateRewards()) {
-                    result |= refineWrtStateRewards(model, rewardModel.getStateActionRewardVector());
+                    result |= refineWrtStateRewards(rewardModel.getStateRewardVector());
+                }
+                if (rewardModel.hasStateActionRewards()) {
+                    result |= refineWrtStateRewards(rewardModel.getStateActionRewardVector());
                 }
                 return result;
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            bool PartitionRefiner<DdType, ValueType>::refineWrtStateRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateRewards) {
+            bool PartitionRefiner<DdType, ValueType>::refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards) {
+                STORM_LOG_TRACE("Refining with respect to state rewards.");
                 Partition<DdType, ValueType> newPartition = signatureRefiner.refine(statePartition, Signature<DdType, ValueType>(stateRewards));
                 if (newPartition == statePartition) {
                     return false;
@@ -97,9 +99,10 @@ namespace storm {
             }
             
             template <storm::dd::DdType DdType, typename ValueType>
-            bool PartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
+            bool PartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
+                STORM_LOG_TRACE("Refining with respect to state-action rewards.");
                 // By default, we treat state-action rewards just like state-rewards, which works for DTMCs and CTMCs.
-                return refineWrtStateRewards(model, stateActionRewards);
+                return refineWrtStateRewards(stateActionRewards);
             }
             
             template <storm::dd::DdType DdType, typename ValueType>

src/storm/storage/dd/bisimulation/PartitionRefiner.h

@@ -36,7 +36,7 @@ namespace storm {
                  * 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<DdType, ValueType> const& model, storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel);
+                bool refineWrtRewardModel(storm::models::symbolic::StandardRewardModel<DdType, ValueType> const& rewardModel);
                 
                 /*!
                  * Retrieves the current state partition in the refinement process.
@@ -51,8 +51,8 @@ namespace storm {
             protected:
                 Partition<DdType, ValueType> internalRefine(SignatureComputer<DdType, ValueType>& stateSignatureComputer, SignatureRefiner<DdType, ValueType>& signatureRefiner, Partition<DdType, ValueType> const& oldPartition, Partition<DdType, ValueType> const& targetPartition, SignatureMode const& mode = SignatureMode::Eager);
                 
-                virtual bool refineWrtStateRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateRewards);
-                virtual bool refineWrtStateActionRewards(storm::models::symbolic::Model<DdType, ValueType> const& model, storm::dd::Add<DdType, ValueType> const& stateActionRewards);
+                virtual bool refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards);
+                virtual bool refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards);
                 
                 // The current status.
                 Status status;