reward bounded cumulative reward formulas + fixes for dimensions that do not need memory

src/storm/logic/CumulativeRewardFormula.cpp

@@ -8,7 +8,7 @@
 
 namespace storm {
     namespace logic {
-        CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundType const& timeBoundType) : timeBoundType(timeBoundType), bound(bound) {
+        CumulativeRewardFormula::CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference) : timeBoundReference(timeBoundReference), bound(bound) {
             // Intentionally left empty.
         }
 
@@ -24,16 +24,30 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        TimeBoundType const& CumulativeRewardFormula::getTimeBoundType() const {
-            return timeBoundType;
+        void CumulativeRewardFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            if (this->isRewardBounded()) {
+                referencedRewardModels.insert(this->getTimeBoundReference().getRewardName());
+            }
+        }
+        
+        TimeBoundType CumulativeRewardFormula::getTimeBoundType() const {
+            return timeBoundReference.getType();
+        }
+        
+        TimeBoundReference const& CumulativeRewardFormula::getTimeBoundReference() const {
+            return timeBoundReference;
         }
 
         bool CumulativeRewardFormula::isStepBounded() const {
-            return timeBoundType == TimeBoundType::Steps;
+            return getTimeBoundType() == TimeBoundType::Steps;
         }
         
         bool CumulativeRewardFormula::isTimeBounded() const {
-            return timeBoundType == TimeBoundType::Time;
+            return getTimeBoundType() == TimeBoundType::Time;
+        }
+        
+        bool CumulativeRewardFormula::isRewardBounded() const {
+            return getTimeBoundType() == TimeBoundType::Reward;
         }
         
         bool CumulativeRewardFormula::isBoundStrict() const {
@@ -87,7 +101,11 @@ namespace storm {
         }
         
         std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
-            out << "C<=" << this->getBound();
+            out << "C";
+             if(getTimeBoundReference().isRewardBound()) {
+                out << "{\"" << getTimeBoundReference().getRewardName() << "\"}";
+             }
+             out << "<=" << this->getBound();
             return out;
         }
     }

src/storm/logic/CumulativeRewardFormula.h

