From c84751f63251f65572361a53259475c3f5077c17 Mon Sep 17 00:00:00 2001 From: dehnert Date: Fri, 20 Mar 2015 15:09:29 +0100 Subject: [PATCH] Started working on reward properties for CTMCs. Former-commit-id: a4e9b9a663c947fd4bed298da0a2128c8b0470d2 --- src/logic/CumulativeRewardFormula.cpp | 32 +++++- src/logic/CumulativeRewardFormula.h | 16 ++- src/logic/InstantaneousRewardFormula.cpp | 32 +++++- src/logic/InstantaneousRewardFormula.h | 16 ++- .../csl/SparseCtmcCslModelChecker.cpp | 104 ++++++++++++++++-- .../csl/SparseCtmcCslModelChecker.h | 16 ++- .../prctl/SparseDtmcPrctlModelChecker.cpp | 6 +- .../prctl/SparseMdpPrctlModelChecker.cpp | 6 +- src/parser/FormulaParser.cpp | 24 +++- src/parser/FormulaParser.h | 4 +- 10 files changed, 214 insertions(+), 42 deletions(-) diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp index 0c74d27f4..ef1dde50e 100644 --- a/src/logic/CumulativeRewardFormula.cpp +++ b/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(timeBound); + } + + bool CumulativeRewardFormula::hasContinuousTimeBound() const { + return timeBound.which() == 1; + } + + double CumulativeRewardFormula::getContinuousTimeBound() const { + if (this->hasDiscreteTimeBound()) { + return this->getDiscreteTimeBound(); + } else { + return boost::get(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; } } diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h index 45cb761b4..d48df1ac4 100644 --- a/src/logic/CumulativeRewardFormula.h +++ b/src/logic/CumulativeRewardFormula.h @@ -1,13 +1,17 @@ #ifndef STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ #define STORM_LOGIC_CUMULATIVEREWARDFORMULA_H_ +#include + #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 timeBound; }; } } diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp index 41234d1ab..579b88413 100644 --- a/src/logic/InstantaneousRewardFormula.cpp +++ b/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(timeBound); + } + + bool InstantaneousRewardFormula::hasContinuousTimeBound() const { + return timeBound.which() == 1; + } + + double InstantaneousRewardFormula::getContinuousTimeBound() const { + if (this->hasDiscreteTimeBound()) { + return this->getDiscreteTimeBound(); + } else { + return boost::get(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; } } diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h index c83afdc85..21e605494 100644 --- a/src/logic/InstantaneousRewardFormula.h +++ b/src/logic/InstantaneousRewardFormula.h @@ -1,13 +1,17 @@ #ifndef STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ #define STORM_LOGIC_INSTANTANEOUSREWARDFORMULA_H_ +#include + #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 timeBound; }; } } diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp index 828542bef..94de9020b 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp +++ b/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 uniformizedMatrix = this->computeUniformizedMatrix(this->getModel().getTransitionMatrix(), statesWithProbabilityGreater0, psiStates, uniformizationRate, exitRates); - + // Finally compute the transient probabilities. std::vector psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero()); storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one()); - std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * upperBound, psiStateValues, *this->linearEquationSolver); + std::vector 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 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 psiStateValues(statesWithProbabilityGreater0.getNumberOfSetBits(), storm::utility::zero()); storm::utility::vector::setVectorValues(psiStateValues, psiStates % statesWithProbabilityGreater0, storm::utility::one()); - std::vector subresult = this->computeTransientProbabilities(uniformizedMatrix, uniformizationRate * (upperBound - lowerBound), psiStateValues, *this->linearEquationSolver); + std::vector 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()); @@ -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 - std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType const& lambda, std::vector values, storm::solver::LinearEquationSolver const& linearEquationSolver) const { + template + std::vector SparseCtmcCslModelChecker::computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolver const& linearEquationSolver) const { + ValueType lambda = timeBound * uniformizationRate; + // If no time can pass, the current values are the result. if (lambda == storm::utility::zero()) { 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(); + + for (auto& element : std::get<3>(foxGlynnResult)) { + sum += element; + element = (1 - sum) / uniformizationRate; + } + } + // Initialize result. std::vector 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(values.size()); + if (computeCumulativeReward) { + result = std::vector(values.size()); + storm::utility::vector::applyPointwiseInPlace(result, [&uniformizationRate] (ValueType const& a) { return a / uniformizationRate; }); + } else { + result = std::vector(values.size()); + } } std::vector 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 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::computeUntilProbabilitiesHelper(transitionMatrix, backwardTransitions, phiStates, psiStates, qualitative, linearEquationSolver); } + template + std::unique_ptr SparseCtmcCslModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); + } + + template + std::vector SparseCtmcCslModelChecker::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 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 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 + std::unique_ptr SparseCtmcCslModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(rewardPathFormula.getContinuousTimeBound()))); + } + + template + std::vector SparseCtmcCslModelChecker::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 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 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 storm::storage::SparseMatrix SparseCtmcCslModelChecker::computeProbabilityMatrix(storm::storage::SparseMatrix const& rateMatrix, std::vector const& exitRates) { // Turn the rates into probabilities by scaling each row with the exit rate of the state. diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.h b/src/modelchecker/csl/SparseCtmcCslModelChecker.h index 3e0966e39..7b3c35e64 100644 --- a/src/modelchecker/csl/SparseCtmcCslModelChecker.h +++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.h @@ -19,7 +19,9 @@ namespace storm { virtual std::unique_ptr computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; virtual std::unique_ptr computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; - + virtual std::unique_ptr computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + virtual std::unique_ptr computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional const& optimalityType = boost::optional()) override; + protected: storm::models::sparse::Ctmc const& getModel() const override; @@ -27,7 +29,9 @@ namespace storm { // The methods that perform the actual checking. std::vector computeBoundedUntilProbabilitiesHelper(storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector const& exitRates, bool qualitative, double lowerBound, double upperBound) const; static std::vector computeUntilProbabilitiesHelper(storm::storage::SparseMatrix const& transitionMatrix, storm::storage::SparseMatrix const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolver const& linearEquationSolver); - + std::vector computeInstantaneousRewardsHelper(double timeBound) const; + std::vector 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 computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType const& lambda, std::vector values, storm::solver::LinearEquationSolver const& linearEquationSolver) const; + template + std::vector computeTransientProbabilities(storm::storage::SparseMatrix const& uniformizedMatrix, ValueType timeBound, ValueType uniformizationRate, std::vector values, storm::solver::LinearEquationSolver const& linearEquationSolver) const; /*! * Converts the given rate-matrix into a time-abstract probability matrix. diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp index a4e9d7ae9..2e5e928ac 100644 --- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp @@ -191,7 +191,8 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(rewardPathFormula.getStepBound()))); + STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(rewardPathFormula.getDiscreteTimeBound()))); } template @@ -211,7 +212,8 @@ namespace storm { template std::unique_ptr SparseDtmcPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional const& optimalityType) { - return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(rewardPathFormula.getStepCount()))); + STORM_LOG_THROW(rewardPathFormula.hasDiscreteTimeBound(), storm::exceptions::InvalidArgumentException, "Formula needs to have a discrete time bound."); + return std::unique_ptr(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(rewardPathFormula.getDiscreteTimeBound()))); } template diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp index 8f30f22b2..973a7731a 100644 --- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp +++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp @@ -202,7 +202,8 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative, boost::optional 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(new ExplicitQuantitativeCheckResult(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(new ExplicitQuantitativeCheckResult(this->computeCumulativeRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getDiscreteTimeBound()))); } template @@ -222,7 +223,8 @@ namespace storm { template std::unique_ptr SparseMdpPrctlModelChecker::computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative, boost::optional 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(new ExplicitQuantitativeCheckResult(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(new ExplicitQuantitativeCheckResult(this->computeInstantaneousRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rewardPathFormula.getDiscreteTimeBound()))); } template diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index d75358d36..218a51734 100644 --- a/src/parser/FormulaParser.cpp +++ b/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 FormulaParser::createInstantaneousRewardFormula(unsigned stepCount) const { - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(stepCount))); + std::shared_ptr FormulaParser::createInstantaneousRewardFormula(boost::variant const& timeBound) const { + if (timeBound.which() == 0) { + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); + } else { + double timeBoundAsDouble = boost::get(timeBound); + STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(timeBoundAsDouble))); + } } - std::shared_ptr FormulaParser::createCumulativeRewardFormula(unsigned stepBound) const { - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(stepBound))); + std::shared_ptr FormulaParser::createCumulativeRewardFormula(boost::variant const& timeBound) const { + if (timeBound.which() == 0) { + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); + } else { + double timeBoundAsDouble = boost::get(timeBound); + STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); + } } std::shared_ptr FormulaParser::createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const { diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index 685160237..c5735286b 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -157,8 +157,8 @@ namespace storm { boost::spirit::qi::real_parser> strict_double; // Methods that actually create the expression objects. - std::shared_ptr createInstantaneousRewardFormula(unsigned stepCount) const; - std::shared_ptr createCumulativeRewardFormula(unsigned stepBound) const; + std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; std::shared_ptr createReachabilityRewardFormula(std::shared_ptr const& stateFormula) const; std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; std::shared_ptr createBooleanLiteralFormula(bool literal) const;