diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp index 6f565fc20..d2db73a6a 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.cpp +++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp @@ -127,9 +127,9 @@ namespace storm { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]]; identifier.name("identifier"); - quantileBoundVariable = ((qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier)[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a, qi::_1)]; - quantileBoundVariable.name("Quantile bound variable"); - quantileFormula = (qi::lit("quantile") > qi::lit("(") >> (quantileBoundVariable % qi::lit(",")) >> qi::lit(",") >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + quantileBoundVariable = (-(qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier >> qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a, qi::_1)]; + quantileBoundVariable.name("quantile bound variable"); + quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)]; quantileFormula.name("Quantile formula"); stateFormula = (orStateFormula | multiFormula | quantileFormula); @@ -424,17 +424,16 @@ namespace storm { } } - std::pair FormulaParserGrammar::createQuantileBoundVariables(storm::solver::OptimizationDirection const& dir, std::string const& variableName) { + storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName) { STORM_LOG_ASSERT(manager, "Mutable expression manager required to define quantile bound variable."); STORM_LOG_THROW(!manager->hasVariable(variableName), storm::exceptions::WrongFormatException, "Invalid quantile variable name '" << variableName << "' in property: variable already exists."); - + STORM_LOG_WARN_COND(!dir.is_initialized(), "Optimization direction '" << dir.get() << "' for quantile variable " << variableName << " is ignored. This information will be derived from the subformula of the quantile."); storm::expressions::Variable var = manager->declareRationalVariable(variableName); addIdentifierExpression(variableName, var); - std::pair result(dir, var); - return result; + return var; } - std::shared_ptr FormulaParserGrammar::createQuantileFormula(std::vector> const& boundVariables, std::shared_ptr const& subformula) { + std::shared_ptr FormulaParserGrammar::createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula) { return std::shared_ptr(new storm::logic::QuantileFormula(boundVariables, subformula)); } diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h index e582abe40..7f2bbf33c 100644 --- a/src/storm-parsers/parser/FormulaParserGrammar.h +++ b/src/storm-parsers/parser/FormulaParserGrammar.h @@ -197,7 +197,7 @@ namespace storm { qi::rule(), Skipper> longRunAverageRewardFormula; qi::rule(), Skipper> multiFormula; - qi::rule(), qi::locals, Skipper> quantileBoundVariable; + qi::rule>, Skipper> quantileBoundVariable; qi::rule(), Skipper> quantileFormula; // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). @@ -232,8 +232,8 @@ namespace storm { std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); std::shared_ptr createMultiFormula(std::vector> const& subformulas); - std::pair createQuantileBoundVariables(storm::solver::OptimizationDirection const& dir, std::string const& variableName); - std::shared_ptr createQuantileFormula(std::vector> const& boundVariables, std::shared_ptr const& subformula); + storm::expressions::Variable createQuantileBoundVariables(boost::optional const& dir, std::string const& variableName); + std::shared_ptr createQuantileFormula(std::vector const& boundVariables, std::shared_ptr const& subformula); std::set getUndefinedConstants(std::shared_ptr const& formula) const; storm::jani::Property createProperty(boost::optional const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr const& formula, std::shared_ptr const& states); diff --git a/src/storm/logic/QuantileFormula.cpp b/src/storm/logic/QuantileFormula.cpp index 322f36fdd..4e1e21aef 100644 --- a/src/storm/logic/QuantileFormula.cpp +++ b/src/storm/logic/QuantileFormula.cpp @@ -7,7 +7,7 @@ namespace storm { namespace logic { - QuantileFormula::QuantileFormula(std::vector> const& boundVariables, std::shared_ptr subformula) : boundVariables(boundVariables), subformula(subformula) { + QuantileFormula::QuantileFormula(std::vector const& boundVariables, std::shared_ptr subformula) : boundVariables(boundVariables), subformula(subformula) { STORM_LOG_THROW(!boundVariables.empty(), storm::exceptions::InvalidArgumentException, "Quantile formula without bound variables are invalid."); } @@ -45,28 +45,18 @@ namespace storm { storm::expressions::Variable const& QuantileFormula::getBoundVariable() const { STORM_LOG_THROW(boundVariables.size() == 1, storm::exceptions::InvalidArgumentException, "Requested unique bound variables. However, there are multiple bound variables defined."); - return boundVariables.front().second; + return boundVariables.front(); } storm::expressions::Variable const& QuantileFormula::getBoundVariable(uint64_t index) const { STORM_LOG_THROW(index < boundVariables.size(), storm::exceptions::InvalidArgumentException, "Requested bound variable with index" << index << ". However, there are only " << boundVariables.size() << " bound variables."); - return boundVariables[index].second; + return boundVariables[index]; } - std::vector> const& QuantileFormula::getBoundVariables() const { + std::vector const& QuantileFormula::getBoundVariables() const { return boundVariables; } - storm::solver::OptimizationDirection const& QuantileFormula::getOptimizationDirection() const { - STORM_LOG_THROW(boundVariables.size() == 1, storm::exceptions::InvalidArgumentException, "Requested unique optimization direction of the bound variables. However, there are multiple bound variables defined."); - return boundVariables.front().first; - } - - storm::solver::OptimizationDirection const& QuantileFormula::getOptimizationDirection(uint64_t index) const { - STORM_LOG_THROW(index < boundVariables.size(), storm::exceptions::InvalidArgumentException, "Requested optimization direction with index" << index << ". However, there are only " << boundVariables.size() << " bound variables."); - return boundVariables[index].first; - } - boost::any QuantileFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const { return visitor.visit(*this, data); } @@ -86,7 +76,7 @@ namespace storm { std::ostream& QuantileFormula::writeToStream(std::ostream& out) const { out << "quantile("; for (auto const& bv : boundVariables) { - out << (storm::solver::minimize(bv.first) ? "min" : "max") << " " << bv.second.getName() << ", "; + out << bv.getName() << ", "; } subformula->writeToStream(out); out << ")"; diff --git a/src/storm/logic/QuantileFormula.h b/src/storm/logic/QuantileFormula.h index 2690171a5..8765013a7 100644 --- a/src/storm/logic/QuantileFormula.h +++ b/src/storm/logic/QuantileFormula.h @@ -1,13 +1,12 @@ #pragma once #include "storm/logic/Formula.h" -#include "storm/solver/OptimizationDirection.h" namespace storm { namespace logic { class QuantileFormula : public Formula { public: - QuantileFormula(std::vector> const& boundVariables, std::shared_ptr subformula); + QuantileFormula(std::vector const& boundVariables, std::shared_ptr subformula); virtual ~QuantileFormula(); @@ -23,9 +22,7 @@ namespace storm { storm::expressions::Variable const& getBoundVariable() const; storm::expressions::Variable const& getBoundVariable(uint64_t index) const; - std::vector> const& getBoundVariables() const; - storm::solver::OptimizationDirection const& getOptimizationDirection() const; - storm::solver::OptimizationDirection const& getOptimizationDirection(uint64_t index) const; + std::vector const& getBoundVariables() const; virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override; virtual void gatherAtomicExpressionFormulas(std::vector>& atomicExpressionFormulas) const override; @@ -34,7 +31,7 @@ namespace storm { virtual std::ostream& writeToStream(std::ostream& out) const override; private: - std::vector> boundVariables; + std::vector boundVariables; std::shared_ptr subformula; }; } diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp index 7fc19c5ab..f965d9794 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp @@ -32,15 +32,14 @@ namespace storm { // Do all kinds of sanity check. std::set quantileVariables; for (auto const& quantileVariable : quantileFormula.getBoundVariables()) { - STORM_LOG_THROW(quantileVariables.count(quantileVariable.second) == 0, storm::exceptions::NotSupportedException, "Quantile formula considers the same bound variable twice."); - quantileVariables.insert(quantileVariable.second); + STORM_LOG_THROW(quantileVariables.count(quantileVariable) == 0, storm::exceptions::NotSupportedException, "Quantile formula considers the same bound variable twice."); + quantileVariables.insert(quantileVariable); } STORM_LOG_THROW(quantileFormula.getSubformula().isProbabilityOperatorFormula(), storm::exceptions::NotSupportedException, "Quantile formula needs probability operator inside. The formula " << quantileFormula << " is not supported."); auto const& probOpFormula = quantileFormula.getSubformula().asProbabilityOperatorFormula(); STORM_LOG_THROW(probOpFormula.hasBound(), storm::exceptions::InvalidOperationException, "Probability operator inside quantile formula needs to have a bound."); STORM_LOG_THROW(!model.isNondeterministicModel() || probOpFormula.hasOptimalityType(), storm::exceptions::InvalidOperationException, "Probability operator inside quantile formula needs to have an optimality type."); STORM_LOG_WARN_COND(probOpFormula.getBound().comparisonType == storm::logic::ComparisonType::Greater || probOpFormula.getBound().comparisonType == storm::logic::ComparisonType::LessEqual, "Probability operator inside quantile formula needs to have bound > or <=. The specified comparison type might lead to non-termination."); // This has to do with letting bound variables approach infinity, e.g., Pr>0.7 [F "goal"] holds iff Pr>0.7 [F<=B "goal"] holds for some B. - bool lowerBounded = storm::logic::isLowerBound(probOpFormula.getBound().comparisonType); STORM_LOG_THROW(probOpFormula.getSubformula().isBoundedUntilFormula(), storm::exceptions::NotSupportedException, "Quantile formula needs bounded until probability operator formula as subformula. The formula " << quantileFormula << " is not supported."); auto const& boundedUntilFormula = probOpFormula.getSubformula().asBoundedUntilFormula(); std::set boundVariables; @@ -65,7 +64,6 @@ namespace storm { // TODO // Multiple quantile formulas in the same file yield constants def clash - // ignore optimization direction for quantile variables // Test cases } @@ -178,19 +176,7 @@ namespace storm { } return res; } - - template - storm::solver::OptimizationDirection const& QuantileHelper::getOptimizationDirForDimension(uint64_t const& dim) const { - storm::expressions::Variable const& dimVar = getVariableForDimension(dim); - for (auto const& boundVar : quantileFormula.getBoundVariables()) { - if (boundVar.second == dimVar) { - return boundVar.first; - } - } - STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "The bound variable '" << dimVar.getName() << "' is not specified within the quantile formula '" << quantileFormula << "'."); - return quantileFormula.getOptimizationDirection(); - } - + template storm::expressions::Variable const& QuantileHelper::getVariableForDimension(uint64_t const& dim) const { auto const& boundedUntil = quantileFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula(); diff --git a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h index f9f92163c..e3bb5fd78 100644 --- a/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h +++ b/src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h @@ -30,25 +30,6 @@ namespace storm { bool computeQuantile(Environment& env, storm::storage::BitVector const& consideredDimensions, storm::logic::ProbabilityOperatorFormula const& boundedUntilOperator, storm::storage::BitVector const& lowerBoundedDimensions, CostLimitClosure& satCostLimits, CostLimitClosure& unsatCostLimits, MultiDimensionalRewardUnfolding& rewardUnfolding); - std::vector> computeTwoDimensionalQuantile(Environment& env) const; - bool exploreTwoDimensionalQuantile(Environment const& env, std::vector> const& startEpochValues, std::vector& currentEpochValues, std::vector>& resultPoints) const; - - /*! - * Computes the limit probability, where the given dimensions approach infinity and the remaining dimensions are set to zero. - */ - ValueType computeLimitValue(Environment const& env, storm::storage::BitVector const& infDimensions) const; - - /*! - * Computes the limit probability, where the given dimensions approach infinity and the remaining dimensions are set to zero. - * The computed value is compared to the probability threshold. - * In sound mode, precision is iteratively increased in case of 'inconsistent' results. - */ - bool checkLimitValue(Environment& env, storm::storage::BitVector const& infDimensions) const; - - /// Computes the quantile with respect to the given dimension. - /// boost::none is returned in case of insufficient precision. - boost::optional> computeQuantileForDimension(Environment const& env, uint64_t dim) const; - /*! * Gets the number of dimensions of the underlying boudned until formula */ @@ -61,7 +42,6 @@ namespace storm { storm::storage::BitVector getOpenDimensions() const; storm::storage::BitVector getDimensionsForVariable(storm::expressions::Variable const& var) const; - storm::solver::OptimizationDirection const& getOptimizationDirForDimension(uint64_t const& dim) const; storm::expressions::Variable const& getVariableForDimension(uint64_t const& dim) const; ModelType const& model;