Multi-dimensional cumulative reward formulas

src/storm/logic/BoundedUntilFormula.cpp

@@ -278,14 +278,19 @@ namespace storm {
                 
                 out << " U";
                 if (this->isMultiDimensional()) {
-                    out << "[";
+                    out << "^{";
                 }
-                for(unsigned i = 0; i < this->getDimension(); ++i) {
+                for (unsigned i = 0; i < this->getDimension(); ++i) {
                     if (i > 0) {
                         out << ",";
                     }
                     if (this->getTimeBoundReference(i).isRewardBound()) {
-                        out << "{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
+                        out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
+                    } else if (this->getTimeBoundReference(i).isStepBound()) {
+                        out << "steps";
+                  //} else if (this->getTimeBoundReference(i).isStepBound())
+                  //  Note: the 'time' keyword is optional.
+                  //    out << "time";
                     }
                     if (this->hasLowerBound(i)) {
                         if (this->hasUpperBound(i)) {
@@ -321,7 +326,7 @@ namespace storm {
                     out << " ";
                 }
                 if (this->isMultiDimensional()) {
-                    out << "]";
+                    out << "}";
                 }
                 
                 this->getRightSubformula().writeToStream(out);

src/storm/logic/CumulativeRewardFormula.cpp

@@ -9,10 +9,16 @@
 
 namespace storm {
     namespace logic {
-        CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReference(timeBoundReference), bound(bound) {
+        CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReferences({timeBoundReference}), bounds({bound}) {
             // Intentionally left empty.
         }
 
+        CumulativeRewardFormula::CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences) : timeBoundReferences(timeBoundReferences), bounds(bounds) {
+
+            STORM_LOG_ASSERT(this->timeBoundReferences.size() == this->bounds.size(), "Number of time bounds and number of time bound references does not match.");
+            STORM_LOG_ASSERT(!this->timeBoundReferences.empty(), "No time bounds given.");
+        }
+
         bool CumulativeRewardFormula::isCumulativeRewardFormula() const {
             return true;
         }
@@ -21,74 +27,95 @@ namespace storm {
             return true;
         }
         
+        bool CumulativeRewardFormula::isMultiDimensional() const {
+            return getDimension() > 1;
+        }
+        
+        unsigned CumulativeRewardFormula::getDimension() const {
+            return timeBoundReferences.size();
+        }
+        
         boost::any CumulativeRewardFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
         
         void CumulativeRewardFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
-            if (this->isRewardBounded()) {
-                referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
+            for (unsigned i = 0; i < this->getDimension(); ++i) {
+                if (getTimeBoundReference(i).isRewardBound()) {
+                    referencedRewardModels.insert(this->getTimeBoundReference(i).getRewardName());
+                }
             }
         }
         
-        TimeBoundType CumulativeRewardFormula::getTimeBoundType() const {
-            return timeBoundReference.getType();
-        }
-        
         TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference() const {
-            return timeBoundReference;
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
+            return getTimeBoundReference(0);
         }
 
-        bool CumulativeRewardFormula::isStepBounded() const {
-            return getTimeBoundType() == TimeBoundType::Steps;
+        TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference(unsigned i) const {
+            return timeBoundReferences.at(i);
         }
-        
-        bool CumulativeRewardFormula::isTimeBounded() const {
-            return getTimeBoundType() == TimeBoundType::Time;
+
+        bool CumulativeRewardFormula::isBoundStrict() const {
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
+            return isBoundStrict(0);
         }
         
-        bool CumulativeRewardFormula::isRewardBounded() const {
-            return getTimeBoundType() == TimeBoundType::Reward;
+        bool CumulativeRewardFormula::isBoundStrict(unsigned i) const {
+            return bounds.at(i).isStrict();
         }
         
-        bool CumulativeRewardFormula::isBoundStrict() const {
-            return bound.isStrict();
+        bool CumulativeRewardFormula::hasIntegerBound() const {
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
+            return hasIntegerBound(0);
         }
         
-        bool CumulativeRewardFormula::hasIntegerBound() const {
-            return bound.getBound().hasIntegerType();
+        bool CumulativeRewardFormula::hasIntegerBound(unsigned i) const {
+            return bounds.at(i).getBound().hasIntegerType();
         }
         
         storm::expressions::Expression const& CumulativeRewardFormula::getBound() const {
-            return bound.getBound();
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
+            return getBound(0);
+        }
+        
+        storm::expressions::Expression const& CumulativeRewardFormula::getBound(unsigned i) const {
+            return bounds.at(i).getBound();
+        }
+        
+        template <typename  ValueType>
+        ValueType CumulativeRewardFormula::getBound() const {
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
+            return getBound<ValueType>(0);
         }
         
         template <>
-        double CumulativeRewardFormula::getBound() const {
-            checkNoVariablesInBound(bound.getBound());
-            double value = bound.getBound().evaluateAsDouble();
-            STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
+        double CumulativeRewardFormula::getBound(unsigned i) const {
+            checkNoVariablesInBound(bounds.at(i).getBound());
+            double value = bounds.at(i).getBound().evaluateAsDouble();
+            STORM_LOG_THROW(value >= 0.0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
 
         template <>
-        storm::RationalNumber CumulativeRewardFormula::getBound() const {
-            checkNoVariablesInBound(bound.getBound());
-            storm::RationalNumber value = bound.getBound().evaluateAsRational();
+        storm::RationalNumber CumulativeRewardFormula::getBound(unsigned i) const {
+            checkNoVariablesInBound(bounds.at(i).getBound());
+            storm::RationalNumber value = bounds.at(i).getBound().evaluateAsRational();
             STORM_LOG_THROW(value >= storm::utility::zero<storm::RationalNumber>(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
 
         template <>
-        uint64_t CumulativeRewardFormula::getBound() const {
-            checkNoVariablesInBound(bound.getBound());
-            uint64_t value = bound.getBound().evaluateAsInt();
+        uint64_t CumulativeRewardFormula::getBound(unsigned i) const {
+            checkNoVariablesInBound(bounds.at(i).getBound());
+            uint64_t value = bounds.at(i).getBound().evaluateAsInt();
             STORM_LOG_THROW(value >= 0, storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number.");
             return value;
         }
         
         template <>
         double CumulativeRewardFormula::getNonStrictBound() const {
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
             double bound = getBound<double>();
             STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
             return bound;
@@ -96,6 +123,7 @@ namespace storm {
         
         template <>
         uint64_t CumulativeRewardFormula::getNonStrictBound() const {
+            STORM_LOG_ASSERT(!isMultiDimensional(), "Cumulative Reward Formula is multi-dimensional.");
             int_fast64_t bound = getBound<uint64_t>();
             if (isBoundStrict()) {
                 STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
@@ -109,13 +137,43 @@ namespace storm {
             STORM_LOG_THROW(!bound.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate time-bound '" << bound << "' as it contains undefined constants.");
         }
         
+        std::shared_ptr<CumulativeRewardFormula const> CumulativeRewardFormula::restrictToDimension(unsigned i) const {
+            return std::make_shared<CumulativeRewardFormula const>(bounds.at(i), getTimeBoundReference(i));
+        }
+        
         std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
             out << "C";
-             if(getTimeBoundReference().isRewardBound()) {
-                out << "{\"" << getTimeBoundReference().getRewardName() << "\"}";
-             }
-             out << "<=" << this->getBound();
+            if (this->isMultiDimensional()) {
+                out << "^{";
+            }
+            for (unsigned i = 0; i < this->getDimension(); ++i) {
+                if (i > 0) {
+                    out << ",";
+                }
+                if (this->getTimeBoundReference(i).isRewardBound()) {
+                    out << "rew{\"" << this->getTimeBoundReference(i).getRewardName() << "\"}";
+                } else if (this->getTimeBoundReference(i).isStepBound()) {
+                    out << "steps";
+              //} else if (this->getTimeBoundReference(i).isStepBound())
+              //  Note: the 'time' keyword is optional.
+              //    out << "time";
+                }
+                if (this->isBoundStrict(i)) {
+                    out << "<";
+                } else {
+                    out << "<=";
+                }
+                out << this->getBound(i);
+            }
+            if (this->isMultiDimensional()) {
+                out << "}";
+            }
             return out;
         }
+        
+        template uint64_t CumulativeRewardFormula::getBound<uint64_t>() const;
+        template double CumulativeRewardFormula::getBound<double>() const;
+        template storm::RationalNumber CumulativeRewardFormula::getBound<storm::RationalNumber>() const;
+        
     }
 }

src/storm/logic/CumulativeRewardFormula.h

@@ -11,43 +11,49 @@ namespace storm {
         class CumulativeRewardFormula : public PathFormula {
         public:
             CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time));
+            CumulativeRewardFormula(std::vector<TimeBound> const& bounds, std::vector<TimeBoundReference> const& timeBoundReferences);
             
-            virtual ~CumulativeRewardFormula() {
-                // Intentionally left empty.
-            }
+            virtual ~CumulativeRewardFormula() = default;
 
             virtual bool isCumulativeRewardFormula() const override;
             virtual bool isRewardPathFormula() const override;
             
+            bool isMultiDimensional() const;
+            unsigned getDimension() const;
+
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
 
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            TimeBoundType getTimeBoundType() const;
             TimeBoundReference const& getTimeBoundReference() const;
-            
-            bool isStepBounded() const;
-            bool isTimeBounded() const;
-            bool isRewardBounded() const;
+            TimeBoundReference const& getTimeBoundReference(unsigned i) const;
             
             bool isBoundStrict() const;
+            bool isBoundStrict(unsigned i) const;
             bool hasIntegerBound() const;
+            bool hasIntegerBound(unsigned i) const;
             
             storm::expressions::Expression const& getBound() const;
+            storm::expressions::Expression const& getBound(unsigned i) const;
             
             template <typename ValueType>
             ValueType getBound() const;
             
+            template <typename ValueType>
+            ValueType getBound(unsigned i) const;
+            
             template <typename ValueType>
             ValueType getNonStrictBound() const;
             
+            std::shared_ptr<CumulativeRewardFormula const> restrictToDimension(unsigned i) const;
+            
         private:
             static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
 
-            TimeBoundReference timeBoundReference;
-            TimeBound bound;
+            std::vector<TimeBoundReference> timeBoundReferences;
+            std::vector<TimeBound> bounds;
         };
     }
 }

src/storm/logic/FormulaInformationVisitor.cpp

@@ -28,18 +28,18 @@ namespace storm {
         boost::any FormulaInformationVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
             FormulaInformation result;
             result.setContainsBoundedUntilFormula(true);
+            for (unsigned i = 0; i < f.getDimension(); ++i) {
+                if (f.getTimeBoundReference(i).isRewardBound()) {
+                    result.setContainsRewardBoundedFormula(true);
+                }
+            }
+            
             if (f.hasMultiDimensionalSubformulas()) {
-                for (unsigned i = 0; i < f.getDimension(); ++i){
-                    if (f.getTimeBoundReference(i).isRewardBound()) {
-                        result.setContainsRewardBoundedFormula(true);
-                    }
+                for (unsigned i = 0; i < f.getDimension(); ++i) {
                     result.join(boost::any_cast<FormulaInformation>(f.getLeftSubformula(i).accept(*this, data)));
                     result.join(boost::any_cast<FormulaInformation>(f.getRightSubformula(i).accept(*this, data)));
                 }
             } else {
-                if (f.getTimeBoundReference().isRewardBound()) {
-                    result.setContainsRewardBoundedFormula(true);
-                }
                 result.join(boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)));
                 result.join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this, data)));
             }
@@ -53,8 +53,10 @@ namespace storm {
         boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
             FormulaInformation result;
             result.setContainsCumulativeRewardFormula(true);
-            if (f.getTimeBoundReference().isRewardBound()) {
-                result.setContainsRewardBoundedFormula(true);
+            for (unsigned i = 0; i < f.getDimension(); ++i) {
+                if (f.getTimeBoundReference(i).isRewardBound()) {
+                    result.setContainsRewardBoundedFormula(true);
+                }
             }
             return result;
         }

src/storm/logic/FragmentChecker.cpp

@@ -117,14 +117,17 @@ namespace storm {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             
             bool result = inherited.getSpecification().areCumulativeRewardFormulasAllowed();
-            auto const& tbr = f.getTimeBoundReference();
-            if (tbr.isStepBound()) {
-                result = result && inherited.getSpecification().areStepBoundedCumulativeRewardFormulasAllowed();
-            } else if(tbr.isTimeBound()) {
-                result = result && inherited.getSpecification().areTimeBoundedCumulativeRewardFormulasAllowed();
-            } else {
-                assert(tbr.isRewardBound());
-                result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed();
+            result = result && (!f.isMultiDimensional() || inherited.getSpecification().areMultiDimensionalCumulativeRewardFormulasAllowed());
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                auto tbr = f.getTimeBoundReference(i);
+                if (tbr.isStepBound()) {
+                    result = result && inherited.getSpecification().areStepBoundedCumulativeRewardFormulasAllowed();
+                } else if(tbr.isTimeBound()) {
+                    result = result && inherited.getSpecification().areTimeBoundedCumulativeRewardFormulasAllowed();
+                } else {
+                    assert(tbr.isRewardBound());
+                    result = result && inherited.getSpecification().areRewardBoundedCumulativeRewardFormulasAllowed();
+                }
             }
             return result;
         }

src/storm/logic/FragmentSpecification.cpp

@@ -152,6 +152,7 @@ namespace storm {
             stepBoundedCumulativeRewardFormulas = false;
             timeBoundedCumulativeRewardFormulas = false;
             rewardBoundedCumulativeRewardFormulas = false;
+            multiDimensionalCumulativeRewardFormulas = false;
             varianceAsMeasureType = false;
             
             qualitativeOperatorResults = true;
@@ -481,6 +482,15 @@ namespace storm {
             return *this;
         }
         
+        bool FragmentSpecification::areMultiDimensionalCumulativeRewardFormulasAllowed() const {
+            return this->multiDimensionalCumulativeRewardFormulas;
+        }
+
+        FragmentSpecification& FragmentSpecification::setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue) {
+            this->multiDimensionalCumulativeRewardFormulas = newValue;
+            return *this;
+        }
+        
         FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) {
             this->setProbabilityOperatorsAllowed(newValue);
             this->setRewardOperatorsAllowed(newValue);

src/storm/logic/FragmentSpecification.h

@@ -106,6 +106,9 @@ namespace storm {
             bool areRewardBoundedUntilFormulasAllowed() const;
             FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue);
             
+            bool areMultiDimensionalBoundedUntilFormulasAllowed() const;
+            FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue);
+            
             bool areStepBoundedCumulativeRewardFormulasAllowed() const;
             FragmentSpecification& setStepBoundedCumulativeRewardFormulasAllowed(bool newValue);
             
@@ -115,8 +118,8 @@ namespace storm {
             bool areRewardBoundedCumulativeRewardFormulasAllowed() const;
             FragmentSpecification& setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue);
             
-            bool areMultiDimensionalBoundedUntilFormulasAllowed() const;
-            FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue);
+            bool areMultiDimensionalCumulativeRewardFormulasAllowed() const;
+            FragmentSpecification& setMultiDimensionalCumulativeRewardFormulasAllowed(bool newValue);
             
             bool isVarianceMeasureTypeAllowed() const;
             FragmentSpecification& setVarianceMeasureTypeAllowed(bool newValue);
@@ -181,10 +184,11 @@ namespace storm {
             bool stepBoundedUntilFormulas;
             bool timeBoundedUntilFormulas;
             bool rewardBoundedUntilFormulas;
+            bool multiDimensionalBoundedUntilFormulas;
             bool stepBoundedCumulativeRewardFormulas;
             bool timeBoundedCumulativeRewardFormulas;
             bool rewardBoundedCumulativeRewardFormulas;
-            bool multiDimensionalBoundedUntilFormulas;
+            bool multiDimensionalCumulativeRewardFormulas;
             bool varianceAsMeasureType;
             bool quantitativeOperatorResults;
             bool qualitativeOperatorResults;

src/storm/logic/VariableSubstitutionVisitor.cpp

@@ -65,7 +65,13 @@ namespace storm {
         }
         
         boost::any VariableSubstitutionVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
-            return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(storm::logic::TimeBound(f.isBoundStrict(), f.getBound().substitute(substitution)), f.getTimeBoundReference()));
+            std::vector<TimeBound> bounds;
+            std::vector<TimeBoundReference> timeBoundReferences;
+            for (uint64_t i = 0; i < f.getDimension(); ++i) {
+                bounds.emplace_back(TimeBound(f.isBoundStrict(i), f.getBound(i).substitute(substitution)));
+                timeBoundReferences.push_back(f.getTimeBoundReference(i));
+            }
+            return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(bounds, timeBoundReferences));
         }
         
         boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const {

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -352,13 +352,18 @@ namespace storm {
             void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessCumulativeRewardFormula(storm::logic::CumulativeRewardFormula const& formula, storm::logic::OperatorInformation const& opInfo, PreprocessorData& data, boost::optional<std::string> const& optionalRewardModelName) {
                 STORM_LOG_THROW(data.originalModel.isOfType(storm::models::ModelType::Mdp), storm::exceptions::InvalidPropertyException, "Cumulative reward formulas are not supported for the given model type.");
                 
-                storm::logic::TimeBound bound(formula.isBoundStrict(), formula.getBound());
-                storm::logic::TimeBoundReference tbr(formula.getTimeBoundReference());
-                auto cumulativeRewardFormula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, tbr);
+                auto cumulativeRewardFormula = std::make_shared<storm::logic::CumulativeRewardFormula>(formula);
                 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(cumulativeRewardFormula, *optionalRewardModelName, opInfo);
-                data.upperResultBoundObjectives.set(data.objectives.size() - 1, true);
-                if (tbr.isRewardBound()) {
+                bool onlyRewardBounds = true;
+                for (uint64_t i = 0; i < cumulativeRewardFormula->getDimension(); ++i) {
+                    if (!cumulativeRewardFormula->getTimeBoundReference(i).isRewardBound()) {
+                        onlyRewardBounds = false;
+                        break;
+                    }
+                }
+                if (onlyRewardBounds) {
                     data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
+                    data.upperResultBoundObjectives.set(data.objectives.size() - 1, true);
                 }
             }
             
@@ -513,7 +518,6 @@ namespace storm {
                 } else {
                     result.rewardLessInfinityEStates = allStates;
                 }
-                
             }
         
             template<typename SparseModelType>

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h

@@ -50,10 +50,19 @@ namespace storm {
                 }
                 
                 bool containsOnlyTrivialObjectives() const {
+                    // Trivial objectives are either total reward formulas or single-dimensional step or time bounded cumulative reward formulas
                     for (auto const& obj : objectives) {
-                        if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || (obj.formula->getSubformula().isCumulativeRewardFormula() && !obj.formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound())))) {
-                            return false;
+                        if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isTotalRewardFormula()) {
+                            continue;
                         }
+                        if (obj.formula->isRewardOperatorFormula() && obj.formula->getSubformula().isCumulativeRewardFormula()) {
+                            auto const& subf = obj.formula->getSubformula().asCumulativeRewardFormula();
+                            if (!subf.isMultiDimensional() && (subf.getTimeBoundReference().isTimeBound() || subf.getTimeBoundReference().isStepBound())) {
+                                continue;
+                            }
+                        }
+                        // Reaching this point means that the objective is considered as non-trivial
+                        return false;
                     }
                     return true;
                 }

src/storm/modelchecker/multiobjective/pcaa/SparseMaPcaaWeightVectorChecker.cpp

@@ -48,7 +48,7 @@ namespace storm {
                             }
                         }
                     } else {
-                        STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().isTimeBounded(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula());
+                        STORM_LOG_THROW(formula.getSubformula().isCumulativeRewardFormula() && formula.getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isTimeBound(), storm::exceptions::UnexpectedException, "Unexpected type of sub-formula: " << formula.getSubformula());
                         STORM_LOG_THROW(!rewModel.hasStateRewards(), storm::exceptions::InvalidPropertyException, "Found state rewards for time bounded objective " << this->objectives[objIndex].originalFormula << ". This is not supported.");
                         STORM_LOG_WARN_COND(this->objectives[objIndex].originalFormula->isProbabilityOperatorFormula() && this->objectives[objIndex].originalFormula->asProbabilityOperatorFormula().getSubformula().isBoundedUntilFormula(), "Objective " << this->objectives[objIndex].originalFormula << " was simplified to a cumulative reward formula. Correctness of the algorithm is unknown for this type of property.");
                     }

src/storm/modelchecker/multiobjective/rewardbounded/ProductModel.cpp

@@ -406,8 +406,12 @@ namespace storm {
                         STORM_LOG_THROW(!rewModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Reward model has transition rewards which is not expected.");
                         bool rewardCollectedInEpoch = true;
                         if (formula.getSubformula().isCumulativeRewardFormula()) {
-                            assert(objectiveDimensions[objIndex].getNumberOfSetBits() == 1);
-                            rewardCollectedInEpoch = !epochManager.isBottomDimensionEpochClass(epochClass, *objectiveDimensions[objIndex].begin());
+                            for (auto const& dim : objectiveDimensions[objIndex]) {
+                                if (epochManager.isBottomDimensionEpochClass(epochClass, dim)) {
+                                    rewardCollectedInEpoch = false;
+                                    break;
+                                }
+                            }
                         } else {
                             STORM_LOG_THROW(formula.getSubformula().isTotalRewardFormula(), storm::exceptions::UnexpectedException, "Unexpected type of formula " << formula);
                         }

src/storm/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -43,14 +43,14 @@ namespace storm {
         template<typename SparseMdpModelType>
         bool SparseMdpPrctlModelChecker<SparseMdpModelType>::canHandle(CheckTask<storm::logic::Formula, ValueType> const& checkTask) const {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true))) {
+            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true))) {
                 return true;
             } else {
                 // Check whether we consider a multi-objective formula
                 // For multi-objective model checking, each initial state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude multiple initial states.
                 if (this->getModel().getInitialStates().getNumberOfSetBits() > 1) return false;
                 if (!checkTask.isOnlyInitialStatesRelevantSet()) return false;
-                return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true));
+                return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true).setTimeBoundedCumulativeRewardFormulasAllowed(true).setStepBoundedCumulativeRewardFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(true).setMultiDimensionalCumulativeRewardFormulasAllowed(true));
             }
         }
         

src/storm/modelchecker/prctl/helper/rewardbounded/MultiDimensionalRewardUnfolding.cpp

@@ -108,25 +108,27 @@ namespace storm {
                             }
                         } else if (formula.isRewardOperatorFormula() && formula.getSubformula().isCumulativeRewardFormula()) {
                             auto const& subformula = formula.getSubformula().asCumulativeRewardFormula();
-                            Dimension<ValueType> dimension;
-                            dimension.formula = formula.getSubformula().asSharedPointer();
-                            dimension.objectiveIndex = objIndex;
-                            dimension.isUpperBounded = true;
-                            if (subformula.getTimeBoundReference().isTimeBound() || subformula.getTimeBoundReference().isStepBound()) {
-                                dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
-                                dimension.scalingFactor = storm::utility::one<ValueType>();
-                            } else {
-                                STORM_LOG_ASSERT(subformula.getTimeBoundReference().isRewardBound(), "Unexpected type of time bound.");
-                                std::string const& rewardName = subformula.getTimeBoundReference().getRewardName();
-                                STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found.");
-                                auto const& rewardModel = this->model.getRewardModel(rewardName);
-                                STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds.");
-                                std::vector<ValueType> actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix());
-                                auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector<ValueType, uint64_t>(actionRewards);
-                                dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first));
-                                dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second);
+                            for (uint64_t dim = 0; dim < subformula.getDimension(); ++dim) {
+                                Dimension<ValueType> dimension;
+                                dimension.formula = subformula.restrictToDimension(dim);
+                                dimension.objectiveIndex = objIndex;
+                                dimension.isUpperBounded = true;
+                                if (subformula.getTimeBoundReference(dim).isTimeBound() || subformula.getTimeBoundReference(dim).isStepBound()) {
+                                    dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
+                                    dimension.scalingFactor = storm::utility::one<ValueType>();
+                                } else {
+                                    STORM_LOG_ASSERT(subformula.getTimeBoundReference(dim).isRewardBound(), "Unexpected type of time bound.");
+                                    std::string const& rewardName = subformula.getTimeBoundReference(dim).getRewardName();
+                                    STORM_LOG_THROW(this->model.hasRewardModel(rewardName), storm::exceptions::IllegalArgumentException, "No reward model with name '" << rewardName << "' found.");
+                                    auto const& rewardModel = this->model.getRewardModel(rewardName);
+                                    STORM_LOG_THROW(!rewardModel.hasTransitionRewards(), storm::exceptions::NotSupportedException, "Transition rewards are currently not supported as reward bounds.");
+                                    std::vector<ValueType> actionRewards = rewardModel.getTotalRewardVector(this->model.getTransitionMatrix());
+                                    auto discretizedRewardsAndFactor = storm::utility::vector::toIntegralVector<ValueType, uint64_t>(actionRewards);
+                                    dimensionWiseEpochSteps.push_back(std::move(discretizedRewardsAndFactor.first));
+                                    dimension.scalingFactor = std::move(discretizedRewardsAndFactor.second);
+                                }
+                                dimensions.emplace_back(std::move(dimension));
                             }
-                            dimensions.emplace_back(std::move(dimension));
                         }
                     }
                     
