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

QuantileFormulas: A boost::spiritual abyss.

tempestpy_adaptions
TimQu 6 years ago
parent
7e66787c9c
commit
9e282c8bb2
2 changed files with 29 additions and 5 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. 25
      src/storm-parsers/parser/FormulaParserGrammar.cpp
  2. 7
      src/storm-parsers/parser/FormulaParserGrammar.h

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

@ -124,12 +124,17 @@ namespace storm {
multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)];
multiFormula.name("Multi formula");
stateFormula = (orStateFormula | multiFormula);
stateFormula.name("state formula");
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)];
quantileFormula.name("Quantile formula");
stateFormula = (orStateFormula | multiFormula | quantileFormula);
stateFormula.name("state formula");
formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
formulaName.name("formula name");
@ -419,6 +424,20 @@ namespace storm {
}
}
std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable> FormulaParserGrammar::createQuantileBoundVariables(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::expressions::Variable var = manager->declareRationalVariable(variableName);
addIdentifierExpression(variableName, var);
std::pair<storm::solver::OptimizationDirection, storm::expressions::Variable> result(dir, var);
return result;
}
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) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::QuantileFormula(boundVariables, subformula));
}
std::set<storm::expressions::Variable> FormulaParserGrammar::getUndefinedConstants(std::shared_ptr<storm::logic::Formula const> const& formula) const {
std::set<storm::expressions::Variable> result;
std::set<storm::expressions::Variable> usedVariables = formula->getUsedVariables();

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

@ -50,7 +50,8 @@ namespace storm {
("F", 5)
("G", 6)
("X", 7)
("multi", 8);
("multi", 8)
("quantile", 9);
}
};
@ -196,6 +197,8 @@ 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, std::shared_ptr<storm::logic::Formula const>(), Skipper> quantileFormula;
// Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser).
boost::spirit::qi::real_parser<double, boost::spirit::qi::strict_real_policies<double>> strict_double;
@ -229,6 +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);
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);

Write Preview
Loading…
Cancel
Save