fragment checker checks reward accumulations

src/storm/logic/FragmentChecker.cpp

@@ -70,6 +70,9 @@ namespace storm {
                 } else {
                     assert(tbr.isRewardBound());
                     result = result && inherited.getSpecification().areRewardBoundedUntilFormulasAllowed();
+                    if (tbr.hasRewardAccumulation()) {
+                        result = result && inherited.getSpecification().isRewardAccumulationAllowed();
+                    }
                 }
             }
             
@@ -118,6 +121,7 @@ namespace storm {
             
             bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed();
             result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed());
+            result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
             for (uint64_t i = 0; i < f.getDimension(); ++i) {
                 auto tbr = f.getTimeBoundReference(i);
                 if (tbr.isStepBound()) {
@@ -127,6 +131,9 @@ namespace storm {
                 } else {
                     assert(tbr.isRewardBound());
                     result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed();
+                    if (tbr.hasRewardAccumulation()) {
+                        result = result && inherited.getSpecification().isRewardAccumulationAllowed();
+                    }
                 }
             }
             return result;
@@ -140,12 +147,15 @@ namespace storm {
                 if (!inherited.getSpecification().areNestedPathFormulasAllowed()) {
                     result = result && !f.getSubformula().isPathFormula();
                 }
+                result = result && !f.hasRewardAccumulation();
             } else if (f.isReachabilityRewardFormula()) {
                 result = result && inherited.getSpecification().areReachabilityRewardFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
+                result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
             } else if (f.isReachabilityTimeFormula()) {
                 result = result && inherited.getSpecification().areReachbilityTimeFormulasAllowed();
                 result = result && f.getSubformula().isStateFormula();
+                result = result && (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
             }
             result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
             return result;
@@ -250,6 +260,7 @@ namespace storm {
             result = result && (!f.hasQuantitativeResult() || inherited.getSpecification().areQuantitativeOperatorResultsAllowed());
             result = result && (f.getSubformula().isRewardPathFormula() || f.getSubformula().isConditionalRewardFormula());
             result = result && (inherited.getSpecification().isVarianceMeasureTypeAllowed() || f.getMeasureType() == RewardMeasureType::Expectation);
+            
             if (!inherited.getSpecification().areNestedOperatorsAllowed()) {
                 result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, InheritedInformation(inherited.getSpecification().copy().setOperatorsAllowed(false))));
             } else {
@@ -258,9 +269,11 @@ namespace storm {
             return result;
         }
         
-        boost::any FragmentChecker::visit(TotalRewardFormula const&, boost::any const& data) const {
+        boost::any FragmentChecker::visit(TotalRewardFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
-            return inherited.getSpecification().areTotalRewardFormulasAllowed();
+            bool result = (!f.hasRewardAccumulation() || inherited.getSpecification().isRewardAccumulationAllowed());
+            result = result && inherited.getSpecification().areTotalRewardFormulasAllowed();
+            return result;
         }
         
         boost::any FragmentChecker::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {

src/storm/logic/FragmentSpecification.cpp

@@ -1,6 +1,7 @@
 #include "storm/logic/FragmentSpecification.h"
 
 #include <iostream>
+#include "storm/logic/RewardAccumulation.h"
 
 namespace storm {
     namespace logic {
@@ -161,6 +162,8 @@ namespace storm {
             operatorAtTopLevelRequired = false;
             multiObjectiveFormulaAtTopLevelRequired = false;
             operatorsAtTopLevelOfMultiObjectiveFormulasRequired = false;
+            
+            rewardAccumulation = false;
         }
         
         FragmentSpecification FragmentSpecification::copy() const {
@@ -564,5 +567,15 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::isRewardAccumulationAllowed() const {
+            return rewardAccumulation;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setRewardAccumulationAllowed(bool newValue) {
+            rewardAccumulation = newValue;
+            return *this;
+        }
+
+        
     }
 }

src/storm/logic/FragmentSpecification.h

@@ -1,8 +1,14 @@
 #ifndef STORM_LOGIC_FRAGMENTSPECIFICATION_H_
 #define STORM_LOGIC_FRAGMENTSPECIFICATION_H_
 
+#include <map>
+#include <string>
+
 namespace storm {
     namespace logic {
+        
+        class RewardAccumulation;
+        
         class FragmentSpecification {
         public:
             FragmentSpecification();
@@ -139,6 +145,10 @@ namespace storm {
             bool areOperatorsAtTopLevelOfMultiObjectiveFormulasRequired() const;
             FragmentSpecification& setOperatorsAtTopLevelOfMultiObjectiveFormulasRequired(bool newValue);
             
+            bool isRewardAccumulationAllowed() const;
+            FragmentSpecification& setRewardAccumulationAllowed(bool newValue);
+
+            
             FragmentSpecification& setOperatorsAllowed(bool newValue);
             FragmentSpecification& setTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
@@ -195,6 +205,8 @@ namespace storm {
             bool operatorAtTopLevelRequired;
             bool multiObjectiveFormulaAtTopLevelRequired;
             bool operatorsAtTopLevelOfMultiObjectiveFormulasRequired;
+            
+            bool rewardAccumulation;
         };
         
         // Propositional.

src/storm/logic/RewardAccumulation.cpp

@@ -19,6 +19,10 @@ namespace storm {
             return exit;
         }
 
+        bool RewardAccumulation::implies(RewardAccumulation const& other) const {
+            return (!isStepsSet() || other.isStepsSet()) && (!isTimeSet() || other.isTimeSet()) && (!isExitSet() || other.isExitSet());
+        }
+
         std::ostream& operator<<(std::ostream& out, RewardAccumulation const& acc) {
             bool hasEntry = false;
             if (acc.isStepsSet()) {

src/storm/logic/RewardAccumulation.h

@@ -13,6 +13,8 @@ namespace storm {
             bool isTimeSet() const; // If set, state rewards are accumulated over time (assuming 0 time passes in discrete-time model states)
             bool isExitSet() const; // If set, state rewards are accumulated upon exiting the state
             
+            // Returns true, if every reward-type set in this RewardAccumulation is also set for the other RewardAccumulation
+            bool implies(RewardAccumulation const& other) const;
         private:
             bool time, steps, exit;
         };