@@ -135,27 +137,26 @@ namespace storm {
                     uint64_t dim = 0;
                     for (uint64_t objIndex = 0; objIndex < this->objectives.size(); ++objIndex) {
                         storm::storage::BitVector objDimensions(dimensions.size(), false);
+                        uint64_t objDimensionCount = 0;
+                        bool objDimensionsCanBeSatisfiedIndividually = false;
                         if (objectives[objIndex].formula->isProbabilityOperatorFormula() && objectives[objIndex].formula->getSubformula().isBoundedUntilFormula()) {
-                            auto const& boundedUntilFormula = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula();
-                            for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) {
-                                objDimensions.set(currDim);
-                            }
-                            for (uint64_t currDim = dim; currDim < dim + boundedUntilFormula.getDimension(); ++currDim ) {
-                                if (!boundedUntilFormula.hasMultiDimensionalSubformulas() || dimensions[currDim].isUpperBounded) {
-                                    dimensions[currDim].dependentDimensions = objDimensions;
-                                } else {
-                                    dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false);
-                                    dimensions[currDim].dependentDimensions.set(currDim, true);
-                                }
-                                //  std::cout << "dimension " << currDim << " has depDims: " << dimensions[currDim].dependentDimensions << std::endl;
-                            }
-                            dim += boundedUntilFormula.getDimension();
+                            objDimensionCount = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula().getDimension();
+                            objDimensionsCanBeSatisfiedIndividually = objectives[objIndex].formula->getSubformula().asBoundedUntilFormula().hasMultiDimensionalSubformulas();
                         } else if (objectives[objIndex].formula->isRewardOperatorFormula() && objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) {
-                            objDimensions.set(dim, true);
-                            dimensions[dim].dependentDimensions = objDimensions;
-                            ++dim;
+                            objDimensionCount = objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula().getDimension();
                         }