@@ -10,7 +10,7 @@ namespace storm {
     namespace logic {
         class CumulativeRewardFormula : public PathFormula {
         public:
-            CumulativeRewardFormula(TimeBound const& bound, TimeBoundType const& timeBoundType = TimeBoundType::Time);
+            CumulativeRewardFormula(TimeBound const& bound, TimeBoundReference const& timeBoundReference = TimeBoundReference(TimeBoundType::Time));
             
             virtual ~CumulativeRewardFormula() {
                 // Intentionally left empty.
@@ -21,11 +21,16 @@ namespace storm {
             
             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 const& getTimeBoundType() const;
+            TimeBoundType getTimeBoundType() const;
+            TimeBoundReference const& getTimeBoundReference() const;
+            
             bool isStepBounded() const;
             bool isTimeBounded() const;
+            bool isRewardBounded() const;
             
             bool isBoundStrict() const;
             bool hasIntegerBound() const;
@@ -41,7 +46,7 @@ namespace storm {
         private:
             static void checkNoVariablesInBound(storm::expressions::Expression const& bound);
 
-            TimeBoundType timeBoundType;
+            TimeBoundReference timeBoundReference;
             TimeBound bound;
         };
     }

src/storm/logic/FormulaInformationVisitor.cpp

@@ -30,10 +30,16 @@ namespace storm {
             result.setContainsBoundedUntilFormula(true);
             if (f.hasMultiDimensionalSubformulas()) {
                 for (unsigned i = 0; i < f.getDimension(); ++i){
+                    if (f.getTimeBoundReference(i).isRewardBound()) {
+                        result.setContainsRewardBoundedFormula(true);
+                    }
                     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)));
             }
@@ -44,8 +50,13 @@ namespace storm {
             return boost::any_cast<FormulaInformation>(f.getSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getConditionFormula().accept(*this)));
         }
         
-        boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const {
-            return FormulaInformation();
+        boost::any FormulaInformationVisitor::visit(CumulativeRewardFormula const& f, boost::any const&) const {
+            FormulaInformation result;
+            result.setContainsCumulativeRewardFormula(true);
+            if (f.getTimeBoundReference().isRewardBound()) {
+                result.setContainsRewardBoundedFormula(true);
+            }
+            return result;
         }
         
         boost::any FormulaInformationVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {

src/storm/logic/FragmentChecker.cpp

@@ -113,9 +113,20 @@ namespace storm {
             return result;
         }
         
-        boost::any FragmentChecker::visit(CumulativeRewardFormula const&, boost::any const& data) const {
+        boost::any FragmentChecker::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
-            return inherited.getSpecification().areCumulativeRewardFormulasAllowed();
+            
+            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();
+            }
+            return result;
         }
         
         boost::any FragmentChecker::visit(EventuallyFormula const& f, boost::any const& data) const {

src/storm/logic/FragmentSpecification.cpp

@@ -60,6 +60,8 @@ namespace storm {
             prctl.setInstantaneousFormulasAllowed(true);
             prctl.setReachabilityRewardFormulasAllowed(true);
             prctl.setLongRunAverageOperatorsAllowed(true);
+            prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
+            prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
             
             return prctl;
         }
@@ -80,6 +82,7 @@ namespace storm {
             csrl.setInstantaneousFormulasAllowed(true);
             csrl.setReachabilityRewardFormulasAllowed(true);
             csrl.setLongRunAverageOperatorsAllowed(true);
+            csrl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
             
             return csrl;
         }
@@ -146,6 +149,9 @@ namespace storm {
             timeBoundedUntilFormulas = false;
             rewardBoundedUntilFormulas = false;
             multiDimensionalBoundedUntilFormulas = false;
+            stepBoundedCumulativeRewardFormulas = false;
+            timeBoundedCumulativeRewardFormulas = false;
+            rewardBoundedCumulativeRewardFormulas = false;
             varianceAsMeasureType = false;
             
             qualitativeOperatorResults = true;
@@ -448,6 +454,33 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::areStepBoundedCumulativeRewardFormulasAllowed() const {
+            return this->stepBoundedCumulativeRewardFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setStepBoundedCumulativeRewardFormulasAllowed(bool newValue) {
+            this->stepBoundedCumulativeRewardFormulas = newValue;
+            return *this;
+        }
+        
+        bool FragmentSpecification::areTimeBoundedCumulativeRewardFormulasAllowed() const {
+            return this->timeBoundedCumulativeRewardFormulas;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue) {
+            this->timeBoundedCumulativeRewardFormulas = newValue;
+            return *this;
+        }
+
+        bool FragmentSpecification::areRewardBoundedCumulativeRewardFormulasAllowed() const {
+            return this->rewardBoundedCumulativeRewardFormulas;
+        }
+
+        FragmentSpecification& FragmentSpecification::setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue) {
+            this->rewardBoundedCumulativeRewardFormulas = newValue;
+            return *this;
+        }
+        
         FragmentSpecification& FragmentSpecification::setOperatorsAllowed(bool newValue) {
             this->setProbabilityOperatorsAllowed(newValue);
             this->setRewardOperatorsAllowed(newValue);

src/storm/logic/FragmentSpecification.h

@@ -106,6 +106,15 @@ namespace storm {
             bool areRewardBoundedUntilFormulasAllowed() const;
             FragmentSpecification& setRewardBoundedUntilFormulasAllowed(bool newValue);
             
+            bool areStepBoundedCumulativeRewardFormulasAllowed() const;
+            FragmentSpecification& setStepBoundedCumulativeRewardFormulasAllowed(bool newValue);
+            
+            bool areTimeBoundedCumulativeRewardFormulasAllowed() const;
+            FragmentSpecification& setTimeBoundedCumulativeRewardFormulasAllowed(bool newValue);
+
+            bool areRewardBoundedCumulativeRewardFormulasAllowed() const;
+            FragmentSpecification& setRewardBoundedCumulativeRewardFormulasAllowed(bool newValue);
+            
             bool areMultiDimensionalBoundedUntilFormulasAllowed() const;
             FragmentSpecification& setMultiDimensionalBoundedUntilFormulasAllowed(bool newValue);
             
@@ -172,6 +181,9 @@ namespace storm {
             bool stepBoundedUntilFormulas;
             bool timeBoundedUntilFormulas;
             bool rewardBoundedUntilFormulas;
+            bool stepBoundedCumulativeRewardFormulas;
+            bool timeBoundedCumulativeRewardFormulas;
+            bool rewardBoundedCumulativeRewardFormulas;
             bool multiDimensionalBoundedUntilFormulas;
             bool varianceAsMeasureType;
             bool quantitativeOperatorResults;

src/storm/logic/VariableSubstitutionVisitor.cpp

@@ -65,7 +65,7 @@ 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.getTimeBoundType()));
+            return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(storm::logic::TimeBound(f.isBoundStrict(), f.getBound().substitute(substitution)), f.getTimeBoundReference()));
         }
         
         boost::any VariableSubstitutionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const&) const {

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessor.cpp

@@ -285,7 +285,7 @@ namespace storm {
                     } else {
                         STORM_LOG_THROW(!data.originalModel.isOfType(storm::models::ModelType::MarkovAutomaton) || formula.getTimeBoundReference().isTimeBound(), storm::exceptions::InvalidPropertyException, "Bounded until formulas for Markov Automata are only allowed when time bounds are considered.");
                         storm::logic::TimeBound bound(formula.isUpperBoundStrict(), formula.getUpperBound());
-                        subformula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, formula.getTimeBoundReference().getType());
+                        subformula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, formula.getTimeBoundReference());
                     }
                     preprocessUntilFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), opInfo, data, subformula);
                 } else {
@@ -349,8 +349,13 @@ namespace storm {
                 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());
-                auto cumulativeRewardFormula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, storm::logic::TimeBoundType::Steps);
+                storm::logic::TimeBoundReference tbr(formula.getTimeBoundReference());
+                auto cumulativeRewardFormula = std::make_shared<storm::logic::CumulativeRewardFormula>(bound, tbr);
                 data.objectives.back()->formula = std::make_shared<storm::logic::RewardOperatorFormula>(cumulativeRewardFormula, *optionalRewardModelName, opInfo);
+                data.upperResultBoundObjectives.set(data.objectives.size() - 1, true);
+                if (tbr.isRewardBound()) {
+                    data.finiteRewardCheckObjectives.set(data.objectives.size() - 1, true);
+                }
             }
             
             template<typename SparseModelType>
@@ -466,10 +471,19 @@ namespace storm {
                 for (auto const& objIndex : finiteRewardCheckObjectives) {
                     STORM_LOG_ASSERT(result.objectives[objIndex].formula->isRewardOperatorFormula(), "Objective needs to be checked for finite reward but has no reward operator.");
                     auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName());
+                    auto unrelevantChoices = rewModel.getChoicesWithZeroReward(transitions);
+                    // For (upper) reward bounded cumulative reward formulas, we do not need to consider the choices where boundReward is collected.
+                    if (result.objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula()) {
+                        auto const& timeBoundReference = result.objectives[objIndex].formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference();
+                        // Only reward bounded formulas need a finiteness check
+                        assert(timeBoundReference.isRewardBound());
+                        auto const& rewModelOfBound = result.preprocessedModel->getRewardModel(timeBoundReference.getRewardName());
+                        unrelevantChoices |= ~rewModelOfBound.getChoicesWithZeroReward(transitions);
+                    }
                     if (storm::solver::minimize(result.objectives[objIndex].formula->getOptimalityType())) {
-                        minRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions);
+                        minRewardsToCheck &= unrelevantChoices;
                     } else {
-                        maxRewardsToCheck &= rewModel.getChoicesWithZeroReward(transitions);
+                        maxRewardsToCheck &= unrelevantChoices;
                     }
                 }
                 maxRewardsToCheck.complement();
