diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp index 2647f4f25..7ac00e712 100644 --- a/src/parser/ExpressionParser.cpp +++ b/src/parser/ExpressionParser.cpp @@ -5,28 +5,28 @@ namespace storm { namespace parser { - ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, 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_(), trueFalse_(manager), manager(manager.getSharedPointer()), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) { identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)]; identifier.name("identifier"); if (allowBacktracking) { - floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; + floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) >> expression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; } else { - floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > iteExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; + floorCeilExpression = ((floorCeilOperator_ >> qi::lit("(")) > expression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createFloorCeilExpression, phoenix::ref(*this), qi::_1, qi::_2)]; } floorCeilExpression.name("floor/ceil expression"); if (allowBacktracking) { - minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] >> qi::lit("(")) >> iteExpression[qi::_val = qi::_1] >> +(qi::lit(",") >> iteExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]) >> qi::lit(")"); + 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::lit(")"); } else { - minMaxExpression = ((minMaxOperator_[qi::_a = qi::_1] > qi::lit("(")) > iteExpression[qi::_val = qi::_1] > +(qi::lit(",") > iteExpression)[qi::_val = phoenix::bind(&ExpressionParser::createMinimumMaximumExpression, phoenix::ref(*this), qi::_val, qi::_a, qi::_1)]) > qi::lit(")"); + 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::lit(")"); } minMaxExpression.name("min/max expression"); if (allowBacktracking) { - prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) >> iteExpression >> qi::lit(",") >> iteExpression >> qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + 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)]; } else { - prefixPowerExpression = ((prefixPowerOperator_ >> qi::lit("(")) > iteExpression > qi::lit(",") > iteExpression > qi::lit(")"))[qi::_val = phoenix::bind(&ExpressionParser::createPowerExpression, phoenix::ref(*this), qi::_2, qi::_1, qi::_3)]; + 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)]; } prefixPowerExpression.name("pow expression"); @@ -106,22 +106,23 @@ namespace storm { debug(identifierExpression); */ - - // Enable error reporting. - qi::on_error(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); - qi::on_error(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + if (enableErrorHandling) { + // Enable error reporting. + qi::on_error(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + qi::on_error(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4)); + } } void ExpressionParser::setIdentifierMapping(qi::symbols const* identifiers_) { diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h index 4277819b2..d3c415d61 100644 --- a/src/parser/ExpressionParser.h +++ b/src/parser/ExpressionParser.h @@ -4,10 +4,9 @@ #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/utility/macros.h" -#include "src/exceptions/WrongFormatException.h" namespace storm { namespace parser { @@ -21,11 +20,13 @@ namespace storm { * * @param manager The manager responsible for the expressions. * @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected. + * @param enableErrorHandling Enables error handling within the parser. Note that this should should be set + * to true when using the parser as the top level parser. * @param allowBacktracking A flag that indicates whether or not the parser is supposed to backtrack beyond * points it would typically allow. This can, for example, be used to prevent errors if the outer grammar * also parses boolean conjuncts that are erroneously consumed by the expression parser. */ - ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool allowBacktracking = false); + ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols const& invalidIdentifiers_, bool enableErrorHandling = true, bool allowBacktracking = false); ExpressionParser(ExpressionParser const& other) = default; ExpressionParser& operator=(ExpressionParser const& other) = default; @@ -241,21 +242,8 @@ namespace storm { bool isValidIdentifier(std::string const& identifier); - // Functor used for displaying error information. - struct ErrorHandler { - typedef qi::error_handler_result result_type; - - template - qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { - std::stringstream whatAsString; - whatAsString << what; - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << "."); - return qi::fail; - } - }; - // An error handler function. - phoenix::function handler; + phoenix::function handler; }; } // namespace parser } // namespace storm diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp index 53fbe6522..bcffe38e3 100644 --- a/src/parser/FormulaParser.cpp +++ b/src/parser/FormulaParser.cpp @@ -2,6 +2,8 @@ #include +#include "src/parser/SpiritErrorHandler.h" + // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFormatException.h" @@ -89,22 +91,6 @@ namespace storm { // Parser and manager used for recognizing expressions. storm::parser::ExpressionParser expressionParser; - // Functor used for displaying error information. - struct ErrorHandler { - typedef qi::error_handler_result result_type; - - template - qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { - std::stringstream whatAsString; - whatAsString << what; - STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(where) << ": " << " expecting " << whatAsString.str() << "."); - return qi::fail; - } - }; - - // An error handler function. - phoenix::function handler; - // 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_; @@ -167,6 +153,9 @@ namespace storm { std::shared_ptr createProbabilityOperatorFormula(std::tuple, boost::optional, boost::optional> 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->getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { @@ -246,7 +235,7 @@ namespace storm { grammar->addIdentifierExpression(identifier, expression); } - FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), expressionParser(*manager, keywords_, true) { + FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr const& manager) : FormulaParserGrammar::base_type(start), 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); diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index fa5170a9c..b2349ebf7 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -4,6 +4,7 @@ #include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidTypeException.h" +#include "src/utility/macros.h" #include "src/exceptions/WrongFormatException.h" namespace storm { @@ -65,7 +66,7 @@ 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_) { + 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) { // 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"); @@ -199,6 +200,9 @@ namespace storm { qi::on_success(commandDefinition, setLocationInfoFunction); qi::on_success(updateDefinition, setLocationInfoFunction); qi::on_success(assignmentDefinition, setLocationInfoFunction); + + // Enable error reporting. + qi::on_error(start, handler(qi::_1, qi::_2, qi::_3, qi::_4)); } void PrismParser::moveToSecondRun() { diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 428b728f0..44da8fc5a 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -11,8 +11,6 @@ #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expressions.h" -#include "src/utility/macros.h" -#include "src/exceptions/WrongFormatException.h" namespace storm { namespace expressions { @@ -251,6 +249,9 @@ namespace storm { storm::prism::Module createModule(std::string const& moduleName, std::vector const& booleanVariables, std::vector const& integerVariables, std::vector const& commands, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map const& renaming, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; + + // An error handler function. + phoenix::function handler; }; } // namespace parser } // namespace storm diff --git a/src/parser/SpiritErrorHandler.h b/src/parser/SpiritErrorHandler.h new file mode 100644 index 000000000..3e78935bd --- /dev/null +++ b/src/parser/SpiritErrorHandler.h @@ -0,0 +1,34 @@ +#ifndef STORM_PARSER_SPIRITERRORHANDLER_H_ +#define STORM_PARSER_SPIRITERRORHANDLER_H_ + +#include "src/parser/SpiritParserDefinitions.h" + +#include "src/utility/macros.h" +#include "src/exceptions/WrongFormatException.h" + +namespace storm { + namespace parser { + // Functor used for displaying error information. + struct SpiritErrorHandler { + typedef qi::error_handler_result result_type; + + template + qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const { + auto lineStart = boost::spirit::get_line_start(b, where); + auto lineEnd = std::find(where, e, '\n'); + std::string line(++lineStart, lineEnd); + + std::stringstream stream; + stream << "Parsing error at " << get_line(where) << ":" << boost::spirit::get_column(lineStart, where) << ": " << " expecting " << what << ", here:" << std::endl; + stream << "\t" << line << std::endl << "\t"; + auto caretColumn = boost::spirit::get_column(lineStart, where); + stream << std::string(caretColumn - 1, ' ') << "^" << std::endl; + + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, stream.str()); + return qi::fail; + } + }; + } +} + +#endif /* STORM_PARSER_SPIRITERRORHANDLER_H_ */ \ No newline at end of file diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp index fc7a7c08c..b18233581 100644 --- a/src/storage/prism/Program.cpp +++ b/src/storage/prism/Program.cpp @@ -102,11 +102,12 @@ namespace storm { // Now it remains to check that the intersection of the variables used in the program with the undefined // constants' variables is empty (except for the update probabilities). - // Start by checking the defining expressions of all defined constants. + // Start by checking the defining expressions of all defined constants. If it contains a currently undefined + //constant, we need to mark the target constant as undefined as well. for (auto const& constant : this->getConstants()) { if (constant.isDefined()) { if (constant.getExpression().containsVariable(undefinedConstantVariables)) { - return false; + undefinedConstantVariables.insert(constant.getExpressionVariable()); } } }