-                        
+                        for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim ) {
+                            objDimensions.set(currDim);
+                        }
+                        for (uint64_t currDim = dim; currDim < dim + objDimensionCount; ++currDim ) {
+                            if (!objDimensionsCanBeSatisfiedIndividually || dimensions[currDim].isUpperBounded) {
+                                dimensions[currDim].dependentDimensions = objDimensions;
+                            } else {
+                                dimensions[currDim].dependentDimensions = storm::storage::BitVector(dimensions.size(), false);
+                                dimensions[currDim].dependentDimensions.set(currDim, true);
+                            }
+                        }
+                        dim += objDimensionCount;
                         objectiveDimensions.push_back(std::move(objDimensions));
                     }
                     assert(dim == dimensions.size());
@@ -210,6 +211,7 @@ namespace storm {
                                 isStrict = dimFormula.asBoundedUntilFormula().isLowerBoundStrict();
                             }
                         } else if (dimFormula.isCumulativeRewardFormula()) {
+                            assert(!dimFormula.asCumulativeRewardFormula().isMultiDimensional());
                             bound = dimFormula.asCumulativeRewardFormula().getBound();
                             isStrict = dimFormula.asCumulativeRewardFormula().isBoundStrict();
                         }
@@ -562,29 +564,35 @@ namespace storm {
                             if (objective.formula->getSubformula().isCumulativeRewardFormula()) {
                                 // Try to get an upper bound by computing the maximal reward achievable within one epoch step
                                 auto const& cumulativeRewardFormula = objective.formula->getSubformula().asCumulativeRewardFormula();
-                                ValueType rewardBound = cumulativeRewardFormula.template getBound<ValueType>();
-                                if (cumulativeRewardFormula.getTimeBoundReference().isRewardBound()) {
-                                    auto const& costModel = this->model.getRewardModel(cumulativeRewardFormula.getTimeBoundReference().getRewardName());
-                                    if (!costModel.hasTransitionRewards()) {
-                                        auto actionCosts = costModel.getTotalRewardVector(this->model.getTransitionMatrix());
-                                        ValueType largestRewardPerCost = storm::utility::zero<ValueType>();
-                                        bool isFinite = true;
-                                        for (auto rewIt = actionRewards.begin(), costIt = actionCosts.begin(); rewIt != actionRewards.end(); ++rewIt, ++costIt) {
-                                            if (!storm::utility::isZero(*rewIt)) {
-                                                if (storm::utility::isZero(*costIt)) {
-                                                    isFinite = false;
-                                                    break;
+                                for (uint64_t objDim = 0; objDim < cumulativeRewardFormula.getDimension(); ++objDim) {
+                                    boost::optional<ValueType> resBound;
+                                    ValueType rewardBound = cumulativeRewardFormula.template getBound<ValueType>(objDim);
+                                    if (cumulativeRewardFormula.getTimeBoundReference(objDim).isRewardBound()) {
+                                        auto const& costModel = this->model.getRewardModel(cumulativeRewardFormula.getTimeBoundReference(objDim).getRewardName());
+                                        if (!costModel.hasTransitionRewards()) {
+                                            auto actionCosts = costModel.getTotalRewardVector(this->model.getTransitionMatrix());
+                                            ValueType largestRewardPerCost = storm::utility::zero<ValueType>();
+                                            bool isFinite = true;
+                                            for (auto rewIt = actionRewards.begin(), costIt = actionCosts.begin(); rewIt != actionRewards.end(); ++rewIt, ++costIt) {
+                                                if (!storm::utility::isZero(*rewIt)) {
+                                                    if (storm::utility::isZero(*costIt)) {
+                                                        isFinite = false;
+                                                        break;
+                                                    }
+                                                    ValueType rewardPerCost = *rewIt / *costIt;
+                                                    largestRewardPerCost = std::max(largestRewardPerCost, rewardPerCost);
                                                 }
-                                                ValueType rewardPerCost = *rewIt / *costIt;
-                                                largestRewardPerCost = std::max(largestRewardPerCost, rewardPerCost);
+                                            }
+                                            if (isFinite) {
+                                                resBound = largestRewardPerCost * rewardBound;
                                             }
                                         }
-                                        if (isFinite) {
-                                            objective.upperResultBound = largestRewardPerCost * rewardBound;
-                                        }
+                                    } else {
+                                        resBound = (*std::max_element(actionRewards.begin(), actionRewards.end())) * rewardBound;
+                                    }
+                                    if (resBound && (!objective.upperResultBound || objective.upperResultBound.get() > resBound.get())) {
+                                        objective.upperResultBound = resBound;
                                     }
-                                } else {
-                                    objective.upperResultBound = (*std::max_element(actionRewards.begin(), actionRewards.end())) * rewardBound;
                                 }
                                 
                                 // If we could not find an upper bound, try to get an upper bound for the unbounded case

src/storm/parser/FormulaParserGrammar.cpp

@@ -259,7 +259,7 @@ namespace storm {
                 bounds.push_back(std::get<1>(timeBound).get());
                 timeBoundReferences.emplace_back(*std::get<2>(timeBound));
             }
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(bounds.front(), timeBoundReferences.front()));
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(bounds, timeBoundReferences));
         }
         
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTotalRewardFormula() const {

src/storm/parser/FormulaParserGrammar.h

@@ -183,6 +183,7 @@ namespace storm {
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::TimeBoundReference>, Skipper> timeBoundReference;
             qi::rule<Iterator, std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>(), qi::locals<bool, bool>, Skipper> timeBound;
+            qi::rule<Iterator, std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>(), qi::locals<bool, bool>, Skipper> timeBounds;
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> cumulativeRewardFormula;