@@ -500,7 +514,9 @@ namespace storm {
             template<typename SparseModelType>
             boost::optional<typename SparseModelType::ValueType> SparseMultiObjectivePreprocessor<SparseModelType>::computeUpperResultBound(ReturnType const& result, uint64_t objIndex, storm::storage::SparseMatrix<ValueType> const& backwardTransitions) {
                 
-                if (result.objectives[objIndex].formula->isRewardOperatorFormula() && result.objectives[objIndex].formula->getSubformula().isTotalRewardFormula()) {
+                if (result.objectives[objIndex].formula->isRewardOperatorFormula() && (result.objectives[objIndex].formula->getSubformula().isTotalRewardFormula() || result.objectives[objIndex].formula->getSubformula().isCumulativeRewardFormula())) {
+                    // TODO: Consider cumulative reward formulas less naively
+                    // TODO: We have to eliminate ECs here to treat zero-reward ECs
                     auto const& transitions = result.preprocessedModel->getTransitionMatrix();
                     auto const& rewModel = result.preprocessedModel->getRewardModel(result.objectives[objIndex].formula->asRewardOperatorFormula().getRewardModelName());
                     storm::storage::BitVector allStates(result.preprocessedModel->getNumberOfStates(), true);
@@ -528,7 +544,6 @@ namespace storm {
                         storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType> baier(submatrix, rewards, rew0StateProbs);
                         return baier.computeUpperBound();
                     }
-                    
                 }
                 
                 

src/storm/modelchecker/multiobjective/SparseMultiObjectivePreprocessorResult.h

@@ -49,9 +49,9 @@ namespace storm {
                     // Intentionally left empty
                 }
                 
-                bool containsOnlyRewardObjectives() const {
+                bool containsOnlyTrivialObjectives() const {
                     for (auto const& obj : objectives) {
-                        if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || obj.formula->getSubformula().isCumulativeRewardFormula()))) {
+                        if (!(obj.formula->isRewardOperatorFormula() && (obj.formula->getSubformula().isTotalRewardFormula() || (obj.formula->getSubformula().isCumulativeRewardFormula() && !obj.formula->getSubformula().asCumulativeRewardFormula().getTimeBoundReference().isRewardBound())))) {
                             return false;
                         }
                     }

src/storm/modelchecker/multiobjective/constraintbased/SparseCbQuery.cpp

@@ -25,7 +25,7 @@ namespace storm {
              
                 STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult<SparseModelType>::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
                 STORM_LOG_THROW(preprocessorResult.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
-                STORM_LOG_THROW(preprocessorResult.containsOnlyRewardObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker.");
+                STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker.");
                 STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
                 
                 // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers.

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

@@ -54,9 +54,10 @@ namespace storm {
             template <typename ModelType>
             template<typename VT, typename std::enable_if<std::is_same<ModelType, storm::models::sparse::Mdp<VT>>::value, int>::type>
             std::unique_ptr<PcaaWeightVectorChecker<ModelType>>  WeightVectorCheckerFactory<ModelType>::create(SparseMultiObjectivePreprocessorResult<ModelType> const& preprocessorResult) {
-                if (preprocessorResult.containsOnlyRewardObjectives()) {
+                if (preprocessorResult.containsOnlyTrivialObjectives()) {
                     return std::make_unique<SparseMdpPcaaWeightVectorChecker<ModelType>>(preprocessorResult);
                 } else {
+                    STORM_LOG_DEBUG("Query contains reward bounded formula");
                     return std::make_unique<SparseMdpRewardBoundedPcaaWeightVectorChecker<ModelType>>(preprocessorResult);
                 }
             }

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

@@ -38,6 +38,8 @@ namespace storm {
             
             template <class SparseMdpModelType>
             void SparseMdpRewardBoundedPcaaWeightVectorChecker<SparseMdpModelType>::check(std::vector<ValueType> const& weightVector) {
+                STORM_LOG_DEBUG("Analyzing weight vector " << storm::utility::vector::toString(weightVector));
+
                 ++numChecks;
                 
                 // In case we want to export the cdf, we will collect the corresponding data
@@ -183,6 +185,7 @@ namespace storm {
                     }
                     assert(x.size() == choices.size());
                     auto req = cachedData.linEqSolver->getRequirements();
+                    cachedData.linEqSolver->clearBounds();
                     if (obj.lowerResultBound) {
                         req.clearLowerBounds();
                         cachedData.linEqSolver->setLowerBound(*obj.lowerResultBound);

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

@@ -32,7 +32,7 @@ namespace storm {
                 
                 STORM_LOG_THROW(preprocessorResult.rewardFinitenessType != SparseMultiObjectivePreprocessorResult<SparseModelType>::RewardFinitenessType::Infinite, storm::exceptions::NotSupportedException, "There is no Pareto optimal scheduler that yields finite reward for all objectives. This is not supported.");
                 STORM_LOG_THROW(preprocessorResult.rewardLessInfinityEStates, storm::exceptions::UnexpectedException, "The set of states with reward < infinity for some scheduler has not been computed during preprocessing.");
-                STORM_LOG_THROW(preprocessorResult.containsOnlyRewardObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker.");
+                STORM_LOG_THROW(preprocessorResult.containsOnlyTrivialObjectives(), storm::exceptions::NotSupportedException, "At least one objective was not reduced to an expected (total or cumulative) reward objective during preprocessing. This is not supported by the considered weight vector checker.");
                 STORM_LOG_THROW(preprocessorResult.preprocessedModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "The model has multiple initial states.");
                 
             }
@@ -264,6 +264,7 @@ namespace storm {
                                // Now solve the resulting equation system.
                                std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(std::move(submatrix));
                                auto req = solver->getRequirements();
+                               solver->clearBounds();
                                if (obj.lowerResultBound) {
                                    req.clearLowerBounds();
                                    solver->setLowerBound(*obj.lowerResultBound);

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

@@ -8,7 +8,7 @@ namespace storm {
     namespace modelchecker {
         namespace multiobjective {
             
-            MemoryStateManager::MemoryStateManager(uint64_t dimensionCount) : dimensionCount(dimensionCount), dimensionBitMask(1ull), relevantBitsMask((1ull << dimensionCount) - 1), stateCount(dimensionBitMask << dimensionCount) {
+            MemoryStateManager::MemoryStateManager(uint64_t dimensionCount) : dimensionCount(dimensionCount), dimensionBitMask(1ull), relevantBitsMask((1ull << dimensionCount) - 1), stateCount(dimensionBitMask << dimensionCount), dimensionsWithoutMemoryMask(0), upperMemoryStateBound(stateCount) {
                 STORM_LOG_THROW(dimensionCount > 0, storm::exceptions::IllegalArgumentException, "Invoked MemoryStateManager with zero dimension count.");
                 STORM_LOG_THROW(dimensionCount <= 64, storm::exceptions::IllegalArgumentException, "Invoked MemoryStateManager with too many dimensions.");
             }
@@ -21,6 +21,19 @@ namespace storm {
                 return stateCount;
             }
             
+            MemoryStateManager::MemoryState const& MemoryStateManager::getUpperMemoryStateBound() const {
+                return upperMemoryStateBound;
+            }
+            
+            void MemoryStateManager::setDimensionWithoutMemory(uint64_t dimension) {
+                STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count.");
+                STORM_LOG_ASSERT(dimension < dimensionCount, "Tried to set a dimension that is larger then the number of considered dimensions");
+                if (((dimensionBitMask << dimension) & dimensionsWithoutMemoryMask) == 0) {
+                    stateCount = (stateCount >> 1);
+                }
+                dimensionsWithoutMemoryMask |= (dimensionBitMask << dimension);
+            }
+
             MemoryStateManager::MemoryState MemoryStateManager::getInitialMemoryState() const {
                 STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count.");
                 return relevantBitsMask;
@@ -28,18 +41,19 @@ namespace storm {
             
             bool MemoryStateManager::isRelevantDimension(MemoryState const& state, uint64_t dimension) const {
                 STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count.");
+                STORM_LOG_ASSERT((state & dimensionsWithoutMemoryMask) == dimensionsWithoutMemoryMask, "Invalid memory state found.");
                 return (state & (dimensionBitMask << dimension)) != 0;
             }
             
             void MemoryStateManager::setRelevantDimension(MemoryState& state, uint64_t dimension, bool value) const {
                 STORM_LOG_ASSERT(dimensionCount > 0, "Invoked MemoryStateManager with zero dimension count.");
                 STORM_LOG_ASSERT(dimension < dimensionCount, "Tried to set a dimension that is larger then the number of considered dimensions");
+                STORM_LOG_ASSERT(((dimensionBitMask << dimension) & dimensionsWithoutMemoryMask) == 0, "Tried to change a memory state for a dimension but the dimension is assumed to have no memory.");
                 if (value) {
                     state |= (dimensionBitMask << dimension);
                 } else {
                     state &= ~(dimensionBitMask << dimension);
                 }
-                assert(state < getMemoryStateCount());
             }
             
             void MemoryStateManager::setRelevantDimensions(MemoryState& state, storm::storage::BitVector const& dimensions, bool value) const {
@@ -47,14 +61,15 @@ namespace storm {
                 STORM_LOG_ASSERT(dimensions.size() == dimensionCount, "Invalid size of given bitset.");
                 if (value) {
                     for (auto const& d : dimensions) {
+                        STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'relevant'-memory state but the dimension is assumed to have no memory.");
                         state |= (dimensionBitMask << d);
                     }
                 } else {
                     for (auto const& d : dimensions) {
+                        STORM_LOG_ASSERT(((dimensionBitMask << d) & dimensionsWithoutMemoryMask) == 0, "Tried to set a dimension to 'unrelevant'-memory state but the dimension is assumed to have no memory.");
                         state &= ~(dimensionBitMask << d);
                     }
                 }
-                assert(state < getMemoryStateCount());
             }
             
             std::string MemoryStateManager::toString(MemoryState const& state) const {

src/storm/modelchecker/multiobjective/rewardbounded/MemoryStateManager.h

@@ -18,8 +18,11 @@ namespace storm {
                 
                 MemoryStateManager(uint64_t dimensionCount);
                 
+                void setDimensionWithoutMemory(uint64_t dimension);
+                
                 uint64_t const& getDimensionCount() const;
                 uint64_t const& getMemoryStateCount() const;
+                MemoryState const& getUpperMemoryStateBound() const; // is larger then every valid memory state m, i.e., m < getUpperMemoryStateBound() holds for all m
                 
                 MemoryState getInitialMemoryState() const;
                 bool isRelevantDimension(MemoryState const& state, uint64_t dimension) const;
@@ -32,7 +35,9 @@ namespace storm {
                 uint64_t const dimensionCount;
                 uint64_t const dimensionBitMask;
                 uint64_t const relevantBitsMask;
-                uint64_t const stateCount;
+                uint64_t stateCount;
+                uint64_t dimensionsWithoutMemoryMask;
+                MemoryState const upperMemoryStateBound;
 
             };
         }

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

@@ -26,15 +26,20 @@ namespace storm {
             }
             
             template<typename ValueType, bool SingleObjectiveMode>
-            MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::ProbabilityOperatorFormula const> objectiveFormula) : model(model) {
+            MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula) : model(model) {
                 
                 STORM_LOG_THROW(objectiveFormula->hasOptimalityType(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
-                if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) {
-                    for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) {
-                        STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << ".");
+                if (objectiveFormula->isProbabilityOperatorFormula()) {
+                    if (objectiveFormula->getSubformula().isMultiObjectiveFormula()) {
+                        for (auto const& subFormula : objectiveFormula->getSubformula().asMultiObjectiveFormula().getSubformulas()) {
+                            STORM_LOG_THROW(subFormula->isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << *subFormula << ".");
+                        }
+                    } else {
+                        STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << ".");
                     }
                 } else {
-                    STORM_LOG_THROW(objectiveFormula->getSubformula().isBoundedUntilFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported. Invalid subformula " << objectiveFormula->getSubformula() << ".");
+                    STORM_LOG_THROW(objectiveFormula->isRewardOperatorFormula() && objectiveFormula->getSubformula().isCumulativeRewardFormula(), storm::exceptions::InvalidPropertyException, "Formula " << objectiveFormula << " is not supported.");
+                    
                 }
                 
                 // Build an objective from the formula.
@@ -42,8 +47,6 @@ namespace storm {
                 objective.formula = objectiveFormula;
                 objective.originalFormula = objective.formula;
                 objective.considersComplementaryEvent = false;
-                objective.lowerResultBound = storm::utility::zero<ValueType>();
-                objective.upperResultBound = storm::utility::one<ValueType>();
                 objectives.push_back(std::move(objective));
                 
                 initialize();
@@ -103,13 +106,26 @@ namespace storm {
                             dimensions.emplace_back(std::move(dimension));
                         }
                     } 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;
-                        dimension.scalingFactor = storm::utility::one<ValueType>();
+                        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);
+                        }
                         dimensions.emplace_back(std::move(dimension));
-                        dimensionWiseEpochSteps.push_back(std::vector<uint64_t>(model.getNumberOfChoices(), 1));
                     }
                 }
                 
@@ -265,7 +281,7 @@ namespace storm {
             
             template<typename ValueType, bool SingleObjectiveMode>
             typename MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::EpochModel& MultiDimensionalRewardUnfolding<ValueType, SingleObjectiveMode>::setCurrentEpoch(Epoch const& epoch) {
-                // std::cout << "Setting model for epoch " << epochManager.toString(epoch) << std::endl;
+                STORM_LOG_DEBUG("Setting model for epoch " << epochManager.toString(epoch));
                 
                 // Check if we need to update the current epoch class
                 if (!currentEpoch || !epochManager.compareEpochClass(epoch, currentEpoch.get())) {

src/storm/modelchecker/multiobjective/rewardbounded/MultiDimensionalRewardUnfolding.h

@@ -44,7 +44,7 @@ namespace storm {
                  *
                  */
                 MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives);
-                MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::ProbabilityOperatorFormula const> objectiveFormula);
+                MultiDimensionalRewardUnfolding(storm::models::sparse::Mdp<ValueType> const& model, std::shared_ptr<storm::logic::OperatorFormula const> objectiveFormula);
                 
                 ~MultiDimensionalRewardUnfolding() {
                     std::cout << "Unfolding statistics: " << std::endl;

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

@@ -20,6 +20,12 @@ namespace storm {
             template<typename ValueType>
             ProductModel<ValueType>::ProductModel(storm::models::sparse::Mdp<ValueType> const& model, std::vector<storm::modelchecker::multiobjective::Objective<ValueType>> const& objectives, std::vector<Dimension<ValueType>> const& dimensions, std::vector<storm::storage::BitVector> const& objectiveDimensions, EpochManager const& epochManager, std::vector<Epoch> const& originalModelSteps) : dimensions(dimensions), objectiveDimensions(objectiveDimensions), epochManager(epochManager), memoryStateManager(dimensions.size()) {
                 
+                for (uint64_t dim = 0; dim < dimensions.size(); ++dim) {
+                    if (!dimensions[dim].memoryLabel) {
+                        memoryStateManager.setDimensionWithoutMemory(dim);
+                    }
+                }
+                
                 storm::storage::MemoryStructure memory = computeMemoryStructure(model, objectives);
                 assert(memoryStateManager.getMemoryStateCount() == memory.getNumberOfStates());
                 std::vector<MemoryState> memoryStateMap = computeMemoryStateMap(memory);
@@ -30,18 +36,19 @@ namespace storm {
                 product = productBuilder.build()->template as<storm::models::sparse::Mdp<ValueType>>();
                 
                 uint64_t numModelStates = productBuilder.getOriginalModel().getNumberOfStates();
+                MemoryState upperMemStateBound = memoryStateManager.getUpperMemoryStateBound();
                 uint64_t numMemoryStates = memoryStateManager.getMemoryStateCount();
                 uint64_t numProductStates = getProduct().getNumberOfStates();
                 
                 // Compute a mappings from product states to model/memory states and back
-                modelMemoryToProductStateMap.resize(numMemoryStates * numModelStates, std::numeric_limits<uint64_t>::max());
+                modelMemoryToProductStateMap.resize(upperMemStateBound * numModelStates, std::numeric_limits<uint64_t>::max());
                 productToModelStateMap.resize(numProductStates, std::numeric_limits<uint64_t>::max());
                 productToMemoryStateMap.resize(numProductStates, std::numeric_limits<uint64_t>::max());
                 for (uint64_t modelState = 0; modelState < numModelStates; ++modelState) {
                     for (uint64_t memoryStateIndex = 0; memoryStateIndex < numMemoryStates; ++memoryStateIndex) {
                         if (productBuilder.isStateReachable(modelState, memoryStateIndex)) {
                             uint64_t productState = productBuilder.getResultState(modelState, memoryStateIndex);
-                            modelMemoryToProductStateMap[modelState * numMemoryStates + memoryStateMap[memoryStateIndex]] = productState;
+                            modelMemoryToProductStateMap[modelState * upperMemStateBound + memoryStateMap[memoryStateIndex]] = productState;
                             productToModelStateMap[productState] = modelState;
                             productToMemoryStateMap[productState] = memoryStateMap[memoryStateIndex];
                         }
@@ -190,10 +197,12 @@ namespace storm {
                     MemoryState memState = memoryStateManager.getInitialMemoryState();
                     std::set<std::string> stateLabels = memory.getStateLabeling().getLabelsOfState(memStateIndex);
                     for (uint64_t dim = 0; dim < epochManager.getDimensionCount(); ++dim) {
-                        if (dimensions[dim].memoryLabel && stateLabels.find(dimensions[dim].memoryLabel.get()) != stateLabels.end()) {
-                            memoryStateManager.setRelevantDimension(memState, dim, true);
-                        } else {
-                            memoryStateManager.setRelevantDimension(memState, dim, false);
+                        if (dimensions[dim].memoryLabel) {
+                            if (stateLabels.find(dimensions[dim].memoryLabel.get()) != stateLabels.end()) {
+                                memoryStateManager.setRelevantDimension(memState, dim, true);
+                            } else {
+                                memoryStateManager.setRelevantDimension(memState, dim, false);
+                            }
                         }
                     }
                     result.push_back(std::move(memState));
@@ -204,7 +213,7 @@ namespace storm {
             template<typename ValueType>
             void ProductModel<ValueType>::setReachableProductStates(storm::storage::SparseModelMemoryProduct<ValueType>& productBuilder, std::vector<Epoch> const& originalModelSteps, std::vector<MemoryState> const& memoryStateMap) const {
 
-                std::vector<uint64_t> inverseMemoryStateMap(memoryStateMap.size(), std::numeric_limits<uint64_t>::max());
+                std::vector<uint64_t> inverseMemoryStateMap(memoryStateManager.getUpperMemoryStateBound(), std::numeric_limits<uint64_t>::max());
                 for (uint64_t memStateIndex = 0; memStateIndex < memoryStateMap.size(); ++memStateIndex) {
                     inverseMemoryStateMap[memoryStateMap[memStateIndex]] = memStateIndex;
                 }
@@ -213,14 +222,17 @@ namespace storm {
                 auto const& model = productBuilder.getOriginalModel();
                 auto const& modelTransitions = model.getTransitionMatrix();
                 
-                std::vector<storm::storage::BitVector> reachableStates(memoryStateManager.getMemoryStateCount(), storm::storage::BitVector(model.getNumberOfStates(), false));
+                std::vector<storm::storage::BitVector> reachableProductStates(memoryStateManager.getUpperMemoryStateBound());
+                for (auto const& memState : memoryStateMap) {
+                    reachableProductStates[memState] = storm::storage::BitVector(model.getNumberOfStates(), false);
+                }
                 
                 // Initialize the reachable states with the initial states
                 EpochClass initEpochClass = epochManager.getEpochClass(epochManager.getZeroEpoch());
                 auto memStateIt = memory.getInitialMemoryStates().begin();
                 for (auto const& initState : model.getInitialStates()) {
                     uint64_t transformedMemoryState = transformMemoryState(memoryStateMap[*memStateIt], initEpochClass, memoryStateManager.getInitialMemoryState());
-                    reachableStates[transformedMemoryState].set(initState, true);
+                    reachableProductStates[transformedMemoryState].set(initState, true);
                     ++memStateIt;
                 }
                 assert(memStateIt == memory.getInitialMemoryStates().end());
@@ -238,7 +250,7 @@ namespace storm {
                     // Find the remaining set of reachable states via DFS.
                     std::vector<std::pair<uint64_t, MemoryState>> dfsStack;
                     for (MemoryState const& memState : memoryStateMap) {
-                        for (auto const& modelState : reachableStates[memState]) {
+                        for (auto const& modelState : reachableProductStates[memState]) {
                             dfsStack.emplace_back(modelState, memState);
                         }
                     }
@@ -255,8 +267,8 @@ namespace storm {
                                 
                                 MemoryState successorMemoryState = memoryStateMap[memory.getSuccessorMemoryState(currentMemoryStateIndex, transitionIt - modelTransitions.begin())];
                                 successorMemoryState = transformMemoryState(successorMemoryState, epochClass, currentMemoryState);
-                                if (!reachableStates[successorMemoryState].get(transitionIt->getColumn())) {
-                                    reachableStates[successorMemoryState].set(transitionIt->getColumn(), true);
+                                if (!reachableProductStates[successorMemoryState].get(transitionIt->getColumn())) {
+                                    reachableProductStates[successorMemoryState].set(transitionIt->getColumn(), true);
                                     dfsStack.emplace_back(transitionIt->getColumn(), successorMemoryState);
                                 }
                             }
@@ -265,7 +277,7 @@ namespace storm {
                 }
                 
                 for (uint64_t memStateIndex = 0; memStateIndex < memoryStateManager.getMemoryStateCount(); ++memStateIndex) {
-                    for (auto const& modelState : reachableStates[memoryStateMap[memStateIndex]]) {
+                    for (auto const& modelState : reachableProductStates[memoryStateMap[memStateIndex]]) {
                         productBuilder.addReachableState(modelState, memStateIndex);
                     }
                 }
@@ -283,13 +295,13 @@ namespace storm {
             
             template<typename ValueType>
             bool ProductModel<ValueType>::productStateExists(uint64_t const& modelState, MemoryState const& memoryState) const {
-                return modelMemoryToProductStateMap[modelState * memoryStateManager.getMemoryStateCount() + memoryState] < getProduct().getNumberOfStates();
+                return modelMemoryToProductStateMap[modelState * memoryStateManager.getUpperMemoryStateBound() + memoryState] < getProduct().getNumberOfStates();
             }
             
             template<typename ValueType>
             uint64_t ProductModel<ValueType>::getProductState(uint64_t const& modelState, MemoryState const& memoryState) const {
                 STORM_LOG_ASSERT(productStateExists(modelState, memoryState), "Tried to obtain a state in the model-memory-product that does not exist");
-                return modelMemoryToProductStateMap[modelState * memoryStateManager.getMemoryStateCount() + memoryState];
+                return modelMemoryToProductStateMap[modelState * memoryStateManager.getUpperMemoryStateBound() + memoryState];
             }
 
             template<typename ValueType>
@@ -560,14 +572,16 @@ namespace storm {
                 for (auto const& objDimensions : objectiveDimensions) {
                     for (auto const& dim : objDimensions) {
                         auto const& dimension = dimensions[dim];
-                        bool dimUpperBounded = dimension.isUpperBounded;
-                        bool dimBottom = epochManager.isBottomDimensionEpochClass(epochClass, dim);
-                        if (dimUpperBounded && dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) {
-                            STORM_LOG_ASSERT(objDimensions == dimension.dependentDimensions, "Unexpected set of dependent dimensions");
-                            memoryStateManager.setRelevantDimensions(memoryStatePrime, objDimensions, false);
-                            break;
-                        } else if (!dimUpperBounded && !dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) {
-                            memoryStateManager.setRelevantDimensions(memoryStatePrime, dimension.dependentDimensions, true);
+                        if (dimension.memoryLabel) {
+                            bool dimUpperBounded = dimension.isUpperBounded;
+                            bool dimBottom = epochManager.isBottomDimensionEpochClass(epochClass, dim);
+                            if (dimUpperBounded && dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) {
+                                STORM_LOG_ASSERT(objDimensions == dimension.dependentDimensions, "Unexpected set of dependent dimensions");
+                                memoryStateManager.setRelevantDimensions(memoryStatePrime, objDimensions, false);
+                                break;
+                            } else if (!dimUpperBounded && !dimBottom && memoryStateManager.isRelevantDimension(predecessorMemoryState, dim)) {
+                                memoryStateManager.setRelevantDimensions(memoryStatePrime, dimension.dependentDimensions, true);
+                            }
                         }
                     }
                 }

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).setMultiDimensionalBoundedUntilFormulasAllowed(true))) {
+            if(formula.isInFragment(storm::logic::prctl().setLongRunAverageRewardFormulasAllowed(true).setLongRunAverageProbabilitiesAllowed(true).setConditionalProbabilityFormulasAllowed(true).setOnlyEventuallyFormuluasInConditionalFormulasAllowed(true).setRewardBoundedUntilFormulasAllowed(true).setRewardBoundedCumulativeRewardFormulasAllowed(true).setMultiDimensionalBoundedUntilFormulasAllowed(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).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));
             }
         }
         
@@ -67,7 +67,7 @@ namespace storm {
                 }
                 auto formula = std::make_shared<storm::logic::ProbabilityOperatorFormula>(checkTask.getFormula().asSharedPointer(), opInfo);
                 storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
-                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeNonTrivialBoundedUntilProbabilities(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory);
+                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory, storm::utility::one<ValueType>());
                 return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
             } else {
                 STORM_LOG_THROW(!pathFormula.hasLowerBound() && pathFormula.hasUpperBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have single upper time bound.");
@@ -137,9 +137,23 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<SparseMdpModelType>::computeCumulativeRewards(storm::logic::RewardMeasureType, CheckTask<storm::logic::CumulativeRewardFormula, ValueType> const& checkTask) {
             storm::logic::CumulativeRewardFormula const& rewardPathFormula = checkTask.getFormula();
             STORM_LOG_THROW(checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
-            STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
-            std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            if (rewardPathFormula.getTimeBoundReference().isRewardBound()) {
+                STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::InvalidOperationException, "Checking reward bounded cumulative reward formulas can only be done for the initial states of the model.");
+                STORM_LOG_WARN_COND(!checkTask.isQualitativeSet(), "Checking reward bounded until formulas is not optimized w.r.t. qualitative queries");
+                storm::logic::OperatorInformation opInfo(checkTask.getOptimizationDirection());
+                if (checkTask.isBoundSet()) {
+                    opInfo.bound = checkTask.getBound();
+                }
+                auto formula = std::make_shared<storm::logic::RewardOperatorFormula>(checkTask.getFormula().asSharedPointer(), checkTask.getRewardModel(), opInfo);
+                storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true> rewardUnfolding(this->getModel(), formula);
+                auto numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(checkTask.getOptimizationDirection(), rewardUnfolding, this->getModel().getInitialStates(), *minMaxLinearEquationSolverFactory);
+                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            } else {
+                
+                STORM_LOG_THROW(rewardPathFormula.hasIntegerBound(), storm::exceptions::InvalidPropertyException, "Formula needs to have a discrete time bound.");
+                std::vector<ValueType> numericResult = storm::modelchecker::helper::SparseMdpPrctlHelper<ValueType>::computeCumulativeRewards(storm::solver::SolveGoal<ValueType>(this->getModel(), checkTask), this->getModel().getTransitionMatrix(), checkTask.isRewardModelSet() ? this->getModel().getRewardModel(checkTask.getRewardModel()) : this->getModel().getRewardModel(""), rewardPathFormula.getNonStrictBound<uint64_t>(), *minMaxLinearEquationSolverFactory);
+                return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
+            }
         }
         
         template<typename SparseMdpModelType>

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp

@@ -77,7 +77,7 @@ namespace storm {
             }
 
             template<typename ValueType>
-            std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory) {
+            std::map<storm::storage::sparse::state_type, ValueType> SparseMdpPrctlHelper<ValueType>::computeRewardBoundedValues(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<ValueType> const& upperBound) {
                 auto initEpoch = rewardUnfolding.getStartEpoch();
                 auto epochOrder = rewardUnfolding.getEpochComputationOrder(initEpoch);
                 
@@ -93,11 +93,14 @@ namespace storm {
                         minMaxSolver->setOptimizationDirection(dir);
                         minMaxSolver->setCachingEnabled(true);
                         minMaxSolver->setTrackScheduler(true);
-                        minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
-                        minMaxSolver->setUpperBound(storm::utility::one<ValueType>());
                         auto req = minMaxSolver->getRequirements(storm::solver::EquationSystemType::StochasticShortestPath, dir);
+                        minMaxSolver->setLowerBound(storm::utility::zero<ValueType>());
+                        req.clearLowerBounds();
+                        if (upperBound) {
+                            minMaxSolver->setUpperBound(upperBound.get());
+                            req.clearUpperBounds();
+                        }
                         req.clearNoEndComponents();
-                        req.clearBounds();
                         STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "A solver requirement is not satisfied.");
                         minMaxSolver->setRequirementsChecked();
                     } else {

src/storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h

@@ -36,7 +36,7 @@ namespace storm {
             public:
                 static std::vector<ValueType> computeStepBoundedUntilProbabilities(storm::solver::SolveGoal<ValueType>&& goal, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, ModelCheckerHint const& hint = ModelCheckerHint());
 
-                static std::map<storm::storage::sparse::state_type, ValueType> computeNonTrivialBoundedUntilProbabilities(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
+                static std::map<storm::storage::sparse::state_type, ValueType> computeRewardBoundedValues(OptimizationDirection dir, storm::modelchecker::multiobjective::MultiDimensionalRewardUnfolding<ValueType, true>& rewardUnfolding, storm::storage::BitVector const& initialStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory, boost::optional<ValueType> const& upperBound = boost::none);
                 
                 static std::vector<ValueType> computeNextProbabilities(OptimizationDirection dir, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::BitVector const& nextStates, storm::solver::MinMaxLinearEquationSolverFactory<ValueType> const& minMaxLinearEquationSolverFactory);
 

src/storm/parser/FormulaParserGrammar.cpp

@@ -26,7 +26,7 @@ namespace storm {
             instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
             instantaneousRewardFormula.name("instantaneous reward formula");
             
-            cumulativeRewardFormula = ((qi::lit("C<=")[qi::_a = false] | qi::lit("C<")[qi::_a = true]) > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1, qi::_a)];
+            cumulativeRewardFormula = (qi::lit("C") >> timeBound)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
             cumulativeRewardFormula.name("cumulative reward formula");
             
             totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))];
@@ -60,7 +60,6 @@ namespace storm {
             notStateFormula.name("negation formula");
             
             eventuallyFormula = (qi::lit("F") >> -(timeBound % qi::lit(",")) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
-  //          eventuallyFormula = (qi::lit("F") >> -timeBound >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
             eventuallyFormula.name("eventually formula");
             
             globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
@@ -237,8 +236,16 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(timeBound));
         }
         
-        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const {
-            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(storm::logic::TimeBound(strict, timeBound)));
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createCumulativeRewardFormula(std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, boost::optional<std::string>> const& timeBound) const {
+            STORM_LOG_THROW(!std::get<0>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas with lower time bound are not allowed.");
+            STORM_LOG_THROW(std::get<1>(timeBound), storm::exceptions::WrongFormatException, "Cumulative reward formulas require an upper bound.");
+            if (std::get<2>(timeBound)) {
+                storm::logic::TimeBoundReference tbr(std::get<2>(timeBound).get());
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(std::get<1>(timeBound).get(), tbr));
+            } else {
+                storm::logic::TimeBoundReference tbr(storm::logic::TimeBoundType::Time);
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(std::get<1>(timeBound).get(), tbr));
+            }
         }
         
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTotalRewardFormula() const {

src/storm/parser/FormulaParserGrammar.h

@@ -203,7 +203,7 @@ namespace storm {
 
                 // Methods that actually create the expression objects.
             std::shared_ptr<storm::logic::Formula const> createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const;
-            std::shared_ptr<storm::logic::Formula const> createCumulativeRewardFormula(storm::expressions::Expression const& timeBound, bool strict) const;
+            std::shared_ptr<storm::logic::Formula const> createCumulativeRewardFormula(std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, boost::optional<std::string>> const& timeBound) const;
             std::shared_ptr<storm::logic::Formula const> createTotalRewardFormula() const;
             std::shared_ptr<storm::logic::Formula const> createLongRunAverageRewardFormula() const;
             std::shared_ptr<storm::logic::Formula const> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;

src/storm/parser/JaniParser.cpp

@@ -273,7 +273,7 @@ namespace storm {
                         } else {
                             if (rewExpr.isVariable()) {
                                 std::string rewardName = rewExpr.getVariables().begin()->getName();
-                                return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundType::Steps), rewardName, opInfo);
+                                return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, stepInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Steps)), rewardName, opInfo);
                             } else {
                                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported");
                             }
@@ -294,7 +294,7 @@ namespace storm {
                         } else {
                             if (rewExpr.isVariable()) {
                                 std::string rewardName = rewExpr.getVariables().begin()->getName();
-                                return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundType::Time), rewardName, opInfo);
+                                return std::make_shared<storm::logic::RewardOperatorFormula>(std::make_shared<storm::logic::CumulativeRewardFormula>(storm::logic::TimeBound(false, timeInstantExpr), storm::logic::TimeBoundReference(storm::logic::TimeBoundType::Time)), rewardName, opInfo);
                             } else {
                                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only simple reward expressions are currently supported");
                             }
@@ -619,7 +619,7 @@ namespace storm {
                             initVal = expressionManager->rational(defaultRationalInitialValue);
                         } else {
                             initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
-                            STORM_LOG_THROW(initVal.get().hasRationalType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a rational");
+                            STORM_LOG_THROW(initVal.get().hasRationalType() || initVal.get().hasIntegerType(), storm::exceptions::InvalidJaniException, "Initial value for rational variable " + name + "(scope " + scopeDescription + ") should be a rational");
                         }
                         return std::make_shared<storm::jani::RealVariable>(name, expressionManager->declareRationalVariable(exprManagerName), initVal.get(), transientVar);
                         
@@ -632,7 +632,7 @@ namespace storm {
                             initVal = expressionManager->boolean(defaultBooleanInitialValue);
                         } else {
                             initVal = parseExpression(variableStructure.at("initial-value"), "Initial value for variable " + name + " (scope: " + scopeDescription + ") ", globalVars, constants, localVars);
-                            STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for integer variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
+                            STORM_LOG_THROW(initVal.get().hasBooleanType(), storm::exceptions::InvalidJaniException, "Initial value for boolean variable " + name + "(scope " + scopeDescription + ") should be a Boolean");
                         }
                         if(transientVar) {
                             labels.insert(name);