Bounds of operator formulas are now expressions, allowing formulas such as P<1/N [ F "goal" ] for model constant N

src/storm/logic/Bound.h

@@ -2,37 +2,29 @@
 #define	STORM_LOGIC_BOUND_H_
 
 #include "storm/logic/ComparisonType.h"
+#include "storm/storage/expressions/Expression.h"
 #include "storm/utility/constants.h"
 
+
 namespace storm {
     namespace logic {
-        template<typename ValueType>
         struct Bound {
-            Bound(ComparisonType comparisonType, ValueType const& threshold) : comparisonType(comparisonType), threshold(threshold) {
+            Bound(ComparisonType comparisonType, storm::expressions::Expression const& threshold) : comparisonType(comparisonType), threshold(threshold) {
                 // Intentionally left empty.
             }
 
-            template<typename OtherValueType>
-            Bound<OtherValueType> convertToOtherValueType() const {
-                return Bound<OtherValueType>(comparisonType, storm::utility::convertNumber<OtherValueType>(threshold));
-            }
-            
             ComparisonType comparisonType;
-            ValueType threshold;
+            storm::expressions::Expression threshold;
 
-            template<typename ValueTypePrime>
-            friend std::ostream& operator<<(std::ostream& out, Bound<ValueTypePrime> const& bound);
+            friend std::ostream& operator<<(std::ostream& out, Bound const& bound);
         };
 
-        template<typename ValueType>
-        std::ostream& operator<<(std::ostream& out, Bound<ValueType> const& bound) {
+        inline std::ostream& operator<<(std::ostream& out, Bound const& bound) {
             out << bound.comparisonType << bound.threshold;
             return out;
         }
     }
     
-    template<typename ValueType>
-    using Bound = typename logic::Bound<ValueType>;
 }
 
 #endif	/* STORM_LOGIC_BOUND_H_ */

src/storm/logic/FormulasForwardDeclarations.h

@@ -23,6 +23,7 @@ namespace storm {
         class MultiObjectiveFormula;
         class NextFormula;
         class OperatorFormula;
+        struct OperatorInformation;
         class PathFormula;
         class ProbabilityOperatorFormula;
         class RewardOperatorFormula;

src/storm/logic/OperatorFormula.cpp

@@ -1,8 +1,12 @@
 #include "storm/logic/OperatorFormula.h"
 
+#include "storm/adapters/CarlAdapter.h"
+
+#include "storm/exceptions/InvalidOperationException.h"
+
 namespace storm {
     namespace logic {
-        OperatorInformation::OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound<RationalNumber>> const& bound) : optimalityType(optimizationDirection), bound(bound) {
+        OperatorInformation::OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound> const& bound) : optimalityType(optimizationDirection), bound(bound) {
             // Intentionally left empty.
         }
         
@@ -23,19 +27,37 @@ namespace storm {
             operatorInformation.bound.get().comparisonType = newComparisonType;
         }
         
-        RationalNumber const& OperatorFormula::getThreshold() const {
+        storm::expressions::Expression const& OperatorFormula::getThreshold() const {
             return operatorInformation.bound.get().threshold;
         }
         
-        void OperatorFormula::setThreshold(RationalNumber const& newThreshold) {
+        template <>
+        double OperatorFormula::getThresholdAs() const {
+            STORM_LOG_THROW(!operatorInformation.bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << operatorInformation.bound.get().threshold << "' as it contains undefined constants.");
+            return operatorInformation.bound.get().threshold.evaluateAsDouble();
+        }
+        
+        template <>
+        storm::RationalNumber OperatorFormula::getThresholdAs() const {
+            STORM_LOG_THROW(!operatorInformation.bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << operatorInformation.bound.get().threshold << "' as it contains undefined constants.");
+            return operatorInformation.bound.get().threshold.evaluateAsRational();
+        }
+        
+        template <>
+        storm::RationalFunction OperatorFormula::getThresholdAs() const {
+            STORM_LOG_THROW(!operatorInformation.bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << operatorInformation.bound.get().threshold << "' as it contains undefined constants.");
+            return storm::utility::convertNumber<storm::RationalFunction>(operatorInformation.bound.get().threshold.evaluateAsRational());
+        }
+        
+        void OperatorFormula::setThreshold(storm::expressions::Expression const& newThreshold) {
             operatorInformation.bound.get().threshold = newThreshold;
         }
         
-        Bound<RationalNumber> const& OperatorFormula::getBound() const {
+        Bound const& OperatorFormula::getBound() const {
             return operatorInformation.bound.get();
         }
         
-        void OperatorFormula::setBound(Bound<RationalNumber> const& newBound) {
+        void OperatorFormula::setBound(Bound const& newBound) {
             operatorInformation.bound = newBound;
         }
         

src/storm/logic/OperatorFormula.h

@@ -6,18 +6,18 @@
 #include "storm/logic/UnaryStateFormula.h"
 #include "storm/logic/Bound.h"
 #include "storm/solver/OptimizationDirection.h"
+#include "storm/storage/expressions/Expression.h"
 
-#include "storm/adapters/CarlAdapter.h"
 #include "storm/utility/constants.h"
 
 namespace storm {
     namespace logic {
 
         struct OperatorInformation {
-            OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<RationalNumber>> const& bound = boost::none);
+            OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound> const& bound = boost::none);
 
             boost::optional<storm::solver::OptimizationDirection> optimalityType;
-            boost::optional<Bound<RationalNumber>> bound;
+            boost::optional<Bound> bound;
         };
         
         class OperatorFormula : public UnaryStateFormula {
@@ -32,14 +32,12 @@ namespace storm {
             bool hasBound() const;
             ComparisonType getComparisonType() const;
             void setComparisonType(ComparisonType newComparisonType);
-            RationalNumber const& getThreshold() const;
-            template<typename ValueType=RationalNumber>
-            ValueType getThresholdAs() const {
-                return storm::utility::convertNumber<ValueType>(this->getThreshold());
-            }
-            void setThreshold(RationalNumber const& newThreshold);
-            Bound<RationalNumber> const& getBound() const;
-            void setBound(Bound<RationalNumber> const& newBound);
+            storm::expressions::Expression const& getThreshold() const;
+            template <typename ValueType>
+            ValueType getThresholdAs() const;
+            void setThreshold(storm::expressions::Expression const& newThreshold);
+            Bound const& getBound() const;
+            void setBound(Bound const& newBound);
             
             // Optimality-type-related accessors.
             bool hasOptimalityType() const;

src/storm/logic/VariableSubstitutionVisitor.cpp

@@ -13,6 +13,26 @@ namespace storm {
             boost::any result = f.accept(*this, boost::any());
             return boost::any_cast<std::shared_ptr<Formula>>(result);
         }
+               
+        boost::any VariableSubstitutionVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<TimeOperatorFormula>(subformula, substituteOperatorInformation(f.getOperatorInformation())));
+        }
+        
+        boost::any VariableSubstitutionVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageOperatorFormula>(subformula, substituteOperatorInformation(f.getOperatorInformation())));
+        }
+        
+        boost::any VariableSubstitutionVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<ProbabilityOperatorFormula>(subformula, substituteOperatorInformation(f.getOperatorInformation())));
+        }
+        
+        boost::any VariableSubstitutionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), substituteOperatorInformation(f.getOperatorInformation())));
+        }
         
         boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
             auto left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
