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

modified parser to accept more legal formulas 

Former-commit-id: acf383c4a3
tempestpy_adaptions
dehnert 10 years ago
parent
ce58a5fa6f
commit
1b9860ece0
4 changed files with 37 additions and 8 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 35
      src/parser/ExpressionParser.cpp
  2. 2
      src/parser/ExpressionParser.h
  3. 7
      src/parser/FormulaParser.cpp
  4. 1
      src/parser/FormulaParser.h

35
src/parser/ExpressionParser.cpp
View File

@ -23,7 +23,7 @@ namespace storm {
} }
minMaxExpression.name("min/max expression"); minMaxExpression.name("min/max expression");
identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, phoenix::ref(qi::_pass))];
identifierExpression.name("identifier expression"); identifierExpression.name("identifier expression");
literalExpression = trueFalse_[qi::_val = qi::_1] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)]; literalExpression = trueFalse_[qi::_val = qi::_1] | strict_double[qi::_val = phoenix::bind(&ExpressionParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)];
@ -53,7 +53,7 @@ namespace storm {
plusExpression.name("plus expression"); plusExpression.name("plus expression");
if (allowBacktracking) { if (allowBacktracking) {
relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
relativeExpression = plusExpression[qi::_val = qi::_1] >> -(relationalOperator_ >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
} else { } else {
relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
} }
@ -70,7 +70,7 @@ namespace storm {
andExpression.name("and expression"); andExpression.name("and expression");
if (allowBacktracking) { if (allowBacktracking) {
orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ >> andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
orExpression = andExpression[qi::_val = qi::_1] >> *(orOperator_ >> andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
} else { } else {
orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)]; orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
} }
@ -82,6 +82,24 @@ namespace storm {
expression %= iteExpression; expression %= iteExpression;
expression.name("expression"); expression.name("expression");
/*!
* Enable this for debugging purposes.
debug(expression);
debug(iteExpression);
debug(orExpression);
debug(andExpression);
debug(equalityExpression);
debug(relativeExpression);
debug(plusExpression);
debug(multiplicationExpression);
debug(powerExpression);
debug(unaryExpression);
debug(atomicExpression);
debug(literalExpression);
debug(identifierExpression);
*/
// Enable error reporting. // Enable error reporting.
qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
@ -304,11 +322,18 @@ namespace storm {
return manager.boolean(false); return manager.boolean(false);
} }
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const {
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const {
if (this->createExpressions) { if (this->createExpressions) {
STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping."); STORM_LOG_THROW(this->identifiers_ != nullptr, storm::exceptions::WrongFormatException, "Unable to substitute identifier expressions without given mapping.");
storm::expressions::Expression const* expression = this->identifiers_->find(identifier); storm::expressions::Expression const* expression = this->identifiers_->find(identifier);
STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
if (expression == nullptr) {
if (allowBacktracking) {
pass = false;
return manager.boolean(false);
} else {
STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
}
}
return *expression; return *expression;
} else { } else {
return manager.boolean(false); return manager.boolean(false);

2
src/parser/ExpressionParser.h
View File

@ -223,7 +223,7 @@ namespace storm {
storm::expressions::Expression createIntegerLiteralExpression(int value) const; storm::expressions::Expression createIntegerLiteralExpression(int value) const;
storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const; storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const;
storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const; storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const;
storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const;
storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const;
bool isValidIdentifier(std::string const& identifier); bool isValidIdentifier(std::string const& identifier);

7
src/parser/FormulaParser.cpp
View File

@ -38,7 +38,10 @@ namespace storm {
booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)]; booleanLiteralFormula = (qi::lit("true")[qi::_a = true] | qi::lit("false")[qi::_a = false])[qi::_val = phoenix::bind(&FormulaParser::createBooleanLiteralFormula, phoenix::ref(*this), qi::_a)];
booleanLiteralFormula.name("boolean literal formula"); booleanLiteralFormula.name("boolean literal formula");
atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")"));
operatorFormula = probabilityOperator | rewardOperator | steadyStateOperator;
operatorFormula.name("operator formulas");
atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
atomicStateFormula.name("atomic state formula"); atomicStateFormula.name("atomic state formula");
notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)];
@ -89,7 +92,7 @@ namespace storm {
orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)]; orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParser::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
orStateFormula.name("or state formula"); orStateFormula.name("or state formula");
stateFormula = (probabilityOperator | rewardOperator | steadyStateOperator | orStateFormula);
stateFormula = (orStateFormula);
stateFormula.name("state formula"); stateFormula.name("state formula");
start = qi::eps > stateFormula >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi; start = qi::eps > stateFormula >> qi::skip(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - (qi::eol | qi::eoi)))[qi::eps] >> qi::eoi;

1
src/parser/FormulaParser.h
View File

@ -132,6 +132,7 @@ namespace storm {
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormulaWithoutUntil; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> pathFormulaWithoutUntil;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simplePathFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> simplePathFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> atomicStateFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> atomicStateFormula;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> operatorFormula;
qi::rule<Iterator, std::string(), Skipper> label; qi::rule<Iterator, std::string(), Skipper> label;
qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> andStateFormula; qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> andStateFormula;

Write Preview
Loading…
Cancel
Save