diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h index b5a91248d..05656aea7 100644 --- a/src/adapters/CarlAdapter.h +++ b/src/adapters/CarlAdapter.h @@ -51,12 +51,10 @@ namespace cln { } } + +#include "NumberAdapter.h" + namespace storm { -#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS - typedef cln::cl_RA RationalNumber; -#else - typedef mpq_class RationalNumber; -#endif typedef carl::Variable RationalFunctionVariable; typedef carl::MultivariatePolynomial RawPolynomial; typedef carl::FactorizedPolynomial Polynomial; diff --git a/src/adapters/NumberAdapter.h b/src/adapters/NumberAdapter.h new file mode 100644 index 000000000..73d567353 --- /dev/null +++ b/src/adapters/NumberAdapter.h @@ -0,0 +1,17 @@ +#pragma once + +#include "storm-config.h" + +#include + +#ifdef STORM_HAVE_CARL + +#include +namespace storm { +#if defined STORM_HAVE_CLN && defined USE_CLN_NUMBERS + typedef cln::cl_RA RationalNumber; +#else + typedef mpq_class RationalNumber; +#endif +} +#endif \ No newline at end of file diff --git a/src/parser/ExpressionCreator.cpp b/src/parser/ExpressionCreator.cpp new file mode 100644 index 000000000..85f65b012 --- /dev/null +++ b/src/parser/ExpressionCreator.cpp @@ -0,0 +1,265 @@ +#include "ExpressionCreator.h" + +#include "src/storage/expressions/Expression.h" +#include "src/storage/expressions/ExpressionManager.h" +#include "src/exceptions/InvalidTypeException.h" +#include "src/exceptions/InvalidArgumentException.h" +#include "src/exceptions/WrongFormatException.h" + +#include "src/utility/constants.h" +#include "src/utility/macros.h" + +namespace storm { + namespace parser { + + ExpressionCreator::ExpressionCreator(storm::expressions::ExpressionManager const& manager) : manager(manager) { + // Intenetionally left empty. + } + + storm::expressions::Expression ExpressionCreator::createIteExpression(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2, storm::expressions::Expression const& e3, bool& pass) const { + if (this->createExpressions) { + try { + return storm::expressions::ite(e1, e2, e3); + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Or: return e1 || e2; break; + case storm::expressions::OperatorType::Implies: return storm::expressions::implies(e1, e2); break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + storm::expressions::Expression result; + try { + switch (operatorType) { + case storm::expressions::OperatorType::And: result = e1 && e2; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + return result; + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::GreaterOrEqual: return e1 >= e2; break; + case storm::expressions::OperatorType::Greater: return e1 > e2; break; + case storm::expressions::OperatorType::LessOrEqual: return e1 <= e2; break; + case storm::expressions::OperatorType::Less: return e1 < e2; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Equal: return e1.hasBooleanType() && e2.hasBooleanType() ? storm::expressions::iff(e1, e2) : e1 == e2; break; + case storm::expressions::OperatorType::NotEqual: return e1 != e2; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Plus: return e1 + e2; break; + case storm::expressions::OperatorType::Minus: return e1 - e2; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Times: return e1 * e2; break; + case storm::expressions::OperatorType::Divide: return e1 / e2; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Power: return e1 ^ e2; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const { + if (this->createExpressions) { + try { + if (operatorType) { + switch (operatorType.get()) { + case storm::expressions::OperatorType::Not: return !e1; break; + case storm::expressions::OperatorType::Minus: return -e1; break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } else { + return e1; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createRationalLiteralExpression(storm::RationalNumber const& 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 manager.rational(value); + } else { + return manager.boolean(false); + } + } + + storm::expressions::Expression ExpressionCreator::createIntegerLiteralExpression(int value, bool& pass) const { + if (this->createExpressions) { + return manager.integer(value); + } else { + return manager.boolean(false); + } + } + + + storm::expressions::Expression ExpressionCreator::createBooleanLiteralExpression(bool value, bool& pass) const { + if (this->createExpressions) { + return manager.boolean(value); + } else { + return manager.boolean(false); + } + } + + storm::expressions::Expression ExpressionCreator::createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Min: return storm::expressions::minimum(e1, e2); break; + case storm::expressions::OperatorType::Max: return storm::expressions::maximum(e1, e2); break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const { + if (this->createExpressions) { + try { + switch (operatorType) { + case storm::expressions::OperatorType::Floor: return storm::expressions::floor(e1); break; + case storm::expressions::OperatorType::Ceil: return storm::expressions::ceil(e1); break; + default: STORM_LOG_ASSERT(false, "Invalid operation."); break; + } + } catch (storm::exceptions::InvalidTypeException const& e) { + pass = false; + } + } + return manager.boolean(false); + } + + storm::expressions::Expression ExpressionCreator::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const { + if (this->createExpressions) { + 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); + if (expression == nullptr) { + pass = false; + return manager.boolean(false); + } + return *expression; + } else { + return manager.boolean(false); + } + } + + void ExpressionCreator::setIdentifierMapping(qi::symbols const* identifiers_) { + + if (identifiers_ != nullptr) { + createExpressions = true; + identifiers = identifiers_; + } else { + createExpressions = false; + identifiers = nullptr; + } + } + + void ExpressionCreator::setIdentifierMapping(std::unordered_map const& identifierMapping) { + unsetIdentifierMapping(); + + createExpressions =true; + identifiers = new qi::symbols(); + for (auto const& identifierExpressionPair : identifierMapping) { + identifiers->add(identifierExpressionPair.first, identifierExpressionPair.second); + } + deleteIdentifierMapping = true; + } + + void ExpressionCreator::unsetIdentifierMapping() { + createExpressions = false; + if (deleteIdentifierMapping) { + delete this->identifiers; + deleteIdentifierMapping = false; + } + this->identifiers = nullptr; + } + + + + + } +} \ No newline at end of file diff --git a/src/parser/ExpressionCreator.h b/src/parser/ExpressionCreator.h new file mode 100644 index 000000000..0d6d45c5e --- /dev/null +++ b/src/parser/ExpressionCreator.h @@ -0,0 +1,93 @@ +#pragma once +#include +// Very ugly, but currently we would like to have the symbol table here. +#include "src/parser/SpiritParserDefinitions.h" + +#include +#include "src/adapters/NumberAdapter.h" + +namespace storm { + + namespace expressions { + class Expression; + class ExpressionManager; + enum struct OperatorType; + } + + namespace parser { + class ExpressionCreator { + public: + ExpressionCreator(storm::expressions::ExpressionManager const& manager); + + virtual ~ExpressionCreator() { + if (deleteIdentifierMapping) { + delete this->identifiers; + } + } + + /*! + * 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 const* identifiers_); + + /*! + * 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 identifierMapping A mapping from identifiers to expressions. + */ + void setIdentifierMapping(std::unordered_map const& identifierMapping); + + /*! + * 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(); + + bool getAcceptDoubleLiterals() const { + return acceptDoubleLiterals; + } + + void setAcceptDoubleLiterals(bool set = true) { + acceptDoubleLiterals = set; + } + + + + storm::expressions::Expression createIteExpression(storm::expressions::Expression const& e1, storm::expressions::Expression const& e2, storm::expressions::Expression const& e3, bool& pass) const; + + storm::expressions::Expression createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; + storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const; + storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const; + storm::expressions::Expression createBooleanLiteralExpression(bool value, bool& pass) const; + storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; + storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; + storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const; + + + private: + // The manager responsible for the expressions. + storm::expressions::ExpressionManager const& manager; + qi::symbols const* identifiers = nullptr; + + bool createExpressions = false; + + bool acceptDoubleLiterals = true; + + bool deleteIdentifierMapping = false; + + }; + } +} \ No newline at end of file diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index eb2b1cca1..1d78a2c64 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -4,6 +4,9 @@ #include "src/exceptions/WrongFormatException.h" #include "src/utility/constants.h" +#include "src/parser/ExpressionCreator.h" +#include "src/storage/expressions/Expression.h" + namespace boost { namespace spirit { @@ -33,85 +36,91 @@ namespace boost { namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { + ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling, bool allowBacktracking) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), infixPowerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), prefixPowerOperator_(), invalidIdentifiers_(invalidIdentifiers_) { + + expressionCreator = new ExpressionCreator(manager); + identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); if (allowBacktracking) { - floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2, qi::_pass)]; + floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; } else { - floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2, qi::_pass)]; + floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createFloorCeilExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; } floorCeilExpression.name("floor/ceil expression"); if (allowBacktracking) { - minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> expression[qi::_val = qi::_1] >> +(qi::lit(",") >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1, qi::_pass)]) >> qi::lit(")"); + minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> expression[qi::_val = qi::_1] >> +(qi::lit(",") >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_a, qi::_1, qi::_pass)]) >> qi::lit(")"); } else { - minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) > expression[qi::_val = qi::_1] > +(qi::lit(",") > expression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1, qi::_pass)]) > qi::lit(")"); + minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) > expression[qi::_val = qi::_1] > +(qi::lit(",") > expression)[qi::_val = phoenix::bind(&ExpressionCreator::createMinimumMaximumExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_a, qi::_1, qi::_pass)]) > qi::lit(")"); } minMaxExpression.name("min/max expression"); if (allowBacktracking) { - prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3, qi::_pass)]; + prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> expression >> qi::lit(",") >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; } else { - prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3, qi::_pass)]; + prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > expression > qi::lit(",") > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_2, qi::_1, qi::_3, qi::_pass)]; } prefixPowerExpression.name("pow expression"); - identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionParser::getIdentifierExpression, phoenix::ref(*this), qi::_1, allowBacktracking, qi::_pass)]; + identifierExpression = identifier[qi::_val = phoenix::bind(&ExpressionCreator::getIdentifierExpression, phoenix::ref(*expressionCreator), qi::_1, allowBacktracking, qi::_pass)]; identifierExpression.name("identifier expression"); - literalExpression = trueFalse_[qi::_val = qi::_1] | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionParser::createRationalLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)] | qi::int_[qi::_val = phoenix::bind(&ExpressionParser::createIntegerLiteralExpression, phoenix::ref(*this), qi::_1, qi::_pass)]; + literalExpression = qi::lit("true")[qi::_val = phoenix::bind(&ExpressionCreator::createBooleanLiteralExpression, phoenix::ref(*expressionCreator), true, qi::_pass)] + | qi::lit("false")[qi::_val = phoenix::bind(&ExpressionCreator::createBooleanLiteralExpression, phoenix::ref(*expressionCreator), false, qi::_pass)] + | rationalLiteral_[qi::_val = phoenix::bind(&ExpressionCreator::createRationalLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)] + | qi::int_[qi::_val = phoenix::bind(&ExpressionCreator::createIntegerLiteralExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_pass)]; literalExpression.name("literal expression"); atomicExpression = floorCeilExpression | prefixPowerExpression | minMaxExpression | (qi::lit("(") >> expression >> qi::lit(")")) | literalExpression | identifierExpression; atomicExpression.name("atomic expression"); - unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionParser::createUnaryExpression, phoenix::ref(*this), qi::_1, qi::_2, qi::_pass)]; + unaryExpression = (-unaryOperator_ >> atomicExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createUnaryExpression, phoenix::ref(*expressionCreator), qi::_1, qi::_2, qi::_pass)]; unaryExpression.name("unary expression"); if (allowBacktracking) { - infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ > expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + infixPowerExpression = unaryExpression[qi::_val = qi::_1] > -(infixPowerOperator_ >> expression)[qi::_val = phoenix::bind(&ExpressionCreator::createPowerExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } infixPowerExpression.name("power expression"); if (allowBacktracking) { - multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] >> *(multiplicationOperator_ >> infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMultExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + multiplicationExpression = infixPowerExpression[qi::_val = qi::_1] > *(multiplicationOperator_ > infixPowerExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createMultExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } multiplicationExpression.name("multiplication expression"); - plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionParser::createPlusExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + plusExpression = multiplicationExpression[qi::_val = qi::_1] > *(plusOperator_ >> multiplicationExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createPlusExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; plusExpression.name("plus expression"); 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, qi::_pass)]; + relativeExpression = plusExpression[qi::_val = qi::_1] >> -(relationalOperator_ >> plusExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createRelationalExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionParser::createRelationalExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + relativeExpression = plusExpression[qi::_val = qi::_1] > -(relationalOperator_ > plusExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createRelationalExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } relativeExpression.name("relative expression"); - equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionParser::createEqualsExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + equalityExpression = relativeExpression[qi::_val = qi::_1] >> *(equalityOperator_ >> relativeExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createEqualsExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; equalityExpression.name("equality expression"); if (allowBacktracking) { - andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ >> equalityExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createAndExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionParser::createAndExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + andExpression = equalityExpression[qi::_val = qi::_1] >> *(andOperator_ > equalityExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createAndExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } andExpression.name("and expression"); 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, qi::_pass)]; + orExpression = andExpression[qi::_val = qi::_1] >> *(orOperator_ >> andExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createOrExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } else { - orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionParser::createOrExpression, phoenix::ref(*this), qi::_val, qi::_1, qi::_2, qi::_pass)]; + orExpression = andExpression[qi::_val = qi::_1] > *(orOperator_ > andExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createOrExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; } 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, qi::_pass)]; + iteExpression = orExpression[qi::_val = qi::_1] > -(qi::lit("?") > orExpression > qi::lit(":") > orExpression)[qi::_val = phoenix::bind(&ExpressionCreator::createIteExpression, phoenix::ref(*expressionCreator), qi::_val, qi::_1, qi::_2, qi::_pass)]; iteExpression.name("if-then-else expression"); expression %= iteExpression; @@ -154,240 +163,22 @@ namespace storm { } void ExpressionParser::setIdentifierMapping(qi::symbols const* identifiers_) { - if (identifiers_ != nullptr) { - this->createExpressions = true; - this->identifiers_ = identifiers_; - } else { - this->createExpressions = false; - this->identifiers_ = nullptr; - } + expressionCreator->setIdentifierMapping(identifiers_); } void ExpressionParser::setIdentifierMapping(std::unordered_map const& identifierMapping) { - unsetIdentifierMapping(); - this->createExpressions = true; - this->identifiers_ = new qi::symbols(); - for (auto const& identifierExpressionPair : identifierMapping) { - this->identifiers_->add(identifierExpressionPair.first, identifierExpressionPair.second); - } - deleteIdentifierMapping = true; + expressionCreator->setIdentifierMapping(identifierMapping); } void ExpressionParser::unsetIdentifierMapping() { - this->createExpressions = false; - if (deleteIdentifierMapping) { - delete this->identifiers_; - deleteIdentifierMapping = false; - } - this->identifiers_ = nullptr; + expressionCreator->unsetIdentifierMapping(); } 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, bool& pass) const { - if (this->createExpressions) { - try { - return storm::expressions::ite(e1, e2, e3); - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Or: return e1 || e2; break; - case storm::expressions::OperatorType::Implies: return storm::expressions::implies(e1, e2); break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - storm::expressions::Expression result; - try { - switch (operatorType) { - case storm::expressions::OperatorType::And: result = e1 && e2; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - return result; - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::GreaterOrEqual: return e1 >= e2; break; - case storm::expressions::OperatorType::Greater: return e1 > e2; break; - case storm::expressions::OperatorType::LessOrEqual: return e1 <= e2; break; - case storm::expressions::OperatorType::Less: return e1 < e2; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Equal: return e1.hasBooleanType() && e2.hasBooleanType() ? storm::expressions::iff(e1, e2) : e1 == e2; break; - case storm::expressions::OperatorType::NotEqual: return e1 != e2; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Plus: return e1 + e2; break; - case storm::expressions::OperatorType::Minus: return e1 - e2; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Times: return e1 * e2; break; - case storm::expressions::OperatorType::Divide: return e1 / e2; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Power: return e1 ^ e2; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const { - if (this->createExpressions) { - try { - if (operatorType) { - switch (operatorType.get()) { - case storm::expressions::OperatorType::Not: return !e1; break; - case storm::expressions::OperatorType::Minus: return -e1; break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } else { - return e1; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); + expressionCreator->setAcceptDoubleLiterals(flag); } + - storm::expressions::Expression ExpressionParser::createRationalLiteralExpression(storm::RationalNumber const& 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 manager->rational(value); - } else { - return manager->boolean(false); - } - } - - storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value, bool& pass) const { - if (this->createExpressions) { - return manager->integer(value); - } else { - return manager->boolean(false); - } - } - - storm::expressions::Expression ExpressionParser::createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Min: return storm::expressions::minimum(e1, e2); break; - case storm::expressions::OperatorType::Max: return storm::expressions::maximum(e1, e2); break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const { - if (this->createExpressions) { - try { - switch (operatorType) { - case storm::expressions::OperatorType::Floor: return storm::expressions::floor(e1); break; - case storm::expressions::OperatorType::Ceil: return storm::expressions::ceil(e1); break; - default: STORM_LOG_ASSERT(false, "Invalid operation."); break; - } - } catch (storm::exceptions::InvalidTypeException const& e) { - pass = false; - } - } - return manager->boolean(false); - } - - storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const { - if (this->createExpressions) { - 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); - if (expression == nullptr) { - pass = false; - return manager->boolean(false); - } - return *expression; - } else { - return manager->boolean(false); - } - } - bool ExpressionParser::isValidIdentifier(std::string const& identifier) { if (this->invalidIdentifiers_.find(identifier) != nullptr) { return false; diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 077be8db2..15c039255 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -1,16 +1,19 @@ -#ifndef STORM_PARSER_EXPRESSIONPARSER_H_ -#define STORM_PARSER_EXPRESSIONPARSER_H_ +#pragma once #include #include "src/parser/SpiritParserDefinitions.h" #include "src/parser/SpiritErrorHandler.h" -#include "src/storage/expressions/Expression.h" -#include "src/storage/expressions/ExpressionManager.h" +#include "src/storage/expressions/OperatorType.h" -#include "src/adapters/CarlAdapter.h" +#include "src/adapters/NumberAdapter.h" namespace storm { + namespace expressions { + class Expression; + class ExpressionManager; + } + namespace parser { template struct RationalPolicies : boost::spirit::qi::strict_real_policies { @@ -22,6 +25,8 @@ namespace storm { static bool parse_inf(It&, It const&, Attr&) { return false; } }; + class ExpressionCreator; + class ExpressionParser : public qi::grammar { public: /*! @@ -197,33 +202,9 @@ namespace storm { // A parser used for recognizing the operators at the "power" precedence level. prefixPowerOperatorStruct prefixPowerOperator_; - struct trueFalseOperatorStruct : qi::symbols { - trueFalseOperatorStruct(storm::expressions::ExpressionManager const& manager) { - add - ("true", manager.boolean(true)) - ("false", manager.boolean(false)); - } - }; - - // A parser used for recognizing the literals true and false. - trueFalseOperatorStruct trueFalse_; - - // The manager responsible for the expressions. - std::shared_ptr manager; - - // 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; - // A flag that indicates whether the mapping must be deleted on unsetting. - bool deleteIdentifierMapping; + ExpressionCreator* expressionCreator; - // The currently used mapping of identifiers to expressions. This is used if the parser is set to create - // expressions. - qi::symbols const* identifiers_; // The symbol table of invalid identifiers. qi::symbols invalidIdentifiers_; @@ -250,21 +231,6 @@ namespace storm { // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). boost::spirit::qi::real_parser> rationalLiteral_; - // Helper functions to create expressions. - storm::expressions::Expression createIteExpression(storm::expressions::Expression e1, storm::expressions::Expression e2, storm::expressions::Expression e3, bool& pass) const; - storm::expressions::Expression createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createUnaryExpression(boost::optional const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; - storm::expressions::Expression createRationalLiteralExpression(storm::RationalNumber const& value, bool& pass) const; - storm::expressions::Expression createIntegerLiteralExpression(int value, bool& pass) const; - storm::expressions::Expression createMinimumMaximumExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2, bool& pass) const; - storm::expressions::Expression createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1, bool& pass) const; - storm::expressions::Expression getIdentifierExpression(std::string const& identifier, bool allowBacktracking, bool& pass) const; bool isValidIdentifier(std::string const& identifier); @@ -274,4 +240,3 @@ namespace storm { } // namespace parser } // namespace storm -#endif /* STORM_PARSER_EXPRESSIONPARSER_H_ */ diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index f6aaf82a4..318c110c2 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -11,174 +11,12 @@ #include "src/exceptions/WrongFormatException.h" #include "src/storage/expressions/ExpressionEvaluator.h" +#include "FormulaParserGrammar.h" +#include "src/storage/expressions/ExpressionManager.h" namespace storm { namespace parser { - class FormulaParserGrammar : public qi::grammar>(), Skipper> { - public: - FormulaParserGrammar(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); - - FormulaParserGrammar(FormulaParserGrammar const& other) = default; - FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default; - - /*! - * 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. - * - * @param identifier The identifier that is supposed to be substituted. - * @param expression The expression it is to be substituted with. - */ - void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); - - private: - struct keywordsStruct : qi::symbols { - keywordsStruct() { - add - ("true", 1) - ("false", 2) - ("min", 3) - ("max", 4) - ("F", 5) - ("G", 6) - ("X", 7); - } - }; - - // A parser used for recognizing the keywords. - keywordsStruct keywords_; - - struct relationalOperatorStruct : qi::symbols { - relationalOperatorStruct() { - add - (">=", storm::logic::ComparisonType::GreaterEqual) - (">", storm::logic::ComparisonType::Greater) - ("<=", storm::logic::ComparisonType::LessEqual) - ("<", storm::logic::ComparisonType::Less); - } - }; - - // A parser used for recognizing the operators at the "relational" precedence level. - relationalOperatorStruct relationalOperator_; - - struct binaryBooleanOperatorStruct : qi::symbols { - binaryBooleanOperatorStruct() { - add - ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And) - ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); - } - }; - - // A parser used for recognizing the operators at the "binary" precedence level. - binaryBooleanOperatorStruct binaryBooleanOperator_; - - struct unaryBooleanOperatorStruct : qi::symbols { - 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 { - optimalityOperatorStruct() { - add - ("min", storm::OptimizationDirection::Minimize) - ("max", storm::OptimizationDirection::Maximize); - } - }; - - // A parser used for recognizing the optimality operators. - optimalityOperatorStruct optimalityOperator_; - - struct rewardMeasureTypeStruct : qi::symbols { - rewardMeasureTypeStruct() { - add - ("exp", storm::logic::RewardMeasureType::Expectation) - ("var", storm::logic::RewardMeasureType::Variance); - } - }; - - // A parser used for recognizing the reward measure types. - rewardMeasureTypeStruct rewardMeasureType_; - - // The manager used to parse expressions. - std::shared_ptr 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 identifiers_; - - qi::rule>(), Skipper> start; - - qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; - qi::rule rewardMeasureType; - qi::rule(), Skipper> probabilityOperator; - qi::rule(), Skipper> rewardOperator; - qi::rule(), Skipper> timeOperator; - qi::rule(), Skipper> longRunAverageOperator; - - qi::rule(), Skipper> simpleFormula; - qi::rule(), Skipper> stateFormula; - qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; - qi::rule(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil; - qi::rule(), Skipper> simplePathFormula; - qi::rule(), Skipper> atomicStateFormula; - qi::rule(), Skipper> operatorFormula; - qi::rule label; - qi::rule rewardModelName; - - qi::rule(), Skipper> andStateFormula; - qi::rule(), Skipper> orStateFormula; - qi::rule(), Skipper> notStateFormula; - qi::rule(), Skipper> labelFormula; - qi::rule(), Skipper> expressionFormula; - qi::rule(), qi::locals, Skipper> booleanLiteralFormula; - - qi::rule(storm::logic::FormulaContext), Skipper> conditionalFormula; - qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; - qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; - qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; - qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; - qi::rule, uint_fast64_t>(), Skipper> timeBound; - - qi::rule(), Skipper> rewardPathFormula; - qi::rule(), Skipper> cumulativeRewardFormula; - qi::rule(), Skipper> instantaneousRewardFormula; - qi::rule(), Skipper> longRunAverageRewardFormula; - - // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). - boost::spirit::qi::real_parser> strict_double; - - // Methods that actually create the expression objects. - std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; - std::shared_ptr createLongRunAverageRewardFormula() const; - std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; - std::shared_ptr createBooleanLiteralFormula(bool literal) const; - std::shared_ptr createAtomicLabelFormula(std::string const& label) const; - std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; - std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; - std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); - std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; - storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; - std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; - std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); - std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); - std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); - - // An error handler function. - phoenix::function handler; - }; - FormulaParser::FormulaParser(std::shared_ptr const& manager) : manager(manager), grammar(new FormulaParserGrammar(manager)) { // Intentionally left empty. } @@ -256,278 +94,5 @@ namespace storm { grammar->addIdentifierExpression(identifier, expression); } - FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), manager(manager), expressionParser(*manager, keywords_, true, true) { - // Register all variables so we can parse them in the expressions. - for (auto variableTypePair : *manager) { - 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::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; - longRunAverageRewardFormula.name("long run average reward formula"); - - instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; - instantaneousRewardFormula.name("instantaneous reward formula"); - - cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; - cumulativeRewardFormula.name("cumulative reward formula"); - - rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula; - 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"); - - notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; - notStateFormula.name("negation formula"); - - eventuallyFormula = (qi::lit("F") >> -timeBound >> 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") >> -timeBound >> 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"); - - timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; - timeBound.name("time bound"); - - 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"); - - stateFormula = (orStateFormula); - stateFormula.name("state formula"); - - start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | 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(stateFormula); - debug(orStateFormula); - debug(andStateFormula); - debug(probabilityOperator); - debug(rewardOperator); - debug(longRunAverageOperator); - debug(timeOperator); - debug(pathFormulaWithoutUntil); - debug(pathFormula); -// debug(conditionalFormula); - debug(nextFormula); - debug(globallyFormula); -// debug(eventuallyFormula); - debug(atomicStateFormula); - debug(booleanLiteralFormula); - debug(labelFormula); - debug(expressionFormula); - debug(rewardPathFormula); - debug(cumulativeRewardFormula); - debug(instantaneousRewardFormula); - */ - - // Enable error reporting. - qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(timeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(instantaneousRewardFormula, 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); - } - - std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { - if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); - } else { - double timeBoundAsDouble = boost::get(timeBound); - STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Instantaneous reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBoundAsDouble)); - } - } - - std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { - if (timeBound.which() == 0) { - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); - } else { - double timeBoundAsDouble = boost::get(timeBound); - STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); - return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); - } - } - - std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { - return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); - } - - std::shared_ptr 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(new storm::logic::AtomicExpressionFormula(expression)); - } - - std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { - return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); - } - - std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { - return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); - } - - std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { - if (timeBound) { - if (timeBound.get().which() == 0) { - std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); - } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); - } - } else { - return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); - } - } - - std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); - } - - std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::NextFormula(subformula)); - } - - std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { - if (timeBound) { - if (timeBound.get().which() == 0) { - std::pair const& bounds = boost::get>(timeBound.get()); - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); - } else { - return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); - } - } else { - return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); - } - } - - std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const { - return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); - } - - storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { - if (comparisonType && threshold) { - storm::expressions::ExpressionEvaluator evaluator(*manager); - return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), evaluator.asRational(threshold.get()))); - } else { - return storm::logic::OperatorInformation(optimizationDirection, boost::none); - } - } - - std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { - return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); - } - - std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { - storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; - if (rewardMeasureType) { - measureType = rewardMeasureType.get(); - } - return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType)); - } - - std::shared_ptr FormulaParserGrammar::createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { - storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; - if (rewardMeasureType) { - measureType = rewardMeasureType.get(); - } - return std::shared_ptr(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType)); - } - - std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { - return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); - } - - std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { - return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); - } - - std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { - if (operatorType) { - return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); - } else { - return subformula; - } - } - } // namespace parser } // namespace storm diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h index f69fa6eb2..3dcbb0292 100644 --- a/src/parser/FormulaParser.h +++ b/src/parser/FormulaParser.h @@ -21,7 +21,7 @@ namespace storm { class FormulaParser { public: - FormulaParser(std::shared_ptr const& manager = std::shared_ptr(new storm::expressions::ExpressionManager())); + FormulaParser(std::shared_ptr const& manager); FormulaParser(storm::prism::Program const& program); FormulaParser(FormulaParser const& other); diff --git a/src/parser/FormulaParserGrammar.cpp b/src/parser/FormulaParserGrammar.cpp new file mode 100644 index 000000000..a4bc1bc73 --- /dev/null +++ b/src/parser/FormulaParserGrammar.cpp @@ -0,0 +1,281 @@ +#include "FormulaParserGrammar.h" +#include "src/storage/expressions/ExpressionManager.h" + +namespace storm { + namespace parser { + + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), manager(manager), expressionParser(*manager, keywords_, true, true) { + // Register all variables so we can parse them in the expressions. + for (auto variableTypePair : *manager) { + 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::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageRewardFormula, phoenix::ref(*this))]; + longRunAverageRewardFormula.name("long run average reward formula"); + + instantaneousRewardFormula = (qi::lit("I=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("I=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createInstantaneousRewardFormula, phoenix::ref(*this), qi::_1)]; + instantaneousRewardFormula.name("instantaneous reward formula"); + + cumulativeRewardFormula = (qi::lit("C<=") >> strict_double)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)] | (qi::lit("C<=") > qi::uint_)[qi::_val = phoenix::bind(&FormulaParserGrammar::createCumulativeRewardFormula, phoenix::ref(*this), qi::_1)]; + cumulativeRewardFormula.name("cumulative reward formula"); + + rewardPathFormula = longRunAverageRewardFormula | conditionalFormula(storm::logic::FormulaContext::Reward) | eventuallyFormula(storm::logic::FormulaContext::Reward) | cumulativeRewardFormula | instantaneousRewardFormula; + 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"); + + notStateFormula = (-unaryBooleanOperator_ >> atomicStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)]; + notStateFormula.name("negation formula"); + + eventuallyFormula = (qi::lit("F") >> -timeBound >> 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") >> -timeBound >> 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"); + + timeBound = (qi::lit("[") > qi::double_ > qi::lit(",") > qi::double_ > qi::lit("]"))[qi::_val = phoenix::construct>(qi::_1, qi::_2)] | (qi::lit("<=") >> strict_double)[qi::_val = phoenix::construct>(0, qi::_1)] | (qi::lit("<=") > qi::uint_)[qi::_val = qi::_1]; + timeBound.name("time bound"); + + 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"); + + stateFormula = (orStateFormula); + stateFormula.name("state formula"); + + start = qi::eps > (stateFormula % +(qi::char_("\n;"))) >> qi::skip(boost::spirit::ascii::space | 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(stateFormula); + debug(orStateFormula); + debug(andStateFormula); + debug(probabilityOperator); + debug(rewardOperator); + debug(longRunAverageOperator); + debug(timeOperator); + debug(pathFormulaWithoutUntil); + debug(pathFormula); + // debug(conditionalFormula); + debug(nextFormula); + debug(globallyFormula); + // debug(eventuallyFormula); + debug(atomicStateFormula); + debug(booleanLiteralFormula); + debug(labelFormula); + debug(expressionFormula); + debug(rewardPathFormula); + debug(cumulativeRewardFormula); + debug(instantaneousRewardFormula); + */ + + // Enable error reporting. + qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(stateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(orStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(andStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(probabilityOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(rewardOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(longRunAverageOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(timeOperator, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(operatorInformation, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(pathFormulaWithoutUntil, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(pathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(conditionalFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(untilFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(nextFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(globallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(eventuallyFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(atomicStateFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(booleanLiteralFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(labelFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(expressionFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(rewardPathFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(cumulativeRewardFormula, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(instantaneousRewardFormula, 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); + } + + std::shared_ptr FormulaParserGrammar::createInstantaneousRewardFormula(boost::variant const& timeBound) const { + if (timeBound.which() == 0) { + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(static_cast(boost::get(timeBound)))); + } else { + double timeBoundAsDouble = boost::get(timeBound); + STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Instantaneous reward property must have non-negative bound."); + return std::shared_ptr(new storm::logic::InstantaneousRewardFormula(timeBoundAsDouble)); + } + } + + std::shared_ptr FormulaParserGrammar::createCumulativeRewardFormula(boost::variant const& timeBound) const { + if (timeBound.which() == 0) { + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(boost::get(timeBound)))); + } else { + double timeBoundAsDouble = boost::get(timeBound); + STORM_LOG_THROW(timeBoundAsDouble >= 0, storm::exceptions::WrongFormatException, "Cumulative reward property must have non-negative bound."); + return std::shared_ptr(new storm::logic::CumulativeRewardFormula(static_cast(timeBoundAsDouble))); + } + } + + std::shared_ptr FormulaParserGrammar::createLongRunAverageRewardFormula() const { + return std::shared_ptr(new storm::logic::LongRunAverageRewardFormula()); + } + + std::shared_ptr 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(new storm::logic::AtomicExpressionFormula(expression)); + } + + std::shared_ptr FormulaParserGrammar::createBooleanLiteralFormula(bool literal) const { + return std::shared_ptr(new storm::logic::BooleanLiteralFormula(literal)); + } + + std::shared_ptr FormulaParserGrammar::createAtomicLabelFormula(std::string const& label) const { + return std::shared_ptr(new storm::logic::AtomicLabelFormula(label)); + } + + std::shared_ptr FormulaParserGrammar::createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const { + if (timeBound) { + if (timeBound.get().which() == 0) { + std::pair const& bounds = boost::get>(timeBound.get()); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, bounds.first, bounds.second)); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(createBooleanLiteralFormula(true), subformula, static_cast(boost::get(timeBound.get())))); + } + } else { + return std::shared_ptr(new storm::logic::EventuallyFormula(subformula, context)); + } + } + + std::shared_ptr FormulaParserGrammar::createGloballyFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::GloballyFormula(subformula)); + } + + std::shared_ptr FormulaParserGrammar::createNextFormula(std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::NextFormula(subformula)); + } + + std::shared_ptr FormulaParserGrammar::createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula) { + if (timeBound) { + if (timeBound.get().which() == 0) { + std::pair const& bounds = boost::get>(timeBound.get()); + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, bounds.first, bounds.second)); + } else { + return std::shared_ptr(new storm::logic::BoundedUntilFormula(leftSubformula, rightSubformula, static_cast(boost::get(timeBound.get())))); + } + } else { + return std::shared_ptr(new storm::logic::UntilFormula(leftSubformula, rightSubformula)); + } + } + + std::shared_ptr FormulaParserGrammar::createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const { + return std::shared_ptr(new storm::logic::ConditionalFormula(leftSubformula, rightSubformula, context)); + } + + storm::logic::OperatorInformation FormulaParserGrammar::createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const { + if (comparisonType && threshold) { + storm::expressions::ExpressionEvaluator evaluator(*manager); + return storm::logic::OperatorInformation(optimizationDirection, storm::logic::Bound(comparisonType.get(), evaluator.asRational(threshold.get()))); + } else { + return storm::logic::OperatorInformation(optimizationDirection, boost::none); + } + } + + std::shared_ptr FormulaParserGrammar::createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + return std::shared_ptr(new storm::logic::LongRunAverageOperatorFormula(subformula, operatorInformation)); + } + + std::shared_ptr FormulaParserGrammar::createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; + if (rewardMeasureType) { + measureType = rewardMeasureType.get(); + } + return std::shared_ptr(new storm::logic::RewardOperatorFormula(subformula, rewardModelName, operatorInformation, measureType)); + } + + std::shared_ptr FormulaParserGrammar::createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const { + storm::logic::RewardMeasureType measureType = storm::logic::RewardMeasureType::Expectation; + if (rewardMeasureType) { + measureType = rewardMeasureType.get(); + } + return std::shared_ptr(new storm::logic::TimeOperatorFormula(subformula, operatorInformation, measureType)); + } + + std::shared_ptr FormulaParserGrammar::createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) { + return std::shared_ptr(new storm::logic::ProbabilityOperatorFormula(subformula, operatorInformation)); + } + + std::shared_ptr FormulaParserGrammar::createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType) { + return std::shared_ptr(new storm::logic::BinaryBooleanStateFormula(operatorType, leftSubformula, rightSubformula)); + } + + std::shared_ptr FormulaParserGrammar::createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType) { + if (operatorType) { + return std::shared_ptr(new storm::logic::UnaryBooleanStateFormula(operatorType.get(), subformula)); + } else { + return subformula; + } + } + + } +} \ No newline at end of file diff --git a/src/parser/FormulaParserGrammar.h b/src/parser/FormulaParserGrammar.h new file mode 100644 index 000000000..227c5aa47 --- /dev/null +++ b/src/parser/FormulaParserGrammar.h @@ -0,0 +1,185 @@ +#pragma once + +#include +#include + +#include "src/parser/SpiritErrorHandler.h" +#include "src/exceptions/WrongFormatException.h" +#include "src/logic/Formulas.h" +#include "src/parser/ExpressionParser.h" + +#include "src/storage/expressions/ExpressionEvaluator.h" + +namespace storm { + namespace logic { + class Formula; + } + + namespace parser { + + class FormulaParserGrammar : public qi::grammar>(), Skipper> { + public: + FormulaParserGrammar(std::shared_ptr const& manager); + + FormulaParserGrammar(FormulaParserGrammar const& other) = default; + FormulaParserGrammar& operator=(FormulaParserGrammar const& other) = default; + + /*! + * 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. + * + * @param identifier The identifier that is supposed to be substituted. + * @param expression The expression it is to be substituted with. + */ + void addIdentifierExpression(std::string const& identifier, storm::expressions::Expression const& expression); + + private: + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("true", 1) + ("false", 2) + ("min", 3) + ("max", 4) + ("F", 5) + ("G", 6) + ("X", 7); + } + }; + + // A parser used for recognizing the keywords. + keywordsStruct keywords_; + + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + (">=", storm::logic::ComparisonType::GreaterEqual) + (">", storm::logic::ComparisonType::Greater) + ("<=", storm::logic::ComparisonType::LessEqual) + ("<", storm::logic::ComparisonType::Less); + } + }; + + // A parser used for recognizing the operators at the "relational" precedence level. + relationalOperatorStruct relationalOperator_; + + struct binaryBooleanOperatorStruct : qi::symbols { + binaryBooleanOperatorStruct() { + add + ("&", storm::logic::BinaryBooleanStateFormula::OperatorType::And) + ("|", storm::logic::BinaryBooleanStateFormula::OperatorType::Or); + } + }; + + // A parser used for recognizing the operators at the "binary" precedence level. + binaryBooleanOperatorStruct binaryBooleanOperator_; + + struct unaryBooleanOperatorStruct : qi::symbols { + 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 { + optimalityOperatorStruct() { + add + ("min", storm::OptimizationDirection::Minimize) + ("max", storm::OptimizationDirection::Maximize); + } + }; + + // A parser used for recognizing the optimality operators. + optimalityOperatorStruct optimalityOperator_; + + struct rewardMeasureTypeStruct : qi::symbols { + rewardMeasureTypeStruct() { + add + ("exp", storm::logic::RewardMeasureType::Expectation) + ("var", storm::logic::RewardMeasureType::Variance); + } + }; + + // A parser used for recognizing the reward measure types. + rewardMeasureTypeStruct rewardMeasureType_; + + // The manager used to parse expressions. + std::shared_ptr 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 identifiers_; + + qi::rule>(), Skipper> start; + + qi::rule, boost::optional, boost::optional>, Skipper> operatorInformation; + qi::rule rewardMeasureType; + qi::rule(), Skipper> probabilityOperator; + qi::rule(), Skipper> rewardOperator; + qi::rule(), Skipper> timeOperator; + qi::rule(), Skipper> longRunAverageOperator; + + qi::rule(), Skipper> simpleFormula; + qi::rule(), Skipper> stateFormula; + qi::rule(storm::logic::FormulaContext), Skipper> pathFormula; + qi::rule(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil; + qi::rule(), Skipper> simplePathFormula; + qi::rule(), Skipper> atomicStateFormula; + qi::rule(), Skipper> operatorFormula; + qi::rule label; + qi::rule rewardModelName; + + qi::rule(), Skipper> andStateFormula; + qi::rule(), Skipper> orStateFormula; + qi::rule(), Skipper> notStateFormula; + qi::rule(), Skipper> labelFormula; + qi::rule(), Skipper> expressionFormula; + qi::rule(), qi::locals, Skipper> booleanLiteralFormula; + + qi::rule(storm::logic::FormulaContext), Skipper> conditionalFormula; + qi::rule(storm::logic::FormulaContext), Skipper> eventuallyFormula; + qi::rule(storm::logic::FormulaContext), Skipper> nextFormula; + qi::rule(storm::logic::FormulaContext), Skipper> globallyFormula; + qi::rule(storm::logic::FormulaContext), Skipper> untilFormula; + qi::rule, uint_fast64_t>(), Skipper> timeBound; + + qi::rule(), Skipper> rewardPathFormula; + qi::rule(), Skipper> cumulativeRewardFormula; + qi::rule(), Skipper> instantaneousRewardFormula; + qi::rule(), Skipper> longRunAverageRewardFormula; + + // Parser that is used to recognize doubles only (as opposed to Spirit's double_ parser). + boost::spirit::qi::real_parser> strict_double; + + // Methods that actually create the expression objects. + std::shared_ptr createInstantaneousRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createCumulativeRewardFormula(boost::variant const& timeBound) const; + std::shared_ptr createLongRunAverageRewardFormula() const; + std::shared_ptr createAtomicExpressionFormula(storm::expressions::Expression const& expression) const; + std::shared_ptr createBooleanLiteralFormula(bool literal) const; + std::shared_ptr createAtomicLabelFormula(std::string const& label) const; + std::shared_ptr createEventuallyFormula(boost::optional, uint_fast64_t>> const& timeBound, storm::logic::FormulaContext context, std::shared_ptr const& subformula) const; + std::shared_ptr createGloballyFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createNextFormula(std::shared_ptr const& subformula) const; + std::shared_ptr createUntilFormula(std::shared_ptr const& leftSubformula, boost::optional, uint_fast64_t>> const& timeBound, std::shared_ptr const& rightSubformula); + std::shared_ptr createConditionalFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::FormulaContext context) const; + storm::logic::OperatorInformation createOperatorInformation(boost::optional const& optimizationDirection, boost::optional const& comparisonType, boost::optional const& threshold) const; + std::shared_ptr createLongRunAverageOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createRewardOperatorFormula(boost::optional const& rewardMeasureType, boost::optional const& rewardModelName, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createTimeOperatorFormula(boost::optional const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula) const; + std::shared_ptr createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr const& subformula); + std::shared_ptr createBinaryBooleanStateFormula(std::shared_ptr const& leftSubformula, std::shared_ptr const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); + std::shared_ptr createUnaryBooleanStateFormula(std::shared_ptr const& subformula, boost::optional const& operatorType); + + // An error handler function. + phoenix::function handler; + }; + + } +} \ No newline at end of file diff --git a/src/parser/PgclParser.cpp b/src/parser/PgclParser.cpp index 56bf4c0fe..4c3c840f5 100755 --- a/src/parser/PgclParser.cpp +++ b/src/parser/PgclParser.cpp @@ -1,10 +1,3 @@ -/* - * File: PgclParser.cpp - * Author: Lukas Westhofen - * - * Created on 1. April 2015, 19:12 - */ - #include "src/parser/PgclParser.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -60,22 +53,24 @@ namespace storm { } PgclParser::PgclParser(std::string const& filename, Iterator first) : - PgclParser::base_type(program, "PGCL grammar"), - annotate(first), - expressionManager(std::shared_ptr(new storm::expressions::ExpressionManager())), - expressionParser(*expressionManager, invalidIdentifiers) { + PgclParser::base_type(program, "PGCL grammar"), + annotate(first), + expressionManager(std::shared_ptr(new storm::expressions::ExpressionManager())), + expressionParser(*expressionManager, invalidIdentifiers) + { this->enableExpressions(); /* * PGCL grammar is defined here */ // Rough program structure - program = (qi::lit("function ") >> programName >> qi::lit("(") >> -(doubleDeclaration % qi::lit(",")) >> qi::lit(")") >> qi::lit("{") >> - variableDeclarations >> - sequenceOfStatements >> + program = (qi::lit("function ") > programName > qi::lit("(") > -(doubleDeclaration % qi::lit(",")) > qi::lit(")") > qi::lit("{") > + variableDeclarations > + sequenceOfStatements > qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createProgram, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)]; sequenceOfStatements %= +(statement); + sequenceOfStatements.name("sequence of statements"); - variableDeclarations %= qi::lit("var") >> qi::lit("{") >> +(integerDeclaration | booleanDeclaration) >> qi::lit("}"); + variableDeclarations %= qi::lit("var") > qi::lit("{") > +(integerDeclaration | booleanDeclaration) > qi::lit("}"); variableDeclarations.name("variable declarations"); // Statements @@ -86,32 +81,39 @@ namespace storm { // Simple statements doubleDeclaration = (qi::lit("double ") >> variableName)[qi::_val = phoenix::bind(&PgclParser::declareDoubleVariable, phoenix::ref(*this), qi::_1)]; integerDeclaration = (qi::lit("int ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createIntegerDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)]; + integerDeclaration.name("integer declaration"); booleanDeclaration = (qi::lit("bool ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createBooleanDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)]; - - assignmentStatement = (variableName >> qi::lit(":=") >> (expression | uniformExpression) >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createAssignmentStatement, phoenix::ref(*this), qi::_1, qi::_2)]; - observeStatement = (qi::lit("observe") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createObserveStatement, phoenix::ref(*this), qi::_1)]; + booleanDeclaration.name("boolean declaration"); + + assignmentStatement = (variableName > qi::lit(":=") > (expression | uniformExpression) > qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createAssignmentStatement, phoenix::ref(*this), qi::_1, qi::_2)]; + observeStatement = (qi::lit("observe") > qi::lit("(") >> booleanCondition >> qi::lit(")") > qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createObserveStatement, phoenix::ref(*this), qi::_1)]; // Compound statements - ifElseStatement = (qi::lit("if") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >> + ifElseStatement = (qi::lit("if") > qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> -(qi::lit("else") >> qi::lit("{") >> sequenceOfStatements >> qi::lit("}"))) [qi::_val = phoenix::bind(&PgclParser::createIfElseStatement, phoenix::ref(*this), qi::_1, qi::_2, qi::_3)]; + ifElseStatement.name("if/else statement"); branchStatement = nondeterministicBranch | probabilisticBranch; - loopStatement = (qi::lit("while") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit("{") >> + loopStatement = (qi::lit("while") > qi::lit("(") > booleanCondition > qi::lit(")") > qi::lit("{") >> sequenceOfStatements >> qi::lit("}")) [qi::_val = phoenix::bind(&PgclParser::createLoopStatement, phoenix::ref(*this), qi::_1, qi::_2)]; + loopStatement.name("loop statement"); nondeterministicBranch = (qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> qi::lit("[]") >> qi::lit("{") >> sequenceOfStatements>> qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createNondeterministicBranch, phoenix::ref(*this), qi::_1, qi::_2)]; probabilisticBranch = (qi::lit("{") >> sequenceOfStatements >> qi::lit("}") >> qi::lit("[") >> expression >> qi::lit("]") >> qi::lit("{") >> sequenceOfStatements >> qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createProbabilisticBranch, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; // Expression and condition building, and basic identifiers expression %= expressionParser; + expression.name("expression"); booleanCondition = expressionParser[qi::_val = phoenix::bind(&PgclParser::createBooleanExpression, phoenix::ref(*this), qi::_1)]; uniformExpression = (qi::lit("unif") >> qi::lit("(") >> qi::int_ >> qi::lit(",") >> qi::int_ >> qi::lit(")"))[qi::_val = phoenix::bind(&PgclParser::createUniformExpression, phoenix::ref(*this), qi::_1, qi::_2)]; - variableName %= (+(qi::alnum | qi::lit("_"))) - (qi::lit("int") >> +(qi::alnum | qi::lit("_"))); + variableName %= (+(qi::alnum | qi::lit("_"))) - invalidIdentifiers; + variableName.name("variable name"); programName %= +(qi::alnum | qi::lit("_")); + programName.name("program name"); // Enables location tracking for important entities auto setLocationInfoFunction = this->annotate(*qi::_val, qi::_1, qi::_3); @@ -121,8 +123,24 @@ namespace storm { qi::on_success(probabilisticBranch, setLocationInfoFunction); qi::on_success(loopStatement, setLocationInfoFunction); qi::on_success(ifElseStatement, setLocationInfoFunction); - qi::on_success(integerDeclaration, setLocationInfoFunction); - + + // Enable error reporting. + qi::on_error(program, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(variableDeclarations, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(integerDeclaration, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(booleanDeclaration, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + + qi::on_error(assignmentStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(observeStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(ifElseStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(loopStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(branchStatement, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + + + qi::on_error(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(booleanCondition, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(uniformExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + // Adds dummy to the 0-th location. std::shared_ptr dummy(new storm::pgcl::AssignmentStatement()); this->locationToStatement.insert(this->locationToStatement.begin(), dummy); @@ -139,15 +157,20 @@ namespace storm { * throw excpetions in case something unexpected was parsed, e.g. * (x+5) as a boolean expression, or types of assignments don't match. */ - storm::pgcl::PgclProgram PgclParser::createProgram(std::string const& programName, boost::optional> parameters, std::vector> const& variableDeclarations, std::vector> statements) { + storm::pgcl::PgclProgram PgclParser::createProgram(std::string const& programName, boost::optional> parameters, std::vector> const& variableDeclarations, std::vector> const& statements) { // Creates an empty paramter list in case no parameters were given. std::vector params; if(parameters != boost::none) { params = *parameters; } + std::vector declarations; + for (auto const& decl : variableDeclarations) { + declarations.push_back(*decl); + } + // Creates the actual program. std::shared_ptr result( - new storm::pgcl::PgclProgram(statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated) + new storm::pgcl::PgclProgram(declarations, statements, this->locationToStatement, params, this->expressionManager, this->loopCreated, this->nondetCreated, this->observeCreated) ); result->back()->setLast(true); // Sets the current program as a parent to all its direct children statements. @@ -181,7 +204,7 @@ namespace storm { return newAssignment; } - std::shared_ptr PgclParser::createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) { + std::shared_ptr PgclParser::createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) { storm::expressions::Variable variable; if(!(*expressionManager).hasVariable(variableName)) { variable = (*expressionManager).declareIntegerVariable(variableName); @@ -191,14 +214,11 @@ namespace storm { variable = (*expressionManager).getVariable(variableName); STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Declaration of integer variable " << variableName << " which was already declared previously."); } - std::shared_ptr newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression)); - newAssignment->setLocationNumber(this->currentLocationNumber); - this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment); - currentLocationNumber++; - return newAssignment; + // Todo add some checks + return std::make_shared(variable, assignedExpression); } - std::shared_ptr PgclParser::createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) { + std::shared_ptr PgclParser::createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) { storm::expressions::Variable variable; if(!(*expressionManager).hasVariable(variableName)) { variable = (*expressionManager).declareBooleanVariable(variableName); @@ -208,11 +228,8 @@ namespace storm { variable = (*expressionManager).getVariable(variableName); STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Declaration of boolean variable " << variableName << " which was already declared previously."); } - std::shared_ptr newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression)); - newAssignment->setLocationNumber(this->currentLocationNumber); - this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment); - currentLocationNumber++; - return newAssignment; + // TODO add some checks. + return std::make_shared(variable, assignedExpression); } std::shared_ptr PgclParser::createObserveStatement(storm::pgcl::BooleanExpression const& condition) { diff --git a/src/parser/PgclParser.h b/src/parser/PgclParser.h index a9b99ef09..223079e3b 100755 --- a/src/parser/PgclParser.h +++ b/src/parser/PgclParser.h @@ -1,12 +1,4 @@ -/* - * File: PgclParser.h - * Author: Lukas Westhofen - * - * Created on 1. April 2015, 19:12 - */ - -#ifndef PGCLPARSER_H -#define PGCLPARSER_H +#pragma once // Includes files for file input. #include @@ -14,6 +6,7 @@ #include // Includes files for building and parsing the PGCL program #include "src/parser/SpiritParserDefinitions.h" +#include "src/parser/SpiritErrorHandler.h" #include "src/parser/ExpressionParser.h" #include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/Expression.h" @@ -29,6 +22,10 @@ #include "src/storage/pgcl/Statement.h" namespace storm { + namespace pgcl { + class IfStatement; + } + namespace parser { class PgclParser : public qi::grammar { @@ -74,11 +71,14 @@ namespace storm { qi::rule variableName; qi::rule programName; - qi::rule>(), Skipper> variableDeclarations; - qi::rule(), Skipper> integerDeclaration; - qi::rule(), Skipper> booleanDeclaration; + qi::rule>(), Skipper> variableDeclarations; + qi::rule(), Skipper> integerDeclaration; + qi::rule(), Skipper> booleanDeclaration; qi::rule doubleDeclaration; + // An error handler function. + phoenix::function handler; + /// Denotes the invalid identifiers, which are later passed to the expression parser. struct keywordsStruct : qi::symbols { keywordsStruct() { @@ -87,7 +87,8 @@ namespace storm { ("if", 2) ("observe", 3) ("int", 4) - ("function", 5); + ("bool", 5) + ("function", 6); } }; @@ -138,11 +139,11 @@ namespace storm { void enableExpressions(); // Constructors for the single program parts. They just wrap the statement constructors and throw exceptions in case something unexpected was parsed. - storm::pgcl::PgclProgram createProgram(std::string const& programName, boost::optional > parameters, std::vector> const& variableDeclarations, std::vector > statements); + storm::pgcl::PgclProgram createProgram(std::string const& programName, boost::optional > parameters, std::vector> const& variableDeclarations, std::vector > const& statements); storm::expressions::Variable declareDoubleVariable(std::string const& variableName); std::shared_ptr createAssignmentStatement(std::string const& variableName, boost::variant const& assignedExpression); - std::shared_ptr createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression); - std::shared_ptr createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression); + std::shared_ptr createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression); + std::shared_ptr createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression); std::shared_ptr createObserveStatement(storm::pgcl::BooleanExpression const& condition); std::shared_ptr createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector > const& if_body, boost::optional > > const& else_body); std::shared_ptr createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector > const& body); @@ -154,5 +155,4 @@ namespace storm { } // namespace parser } // namespace storm -#endif /* PGCLPARSER_H */ diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index d3e5191e2..ba7546a6e 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -9,6 +9,10 @@ #include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" +#include "src/storage/expressions/ExpressionManager.h" + +#include "src/parser/ExpressionParser.h" + namespace storm { namespace parser { storm::prism::Program PrismParser::parse(std::string const& filename) { @@ -70,7 +74,9 @@ namespace storm { return result; } - PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(*manager, keywords_, false, false) { + PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(new ExpressionParser(*manager, keywords_, false, false)) { + + ExpressionParser& expression_ = *expressionParser; // 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"); @@ -90,25 +96,25 @@ namespace storm { undefinedConstantDefinition = (undefinedBooleanConstantDefinition | undefinedIntegerConstantDefinition | undefinedDoubleConstantDefinition); undefinedConstantDefinition.name("undefined constant definition"); - 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 = ((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.name("defined boolean constant declaration"); - 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 = ((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.name("defined integer constant declaration"); - 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 = ((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.name("defined double constant declaration"); definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); definedConstantDefinition.name("defined constant definition"); - formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)]; + formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expression_ > 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") > expressionParser[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; + booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > -((qi::lit("init") > expression_[qi::_a = qi::_1]) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_a)]; booleanVariableDefinition.name("boolean variable definition"); - integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser > 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 = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expression_ > 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.name("integer variable definition"); variableDefinition = (booleanVariableDefinition[phoenix::push_back(qi::_r1, qi::_1)] | integerVariableDefinition[phoenix::push_back(qi::_r2, qi::_1)]); @@ -117,13 +123,13 @@ 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 = (expressionParser > qi::lit(":") > expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; + stateRewardDefinition = (expression_ > qi::lit(":") > expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateReward, phoenix::ref(*this), qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); - stateActionRewardDefinition = (qi::lit("[") >> -identifier >> qi::lit("]") >> expressionParser >> qi::lit(":") >> expressionParser >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)]; + stateActionRewardDefinition = (qi::lit("[") >> -identifier >> qi::lit("]") >> expression_ >> qi::lit(":") >> expression_ >> qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createStateActionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_r1)]; stateActionRewardDefinition.name("state action reward definition"); - transitionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > expressionParser > qi::lit("->") > expressionParser > qi::lit(":") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4, qi::_r1)]; + transitionRewardDefinition = (qi::lit("[") > -identifier > qi::lit("]") > expression_ > qi::lit("->") > expression_ > qi::lit(":") > expression_ > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createTransitionReward, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4, qi::_r1)]; transitionRewardDefinition.name("transition reward definition"); rewardModelDefinition = (qi::lit("rewards") > -(qi::lit("\"") > identifier[qi::_a = qi::_1] > qi::lit("\"")) @@ -134,7 +140,7 @@ namespace storm { >> qi::lit("endrewards"))[qi::_val = phoenix::bind(&PrismParser::createRewardModel, phoenix::ref(*this), qi::_a, qi::_b, qi::_c, qi::_d)]; rewardModelDefinition.name("reward model definition"); - initialStatesConstruct = (qi::lit("init") > expressionParser > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; + initialStatesConstruct = (qi::lit("init") > expression_ > qi::lit("endinit"))[qi::_pass = phoenix::bind(&PrismParser::addInitialStatesConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; initialStatesConstruct.name("initial construct"); systemCompositionConstruct = (qi::lit("system") > parallelComposition > qi::lit("endsystem"))[phoenix::bind(&PrismParser::addSystemCompositionConstruct, phoenix::ref(*this), qi::_1, qi::_r1)]; @@ -176,16 +182,16 @@ namespace storm { moduleComposition = identifier[qi::_val = phoenix::bind(&PrismParser::createModuleComposition, phoenix::ref(*this), qi::_1)]; moduleComposition.name("module composition"); - 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 = (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.name("label definition"); - 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 = (qi::lit("(") > identifier > qi::lit("'") > qi::lit("=") > expression_ > qi::lit(")"))[qi::_val = phoenix::bind(&PrismParser::createAssignment, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentDefinition.name("assignment"); assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct>()]; assignmentDefinitionList.name("assignment list"); - updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; + updateDefinition = (((expression_ >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)]; updateDefinition.name("update"); updateListDefinition %= +updateDefinition(qi::_r1) % "+"; @@ -254,17 +260,17 @@ namespace storm { commandDefinition = (((qi::lit("[") > -identifier > qi::lit("]")) | (qi::lit("<") > -identifier > qi::lit(">")[qi::_a = true])) - > expressionParser + > *expressionParser > qi::lit("->") > updateListDefinition(qi::_r1) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createCommand, phoenix::ref(*this), qi::_a, qi::_1, qi::_2, qi::_3, qi::_r1)]; this->secondRun = true; - this->expressionParser.setIdentifierMapping(&this->identifiers_); + this->expressionParser->setIdentifierMapping(&this->identifiers_); } void PrismParser::allowDoubleLiterals(bool flag) { - this->expressionParser.setAcceptDoubleLiterals(flag); + this->expressionParser->setAcceptDoubleLiterals(flag); } std::string const& PrismParser::getFilename() const { diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 2a83e3193..3d10a6c6a 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -7,7 +7,7 @@ #include #include "src/parser/SpiritParserDefinitions.h" -#include "src/parser/ExpressionParser.h" +#include "src/parser/SpiritErrorHandler.h" #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expressions.h" @@ -20,6 +20,8 @@ namespace storm { namespace storm { namespace parser { + class ExpressionParser; + // A class that stores information about the parsed program. class GlobalProgramInformation { public: @@ -237,7 +239,8 @@ namespace storm { // Parser and manager used for recognizing expressions. std::shared_ptr manager; - storm::parser::ExpressionParser expressionParser; + // TODO shared? + std::shared_ptr expressionParser; // Helper methods used in the grammar. bool isValidIdentifier(std::string const& identifier); diff --git a/src/parser/SpiritErrorHandler.h b/src/parser/SpiritErrorHandler.h index 949ad9b12..6374ccfba 100644 --- a/src/parser/SpiritErrorHandler.h +++ b/src/parser/SpiritErrorHandler.h @@ -1,5 +1,4 @@ -#ifndef STORM_PARSER_SPIRITERRORHANDLER_H_ -#define STORM_PARSER_SPIRITERRORHANDLER_H_ +#pragma once #include "src/parser/SpiritParserDefinitions.h" @@ -30,5 +29,3 @@ namespace storm { }; } } - -#endif /* STORM_PARSER_SPIRITERRORHANDLER_H_ */ \ No newline at end of file diff --git a/src/utility/storm.cpp b/src/utility/storm.cpp index b1ad84cc6..d4fb44290 100644 --- a/src/utility/storm.cpp +++ b/src/utility/storm.cpp @@ -37,7 +37,8 @@ namespace storm { } std::vector> parseFormulasForExplicit(std::string const& inputString) { - storm::parser::FormulaParser formulaParser; + auto exprManager = std::make_shared(); + storm::parser::FormulaParser formulaParser(exprManager); return parseFormulas(formulaParser, inputString); }