sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

QuantileFormulas: ignore optimization direction (min/max) for quantile variables.

tempestpy_adaptions
Tim Quatmann 6 years ago
parent
38121c28cb
commit
8a72aee764
6 changed files with 21 additions and 69 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 15
      src/storm-parsers/parser/FormulaParserGrammar.cpp
  2. 6
      src/storm-parsers/parser/FormulaParserGrammar.h
  3. 20
      src/storm/logic/QuantileFormula.cpp
  4. 9
      src/storm/logic/QuantileFormula.h
  5. 20
      src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp
  6. 20
      src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h

15
src/storm-parsers/parser/FormulaParserGrammar.cpp
View File

@ -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<storm::solver::OptimizationDirection, storm::expressions::Variable> FormulaParserGrammar::createQuantileBoundVariables(storm::solver::OptimizationDirection const& dir, std::string const& variableName) {
storm::expressions::Variable FormulaParserGrammar::createQuantileBoundVariables(boost::optional<storm::solver::OptimizationDirection> 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<storm::solver::OptimizationDirection, storm::expressions::Variable> result(dir, var);
return result;
return var;
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createQuantileFormula(std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& boundVariables, std::shared_ptr<storm::logic::Formula const> const& subformula) {
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createQuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<storm::logic::Formula const> const& subformula) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::QuantileFormula(boundVariables, subformula));
}

6
src/storm-parsers/parser/FormulaParserGrammar.h
View File

@ -197,7 +197,7 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> longRunAverageRewardFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> multiFormula;
qi::rule<Iterator, std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>(), qi::locals<storm::solver::OptimizationDirection>, Skipper> quantileBoundVariable;
qi::rule<Iterator, storm::expressions::Variable(), qi::locals<boost::optional<storm::solver::OptimizationDirection>>, Skipper> quantileBoundVariable;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), 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<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
std::shared_ptr<storm::logic::Formula const> createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable> createQuantileBoundVariables(storm::solver::OptimizationDirection const& dir, std::string const& variableName);
std::shared_ptr<storm::logic::Formula const> createQuantileFormula(std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& boundVariables, std::shared_ptr<storm::logic::Formula const> const& subformula);
storm::expressions::Variable createQuantileBoundVariables(boost::optional<storm::solver::OptimizationDirection> const& dir, std::string const& variableName);
std::shared_ptr<storm::logic::Formula const> createQuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<storm::logic::Formula const> const& subformula);
std::set<storm::expressions::Variable> getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const;
storm::jani::Property createProperty(boost::optional<std::string> const& propertyName, storm::modelchecker::FilterType const& filterType, std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states);

20
src/storm/logic/QuantileFormula.cpp
View File

@ -7,7 +7,7 @@
namespace storm {
namespace logic {
QuantileFormula::QuantileFormula(std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& boundVariables, std::shared_ptr<Formula const> subformula) : boundVariables(boundVariables), subformula(subformula) {
QuantileFormula::QuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<Formula const> 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<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& QuantileFormula::getBoundVariables() const {
std::vector<storm::expressions::Variable> 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 << ")";

9
src/storm/logic/QuantileFormula.h
View File

@ -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<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& boundVariables, std::shared_ptr<Formula const> subformula);
QuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<Formula const> 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<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> const& getBoundVariables() const;
storm::solver::OptimizationDirection const& getOptimizationDirection() const;
storm::solver::OptimizationDirection const& getOptimizationDirection(uint64_t index) const;
std::vector<storm::expressions::Variable> const& getBoundVariables() const;
virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
@ -34,7 +31,7 @@ namespace storm {
virtual std::ostream& writeToStream(std::ostream& out) const override;
private:
std::vector<std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable>> boundVariables;
std::vector<storm::expressions::Variable> boundVariables;
std::shared_ptr<Formula const> subformula;
};
}

20
src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.cpp
View File

@ -32,15 +32,14 @@ namespace storm {
// Do all kinds of sanity check.
std::set<storm::expressions::Variable> 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<storm::expressions::Variable> 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<typename ModelType>
storm::solver::OptimizationDirection const& QuantileHelper<ModelType>::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<typename ModelType>
storm::expressions::Variable const& QuantileHelper<ModelType>::getVariableForDimension(uint64_t const& dim) const {
auto const& boundedUntil = quantileFormula.getSubformula().asProbabilityOperatorFormula().getSubformula().asBoundedUntilFormula();

20
src/storm/modelchecker/prctl/helper/rewardbounded/QuantileHelper.h
View File

@ -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<ValueType, true>& rewardUnfolding);
std::vector<std::vector<ValueType>> computeTwoDimensionalQuantile(Environment& env) const;
bool exploreTwoDimensionalQuantile(Environment const& env, std::vector<std::pair<int64_t, typename ModelType::ValueType>> const& startEpochValues, std::vector<int64_t>& currentEpochValues, std::vector<std::vector<ValueType>>& 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<std::pair<uint64_t, typename ModelType::ValueType>> 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;

Write Preview
Loading…
Cancel
Save