formulae with rational number bounds

Former-commit-id: 17755ccf84

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -985,7 +985,7 @@ namespace storm {
                 STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
                 
                 bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
-                double threshold = probabilityOperator.getThreshold();
+                double threshold = probabilityOperator.getThresholdAs<double>();
 
                 storm::storage::BitVector phiStates;
                 storm::storage::BitVector psiStates;

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -1762,7 +1762,7 @@ namespace storm {
                 STORM_LOG_THROW(probabilityOperator.getSubformula().isUntilFormula() || probabilityOperator.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Path formula is required to be of the form 'phi U psi' for counterexample generation.");
                 
                 bool strictBound = comparisonType == storm::logic::ComparisonType::Less;
-                double threshold = probabilityOperator.getThreshold();
+                double threshold = probabilityOperator.getThresholdAs<double>();
                 
                 storm::storage::BitVector phiStates;
                 storm::storage::BitVector psiStates;

src/logic/Bound.h

@@ -2,6 +2,7 @@
 #define	STORM_LOGIC_BOUND_H_
 
 #include "src/logic/ComparisonType.h"
+#include "src/utility/constants.h"
 
 namespace storm {
     namespace logic {
@@ -10,6 +11,11 @@ namespace storm {
             Bound(ComparisonType comparisonType, ValueType 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;

src/logic/OperatorFormula.cpp

@@ -2,7 +2,7 @@
 
 namespace storm {
     namespace logic {
-        OperatorInformation::OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound<double>> const& bound) : optimalityType(optimizationDirection), bound(bound) {
+        OperatorInformation::OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection, boost::optional<Bound<RationalNumber>> const& bound) : optimalityType(optimizationDirection), bound(bound) {
             // Intentionally left empty.
         }
         
@@ -22,19 +22,19 @@ namespace storm {
             operatorInformation.bound.get().comparisonType = newComparisonType;
         }
         
-        double OperatorFormula::getThreshold() const {
+        RationalNumber const& OperatorFormula::getThreshold() const {
             return operatorInformation.bound.get().threshold;
         }
         
-        void OperatorFormula::setThreshold(double newThreshold) {
+        void OperatorFormula::setThreshold(RationalNumber const& newThreshold) {
             operatorInformation.bound.get().threshold = newThreshold;
         }
         
-        Bound<double> const& OperatorFormula::getBound() const {
+        Bound<RationalNumber> const& OperatorFormula::getBound() const {
             return operatorInformation.bound.get();
         }
         
-        void OperatorFormula::setBound(Bound<double> const& newBound) {
+        void OperatorFormula::setBound(Bound<RationalNumber> const& newBound) {
             operatorInformation.bound = newBound;
         }
         

src/logic/OperatorFormula.h

@@ -7,13 +7,16 @@
 #include "src/logic/Bound.h"
 #include "src/solver/OptimizationDirection.h"
 
+#include "src/adapters/CarlAdapter.h"
+#include "src/utility/constants.h"
+
 namespace storm {
     namespace logic {        
         struct OperatorInformation {
-            OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<double>> const& bound = boost::none);
+            OperatorInformation(boost::optional<storm::solver::OptimizationDirection> const& optimizationDirection = boost::none, boost::optional<Bound<RationalNumber>> const& bound = boost::none);
 
             boost::optional<storm::solver::OptimizationDirection> optimalityType;
-            boost::optional<Bound<double>> bound;
+            boost::optional<Bound<RationalNumber>> bound;
         };
         
         class OperatorFormula : public UnaryStateFormula {
@@ -28,10 +31,14 @@ namespace storm {
             bool hasBound() const;
             ComparisonType getComparisonType() const;
             void setComparisonType(ComparisonType newComparisonType);
-            double getThreshold() const;
-            void setThreshold(double newThreshold);
-            Bound<double> const& getBound() const;
-            void setBound(Bound<double> const& newBound);
+            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);
             
             // Optimality-type-related accessors.
             bool hasOptimalityType() const;

src/modelchecker/AbstractModelChecker.cpp

@@ -183,7 +183,7 @@ namespace storm {
             
             if (stateFormula.hasBound()) {
                 STORM_LOG_THROW(result->isQuantitative(), storm::exceptions::InvalidOperationException, "Unable to perform comparison operation on non-quantitative result.");
-                return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThreshold());
+                return result->asQuantitativeCheckResult().compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getThresholdAs<double>());
             } else {
                 return result;
             }

src/modelchecker/CheckTask.h

@@ -45,7 +45,7 @@ namespace storm {
                     
                     if (operatorFormula.hasBound()) {
                         if (onlyInitialStatesRelevant) {
-                            this->bound = operatorFormula.getBound();
+                            this->bound = operatorFormula.getBound().convertToOtherValueType<ValueType>();
                         }
 
                         if (!optimizationDirection) {
@@ -58,7 +58,7 @@ namespace storm {
                     storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
                     
                     if (probabilityOperatorFormula.hasBound()) {
-                        if (probabilityOperatorFormula.getThreshold() == storm::utility::zero<ValueType>() || probabilityOperatorFormula.getThreshold() == storm::utility::one<ValueType>()) {
+                        if (storm::utility::isZero(probabilityOperatorFormula.getThreshold()) || storm::utility::isOne(probabilityOperatorFormula.getThreshold())) {
                             this->qualitative = true;
                         }
                     }
@@ -67,7 +67,7 @@ namespace storm {
                     this->rewardModel = rewardOperatorFormula.getOptionalRewardModelName();
                     
                     if (rewardOperatorFormula.hasBound()) {
-                        if (rewardOperatorFormula.getThreshold() == storm::utility::zero<ValueType>()) {
+                        if (storm::utility::isZero(rewardOperatorFormula.getThreshold())) {
                             this->qualitative = true;
                         }
                     }

src/parser/FormulaParser.cpp

@@ -478,7 +478,7 @@ namespace storm {
         
         storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<double> const& threshold) const {
             if (comparisonType && threshold) {
-                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<double>(comparisonType.get(), threshold.get()));
+                return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound<RationalNumber>(comparisonType.get(), storm::utility::convertNumber<RationalNumber>(threshold.get())));
             } else {
                 return storm::logic::OperatorInformation(optimizationDirection, boost::none);
             }

src/permissivesched/PermissiveSchedulers.cpp

@@ -26,7 +26,7 @@ namespace storm {
             auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi);
             MilpPermissiveSchedulerComputation<storm::models::sparse::StandardRewardModel<double>> comp(*solver, mdp, goalstates, sinkstates);
             STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported");
-            comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound().threshold);
+            comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getThresholdAs<double>());
             //comp.dumpLpToFile("milpdump.lp");
             std::cout << "Found Solution: " << (comp.foundSolution() ? "yes" : "no") << std::endl;
             if(comp.foundSolution()) {
@@ -54,7 +54,7 @@ namespace storm {
             auto solver = storm::utility::solver::getSmtSolver(*expressionManager);
             SmtPermissiveSchedulerComputation<storm::models::sparse::StandardRewardModel<double>> comp(*solver, mdp, goalstates, sinkstates);
             STORM_LOG_THROW(!storm::logic::isStrict(safeProp.getComparisonType()), storm::exceptions::NotImplementedException, "Strict bounds are not supported");
-            comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getBound().threshold);
+            comp.calculatePermissiveScheduler(storm::logic::isLowerBound(safeProp.getComparisonType()), safeProp.getThresholdAs<double>());
             if(comp.foundSolution()) {
                 return boost::optional<SubMDPPermissiveScheduler<RM>>(comp.getScheduler());
             } else {