@@ -41,5 +61,14 @@ namespace storm {
         boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const&) const {
             return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f.getExpression().substitute(substitution)));
         }
+        
+        OperatorInformation VariableSubstitutionVisitor::substituteOperatorInformation(OperatorInformation const& operatorInformation) const {
+            boost::optional<Bound> bound;
+            if(operatorInformation.bound) {
+               bound = Bound(operatorInformation.bound->comparisonType, operatorInformation.bound->threshold.substitute(substitution));
+            }
+            return OperatorInformation(operatorInformation.optimalityType, bound);
+        }
+
     }
 }

src/storm/logic/VariableSubstitutionVisitor.h

@@ -16,12 +16,20 @@ namespace storm {
             
             std::shared_ptr<Formula> substitute(Formula const& f) const;
             
+
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
             
         private:
+            
+            OperatorInformation substituteOperatorInformation(OperatorInformation const& operatorInformation) const;
+            
             std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution;
         };
         

src/storm/modelchecker/CheckTask.h

@@ -9,6 +9,9 @@
 #include "storm/solver/OptimizationDirection.h"
 #include "storm/logic/ComparisonType.h"
 
+#include "storm/exceptions/InvalidOperationException.h"
+
+
 namespace storm {
     namespace logic {
         class Formula;
@@ -45,7 +48,7 @@ namespace storm {
                     
                     if (operatorFormula.hasBound()) {
                         if (onlyInitialStatesRelevant) {
-                            this->bound = operatorFormula.getBound().convertToOtherValueType<ValueType>();
+                            this->bound = operatorFormula.getBound();
                         }
 
                         if (!optimizationDirection) {
@@ -58,7 +61,7 @@ namespace storm {
                     storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
                     
                     if (probabilityOperatorFormula.hasBound()) {
-                        if (storm::utility::isZero(probabilityOperatorFormula.getThreshold()) || storm::utility::isOne(probabilityOperatorFormula.getThreshold())) {
+                        if (storm::utility::isZero(probabilityOperatorFormula.template getThresholdAs<ValueType>()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs<ValueType>())) {
                             this->qualitative = true;
                         }
                     }
@@ -67,7 +70,7 @@ namespace storm {
                     this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
                     
                     if (rewardOperatorFormula.hasBound()) {
-                        if (storm::utility::isZero(rewardOperatorFormula.getThreshold())) {
+                        if (storm::utility::isZero(rewardOperatorFormula.template getThresholdAs<ValueType>())) {
                             this->qualitative = true;
                         }
                     }
@@ -143,8 +146,9 @@ namespace storm {
             /*!
              * Retrieves the value of the bound (if set).
              */
-            ValueType const& getBoundThreshold() const {
-                return bound.get().threshold;
+            ValueType getBoundThreshold() const {
+                STORM_LOG_THROW(!bound.get().threshold.containsVariables(), storm::exceptions::InvalidOperationException, "Cannot evaluate threshold '" << bound.get().threshold << "' as it contains undefined constants.");
+                return storm::utility::convertNumber<ValueType>(bound.get().threshold.evaluateAsRational());
             }
             
             /*!
@@ -157,14 +161,14 @@ namespace storm {
             /*!
              * Retrieves the bound (if set).
              */
-            storm::logic::Bound<ValueType> const& getBound() const {
+            storm::logic::Bound const& getBound() const {
                 return bound.get();
             }
 
             /*!
              * Retrieves the bound (if set).
              */
-            boost::optional<storm::logic::Bound<ValueType>> const& getOptionalBound() const {
+            boost::optional<storm::logic::Bound> const& getOptionalBound() const {
                 return bound;
             }
 
@@ -236,7 +240,7 @@ namespace storm {
              * @param produceSchedulers If supported by the model checker and the model formalism, schedulers to achieve
              * a value will be produced if this flag is set.
              */
-            CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound<ValueType>> const& bound, bool qualitative, bool produceSchedulers, boost::optional<std::vector<ValueType>> const& resultHint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), resultHint(resultHint) {
+            CheckTask(std::reference_wrapper<FormulaType const> const& formula, boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<std::string> const& rewardModel, bool onlyInitialStatesRelevant, boost::optional<storm::logic::Bound> const& bound, bool qualitative, bool produceSchedulers, boost::optional<std::vector<ValueType>> const& resultHint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), resultHint(resultHint) {
                 // Intentionally left empty.
             }
             
@@ -253,7 +257,7 @@ namespace storm {
             bool onlyInitialStatesRelevant;
 
             // The bound with which the states will be compared.
-            boost::optional<storm::logic::Bound<ValueType>> bound;
+            boost::optional<storm::logic::Bound> bound;
             
             // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1.
             bool qualitative;

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -121,12 +121,11 @@ namespace storm {
         std::unique_ptr<CheckResult> checkForResultAfterQualitativeCheck(CheckTask<storm::logic::Formula> const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd<Type> const& initialStates, storm::dd::Bdd<Type> const& prob0, storm::dd::Bdd<Type> const& prob1) {
             std::unique_ptr<CheckResult> result;
             
-            boost::optional<storm::logic::Bound<ValueType>> const& bound = checkTask.getOptionalBound();
-            if (bound) {
+            if (checkTask.isBoundSet()) {
                 // Despite having a bound, we create a quanitative result so that the next layer can perform the comparison.
                 
                 if (player2Direction == storm::OptimizationDirection::Minimize) {
-                    if (storm::logic::isLowerBound(bound.get().comparisonType)) {
+                    if (storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
                         if ((prob1 && initialStates) == initialStates) {
                             result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::one<ValueType>());
                         }
@@ -136,7 +135,7 @@ namespace storm {
                         }
                     }
                 } else if (player2Direction == storm::OptimizationDirection::Maximize) {
-                    if (!storm::logic::isLowerBound(bound.get().comparisonType)) {
+                    if (!storm::logic::isLowerBound(checkTask.getBoundComparisonType())) {
                         if ((prob0 && initialStates) == initialStates) {
                             result = std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ValueType>>(storm::storage::sparse::state_type(0), storm::utility::zero<ValueType>());
                         }
@@ -173,16 +172,15 @@ namespace storm {
             // return the value because the property will definitely hold. Vice versa, if the minimum value exceeds an
             // upper bound or the maximum value is below a lower bound, the property will definitely not hold and we can
             // return the value.
-            boost::optional<storm::logic::Bound<ValueType>> const& bound = checkTask.getOptionalBound();
-            if (!bound) {
+            if (!checkTask.isBoundSet()) {
                 return result;
             }
             
             ValueType const& lowerValue = initialValueRange.first;
             ValueType const& upperValue = initialValueRange.second;
             
-            storm::logic::ComparisonType comparisonType = bound.get().comparisonType;
-            ValueType threshold = bound.get().threshold;
+            storm::logic::ComparisonType comparisonType = checkTask.getBoundComparisonType();
+            ValueType threshold = checkTask.getBoundThreshold();
             
             if (storm::logic::isLowerBound(comparisonType)) {
                 if (player2Direction == storm::OptimizationDirection::Minimize) {

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

@@ -111,7 +111,7 @@ namespace storm {
                 
                 bool formulaMinimizes = false;
                 if(formula.hasBound()) {
-                    currentObjective.threshold = storm::utility::convertNumber<ValueType>(formula.getBound().threshold);
+                    currentObjective.threshold = formula.template getThresholdAs<ValueType>();
                     currentObjective.thresholdIsStrict = storm::logic::isStrict(formula.getBound().comparisonType);
                     //Note that we minimize for upper bounds since we are looking for the EXISTENCE of a satisfying scheduler
                     formulaMinimizes = !storm::logic::isLowerBound(formula.getBound().comparisonType);

src/storm/modelchecker/region/ApproximationModel.cpp

@@ -75,7 +75,7 @@ namespace storm {
                 filter.set(this->solverData.initialStateIndex, true);
                 this->solverData.player1Goal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>(
                             storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize,
-                            formula->getBound().convertToOtherValueType<ConstantType>(),
+                            formula->getComparisonType(), formula->getThresholdAs<ConstantType>(),
                             filter
                         );
             }                

src/storm/modelchecker/region/SamplingModel.cpp

@@ -89,7 +89,7 @@ namespace storm {
                 filter.set(this->solverData.initialStateIndex, true);
                 this->solverData.solveGoal = std::make_unique<storm::solver::BoundedGoal<ConstantType>>(
                             storm::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize,
-                            formula->getBound().convertToOtherValueType<ConstantType>(),
+                            formula->getComparisonType(), formula->getThresholdAs<ConstantType>(),
                             filter
                         );
             }

src/storm/modelchecker/region/SparseRegionModelChecker.cpp

@@ -79,7 +79,7 @@ namespace storm {
 
             template<typename ParametricSparseModelType, typename ConstantType>
             ConstantType SparseRegionModelChecker<ParametricSparseModelType, ConstantType>::getSpecifiedFormulaBound() const {
-                return storm::utility::convertNumber<ConstantType>(this->getSpecifiedFormula()->getThreshold());
+                return this->getSpecifiedFormula()->template getThresholdAs<ConstantType>();
             }
 
             template<typename ParametricSparseModelType, typename ConstantType>

src/storm/parser/FormulaParserGrammar.cpp

@@ -286,7 +286,7 @@ namespace storm {
         storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const {
             if (comparisonType && threshold) {
                 storm::expressions::ExpressionEvaluator<storm::RationalNumber> evaluator(*constManager);
-                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<RationalNumber>(comparisonType.get(), evaluator.asRational(threshold.get())));
+                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get()));
             } else {
                 return storm::logic::OperatorInformation(optimizationDirection, boost::none);
             }

src/storm/parser/JaniParser.cpp

@@ -177,7 +177,7 @@ namespace storm {
         }
 
         
-        std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound) {
+        std::shared_ptr<storm::logic::Formula const> JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound> bound) {
             if (propertyStructure.is_boolean()) {
                 return std::make_shared<storm::logic::BooleanLiteralFormula>(propertyStructure.get<bool>());
             }
@@ -403,13 +403,11 @@ namespace storm {
                     if (propertyStructure.at("left").count("op") > 0 && (propertyStructure.at("left").at("op") == "Pmin" || propertyStructure.at("left").at("op") == "Pmax" || propertyStructure.at("left").at("op") == "Emin" || propertyStructure.at("left").at("op") == "Emax" || propertyStructure.at("left").at("op") == "Smin" || propertyStructure.at("left").at("op") == "Smax")) {
                         auto expr = parseExpression(propertyStructure.at("right"), "Threshold for operator " + propertyStructure.at("left").at("op").get<std::string>());
                         STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported");
-                        // TODO evaluate this expression directly as rational number
-                        return parseFormula(propertyStructure.at("left"), formulaContext, "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble())));
+                        return parseFormula(propertyStructure.at("left"), formulaContext, "", storm::logic::Bound(ct, expr));
                     } else if(propertyStructure.at("right").count("op") > 0 && (propertyStructure.at("right").at("op") == "Pmin" || propertyStructure.at("right").at("op") == "Pmax" || propertyStructure.at("right").at("op") == "Emin" || propertyStructure.at("right").at("op") == "Emax" || propertyStructure.at("right").at("op") == "Smin" || propertyStructure.at("right").at("op") == "Smax")) {
                         auto expr = parseExpression(propertyStructure.at("left"), "Threshold for operator " + propertyStructure.at("right").at("op").get<std::string>());
                         STORM_LOG_THROW(expr.getVariables().empty(), storm::exceptions::NotSupportedException, "Only constant thresholds supported");
-                        // TODO evaluate this expression directly as rational number
-                        return parseFormula(propertyStructure.at("right"),formulaContext, "", storm::logic::Bound<storm::RationalNumber>(ct, storm::utility::convertNumber<storm::RationalNumber>(expr.evaluateAsDouble())));
+                        return parseFormula(propertyStructure.at("right"),formulaContext, "", storm::logic::Bound(ct, expr));
                         
                     } else {
                          STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No complex comparisons are allowed.");

src/storm/parser/JaniParser.h

@@ -58,7 +58,7 @@ namespace storm {
              * Helper for parsing the actions of a model.
              */
             void parseActions(json const& actionStructure, storm::jani::Model& parentModel);
-            std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound<storm::RationalNumber>> bound = boost::none);
+            std::shared_ptr<storm::logic::Formula const> parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional<storm::logic::Bound> bound = boost::none);
             std::vector<storm::expressions::Expression> parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
             std::vector<storm::expressions::Expression> parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring,  std::string const& scopeDescription, std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>> const& localVars = std::unordered_map<std::string, std::shared_ptr<storm::jani::Variable>>(), bool returnNoneOnUnknownOpString = false);
 

src/storm/solver/SolveGoal.h

@@ -60,11 +60,7 @@ namespace storm {
         template<typename ValueType>
         class BoundedGoal : public SolveGoal {
         public:
-            BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType comparisonType, ValueType const& threshold, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(comparisonType, threshold), relevantValueVector(relevantValues) {
-                // Intentionally left empty.
-            }
-            
-            BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::Bound<ValueType> const& bound, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), bound(bound), relevantValueVector(relevantValues) {
+            BoundedGoal(OptimizationDirection optimizationDirection, storm::logic::ComparisonType boundComparisonType, ValueType const& boundThreshold, storm::storage::BitVector const& relevantValues) : SolveGoal(optimizationDirection), comparisonType(boundComparisonType), threshold(boundThreshold), relevantValueVector(relevantValues) {
                 // Intentionally left empty.
             }
             
@@ -77,31 +73,31 @@ namespace storm {
             }
             
             bool boundIsALowerBound() const { 
-                return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::GreaterEqual);
+                return (comparisonType == storm::logic::ComparisonType::Greater || comparisonType == storm::logic::ComparisonType::GreaterEqual);
             }
             
             bool boundIsStrict() const {
-                return (bound.comparisonType == storm::logic::ComparisonType::Greater || bound.comparisonType == storm::logic::ComparisonType::Less);
+                return (comparisonType == storm::logic::ComparisonType::Greater || comparisonType == storm::logic::ComparisonType::Less);
             }
             
             ValueType const& thresholdValue() const {
-                return bound.threshold;
+                return threshold;
             }
 
-            bool achieved(std::vector<ValueType> const& result) const{
-                for(std::size_t i : relevantValueVector){
-                    switch(bound.comparisonType) {
+            bool achieved(std::vector<ValueType> const& result) const {
+                for (auto const& i : relevantValueVector) {
+                    switch(comparisonType) {
                     case storm::logic::ComparisonType::Greater:
-                        if( result[i] <= bound.threshold) return false;
+                        if( result[i] <= threshold) return false;
                         break;
                     case storm::logic::ComparisonType::GreaterEqual:
-                        if( result[i] < bound.threshold) return false;
+                        if( result[i] < threshold) return false;
                         break;
                     case storm::logic::ComparisonType::Less:
-                        if( result[i] >= bound.threshold) return false;
+                        if( result[i] >= threshold) return false;
                         break;
                     case storm::logic::ComparisonType::LessEqual:
-                        if( result[i] > bound.threshold) return false;
+                        if( result[i] > threshold) return false;
                         break;
                     }
                 }
@@ -113,7 +109,8 @@ namespace storm {
             }
             
         private:
-            Bound<ValueType> bound;
+            storm::logic::ComparisonType comparisonType;
+            ValueType threshold;
             storm::storage::BitVector relevantValueVector;
         };
         

src/storm/storage/jani/JSONExporter.cpp

@@ -210,7 +210,7 @@ namespace storm {
                 }
                 opDecl["left"]["exp"] = modernjson::json(1);
                 opDecl["left"]["accumulate"] = modernjson::json(tvec);
-                opDecl["right"] = numberToJson(bound.threshold);
+                opDecl["right"] = ExpressionToJson::translate(bound.threshold);
             } else {
                 if(f.hasOptimalityType()) {
                     opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";
@@ -247,7 +247,7 @@ namespace storm {
                     opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin";
                     opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, data));
                 }
-                opDecl["right"] = numberToJson(bound.threshold);
+                opDecl["right"] = ExpressionToJson::translate(bound.threshold);
             } else {
                 if(f.hasOptimalityType()) {
                     opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
@@ -275,7 +275,7 @@ namespace storm {
 //                    opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Smax" : "Smin";
 //                    opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, boost::none));
 //                }
-//                opDecl["right"] = numberToJson(bound.threshold);
+//                opDecl["right"] = ExpressionToJson::translate(bound.threshold);
 //            } else {
 //                if(f.hasOptimalityType()) {
 //                    opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Smin" : "Smax";
@@ -322,7 +322,7 @@ namespace storm {
                     opDecl["left"]["op"] = (bound.comparisonType == storm::logic::ComparisonType::Less || bound.comparisonType == storm::logic::ComparisonType::LessEqual) ? "Pmax" : "Pmin";
                     opDecl["left"]["exp"] = boost::any_cast<modernjson::json>(f.getSubformula().accept(*this, data));
                 }
-                opDecl["right"] = numberToJson(bound.threshold);
+                opDecl["right"] = ExpressionToJson::translate(bound.threshold);
             } else {
                 if(f.hasOptimalityType()) {
                     opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Pmin" : "Pmax";
@@ -358,7 +358,7 @@ namespace storm {
                 STORM_LOG_THROW(f.hasRewardModelName(), storm::exceptions::NotSupportedException, "Reward name has to be specified for Jani-conversion");
                 opDecl["left"]["exp"] = f.getRewardModelName();
                 opDecl["left"]["accumulate"] = modernjson::json(accvec);
-                opDecl["right"] = numberToJson(bound.threshold);
+                opDecl["right"] = ExpressionToJson::translate(bound.threshold);
             } else {
                 if(f.hasOptimalityType()) {
                     opDecl["op"] = f.getOptimalityType() == storm::solver::OptimizationDirection::Minimize ? "Emin" : "Emax";