From f0ae3a2dfb8671925f8c669ffbe03481930a3088 Mon Sep 17 00:00:00 2001 From: TimQu Date: Mon, 3 Apr 2017 16:46:35 +0200 Subject: [PATCH] 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 | 20 ++++-------- src/storm/logic/FormulasForwardDeclarations.h | 1 + src/storm/logic/OperatorFormula.cpp | 32 ++++++++++++++++--- src/storm/logic/OperatorFormula.h | 20 ++++++------ .../logic/VariableSubstitutionVisitor.cpp | 29 +++++++++++++++++ src/storm/logic/VariableSubstitutionVisitor.h | 8 +++++ src/storm/modelchecker/CheckTask.h | 22 +++++++------ .../abstraction/GameBasedMdpModelChecker.cpp | 14 ++++---- .../pcaa/SparsePcaaPreprocessor.cpp | 2 +- .../region/ApproximationModel.cpp | 2 +- .../modelchecker/region/SamplingModel.cpp | 2 +- .../region/SparseRegionModelChecker.cpp | 2 +- src/storm/parser/FormulaParserGrammar.cpp | 2 +- src/storm/parser/JaniParser.cpp | 8 ++--- src/storm/parser/JaniParser.h | 2 +- src/storm/solver/SolveGoal.h | 29 ++++++++--------- src/storm/storage/jani/JSONExporter.cpp | 10 +++--- 17 files changed, 126 insertions(+), 79 deletions(-) diff --git a/src/storm/logic/Bound.h b/src/storm/logic/Bound.h index 426eb7e92..21f2c7282 100644 --- a/src/storm/logic/Bound.h +++ b/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 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 - Bound convertToOtherValueType() const { - return Bound(comparisonType, storm::utility::convertNumber(threshold)); - } - ComparisonType comparisonType; - ValueType threshold; + storm::expressions::Expression threshold; - template - friend std::ostream& operator<<(std::ostream& out, Bound const& bound); + friend std::ostream& operator<<(std::ostream& out, Bound const& bound); }; - template - std::ostream& operator<<(std::ostream& out, Bound const& bound) { + inline std::ostream& operator<<(std::ostream& out, Bound const& bound) { out << bound.comparisonType << bound.threshold; return out; } } - template - using Bound = typename logic::Bound; } #endif /* STORM_LOGIC_BOUND_H_ */ diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h index fcd24d1ed..3f3f1dfaf 100644 --- a/src/storm/logic/FormulasForwardDeclarations.h +++ b/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; diff --git a/src/storm/logic/OperatorFormula.cpp b/src/storm/logic/OperatorFormula.cpp index 93b692e98..6ee6a6270 100644 --- a/src/storm/logic/OperatorFormula.cpp +++ b/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 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. } @@ -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(operatorInformation.bound.get().threshold.evaluateAsRational()); + } + + void OperatorFormula::setThreshold(storm::expressions::Expression 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/storm/logic/OperatorFormula.h b/src/storm/logic/OperatorFormula.h index b09c8cc62..502cfaec6 100644 --- a/src/storm/logic/OperatorFormula.h +++ b/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 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 { @@ -32,14 +32,12 @@ namespace storm { bool hasBound() const; ComparisonType getComparisonType() const; void setComparisonType(ComparisonType newComparisonType); - 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); + storm::expressions::Expression const& getThreshold() const; + template + 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; diff --git a/src/storm/logic/VariableSubstitutionVisitor.cpp b/src/storm/logic/VariableSubstitutionVisitor.cpp index e0fe0630d..758147c28 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.cpp +++ b/src/storm/logic/VariableSubstitutionVisitor.cpp @@ -13,6 +13,26 @@ namespace storm { boost::any result = f.accept(*this, boost::any()); return boost::any_cast>(result); } + + boost::any VariableSubstitutionVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(subformula, substituteOperatorInformation(f.getOperatorInformation()))); + } + + boost::any VariableSubstitutionVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(subformula, substituteOperatorInformation(f.getOperatorInformation()))); + } + + boost::any VariableSubstitutionVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(subformula, substituteOperatorInformation(f.getOperatorInformation()))); + } + + boost::any VariableSubstitutionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const { + std::shared_ptr subformula = boost::any_cast>(f.getSubformula().accept(*this, data)); + return std::static_pointer_cast(std::make_shared(subformula, f.getOptionalRewardModelName(), substituteOperatorInformation(f.getOperatorInformation()))); + } boost::any VariableSubstitutionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const { auto left = boost::any_cast>(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(std::make_shared(f.getExpression().substitute(substitution))); } + + OperatorInformation VariableSubstitutionVisitor::substituteOperatorInformation(OperatorInformation const& operatorInformation) const { + boost::optional bound; + if(operatorInformation.bound) { + bound = Bound(operatorInformation.bound->comparisonType, operatorInformation.bound->threshold.substitute(substitution)); + } + return OperatorInformation(operatorInformation.optimalityType, bound); + } + } } diff --git a/src/storm/logic/VariableSubstitutionVisitor.h b/src/storm/logic/VariableSubstitutionVisitor.h index 4f5c19e06..80156c064 100644 --- a/src/storm/logic/VariableSubstitutionVisitor.h +++ b/src/storm/logic/VariableSubstitutionVisitor.h @@ -16,12 +16,20 @@ namespace storm { std::shared_ptr 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 const& substitution; }; diff --git a/src/storm/modelchecker/CheckTask.h b/src/storm/modelchecker/CheckTask.h index 435a25e45..6221237ec 100644 --- a/src/storm/modelchecker/CheckTask.h +++ b/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(); + 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()) || storm::utility::isOne(probabilityOperatorFormula.template getThresholdAs())) { 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())) { 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(bound.get().threshold.evaluateAsRational()); } /*! @@ -157,14 +161,14 @@ namespace storm { /*! * Retrieves the bound (if set). */ - storm::logic::Bound const& getBound() const { + storm::logic::Bound const& getBound() const { return bound.get(); } /*! * Retrieves the bound (if set). */ - boost::optional> const& getOptionalBound() const { + boost::optional 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 const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional> const& bound, bool qualitative, bool produceSchedulers, boost::optional> const& resultHint) : formula(formula), optimizationDirection(optimizationDirection), rewardModel(rewardModel), onlyInitialStatesRelevant(onlyInitialStatesRelevant), bound(bound), qualitative(qualitative), produceSchedulers(produceSchedulers), resultHint(resultHint) { + CheckTask(std::reference_wrapper const& formula, boost::optional const& optimizationDirection, boost::optional const& rewardModel, bool onlyInitialStatesRelevant, boost::optional const& bound, bool qualitative, bool produceSchedulers, boost::optional> 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> bound; + boost::optional bound; // A flag specifying whether the property needs to be checked qualitatively, i.e. compared with bounds 0/1. bool qualitative; diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp index b1468d87a..e3d507760 100644 --- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp +++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp @@ -121,12 +121,11 @@ namespace storm { std::unique_ptr checkForResultAfterQualitativeCheck(CheckTask const& checkTask, storm::OptimizationDirection player2Direction, storm::dd::Bdd const& initialStates, storm::dd::Bdd const& prob0, storm::dd::Bdd const& prob1) { std::unique_ptr result; - boost::optional> 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::storage::sparse::state_type(0), storm::utility::one()); } @@ -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::storage::sparse::state_type(0), storm::utility::zero()); } @@ -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> 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) { diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp index 889110a56..36f4a961b 100644 --- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp +++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaPreprocessor.cpp @@ -111,7 +111,7 @@ namespace storm { bool formulaMinimizes = false; if(formula.hasBound()) { - currentObjective.threshold = storm::utility::convertNumber(formula.getBound().threshold); + currentObjective.threshold = formula.template getThresholdAs(); 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); diff --git a/src/storm/modelchecker/region/ApproximationModel.cpp b/src/storm/modelchecker/region/ApproximationModel.cpp index 8666b9d0f..23a9d44da 100644 --- a/src/storm/modelchecker/region/ApproximationModel.cpp +++ b/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::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, - formula->getBound().convertToOtherValueType(), + formula->getComparisonType(), formula->getThresholdAs(), filter ); } diff --git a/src/storm/modelchecker/region/SamplingModel.cpp b/src/storm/modelchecker/region/SamplingModel.cpp index 0aeb8d940..28949147c 100644 --- a/src/storm/modelchecker/region/SamplingModel.cpp +++ b/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::logic::isLowerBound(formula->getComparisonType()) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize, - formula->getBound().convertToOtherValueType(), + formula->getComparisonType(), formula->getThresholdAs(), filter ); } diff --git a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp index e056899bc..518ff8d4d 100644 --- a/src/storm/modelchecker/region/SparseRegionModelChecker.cpp +++ b/src/storm/modelchecker/region/SparseRegionModelChecker.cpp @@ -79,7 +79,7 @@ namespace storm { template ConstantType SparseRegionModelChecker::getSpecifiedFormulaBound() const { - return storm::utility::convertNumber(this->getSpecifiedFormula()->getThreshold()); + return this->getSpecifiedFormula()->template getThresholdAs(); } template diff --git a/src/storm/parser/FormulaParserGrammar.cpp b/src/storm/parser/FormulaParserGrammar.cpp index 70c63f22e..bee6b5117 100644 --- a/src/storm/parser/FormulaParserGrammar.cpp +++ b/src/storm/parser/FormulaParserGrammar.cpp @@ -286,7 +286,7 @@ namespace storm { storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { if (comparisonType && threshold) { storm::expressions::ExpressionEvaluator evaluator(*constManager); - return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(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); } diff --git a/src/storm/parser/JaniParser.cpp b/src/storm/parser/JaniParser.cpp index 4101359d3..adc33aa76 100644 --- a/src/storm/parser/JaniParser.cpp +++ b/src/storm/parser/JaniParser.cpp @@ -177,7 +177,7 @@ namespace storm { } - std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional> bound) { + std::shared_ptr JaniParser::parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional bound) { if (propertyStructure.is_boolean()) { return std::make_shared(propertyStructure.get()); } @@ -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()); 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(ct, storm::utility::convertNumber(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()); 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(ct, storm::utility::convertNumber(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."); diff --git a/src/storm/parser/JaniParser.h b/src/storm/parser/JaniParser.h index 2ac6c8366..be7ca4d8b 100644 --- a/src/storm/parser/JaniParser.h +++ b/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 parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional> bound = boost::none); + std::shared_ptr parseFormula(json const& propertyStructure, storm::logic::FormulaContext formulaContext, std::string const& context, boost::optional bound = boost::none); std::vector parseUnaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); std::vector parseBinaryExpressionArguments(json const& expressionStructure, std::string const& opstring, std::string const& scopeDescription, std::unordered_map> const& localVars = std::unordered_map>(), bool returnNoneOnUnknownOpString = false); diff --git a/src/storm/solver/SolveGoal.h b/src/storm/solver/SolveGoal.h index 14e47d46e..4a84898f2 100644 --- a/src/storm/solver/SolveGoal.h +++ b/src/storm/solver/SolveGoal.h @@ -60,11 +60,7 @@ namespace storm { template 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 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 const& result) const{ - for(std::size_t i : relevantValueVector){ - switch(bound.comparisonType) { + bool achieved(std::vector 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 bound; + storm::logic::ComparisonType comparisonType; + ValueType threshold; storm::storage::BitVector relevantValueVector; }; diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp index fc5346c0d..8d458f4de 100644 --- a/src/storm/storage/jani/JSONExporter.cpp +++ b/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(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(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(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";