Started working on reward properties for CTMCs.

Former-commit-id: a4e9b9a663

src/logic/CumulativeRewardFormula.cpp

@@ -2,7 +2,11 @@
 
 namespace storm {
     namespace logic {
-        CumulativeRewardFormula::CumulativeRewardFormula(uint_fast64_t stepBound) : stepBound(stepBound) {
+        CumulativeRewardFormula::CumulativeRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) {
+            // Intentionally left empty.
+        }
+        
+        CumulativeRewardFormula::CumulativeRewardFormula(double timeBound) : timeBound(timeBound) {
             // Intentionally left empty.
         }
         
@@ -10,12 +14,32 @@ namespace storm {
             return true;
         }
         
-        uint_fast64_t CumulativeRewardFormula::getStepBound() const {
-            return stepBound;
+        bool CumulativeRewardFormula::hasDiscreteTimeBound() const {
+            return timeBound.which() == 0;
+        }
+        
+        uint_fast64_t CumulativeRewardFormula::getDiscreteTimeBound() const {
+            return boost::get<uint_fast64_t>(timeBound);
+        }
+        
+        bool CumulativeRewardFormula::hasContinuousTimeBound() const {
+            return timeBound.which() == 1;
+        }
+        
+        double CumulativeRewardFormula::getContinuousTimeBound() const {
+            if (this->hasDiscreteTimeBound()) {
+                return this->getDiscreteTimeBound();
+            } else {
+                return boost::get<double>(timeBound);
+            }
         }
         
         std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
-            out << "C<=" << stepBound;
+            if (this->hasDiscreteTimeBound()) {
+                out << "C<=" << this->getDiscreteTimeBound();
+            } else {
+                out << "C<=" << this->getContinuousTimeBound();
+            }
             return out;
         }
     }

src/logic/CumulativeRewardFormula.h

@@ -1,13 +1,17 @@
 #ifndef STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_
 #define STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_
 
+#include <boost/variant.hpp>
+
 #include "src/logic/RewardPathFormula.h"
 
 namespace storm {
     namespace logic {
         class CumulativeRewardFormula : public RewardPathFormula {
         public:
-            CumulativeRewardFormula(uint_fast64_t stepBound);
+            CumulativeRewardFormula(uint_fast64_t timeBound);
+            
+            CumulativeRewardFormula(double timeBound);
             
             virtual ~CumulativeRewardFormula() {
                 // Intentionally left empty.
@@ -17,10 +21,16 @@ namespace storm {
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            uint_fast64_t getStepBound() const;
+            bool hasDiscreteTimeBound() const;
+            
+            uint_fast64_t getDiscreteTimeBound() const;
+            
+            bool hasContinuousTimeBound() const;
+            
+            double getContinuousTimeBound() const;
             
         private:
-            uint_fast64_t stepBound;
+            boost::variant<uint_fast64_t, double> timeBound;
         };
     }
 }

src/logic/InstantaneousRewardFormula.cpp

@@ -2,20 +2,44 @@
 
 namespace storm {
     namespace logic {
-        InstantaneousRewardFormula::InstantaneousRewardFormula(uint_fast64_t stepCount) : stepCount(stepCount) {
+        InstantaneousRewardFormula::InstantaneousRewardFormula(uint_fast64_t timeBound) : timeBound(timeBound) {
             // Intentionally left empty.
         }
         
+        InstantaneousRewardFormula::InstantaneousRewardFormula(double timeBound) : timeBound(timeBound) {
+            // Intentionally left empty.            
+        }
+        
         bool InstantaneousRewardFormula::isInstantaneousRewardFormula() const {
             return true;
         }
         
-        uint_fast64_t InstantaneousRewardFormula::getStepCount() const {
-            return stepCount;
+        bool InstantaneousRewardFormula::hasDiscreteTimeBound() const {
+            return timeBound.which() == 0;
+        }
+        
+        uint_fast64_t InstantaneousRewardFormula::getDiscreteTimeBound() const {
+            return boost::get<uint_fast64_t>(timeBound);
+        }
+        
+        bool InstantaneousRewardFormula::hasContinuousTimeBound() const {
+            return timeBound.which() == 1;
+        }
+        
+        double InstantaneousRewardFormula::getContinuousTimeBound() const {
+            if (this->hasDiscreteTimeBound()) {
+                return this->getDiscreteTimeBound();
+            } else {
+                return boost::get<double>(timeBound);
+            }
         }
         
         std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const {
-            out << "I=" << stepCount;
+            if (this->hasDiscreteTimeBound()) {
+                out << "I=" << this->getDiscreteTimeBound();
+            } else {
+                out << "I=" << this->getContinuousTimeBound();
+            }
             return out;
         }
     }

src/logic/InstantaneousRewardFormula.h

@@ -1,13 +1,17 @@
 #ifndef STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_
 #define STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_
 
+#include <boost/variant.hpp>
+
 #include "src/logic/RewardPathFormula.h"
 
 namespace storm {
     namespace logic {
         class InstantaneousRewardFormula : public RewardPathFormula {
         public:
-            InstantaneousRewardFormula(uint_fast64_t stepCount);
+            InstantaneousRewardFormula(uint_fast64_t timeBound);
+            
+            InstantaneousRewardFormula(double timeBound);
             
             virtual ~InstantaneousRewardFormula() {
                 // Intentionally left empty.
@@ -17,10 +21,16 @@ namespace storm {
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            uint_fast64_t getStepCount() const;
+            bool hasDiscreteTimeBound() const;
+            
+            uint_fast64_t getDiscreteTimeBound() const;
+
+            bool hasContinuousTimeBound() const;
+            
+            double getContinuousTimeBound() const;
             
         private:
-            uint_fast64_t stepCount;
+            boost::variant<uint_fast64_t, double> timeBound;
         };
     }
 }

src/modelchecker/csl/SparseCtmcCslModelChecker.cpp

@@ -84,7 +84,7 @@ namespace storm {
             if (comparator.isZero(lowerBound) && comparator.isInfinity(upperBound)) {
                 return this->computeUntilProbabilitiesHelper(this->getModel().getTransitionMatrix(), this->getModel().getBackwardTransitions(), phiStates, psiStates, qualitative, *this->linearEquationSolver);
             }
-
+            
             // From this point on, we know that we have to solve a more complicated problem [t, t'] with either t != 0
             // or t' != inf.
             
@@ -107,7 +107,7 @@ namespace storm {
                     if (comparator.isZero(lowerBound)) {
                         // In this case, the interval is of the form [0, t].
                         // Note that this excludes [0, inf] since this is untimed reachability and we considered this case earlier.
-
+                        
                         // Find the maximal rate of all 'maybe' states to take it as the uniformization rate.
                         ValueType uniformizationRate = 0;
                         for (auto const& state : statesWithProbabilityGreater0NonPsi) {
@@ -118,12 +118,12 @@ namespace storm {
                         
                         // Compute the uniformized matrix.
                         storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, psiStates, uniformizationRate, exitRates);
-
+                        
                         // Finally compute the transient probabilities.
                         std::vector<ValueType> psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>());
                         storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
                         
-                        std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * upperBound, psiStateValues, *this->linearEquationSolver);
+                        std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, upperBound, uniformizationRate, psiStateValues, *this->linearEquationSolver);
                         storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
                     } else if (comparator.isInfinity(upperBound)) {
                         // In this case, the interval is of the form [t, inf] with t != 0.
@@ -149,7 +149,7 @@ namespace storm {
                         storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), absorbingStates, uniformizationRate, exitRates);
                         
                         // Finally compute the transient probabilities.
-                        result = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * lowerBound, result, *this->linearEquationSolver);
+                        result = this->computeTransientProbabilities(uniformizedMatrix, lowerBound, uniformizationRate, result, *this->linearEquationSolver);
                     } else {
                         // In this case, the interval is of the form [t, t'] with t != 0 and t' != inf.
                         
@@ -167,7 +167,7 @@ namespace storm {
                         // Start by computing the transient probabilities of reaching a psi state in time t' - t.
                         std::vector<ValueType> psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero<ValueType>());
                         storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one<ValueType>());
-                        std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * (upperBound - lowerBound), psiStateValues, *this->linearEquationSolver);
+                        std::vector<ValueType> subresult = this->computeTransientProbabilities(uniformizedMatrix, upperBound - lowerBound, uniformizationRate, psiStateValues, *this->linearEquationSolver);
                         storm::utility::vector::setVectorValues(result, statesWithProbabilityGreater0, subresult);
                         
                         // Then compute the transient probabilities of being in such a state after t time units. For this,
@@ -178,7 +178,7 @@ namespace storm {
                             uniformizationRate = std::max(uniformizationRate, exitRates[state]);
                         }
                         uniformizationRate *= 1.02;
-
+                        
                         // Set the result to zero for all states that are known to violate phi.
                         storm::utility::vector::setVectorValues(result, absorbingStates, storm::utility::zero<ValueType>());
                         
@@ -186,7 +186,7 @@ namespace storm {
                         
                         // Finally, we compute the second set of transient probabilities.
                         uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), absorbingStates, uniformizationRate, exitRates);
-                        result = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * lowerBound, result, *this->linearEquationSolver);
+                        result = this->computeTransientProbabilities(uniformizedMatrix, lowerBound, uniformizationRate, result, *this->linearEquationSolver);
                     }
                 }
             }
