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

WIP added grammar rules for gameFormula 

Does not compile at this stage! This commit will be squashed asap.
tempestpy_adaptions
Stefan Pranger 4 years ago
parent
0d7e763b00
commit
07d7ca9189
2 changed files with 124 additions and 110 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. 166
      src/storm-parsers/parser/FormulaParserGrammar.cpp
  2. 68
      src/storm-parsers/parser/FormulaParserGrammar.h

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

@ -3,7 +3,7 @@
namespace storm {
namespace parser {
FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), constManager(manager), manager(nullptr), expressionParser(*manager, keywords_, true, true), propertyCount(0) {
initialize();
}
@ -16,72 +16,72 @@ namespace storm {
// Register all variables so we can parse them in the expressions.
for (auto variableTypePair : *constManager) {
identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);
}
}
// Set the identifier mapping to actually generate expressions.
expressionParser.setIdentifierMapping(&identifiers_);
longRunAverageRewardFormula = (qi::lit("LRA") | qi::lit("S") | qi::lit("MP"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))];
longRunAverageRewardFormula.name("long run average reward formula");
instantaneousRewardFormula = (qi::lit("I=") > expressionParser)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)];
instantaneousRewardFormula.name("instantaneous reward formula");
cumulativeRewardFormula = (qi::lit("C") >> timeBounds)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)];
cumulativeRewardFormula.name("cumulative reward formula");
totalRewardFormula = (qi::lit("C"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTotalRewardFormula, phoenix::ref(*this))];
totalRewardFormula.name("total reward formula");
rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula | totalRewardFormula;
rewardPathFormula.name("reward path formula");
expressionFormula = expressionParser[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicExpressionFormula, phoenix::ref(*this), qi::_1)];
expressionFormula.name("expression formula");
label = qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]];
label.name("label");
labelFormula = (qi::lit("\"") >> label >> qi::lit("\""))[qi::_val = phoenix::bind(&FormulaParserGrammar::createAtomicLabelFormula, phoenix::ref(*this), qi::_1)];
labelFormula.name("label formula");
booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParserGrammar::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
booleanLiteralFormula.name("boolean literal formula");
operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator;
operatorFormula.name("operator formulas");
atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
atomicStateFormula.name("atomic state formula");
atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
atomicStateFormula.name("atomic state formula without expression");
notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1];
notStateFormula.name("negation formula");
eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
eventuallyFormula.name("eventually formula");
globallyFormula = (qi::lit("G") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createGloballyFormula, phoenix::ref(*this), qi::_1)];
globallyFormula.name("globally formula");
nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
nextFormula.name("next formula");
pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula;
pathFormulaWithoutUntil.name("path formula");
untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
untilFormula.name("until formula");
conditionalFormula = untilFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("||") >> untilFormula(storm::logic::FormulaContext::Probability))[qi::_val = phoenix::bind(&FormulaParserGrammar::createConditionalFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_r1)];
conditionalFormula.name("conditional formula");
timeBoundReference = (-qi::lit("rew") >> rewardModelName)[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Reward, qi::_1)]
| (qi::lit("steps"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Steps, boost::none)]
| (-qi::lit("time"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundReference, phoenix::ref(*this), storm::logic::TimeBoundType::Time, boost::none)];
timeBoundReference.name("time bound reference");
timeBound = ((timeBoundReference >> qi::lit("[")) > expressionParser > qi::lit(",") > expressionParser > qi::lit("]"))
[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_3, qi::_1)]
| ( timeBoundReference >> (qi::lit("<=")[qi::_a = true, qi::_b = false] | qi::lit("<")[qi::_a = true, qi::_b = true] | qi::lit(">=")[qi::_a = false, qi::_b = false] | qi::lit(">")[qi::_a = false, qi::_b = true]) >> expressionParser)
@ -89,46 +89,46 @@ namespace storm {
| ( timeBoundReference >> qi::lit("=") >> expressionParser)
[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeBoundFromInterval, phoenix::ref(*this), qi::_2, qi::_2, qi::_1)];
timeBound.name("time bound");
timeBounds = (timeBound % qi::lit(",")) | (((-qi::lit("^") >> qi::lit("{")) >> (timeBound % qi::lit(","))) >> qi::lit("}"));
timeBounds.name("time bounds");
pathFormula = conditionalFormula(qi::_r1);
pathFormula.name("path formula");
rewardMeasureType = qi::lit("[") >> rewardMeasureType_ >> qi::lit("]");
rewardMeasureType.name("reward measure type");
operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
operatorInformation.name("operator information");
longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
longRunAverageOperator.name("long-run average operator");
rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
rewardModelName.name("reward model name");
rewardOperator = (qi::lit("R") > -rewardMeasureType > -rewardModelName > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)];
rewardOperator.name("reward operator");
timeOperator = (qi::lit("T") > -rewardMeasureType > operatorInformation > qi::lit("[") > eventuallyFormula(storm::logic::FormulaContext::Time) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)];
timeOperator.name("time operator");
probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
probabilityOperator.name("probability operator");
andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
andStateFormula.name("and state formula");
orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
orStateFormula.name("or state formula");
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");
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::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)];
@ -141,17 +141,31 @@ namespace storm {
gameFormula.name("game formula");
stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
coalitionOperator = (qi::lit("<<")
> *( (identifier[phoenix::push_back(qi::_a, qi::_1)]
| qi::int_[phoenix::push_back(qi::_b, qi::_1)]) % ','
)
> qi::lit(">>"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createCoalition, phoenix::ref(*this), qi::_a, qi::_b)];
coalitionOperator.name("coalition operator");
// only LRA for now, need to adapt this (beware of cyclic gameFormula pass!)
gameFormula = (coalitionOperator > longRunAverageOperator)[qi::_val = phoenix::bind(&FormulaParserGrammar::createGameFormula, phoenix::ref(*this), storm::logic::Coalition({}, {1}), qi::_1)];
gameFormula.name("game formula");
stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
>>>>>>> f106b8332... WIP added grammar rules for gameFormula
stateFormula.name("state formula");
formulaName = qi::lit("\"") >> identifier >> qi::lit("\"") >> qi::lit(":");
formulaName.name("formula name");
constantDefinition = (qi::lit("const") > -(qi::lit("int")[qi::_a = ConstantDataType::Integer] | qi::lit("bool")[qi::_a = ConstantDataType::Bool] | qi::lit("double")[qi::_a = ConstantDataType::Rational]) >> identifier >> -(qi::lit("=") > expressionParser))[phoenix::bind(&FormulaParserGrammar::addConstant, phoenix::ref(*this), qi::_1, qi::_a, qi::_2)];
constantDefinition.name("constant definition");
#pragma clang diagnostic push
#pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)];
filterProperty.name("filter property");
@ -162,7 +176,7 @@ namespace storm {
| qi::eps)
% +(qi::char_("\n;")) >> qi::skip(storm::spirit_encoding::space_type() | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;
start.name("start");
// Enable the following lines to print debug output for most the rules.
// debug(start);
// debug(constantDefinition);
@ -188,7 +202,7 @@ namespace storm {
// debug(totalRewardFormula);
// debug(instantaneousRewardFormula);
// debug(multiFormula);
// Enable error reporting.
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@ -216,16 +230,16 @@ namespace storm {
qi::on_error<qi::fail>(instantaneousRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4));
}
void FormulaParserGrammar::addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression) {
this->identifiers_.add(identifier, expression);
}
void FormulaParserGrammar::addConstant(std::string const& name, ConstantDataType type, boost::optional<storm::expressions::Expression> const& expression) {
STORM_LOG_ASSERT(manager, "Mutable expression manager required to define new constants.");
storm::expressions::Variable newVariable;
STORM_LOG_THROW(!manager->hasVariable(name), storm::exceptions::WrongFormatException, "Invalid constant definition '" << name << "' in property: variable already exists.");
if (type == ConstantDataType::Bool) {
newVariable = manager->declareBooleanVariable(name);
} else if (type == ConstantDataType::Integer) {
@ -233,7 +247,7 @@ namespace storm {
} else {
newVariable = manager->declareRationalVariable(name);
}
if (expression) {
addIdentifierExpression(name, expression.get());
} else {
@ -241,11 +255,11 @@ namespace storm {
addIdentifierExpression(name, newVariable);
}
}
bool FormulaParserGrammar::areConstantDefinitionsAllowed() const {
return static_cast<bool>(manager);
}
std::shared_ptr<storm::logic::TimeBoundReference> FormulaParserGrammar::createTimeBoundReference(storm::logic::TimeBoundType const& type, boost::optional<std::string> const& rewardModelName) const {
if (type == storm::logic::TimeBoundType::Reward) {
STORM_LOG_THROW(rewardModelName, storm::exceptions::WrongFormatException, "Reward bound does not specify a reward model name.");
@ -254,7 +268,7 @@ namespace storm {
return std::make_shared<storm::logic::TimeBoundReference>(type);
}
}
std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>> FormulaParserGrammar::createTimeBoundFromInterval(storm::expressions::Expression const& lowerBound, storm::expressions::Expression const& upperBound, std::shared_ptr<storm::logic::TimeBoundReference> const& timeBoundReference) const {
// As soon as it somehow does not break everything anymore, I will change return types here.
@ -262,7 +276,7 @@ namespace storm {
storm::logic::TimeBound upper(false, upperBound);
return std::make_tuple(lower, upper, timeBoundReference);
}
std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>> FormulaParserGrammar::createTimeBoundFromSingleBound(storm::expressions::Expression const& bound, bool upperBound, bool strict, std::shared_ptr<storm::logic::TimeBoundReference> const& timeBoundReference) const {
// As soon as it somehow does not break everything anymore, I will change return types here.
if (upperBound) {
@ -271,11 +285,11 @@ namespace storm {
return std::make_tuple(storm::logic::TimeBound(strict, bound), boost::none, timeBoundReference);
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createInstantaneousRewardFormula(storm::expressions::Expression const& timeBound) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::InstantaneousRewardFormula(timeBound));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createCumulativeRewardFormula(std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>> const& timeBounds) const {
std::vector<storm::logic::TimeBound> bounds;
std::vector<storm::logic::TimeBoundReference> timeBoundReferences;
@ -287,28 +301,28 @@ namespace storm {
}
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::CumulativeRewardFormula(bounds, timeBoundReferences));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTotalRewardFormula() const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TotalRewardFormula());
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageRewardFormula() const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageRewardFormula());
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicExpressionFormula(storm::expressions::Expression const& expression) const {
STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::WrongFormatException, "Expected expression of boolean type.");
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicExpressionFormula(expression));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BooleanLiteralFormula(literal));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::AtomicLabelFormula(label));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createEventuallyFormula(boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, storm::logic::FormulaContext context, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
if (timeBounds && !timeBounds.get().empty()) {
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
@ -323,15 +337,15 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::EventuallyFormula(subformula, context));
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createGloballyFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::GloballyFormula(subformula));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createNextFormula(std::shared_ptr<storm::logic::Formula const> const& subformula) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::NextFormula(subformula));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUntilFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, boost::optional<std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>> const& timeBounds, std::shared_ptr<storm::logic::Formula const> const& rightSubformula) {
if (timeBounds && !timeBounds.get().empty()) {
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
@ -346,11 +360,11 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UntilFormula(leftSubformula, rightSubformula));
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createConditionalFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::FormulaContext context) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context));
}
storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional<storm::OptimizationDirection> const& optimizationDirection, boost::optional<storm::logic::ComparisonType> const& comparisonType, boost::optional<storm::expressions::Expression> const& threshold) const {
if (comparisonType && threshold) {
storm::expressions::ExpressionEvaluator<storm::RationalNumber> evaluator(*constManager);
@ -359,11 +373,11 @@ namespace storm {
return storm::logic::OperatorInformation(optimizationDirection, boost::none);
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createRewardOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, boost::optional<std::string> const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
if (rewardMeasureType) {
@ -371,7 +385,7 @@ namespace storm {
}
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const {
storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation;
if (rewardMeasureType) {
@ -379,15 +393,15 @@ namespace storm {
}
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula));
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType) {
if (operatorType) {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula));
@ -395,7 +409,7 @@ namespace storm {
return subformula;
}
}
std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty();
for (auto const& subformula : subformulas) {
@ -404,7 +418,7 @@ namespace storm {
break;
}
}
if (isMultiDimensionalBoundedUntilFormula) {
std::vector<std::shared_ptr<storm::logic::Formula const>> leftSubformulas, rightSubformulas;
std::vector<boost::optional<storm::logic::TimeBound>> lowerBounds, upperBounds;
@ -431,7 +445,7 @@ namespace storm {
return std::shared_ptr<storm::logic::Formula const>(new storm::logic::MultiObjectiveFormula(subformulas));
}
}
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::expressions::Variable var;
@ -450,17 +464,17 @@ namespace storm {
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));
}
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();
std::set_intersection(usedVariables.begin(), usedVariables.end(), undefinedConstants.begin(), undefinedConstants.end(), std::inserter(result, result.begin()));
return result;
}
storm::jani::Property FormulaParserGrammar::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) {
storm::jani::FilterExpression filterExpression(formula, filterType, states);
++propertyCount;
if (propertyName) {
return storm::jani::Property(propertyName.get(), filterExpression, this->getUndefinedConstants(formula));
@ -468,7 +482,7 @@ namespace storm {
return storm::jani::Property(std::to_string(propertyCount - 1), filterExpression, this->getUndefinedConstants(formula));
}
}
storm::jani::Property FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula) {
++propertyCount;
if (propertyName) {

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

@ -19,17 +19,17 @@ namespace storm {
namespace logic {
class Formula;
}
namespace parser {
class FormulaParserGrammar : public qi::grammar<Iterator, std::vector<storm::jani::Property>(), Skipper> {
public:
FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager);
FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager> const& manager);
FormulaParserGrammar(FormulaParserGrammar const& other) = delete;
FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = delete;
/*!
* Adds an identifier and the expression it is supposed to be replaced with. This can, for example be used
* to substitute special identifiers in the formula by expressions.
@ -38,10 +38,10 @@ namespace storm {
* @param expression The expression it is to be substituted with.
*/
void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression);
private:
void initialize();
struct keywordsStruct : qi::symbols<char, uint_fast64_t> {
keywordsStruct() {
add
@ -56,10 +56,10 @@ namespace storm {
("quantile", 9);
}
};
// A parser used for recognizing the keywords.
keywordsStruct keywords_;
struct relationalOperatorStruct : qi::symbols<char, storm::logic::ComparisonType> {
relationalOperatorStruct() {
add
@ -69,10 +69,10 @@ namespace storm {
("<", storm::logic::ComparisonType::Less);
}
};
// A parser used for recognizing the operators at the "relational" precedence level.
relationalOperatorStruct relationalOperator_;
struct binaryBooleanOperatorStruct : qi::symbols<char, storm::logic::BinaryBooleanStateFormula::OperatorType> {
binaryBooleanOperatorStruct() {
add
@ -80,20 +80,20 @@ namespace storm {
("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or);
}
};
// A parser used for recognizing the operators at the "binary" precedence level.
binaryBooleanOperatorStruct binaryBooleanOperator_;
struct unaryBooleanOperatorStruct : qi::symbols<char, storm::logic::UnaryBooleanStateFormula::OperatorType> {
unaryBooleanOperatorStruct() {
add
("!", storm::logic::UnaryBooleanStateFormula::OperatorType::Not);
}
};
// A parser used for recognizing the operators at the "unary" precedence level.
unaryBooleanOperatorStruct unaryBooleanOperator_;
struct optimalityOperatorStruct : qi::symbols<char, storm::OptimizationDirection> {
optimalityOperatorStruct() {
add
@ -101,10 +101,10 @@ namespace storm {
("max", storm::OptimizationDirection::Maximize);
}
};
// A parser used for recognizing the optimality operators.
optimalityOperatorStruct optimalityOperator_;
struct rewardMeasureTypeStruct : qi::symbols<char, storm::logic::RewardMeasureType> {
rewardMeasureTypeStruct() {
add
@ -112,10 +112,10 @@ namespace storm {
("var", storm::logic::RewardMeasureType::Variance);
}
};
// A parser used for recognizing the reward measure types.
rewardMeasureTypeStruct rewardMeasureType_;
struct filterTypeStruct : qi::symbols<char, storm::modelchecker::FilterType> {
filterTypeStruct() {
add
@ -134,28 +134,28 @@ namespace storm {
// A parser used for recognizing the filter type.
filterTypeStruct filterType_;
// The manager used to parse expressions.
std::shared_ptr<storm::expressions::ExpressionManager const> constManager;
std::shared_ptr<storm::expressions::ExpressionManager> manager;
// Parser and manager used for recognizing expressions.
storm::parser::ExpressionParser expressionParser;
// A symbol table that is a mapping from identifiers that can be used in expressions to the expressions
// they are to be replaced with.
qi::symbols<char, storm::expressions::Expression> identifiers_;
qi::rule<Iterator, std::vector<storm::jani::Property>(), Skipper> start;
enum class ConstantDataType {
Bool, Integer, Rational
};
qi::rule<Iterator, qi::unused_type(), qi::locals<ConstantDataType>, Skipper> constantDefinition;
qi::rule<Iterator, std::string(), Skipper> identifier;
qi::rule<Iterator, std::string(), Skipper> formulaName;
qi::rule<Iterator, storm::logic::OperatorInformation(), qi::locals<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<storm::expressions::Expression>>, Skipper> operatorInformation;
qi::rule<Iterator, storm::logic::RewardMeasureType(), Skipper> rewardMeasureType;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> probabilityOperator;
@ -176,30 +176,30 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> operatorFormula;
qi::rule<Iterator, std::string(), Skipper> label;
qi::rule<Iterator, std::string(), Skipper> rewardModelName;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> andStateFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> orStateFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> notStateFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> labelFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> expressionFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> conditionalFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> eventuallyFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> nextFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> globallyFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> untilFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::TimeBoundReference>, Skipper> timeBoundReference;
qi::rule<Iterator, std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>(), qi::locals<bool, bool>, Skipper> timeBound;
qi::rule<Iterator, std::vector<std::tuple<boost::optional<storm::logic::TimeBound>, boost::optional<storm::logic::TimeBound>, std::shared_ptr<storm::logic::TimeBoundReference>>>(), qi::locals<bool, bool>, Skipper> timeBounds;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> rewardPathFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> cumulativeRewardFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> totalRewardFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> instantaneousRewardFormula;
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, storm::expressions::Variable(), qi::locals<boost::optional<storm::solver::OptimizationDirection>>, Skipper> quantileBoundVariable;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> quantileFormula;
@ -242,16 +242,16 @@ namespace storm {
std::shared_ptr<storm::logic::Formula const> createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
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);
storm::jani::Property createPropertyWithDefaultFilterTypeAndStates(boost::optional<std::string> const& propertyName, std::shared_ptr<storm::logic::Formula const> const& formula);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
uint64_t propertyCount;
std::set<storm::expressions::Variable> undefinedConstants;
std::set<storm::expressions::Variable> quantileFormulaVariables;
};

Write Preview
Loading…
Cancel
Save