Fixed that bisimulation did not preserve reward bounded formulas

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;
+        }
     }
 }

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;
         };
         
     }

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());