From cf583ec9dd26e53b9e46bdfb9633ba8720fb5e1f Mon Sep 17 00:00:00 2001 From: sjunges Date: Wed, 3 Aug 2016 17:02:36 +0200 Subject: [PATCH] formulae with rational number bounds Former-commit-id: 17755ccf843776648dab1b4deecfdf19d327f4d6 --- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 2 +- src/logic/Bound.h | 6 ++++++ src/logic/OperatorFormula.cpp | 10 +++++----- src/logic/OperatorFormula.h | 19 +++++++++++++------ src/modelchecker/AbstractModelChecker.cpp | 2 +- src/modelchecker/CheckTask.h | 6 +++--- src/parser/FormulaParser.cpp | 2 +- src/permissivesched/PermissiveSchedulers.cpp | 4 ++-- 9 files changed, 33 insertions(+), 20 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 7597d488a..c9cf5d532 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/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(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 255ad2a19..44ebb71ec 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/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(); storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; diff --git a/src/logic/Bound.h b/src/logic/Bound.h index d0a98853c..e56a2c04f 100644 --- a/src/logic/Bound.h +++ b/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 + Bound convertToOtherValueType() const { + return Bound(comparisonType, storm::utility::convertNumber(threshold)); + } ComparisonType comparisonType; ValueType threshold; diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp index 474a9608b..066dc6fa6 100644 --- a/src/logic/OperatorFormula.cpp +++ b/src/logic/OperatorFormula.cpp @@ -2,7 +2,7 @@ namespace storm { namespace logic { - OperatorInformation::OperatorInformation(boost::optional const& optimizationDirection, boost::optional> const& bound) : optimalityType(optimizationDirection), bound(bound) { + OperatorInformation::OperatorInformation(boost::optional const& optimizationDirection, boost::optional> 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 const& OperatorFormula::getBound() const { + Bound const& OperatorFormula::getBound() const { return operatorInformation.bound.get(); } - void OperatorFormula::setBound(Bound const& newBound) { + void OperatorFormula::setBound(Bound const& newBound) { operatorInformation.bound = newBound; } diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h index ee7f7a87a..04324e2d9 100644 --- a/src/logic/OperatorFormula.h +++ b/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 const& optimizationDirection = boost::none, boost::optional> const& bound = boost::none); + OperatorInformation(boost::optional const& optimizationDirection = boost::none, boost::optional> const& bound = boost::none); boost::optional optimalityType; - boost::optional> bound; + boost::optional> 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 const& getBound() const; - void setBound(Bound const& newBound); + RationalNumber const& getThreshold() const; + template + ValueType getThresholdAs() const { + return storm::utility::convertNumber(this->getThreshold()); + } + void setThreshold(RationalNumber const& newThreshold); + Bound const& getBound() const; + void setBound(Bound const& newBound); // Optimality-type-related accessors. bool hasOptimalityType() const; diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp index 4fd86a13e..1672e51a4 100644 --- a/src/modelchecker/AbstractModelChecker.cpp +++ b/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()); } else { return result; } diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h index 3d45dd5d4..5cf52fdcd 100644 --- a/src/modelchecker/CheckTask.h +++ b/src/modelchecker/CheckTask.h @@ -45,7 +45,7 @@ namespace storm { if (operatorFormula.hasBound()) { if (onlyInitialStatesRelevant) { - this->bound = operatorFormula.getBound(); + this->bound = operatorFormula.getBound().convertToOtherValueType(); } if (!optimizationDirection) { @@ -58,7 +58,7 @@ namespace storm { storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula(); if (probabilityOperatorFormula.hasBound()) { - if (probabilityOperatorFormula.getThreshold() == storm::utility::zero() || probabilityOperatorFormula.getThreshold() == storm::utility::one()) { + 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()) { + if (storm::utility::isZero(rewardOperatorFormula.getThreshold())) { this->qualitative = true; } } diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 53006e750..c709b061a 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -478,7 +478,7 @@ namespace storm { storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { - return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), threshold.get())); + return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), storm::utility::convertNumber(threshold.get()))); } else { return storm::logic::OperatorInformation(optimizationDirection, boost::none); } diff --git a/src/permissivesched/PermissiveSchedulers.cpp b/src/permissivesched/PermissiveSchedulers.cpp index 21aa9227c..816c92d55 100644 --- a/src/permissivesched/PermissiveSchedulers.cpp +++ b/src/permissivesched/PermissiveSchedulers.cpp @@ -26,7 +26,7 @@ namespace storm { auto solver = storm::utility::solver::getLpSolver("Gurobi", storm::solver::LpSolverTypeSelection::Gurobi); MilpPermissiveSchedulerComputation> 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()); //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> 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()); if(comp.foundSolution()) { return boost::optional>(comp.getScheduler()); } else {