@@ -227,7 +227,10 @@ namespace storm {
         }
         
         template<class ValueType>
-        std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType const& lambda, std::vector<ValueType> values, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver) const {
+        template<bool computeCumulativeReward>
+        std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver) const {
+            ValueType lambda = timeBound * uniformizationRate;
+            
             // If no time can pass, the current values are the result.
             if (lambda == storm::utility::zero<ValueType>()) {
                 return values;
@@ -241,6 +244,16 @@ namespace storm {
                 element /= std::get<2>(foxGlynnResult);
             }
             
+            // If the cumulative reward is to be computed, we need to adjust the weights.
+            if (computeCumulativeReward) {
+                ValueType sum = storm::utility::zero<ValueType>();
+                
+                for (auto& element : std::get<3>(foxGlynnResult)) {
+                    sum += element;
+                    element = (1 - sum) / uniformizationRate;
+                }
+            }
+            
             // Initialize result.
             std::vector<ValueType> result;
             uint_fast64_t startingIteration = std::get<0>(foxGlynnResult);
@@ -249,13 +262,26 @@ namespace storm {
                 storm::utility::vector::scaleVectorInPlace(result, std::get<3>(foxGlynnResult)[0]);
                 ++startingIteration;
             } else {
-                result = std::vector<ValueType>(values.size());
+                if (computeCumulativeReward) {
+                    result = std::vector<ValueType>(values.size());
+                    storm::utility::vector::applyPointwiseInPlace(result, [&uniformizationRate] (ValueType const& a) { return a / uniformizationRate; });
+                } else {
+                    result = std::vector<ValueType>(values.size());
+                }
             }
             std::vector<ValueType> multiplicationResult(result.size());
             
-            // Perform the matrix-vector multiplications (without adding).
-            if (std::get<0>(foxGlynnResult) > 1) {
+            if (!computeCumulativeReward && std::get<0>(foxGlynnResult) > 1) {
+                // Perform the matrix-vector multiplications (without adding).
                 linearEquationSolver.performMatrixVectorMultiplication(uniformizedMatrix, values, nullptr, std::get<0>(foxGlynnResult) - 1, &multiplicationResult);
+            } else if (computeCumulativeReward) {
+                std::function<ValueType(ValueType const&, ValueType const&)> addAndScale = [&uniformizationRate] (ValueType const& a, ValueType const& b) { return a + b / uniformizationRate; };
+                
+                // For the iterations below the left truncation point, we need to add and scale the result with the uniformization rate.
+                for (uint_fast64_t index = 1; index < startingIteration; ++index) {
+                    linearEquationSolver.performMatrixVectorMultiplication(uniformizedMatrix, values, nullptr, 1, &multiplicationResult);
+                    storm::utility::vector::applyPointwiseInPlace(result, values, addAndScale);
+                }
             }
             
             // For the indices that fall in between the truncation points, we need to perform the matrix-vector
@@ -277,6 +303,60 @@ namespace storm {
             return SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolver);
         }
         
+        template<class ValueType>
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound())));
+        }
+        
+        template<class ValueType>
+        std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeInstantaneousRewardsHelper(double timeBound) const {
+            // Only compute the result if the model has a state-based reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Initialize result to state rewards of the this->getModel().
+            std::vector<ValueType> result(this->getModel().getStateRewardVector());
+            
+            // If the time-bound is not zero, we need to perform a transient analysis.
+            if (timeBound > 0) {
+                ValueType uniformizationRate = 0;
+                for (auto const& rate : this->getModel().getExitRateVector()) {
+                    uniformizationRate = std::max(uniformizationRate, rate);
+                }
+                
+                storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector());
+                result = this->computeTransientProbabilities(uniformizedMatrix, timeBound, uniformizationRate, result, *this->linearEquationSolver);
+            }
+            
+            return result;
+        }
+        
+        template<class ValueType>
+        std::unique_ptr<CheckResult> SparseCtmcCslModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound())));
+        }
+        
+        template<class ValueType>
+        std::vector<ValueType> SparseCtmcCslModelChecker<ValueType>::computeCumulativeRewardsHelper(double timeBound) const {
+            // Only compute the result if the model has a state-based reward this->getModel().
+            STORM_LOG_THROW(this->getModel().hasStateRewards(), storm::exceptions::InvalidPropertyException, "Missing reward model for formula. Skipping formula.");
+            
+            // Initialize result to state rewards of the this->getModel().
+            std::vector<ValueType> result(this->getModel().getStateRewardVector());
+            
+            // If the time-bound is not zero, we need to perform a transient analysis.
+            if (timeBound > 0) {
+                ValueType uniformizationRate = 0;
+                for (auto const& rate : this->getModel().getExitRateVector()) {
+                    uniformizationRate = std::max(uniformizationRate, rate);
+                }
+                
+                storm::storage::SparseMatrix<ValueType> uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), storm::storage::BitVector(this->getModel().getNumberOfStates(), true), storm::storage::BitVector(this->getModel().getNumberOfStates()), uniformizationRate, this->getModel().getExitRateVector());
+                result = this->computeTransientProbabilities<true>(uniformizedMatrix, timeBound, uniformizationRate, result, *this->linearEquationSolver);
+            }
+            
+            return result;
+        }
+        
         template<class ValueType>
         storm::storage::SparseMatrix<ValueType> SparseCtmcCslModelChecker<ValueType>::computeProbabilityMatrix(storm::storage::SparseMatrix<ValueType> const& rateMatrix, std::vector<ValueType> const& exitRates) {
             // Turn the rates into probabilities by scaling each row with the exit rate of the state.

src/modelchecker/csl/SparseCtmcCslModelChecker.h

@@ -19,7 +19,9 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
-            
+            virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+
         protected:
             storm::models::sparse::Ctmc<ValueType> const& getModel() const override;
             
@@ -27,7 +29,9 @@ namespace storm {
             // The methods that perform the actual checking.
             std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<ValueType> const& exitRates, bool qualitative, double lowerBound, double upperBound) const;
             static std::vector<ValueType> computeUntilProbabilitiesHelper(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver);
-            
+            std::vector<ValueType> computeInstantaneousRewardsHelper(double timeBound) const;
+            std::vector<ValueType> computeCumulativeRewardsHelper(double timeBound) const;
+
             /*!
              * Computes the matrix representing the transitions of the uniformized CTMC.
              *
@@ -44,12 +48,16 @@ namespace storm {
              * Computes the transient probabilities for lambda time steps.
              *
              * @param uniformizedMatrix The uniformized transition matrix.
-             * @param lambda The number of time steps.
+             * @param timeBound The time bound to use.
+             * @param uniformizationRate The used uniformization rate.
              * @param values A vector mapping each state to an initial probability.
              * @param linearEquationSolver The linear equation solver to use.
+             * @param useMixedPoissonProbabilities If set to true, instead of taking the poisson probabilities,  mixed
+             * poisson probabilities are used.
              * @return The vector of transient probabilities.
              */
-            std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType const& lambda, std::vector<ValueType> values, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver) const;
+            template<bool useMixedPoissonProbabilities = false>
+            std::vector<ValueType> computeTransientProbabilities(storm::storage::SparseMatrix<ValueType> const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector<ValueType> values, storm::solver::LinearEquationSolver<ValueType> const& linearEquationSolver) const;
             
             /*!
              * Converts the given rate-matrix into a time-abstract probability matrix.

src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp

@@ -191,7 +191,8 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getStepBound())));
+            STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(rewardPathFormula.getDiscreteTimeBound())));
         }
         
         template<typename ValueType>
@@ -211,7 +212,8 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getStepCount())));
+            STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(rewardPathFormula.getDiscreteTimeBound())));
         }
         
         template<typename ValueType>

src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp

@@ -202,7 +202,8 @@ namespace storm {
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic.");
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepBound())));
+            STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getDiscreteTimeBound())));
         }
         
         template<typename ValueType>
@@ -222,7 +223,8 @@ namespace storm {
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic.");
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getStepCount())));
+            STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound.");
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getDiscreteTimeBound())));
         }
         
         template<typename ValueType>

src/parser/FormulaParser.cpp

@@ -14,10 +14,10 @@ namespace storm {
             // Set the identifier mapping to actually generate expressions.
             expressionParser.setIdentifierMapping(&identifiers_);
             
-            instantaneousRewardFormula = (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
+            instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
             instantaneousRewardFormula.name("instantaneous reward formula");
             
-            cumulativeRewardFormula = (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
+            cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParser::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
             cumulativeRewardFormula.name("cumulative reward formula");
             
             reachabilityRewardFormula = (qi::lit("F") > stateFormula)[qi::_val = phoenix::bind(&FormulaParser::createReachabilityRewardFormula, phoenix::ref(*this), qi::_1)];
@@ -171,12 +171,24 @@ namespace storm {
             return result;
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParser::createInstantaneousRewardFormula(unsigned stepCount) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(stepCount)));
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
+            if (timeBound.which() == 0) {
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
+            } else {
+                double timeBoundAsDouble = boost::get<double>(timeBound);
+                STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::InstantaneousRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
+            }
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParser::createCumulativeRewardFormula(unsigned stepBound) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(stepBound)));
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const {
+            if (timeBound.which() == 0) {
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(boost::get<unsigned>(timeBound))));
+            } else {
+                double timeBoundAsDouble = boost::get<double>(timeBound);
+                STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound.");
+                return std::shared_ptr<storm::logic::Formula>(new storm::logic::CumulativeRewardFormula(static_cast<uint_fast64_t>(timeBoundAsDouble)));
+            }
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParser::createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const {

src/parser/FormulaParser.h

@@ -157,8 +157,8 @@ namespace storm {
             boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
             
             // Methods that actually create the expression objects.
-            std::shared_ptr<storm::logic::Formula> createInstantaneousRewardFormula(unsigned stepCount) const;
-            std::shared_ptr<storm::logic::Formula> createCumulativeRewardFormula(unsigned stepBound) const;
+            std::shared_ptr<storm::logic::Formula> createInstantaneousRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
+            std::shared_ptr<storm::logic::Formula> createCumulativeRewardFormula(boost::variant<unsigned, double> const& timeBound) const;
             std::shared_ptr<storm::logic::Formula> createReachabilityRewardFormula(std::shared_ptr<storm::logic::Formula> const& stateFormula) const;
             std::shared_ptr<storm::logic::Formula> createAtomicExpressionFormula(storm::expressions::Expression const& expression) const;
             std::shared_ptr<storm::logic::Formula> createBooleanLiteralFormula(bool literal) const;