From c7d9b0b61dfa2f25158edf86889467aa555a2148 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 12 Oct 2017 21:29:07 +0200
Subject: [PATCH] Fixed that bisimulation did not preserve reward bounded
 formulas

---
 src/storm/logic/FormulaInformation.cpp        | 20 +++++++++++++++++++
 src/storm/logic/FormulaInformation.h          |  6 ++++++
 .../BisimulationDecomposition.cpp             |  8 ++++----
 3 files changed, 30 insertions(+), 4 deletions(-)

diff --git a/src/storm/logic/FormulaInformation.cpp b/src/storm/logic/FormulaInformation.cpp
index 88bb67b1a..900da239a 100644
--- a/src/storm/logic/FormulaInformation.cpp
+++ b/src/storm/logic/FormulaInformation.cpp
@@ -20,11 +20,21 @@ namespace storm {
             return this->mContainsBoundedUntilFormula;
         }
         
+        bool FormulaInformation::containsCumulativeRewardFormula() const {
+            return this->mContainsCumulativeRewardFormula;
+        }
+        
+        bool FormulaInformation::containsRewardBoundedFormula() const {
+            return this->mContainsRewardBoundedFormula;
+        }
+        
         FormulaInformation FormulaInformation::join(FormulaInformation const& other) {
             FormulaInformation result;
             result.mContainsRewardOperator = this->containsRewardOperator() || other.containsRewardOperator();
             result.mContainsNextFormula = this->containsNextFormula() || other.containsNextFormula();
             result.mContainsBoundedUntilFormula = this->containsBoundedUntilFormula() || other.containsBoundedUntilFormula();
+            result.mContainsCumulativeRewardFormula = this->containsCumulativeRewardFormula() || other.containsCumulativeRewardFormula();
+            result.mContainsRewardBoundedFormula = this->containsRewardBoundedFormula() || other.containsRewardBoundedFormula();
             return result;
         }
         
@@ -42,5 +52,15 @@ namespace storm {
             this->mContainsBoundedUntilFormula = newValue;
             return *this;
         }
+        
+        FormulaInformation& FormulaInformation::setContainsCumulativeRewardFormula(bool newValue) {
+            this->mContainsCumulativeRewardFormula = newValue;
+            return *this;
+        }
+        
+        FormulaInformation& FormulaInformation::setContainsRewardBoundedFormula(bool newValue) {
+            this->mContainsRewardBoundedFormula = newValue;
+            return *this;
+        }
     }
 }
diff --git a/src/storm/logic/FormulaInformation.h b/src/storm/logic/FormulaInformation.h
index 344f69499..06e1ff4ea 100644
--- a/src/storm/logic/FormulaInformation.h
+++ b/src/storm/logic/FormulaInformation.h
@@ -15,17 +15,23 @@ namespace storm {
             bool containsRewardOperator() const;
             bool containsNextFormula() const;
             bool containsBoundedUntilFormula() const;
+            bool containsCumulativeRewardFormula() const;
+            bool containsRewardBoundedFormula() const;
             
             FormulaInformation join(FormulaInformation const& other);
             
             FormulaInformation& setContainsRewardOperator(bool newValue = true);
             FormulaInformation& setContainsNextFormula(bool newValue = true);
             FormulaInformation& setContainsBoundedUntilFormula(bool newValue = true);
+            FormulaInformation& setContainsCumulativeRewardFormula(bool newValue = true);
+            FormulaInformation& setContainsRewardBoundedFormula(bool newValue = true);
             
         private:
             bool mContainsRewardOperator;
             bool mContainsNextFormula;
             bool mContainsBoundedUntilFormula;
+            bool mContainsCumulativeRewardFormula;
+            bool mContainsRewardBoundedFormula;
         };
         
     }
diff --git a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp
index e7a3fab50..fbeb10648 100644
--- a/src/storm/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storm/storage/bisimulation/BisimulationDecomposition.cpp
@@ -62,10 +62,10 @@ namespace storm {
             storm::logic::FormulaInformation info = formula.info();
             
             // Preserve rewards if necessary.
-            keepRewards = keepRewards || info.containsRewardOperator();
+            keepRewards = keepRewards || info.containsRewardOperator() || info.containsRewardBoundedFormula();
             
             // Preserve bounded properties if necessary.
-            bounded = bounded || (info.containsBoundedUntilFormula() || info.containsNextFormula());
+            bounded = bounded || (info.containsBoundedUntilFormula() || info.containsNextFormula() || info.containsCumulativeRewardFormula());
             
             // Compute the relevant labels and expressions.
             this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());
@@ -76,10 +76,10 @@ namespace storm {
             // Retrieve information about formula.
             storm::logic::FormulaInformation info = formula.info();
 
-            keepRewards = info.containsRewardOperator();
+            keepRewards = info.containsRewardOperator() || info.containsRewardBoundedFormula();
             
             // We need to preserve bounded properties iff the formula contains a bounded until or a next subformula.
-            bounded = info.containsBoundedUntilFormula() || info.containsNextFormula();
+            bounded = info.containsBoundedUntilFormula() || info.containsNextFormula() || info.containsCumulativeRewardFormula();
             
             // Compute the relevant labels and expressions.
             this->addToRespectedAtomicPropositions(formula.getAtomicExpressionFormulas(), formula.getAtomicLabelFormulas());