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

Started separating expression parsing from PRISM model parsing. 

Former-commit-id: 84d1354f97
tempestpy_adaptions
dehnert 11 years ago
parent
28eed65a0d
commit
478f5ee38c
5 changed files with 549 additions and 445 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. 382
      src/parser/ExpressionParser.cpp
  2. 126
      src/parser/ExpressionParser.h
  3. 383
      src/parser/PrismParser.cpp
  4. 82
      src/parser/PrismParser.h
  5. 21
      src/parser/SpiritParserDefinitions.h

382
src/parser/ExpressionParser.cpp
View File

@ -0,0 +1,382 @@
#include "src/parser/ExpressionParser.h"
#include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidTypeException.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
namespace parser {
ExpressionParser::ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createFloorExpression, phoenix::ref(*this), qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createCeilExpression, phoenix::ref(*this), qi::_1)]];
floorCeilExpression.name("floor/ceil expression");
minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMinimumExpression, phoenix::ref(*this), qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMaximumExpression, phoenix::ref(*this), qi::_1, qi::_2)]];
minMaxExpression.name("min/max expression");
identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
identifierExpression.name("identifier expression");
literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&ExpressionParser::createTrueExpression, phoenix::ref(*this))] | qi::lit("false")[qi::_val = phoenix::bind(&ExpressionParser::createFalseExpression, phoenix::ref(*this))] | 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.name("literal expression");
atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression;
atomicExpression.name("atomic expression");
unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_1)];
unaryExpression.name("unary expression");
multiplicationExpression = unaryExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> unaryExpression[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createDivExpression, phoenix::ref(*this), qi::_val, qi::_1)]]);
multiplicationExpression.name("multiplication expression");
plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]];
plusExpression.name("plus expression");
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
relativeExpression.name("relative expression");
equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&ExpressionParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ];
equalityExpression.name("equality expression");
andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)];
andExpression.name("and expression");
orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&ExpressionParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
orExpression.name("or expression");
iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
iteExpression.name("if-then-else expression");
expression %= iteExpression;
expression.name("expression");
// Enable error reporting.
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>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
}
void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {
this->createExpressions = true;
this->identifiers_ = identifiers_;
}
void ExpressionParser::unsetIdentifierMapping() {
this->createExpressions = false;
}
void ExpressionParser::setAcceptDoubleLiterals(bool flag) {
this->acceptDoubleLiterals = flag;
}
storm::expressions::Expression ExpressionParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const {
if (this->createExpressions) {
try {
return e1.ite(e2, e3);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1.implies(e2);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 || e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try{
return e1 && e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 > e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 >= e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 < e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 <= e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1.iff(e2);
} else {
return e1 == e2;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1 ^ e2;
} else {
return e1 != e2;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 + e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 - e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 * e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return e1 / e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createNotExpression(storm::expressions::Expression e1) const {
if (this->createExpressions) {
try {
return !e1;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createMinusExpression(storm::expressions::Expression e1) const {
if (this->createExpressions) {
try {
return -e1;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createTrueExpression() const {
if (this->createExpressions) {
return storm::expressions::Expression::createFalse();
} else {
return storm::expressions::Expression::createTrue();
}
}
storm::expressions::Expression ExpressionParser::createFalseExpression() const {
return storm::expressions::Expression::createFalse();
}
storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const {
// If we are not supposed to accept double expressions, we reject it by setting pass to false.
if (!this->acceptDoubleLiterals) {
pass = false;
}
if (this->createExpressions) {
return storm::expressions::Expression::createDoubleLiteral(value);
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const {
if (this->createExpressions) {
return storm::expressions::Expression::createFalse();
} else {
return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value));
}
}
storm::expressions::Expression ExpressionParser::createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return storm::expressions::Expression::minimum(e1, e2);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (this->createExpressions) {
try {
return storm::expressions::Expression::maximum(e1, e2);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createFloorExpression(storm::expressions::Expression e1) const {
if (this->createExpressions) {
try {
return e1.floor();
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::createCeilExpression(storm::expressions::Expression e1) const {
if (this->createExpressions) {
try {
return e1.ceil();
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what() << ".");
}
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const {
if (this->createExpressions) {
return storm::expressions::Expression::createFalse();
} else {
storm::expressions::Expression const* expression = this->identifiers_->find(identifier);
LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
return *expression;
}
}
bool ExpressionParser::isValidIdentifier(std::string const& identifier) {
if (this->invalidIdentifiers_.find(identifier) != nullptr) {
return false;
}
return true;
}
}
}

126
src/parser/ExpressionParser.h
View File

@ -0,0 +1,126 @@
#ifndef STORM_PARSER_EXPRESSIONPARSER_H_
#define STORM_PARSER_EXPRESSIONPARSER_H_
#include "src/parser/SpiritParserDefinitions.h"
#include "src/storage/expressions/Expression.h"
#include "src/exceptions/ExceptionMacros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm {
namespace parser {
class ExpressionParser : public qi::grammar<Iterator, storm::expressions::Expression(), Skipper> {
public:
/*!
* Creates an expression parser. Initially the parser is set to a mode in which it will not generate the
* actual expressions but only perform a syntax check and return the expression "false". To make the parser
* generate the actual expressions, a mapping of valid identifiers to their expressions need to be provided
* later.
*
* @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected.
*/
ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
/*!
* Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to
* expressions will be substituted wherever the key value appears in the parsed expression. After setting
* this, the parser will generate expressions.
*
* @param identifiers A pointer to a mapping from identifiers to expressions.
*/
void setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_);
/*!
* Unsets a previously set identifier mapping. This will make the parser not generate expressions any more
* but merely check for syntactic correctness of an expression.
*/
void unsetIdentifierMapping();
/*!
* Sets whether double literals are to be accepted or not.
*
* @param flag If set to true, double literals are accepted.
*/
void setAcceptDoubleLiterals(bool flag);
private:
// A flag that indicates whether expressions should actually be generated or just a syntax check shall be
// performed.
bool createExpressions;
// A flag that indicates whether double literals are accepted.
bool acceptDoubleLiterals;
// The currently used mapping of identifiers to expressions. This is used if the parser is set to create
// expressions.
qi::symbols<char, storm::expressions::Expression> const* identifiers_;
// The symbol table of invalid identifiers.
qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_;
// Rules for parsing a composed expression.
qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
qi::rule<Iterator, std::string(), Skipper> identifier;
// 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;
// Helper functions to create expressions.
storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createNotExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createTrueExpression() const;
storm::expressions::Expression createFalseExpression() const;
storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const;
storm::expressions::Expression createIntegerLiteralExpression(int value) const;
storm::expressions::Expression createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createFloorExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createCeilExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const;
bool isValidIdentifier(std::string const& identifier);
// Functor used for displaying error information.
struct ErrorHandler {
typedef qi::error_handler_result result_type;
template<typename T1, typename T2, typename T3, typename T4>
qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << ".");
return qi::fail;
}
};
// An error handler function.
phoenix::function<ErrorHandler> handler;
};
} // namespace parser
} // namespace storm
#endif /* STORM_PARSER_EXPRESSIONPARSER_H_ */

383
src/parser/PrismParser.cpp
View File

@ -60,53 +60,11 @@ namespace storm {
return result;
}
PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), allowDoubleLiteralsFlag(true), filename(filename), annotate(first) {
PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), expressionParser(keywords_) {
// Parse simple identifier.
identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
identifier.name("identifier");
floorCeilExpression = ((qi::lit("floor")[qi::_a = true] | qi::lit("ceil")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createFloorExpression, phoenix::ref(*this), qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createCeilExpression, phoenix::ref(*this), qi::_1)]];
floorCeilExpression.name("floor/ceil expression");
minMaxExpression = ((qi::lit("min")[qi::_a = true] | qi::lit("max")[qi::_a = false]) >> qi::lit("(") >> plusExpression >> qi::lit(",") >> plusExpression >> qi::lit(")"))[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createMinimumExpression, phoenix::ref(*this), qi::_1, qi::_2)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMaximumExpression, phoenix::ref(*this), qi::_1, qi::_2)]];
minMaxExpression.name("min/max expression");
identifierExpression = identifier[qi::_val = phoenix::bind(&PrismParser::getIdentifierExpression, phoenix::ref(*this), qi::_1)];
identifierExpression.name("identifier expression");
literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&PrismParser::createTrueExpression, phoenix::ref(*this))] | qi::lit("false")[qi::_val = phoenix::bind(&PrismParser::createFalseExpression, phoenix::ref(*this))] | strict_double[qi::_val = phoenix::bind(&PrismParser::createDoubleLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&PrismParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1)];
literalExpression.name("literal expression");
atomicExpression = minMaxExpression | floorCeilExpression | qi::lit("(") >> expression >> qi::lit(")") | literalExpression | identifierExpression;
atomicExpression.name("atomic expression");
unaryExpression = atomicExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicExpression)[qi::_val = phoenix::bind(&PrismParser::createNotExpression, phoenix::ref(*this), qi::_1)] | (qi::lit("-") >> atomicExpression)[qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_1)];
unaryExpression.name("unary expression");
multiplicationExpression = unaryExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> unaryExpression[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createDivExpression, phoenix::ref(*this), qi::_val, qi::_1)]]);
multiplicationExpression.name("multiplication expression");
plusExpression = multiplicationExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> multiplicationExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createMinusExpression, phoenix::ref(*this), qi::_val, qi::_1)]];
plusExpression.name("plus expression");
relativeExpression = (plusExpression >> qi::lit(">=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit(">") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createGreaterExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<=") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessOrEqualExpression, phoenix::ref(*this), qi::_1, qi::_2)] | (plusExpression >> qi::lit("<") >> plusExpression)[qi::_val = phoenix::bind(&PrismParser::createLessExpression, phoenix::ref(*this), qi::_1, qi::_2)] | plusExpression[qi::_val = qi::_1];
relativeExpression.name("relative expression");
equalityExpression = relativeExpression[qi::_val = qi::_1] >> *((qi::lit("=")[qi::_a = true] | qi::lit("!=")[qi::_a = false]) >> relativeExpression)[phoenix::if_(qi::_a) [ qi::_val = phoenix::bind(&PrismParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] .else_ [ qi::_val = phoenix::bind(&PrismParser::createNotEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1) ] ];
equalityExpression.name("equality expression");
andExpression = equalityExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> equalityExpression)[qi::_val = phoenix::bind(&PrismParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1)];
andExpression.name("and expression");
orExpression = andExpression[qi::_val = qi::_1] >> *((qi::lit("|")[qi::_a = true] | qi::lit("=>")[qi::_a = false]) >> andExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::bind(&PrismParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1)] .else_ [qi::_val = phoenix::bind(&PrismParser::createImpliesExpression, phoenix::ref(*this), qi::_val, qi::_1)] ];
orExpression.name("or expression");
iteExpression = orExpression[qi::_val = qi::_1] >> -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&PrismParser::createIteExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
iteExpression.name("if-then-else expression");
expression %= iteExpression;
expression.name("expression");
modelTypeDefinition %= modelType_;
modelTypeDefinition.name("model type");
@ -122,25 +80,25 @@ namespace storm {
undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition);
undefinedConstantDefinition.name("undefined constant definition");
definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedBooleanConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedBooleanConstantDefinition.name("defined boolean constant declaration");
definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedIntegerConstantDefinition = ((qi::lit("const") >> qi::lit("int") >> identifier >> qi::lit("=")) > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedIntegerConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedIntegerConstantDefinition.name("defined integer constant declaration");
definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedDoubleConstantDefinition = ((qi::lit("const") >> qi::lit("double") >> identifier >> qi::lit("=")) > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createDefinedDoubleConstant, phoenix::ref(*this), qi::_1, qi::_2)];
definedDoubleConstantDefinition.name("defined double constant declaration");
definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
definedConstantDefinition.name("defined constant definition");
formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
formulaDefinition.name("formula definition");
booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expression) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
booleanVariableDefinition.name("boolean variable definition");
integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression[qi::_a = qi::_1] > qi::lit("..") > expression > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expression[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
integerVariableDefinition.name("integer variable definition");
variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]);
@ -149,10 +107,10 @@ namespace storm {
globalVariableDefinition = (qi::lit("global") > (booleanVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalBooleanVariables, qi::_r1), qi::_1)] | integerVariableDefinition[phoenix::push_back(phoenix::bind(&GlobalProgramInformation::globalIntegerVariables, qi::_r1), qi::_1)]));
globalVariableDefinition.name("global variable declaration list");
stateRewardDefinition = (expression > qi::lit(":") > plusExpression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition = (expressionParser > qi::lit(":") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)];
stateRewardDefinition.name("state reward definition");
transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit(":") > plusExpression > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_a, qi::_2, qi::_3)];
transitionRewardDefinition.name("transition reward definition");
rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\""))
@ -162,25 +120,25 @@ namespace storm {
>> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
rewardModelDefinition.name("reward model definition");
initialStatesConstruct = (qi::lit("init") > expression > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
initialStatesConstruct = (qi::lit("init") > expressionParser > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)];
initialStatesConstruct.name("initial construct");
labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
labelDefinition = (qi::lit("label") > -qi::lit("\"") > identifier > -qi::lit("\"") > qi::lit("=") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createLabel, phoenix::ref(*this), qi::_1, qi::_2)];
labelDefinition.name("label definition");
assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
assignmentDefinition = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expressionParser > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)];
assignmentDefinition.name("assignment");
assignmentDefinitionList %= +assignmentDefinition % "&";
assignmentDefinitionList.name("assignment list");
updateDefinition = (((plusExpression > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
updateDefinition.name("update");
updateListDefinition %= +updateDefinition(qi::_r1) % "+";
updateListDefinition.name("update list");
commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expression > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
commandDefinition = (qi::lit("[") > -(identifier[qi::_a = qi::_1]) > qi::lit("]") > expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_2, qi::_3, qi::_r1)];
commandDefinition.name("command definition");
moduleDefinition = ((qi::lit("module") >> identifier >> *(variableDefinition(qi::_a, qi::_b))) > +commandDefinition(qi::_r1) > qi::lit("endmodule"))[qi::_val = phoenix::bind(&PrismParser::createModule, phoenix::ref(*this), qi::_1, qi::_a, qi::_b, qi::_2, qi::_r1)];
@ -209,22 +167,6 @@ namespace storm {
> qi::eoi)[qi::_val = phoenix::bind(&PrismParser::createProgram, phoenix::ref(*this), qi::_a)];
start.name("probabilistic program");
// Enable error reporting.
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>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
// Enable location tracking for important entities.
auto setLocationInfoFunction = this->annotate(qi::_val, qi::_1, qi::_3);
qi::on_success(undefinedBooleanConstantDefinition, setLocationInfoFunction);
@ -250,7 +192,7 @@ namespace storm {
}
void PrismParser::allowDoubleLiterals(bool flag) {
this->allowDoubleLiteralsFlag = flag;
this->expressionParser.setAcceptDoubleLiterals(flag);
}
std::string const& PrismParser::getFilename() const {
@ -274,301 +216,6 @@ namespace storm {
return true;
}
storm::expressions::Expression PrismParser::createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1.ite(e2, e3);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1.implies(e2);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 || e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try{
return e1 && e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 > e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 >= e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 < e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 <= e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1.iff(e2);
} else {
return e1 == e2;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
if (e1.hasBooleanReturnType() && e2.hasBooleanReturnType()) {
return e1 ^ e2;
} else {
return e1 != e2;
}
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 + e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 - e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 * e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1 / e2;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createNotExpression(storm::expressions::Expression e1) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return !e1;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createMinusExpression(storm::expressions::Expression e1) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return -e1;
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createTrueExpression() const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return storm::expressions::Expression::createTrue();
}
}
storm::expressions::Expression PrismParser::createFalseExpression() const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return storm::expressions::Expression::createFalse();
}
}
storm::expressions::Expression PrismParser::createDoubleLiteralExpression(double value, bool& pass) const {
// If we are not supposed to accept double expressions, we reject it by setting pass to false.
if (!this->allowDoubleLiteralsFlag) {
pass = false;
}
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return storm::expressions::Expression::createDoubleLiteral(value);
}
}
storm::expressions::Expression PrismParser::createIntegerLiteralExpression(int value) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value));
}
}
storm::expressions::Expression PrismParser::createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return storm::expressions::Expression::minimum(e1, e2);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return storm::expressions::Expression::maximum(e1, e2);
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createFloorExpression(storm::expressions::Expression e1) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1.floor();
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::createCeilExpression(storm::expressions::Expression e1) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
try {
return e1.ceil();
} catch (storm::exceptions::InvalidTypeException const& e) {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": " << e.what() << ".");
}
}
}
storm::expressions::Expression PrismParser::getIdentifierExpression(std::string const& identifier) const {
if (!this->secondRun) {
return storm::expressions::Expression::createFalse();
} else {
storm::expressions::Expression const* expression = this->identifiers_.find(identifier);
LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
return *expression;
}
}
storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
if (!this->secondRun) {
LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");

82
src/parser/PrismParser.h
View File

@ -6,23 +6,8 @@
#include <memory>
#include <iomanip>
// Include boost spirit.
#define BOOST_SPIRIT_USE_PHOENIX_V3
#include <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
#include <boost/spirit/include/support_line_pos_iterator.hpp>
#include <boost/spirit/home/classic/iterator/position_iterator.hpp>
namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::line_pos_iterator<BaseIteratorType> PositionIteratorType;
typedef PositionIteratorType Iterator;
typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2;
#include "src/parser/SpiritParserDefinitions.h"
#include "src/parser/ExpressionParser.h"
#include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/Expressions.h"
@ -113,17 +98,6 @@ namespace storm {
}
};
// Functor used for displaying error information.
struct ErrorHandler {
typedef qi::error_handler_result result_type;
template<typename T1, typename T2, typename T3, typename T4>
qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << what << ".");
return qi::fail;
}
};
// Functor used for annotating entities with line number information.
class PositionAnnotation {
public:
@ -165,9 +139,6 @@ namespace storm {
*/
void allowDoubleLiterals(bool flag);
// A flag that stores wether to allow or forbid double literals in parsed expressions.
bool allowDoubleLiteralsFlag;
// The name of the file being parsed.
std::string filename;
@ -179,7 +150,6 @@ namespace storm {
std::string const& getFilename() const;
// A function used for annotating the entities with their position.
phoenix::function<ErrorHandler> handler;
phoenix::function<PositionAnnotation> annotate;
// The starting point of the grammar.
@ -237,60 +207,18 @@ namespace storm {
// Rules for identifier parsing.
qi::rule<Iterator, std::string(), Skipper> identifier;
// Rules for parsing a composed expression.
qi::rule<Iterator, storm::expressions::Expression(), Skipper> expression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> iteExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> orExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> andExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> relativeExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> equalityExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> plusExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> multiplicationExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> unaryExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> atomicExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> literalExpression;
qi::rule<Iterator, storm::expressions::Expression(), Skipper> identifierExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> minMaxExpression;
qi::rule<Iterator, storm::expressions::Expression(), qi::locals<bool>, Skipper> floorCeilExpression;
// 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;
// Parsers that recognize special keywords and model types.
storm::parser::PrismParser::keywordsStruct keywords_;
storm::parser::PrismParser::modelTypeStruct modelType_;
qi::symbols<char, storm::expressions::Expression> identifiers_;
// Parser used for recognizing expressions.
storm::parser::ExpressionParser expressionParser;
// Helper methods used in the grammar.
bool isValidIdentifier(std::string const& identifier);
bool addInitialStatesConstruct(storm::expressions::Expression initialStatesExpression, GlobalProgramInformation& globalProgramInformation);
storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3) const;
storm::expressions::Expression createImpliesExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createOrExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createAndExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createGreaterExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createGreaterOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createLessOrEqualExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createNotEqualsExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createPlusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createMultExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createDivExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createNotExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createMinusExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createTrueExpression() const;
storm::expressions::Expression createFalseExpression() const;
storm::expressions::Expression createDoubleLiteralExpression(double value, bool& pass) const;
storm::expressions::Expression createIntegerLiteralExpression(int value) const;
storm::expressions::Expression createMinimumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createMaximumExpression(storm::expressions::Expression e1, storm::expressions::Expression e2) const;
storm::expressions::Expression createFloorExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression createCeilExpression(storm::expressions::Expression e1) const;
storm::expressions::Expression getIdentifierExpression(std::string const& identifier) const;
storm::prism::Constant createUndefinedBooleanConstant(std::string const& newConstant) const;
storm::prism::Constant createUndefinedIntegerConstant(std::string const& newConstant) const;
storm::prism::Constant createUndefinedDoubleConstant(std::string const& newConstant) const;

21
src/parser/SpiritParserDefinitions.h
View File

@ -0,0 +1,21 @@
#ifndef STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
#define STORM_PARSER_SPIRITPARSERDEFINITIONS_H_
// Include boost spirit.
#define BOOST_SPIRIT_USE_PHOENIX_V3
#include <boost/typeof/typeof.hpp>
#include <boost/spirit/include/qi.hpp>
#include <boost/spirit/include/phoenix.hpp>
#include <boost/spirit/include/support_line_pos_iterator.hpp>
#include <boost/spirit/home/classic/iterator/position_iterator.hpp>
namespace qi = boost::spirit::qi;
namespace phoenix = boost::phoenix;
typedef std::string::const_iterator BaseIteratorType;
typedef boost::spirit::line_pos_iterator<BaseIteratorType> PositionIteratorType;
typedef PositionIteratorType Iterator;
typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper;
#endif /* STORM_PARSER_SPIRITPARSERDEFINITIONS_H_ */
Write Preview
Loading…
Cancel
Save