From 2e15674580aa8df78698d9f734d05114ee55cfc0 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Sun, 4 Mar 2018 14:55:23 +0100
Subject: [PATCH] fixed an issue in state-act reward refinement for nondet
 models

---
 .../NondeterministicModelPartitionRefiner.cpp        | 12 ++++++++++++
 .../NondeterministicModelPartitionRefiner.h          |  2 ++
 2 files changed, 14 insertions(+)

diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
index 129c426c7..d047acfde 100644
--- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
+++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.cpp
@@ -73,6 +73,18 @@ namespace storm {
                 return choicePartition;
             }
             
+            template <storm::dd::DdType DdType, typename ValueType>
+            bool NondeterministicModelPartitionRefiner<DdType, ValueType>::refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards) {
+                STORM_LOG_TRACE("Refining with respect to state rewards.");
+                Partition<DdType, ValueType> newStatePartition = this->stateSignatureRefiner.refine(this->statePartition, Signature<DdType, ValueType>(stateRewards));
+                if (newStatePartition == this->statePartition) {
+                    return false;
+                } else {
+                    this->statePartition = newStatePartition;
+                    return true;
+                }
+            }
+            
             template<storm::dd::DdType DdType, typename ValueType>
             bool NondeterministicModelPartitionRefiner<DdType, ValueType>::refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) {
                 STORM_LOG_TRACE("Refining with respect to state-action rewards.");
diff --git a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h
index bf2717998..0dae7f90e 100644
--- a/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h
+++ b/src/storm/storage/dd/bisimulation/NondeterministicModelPartitionRefiner.h
@@ -34,6 +34,8 @@ namespace storm {
             private:
                 virtual bool refineWrtStateActionRewards(storm::dd::Add<DdType, ValueType> const& stateActionRewards) override;
                 
+                virtual bool refineWrtStateRewards(storm::dd::Add<DdType, ValueType> const& stateRewards) override;
+                
                 // The model to refine.
                 storm::models::symbolic::NondeterministicModel<DdType, ValueType> const& model;