From d0551c1d593a9f4756d75c507c858f8cead9dd76 Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 4 Jul 2017 10:48:26 +0200 Subject: [PATCH] getting time/step/reward bounds as rational number --- src/storm/logic/BoundedUntilFormula.cpp | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp index 66b5a29fa..b954d4720 100644 --- a/src/storm/logic/BoundedUntilFormula.cpp +++ b/src/storm/logic/BoundedUntilFormula.cpp @@ -1,5 +1,6 @@ #include "storm/logic/BoundedUntilFormula.h" +#include "storm/utility/constants.h" #include "storm/utility/macros.h" #include "storm/exceptions/InvalidArgumentException.h" @@ -80,6 +81,22 @@ namespace storm { return bound; } + template <> + storm::RationalNumber BoundedUntilFormula::getLowerBound() const { + checkNoVariablesInBound(this->getLowerBound()); + storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + + template <> + storm::RationalNumber BoundedUntilFormula::getUpperBound() const { + checkNoVariablesInBound(this->getUpperBound()); + storm::RationalNumber bound = this->getLowerBound().evaluateAsRational(); + STORM_LOG_THROW(bound >= storm::utility::zero(), storm::exceptions::InvalidPropertyException, "Time-bound must not evaluate to negative number."); + return bound; + } + template <> uint64_t BoundedUntilFormula::getLowerBound() const { checkNoVariablesInBound(this->getLowerBound());