Browse Source

improved spirit error handling a bit

Former-commit-id: 8d4b24a336
tempestpy_adaptions
dehnert 9 years ago
parent
commit
f72f556018
  1. 47
      src/parser/ExpressionParser.cpp
  2. 22
      src/parser/ExpressionParser.h
  3. 23
      src/parser/FormulaParser.cpp
  4. 6
      src/parser/PrismParser.cpp
  5. 5
      src/parser/PrismParser.h
  6. 34
      src/parser/SpiritErrorHandler.h
  7. 5
      src/storage/prism/Program.cpp

47
src/parser/ExpressionParser.cpp

@ -5,28 +5,28 @@
namespace storm { namespace storm {
namespace parser { namespace parser {
ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> 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<char, uint_fast64_t> 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 %= 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"); identifier.name("identifier");
if (allowBacktracking) { 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 { } 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"); floorCeilExpression.name("floor/ceil expression");
if (allowBacktracking) { 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 { } 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"); minMaxExpression.name("min/max expression");
if (allowBacktracking) { 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 { } 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"); prefixPowerExpression.name("pow expression");
@ -106,22 +106,23 @@ namespace storm {
debug(identifierExpression); debug(identifierExpression);
*/ */
// Enable error reporting.
qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
if (enableErrorHandling) {
// Enable error reporting.
qi::on_error<qi::fail>(expression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(iteExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(orExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(andExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(equalityExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(relativeExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(plusExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(multiplicationExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(unaryExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(atomicExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(literalExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(identifierExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(minMaxExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
qi::on_error<qi::fail>(floorCeilExpression, handler(qi::_1, qi::_2, qi::_3, qi::_4));
}
} }
void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) { void ExpressionParser::setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_) {

22
src/parser/ExpressionParser.h

@ -4,10 +4,9 @@
#include <sstream> #include <sstream>
#include "src/parser/SpiritParserDefinitions.h" #include "src/parser/SpiritParserDefinitions.h"
#include "src/parser/SpiritErrorHandler.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/ExpressionManager.h" #include "src/storage/expressions/ExpressionManager.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm { namespace storm {
namespace parser { namespace parser {
@ -21,11 +20,13 @@ namespace storm {
* *
* @param manager The manager responsible for the expressions. * @param manager The manager responsible for the expressions.
* @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected. * @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 * @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 * 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. * also parses boolean conjuncts that are erroneously consumed by the expression parser.
*/ */
ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool allowBacktracking = false);
ExpressionParser(storm::expressions::ExpressionManager const& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_, bool enableErrorHandling = true, bool allowBacktracking = false);
ExpressionParser(ExpressionParser const& other) = default; ExpressionParser(ExpressionParser const& other) = default;
ExpressionParser& operator=(ExpressionParser const& other) = default; ExpressionParser& operator=(ExpressionParser const& other) = default;
@ -241,21 +242,8 @@ namespace storm {
bool isValidIdentifier(std::string const& identifier); bool isValidIdentifier(std::string const& identifier);
// Functor used for displaying error information.
struct ErrorHandler {
typedef qi::error_handler_result result_type;
template<typename T1, typename T2, typename T3, typename T4>
qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
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. // An error handler function.
phoenix::function<ErrorHandler> handler;
phoenix::function<SpiritErrorHandler> handler;
}; };
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

23
src/parser/FormulaParser.cpp

@ -2,6 +2,8 @@
#include <fstream> #include <fstream>
#include "src/parser/SpiritErrorHandler.h"
// If the parser fails due to ill-formed data, this exception is thrown. // If the parser fails due to ill-formed data, this exception is thrown.
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
@ -89,22 +91,6 @@ namespace storm {
// Parser and manager used for recognizing expressions. // Parser and manager used for recognizing expressions.
storm::parser::ExpressionParser expressionParser; storm::parser::ExpressionParser expressionParser;
// Functor used for displaying error information.
struct ErrorHandler {
typedef qi::error_handler_result result_type;
template<typename T1, typename T2, typename T3, typename T4>
qi::error_handler_result operator()(T1 b, T2 e, T3 where, T4 const& what) const {
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<ErrorHandler> handler;
// A symbol table that is a mapping from identifiers that can be used in expressions to the expressions // A symbol table that is a mapping from identifiers that can be used in expressions to the expressions
// they are to be replaced with. // they are to be replaced with.
qi::symbols<char, storm::expressions::Expression> identifiers_; qi::symbols<char, storm::expressions::Expression> identifiers_;
@ -167,6 +153,9 @@ namespace storm {
std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula); std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::OptimizationDirection>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType); std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType); std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
}; };
FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : manager(manager->getSharedPointer()), grammar(new FormulaParserGrammar(manager)) { FormulaParser::FormulaParser(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : manager(manager->getSharedPointer()), grammar(new FormulaParserGrammar(manager)) {
@ -246,7 +235,7 @@ namespace storm {
grammar->addIdentifierExpression(identifier, expression); grammar->addIdentifierExpression(identifier, expression);
} }
FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), expressionParser(*manager, keywords_, true) {
FormulaParserGrammar::FormulaParserGrammar(std::shared_ptr<storm::expressions::ExpressionManager const> const& manager) : FormulaParserGrammar::base_type(start), expressionParser(*manager, keywords_, true, true) {
// Register all variables so we can parse them in the expressions. // Register all variables so we can parse them in the expressions.
for (auto variableTypePair : *manager) { for (auto variableTypePair : *manager) {
identifiers_.add(variableTypePair.first.getName(), variableTypePair.first); identifiers_.add(variableTypePair.first.getName(), variableTypePair.first);

6
src/parser/PrismParser.cpp

@ -4,6 +4,7 @@
#include "src/exceptions/InvalidArgumentException.h" #include "src/exceptions/InvalidArgumentException.h"
#include "src/exceptions/InvalidTypeException.h" #include "src/exceptions/InvalidTypeException.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h" #include "src/exceptions/WrongFormatException.h"
namespace storm { namespace storm {
@ -65,7 +66,7 @@ namespace storm {
return result; 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. // 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 %= 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"); identifier.name("identifier");
@ -199,6 +200,9 @@ namespace storm {
qi::on_success(commandDefinition, setLocationInfoFunction); qi::on_success(commandDefinition, setLocationInfoFunction);
qi::on_success(updateDefinition, setLocationInfoFunction); qi::on_success(updateDefinition, setLocationInfoFunction);
qi::on_success(assignmentDefinition, setLocationInfoFunction); qi::on_success(assignmentDefinition, setLocationInfoFunction);
// Enable error reporting.
qi::on_error<qi::fail>(start, handler(qi::_1, qi::_2, qi::_3, qi::_4));
} }
void PrismParser::moveToSecondRun() { void PrismParser::moveToSecondRun() {

5
src/parser/PrismParser.h

@ -11,8 +11,6 @@
#include "src/storage/prism/Program.h" #include "src/storage/prism/Program.h"
#include "src/storage/expressions/Expression.h" #include "src/storage/expressions/Expression.h"
#include "src/storage/expressions/Expressions.h" #include "src/storage/expressions/Expressions.h"
#include "src/utility/macros.h"
#include "src/exceptions/WrongFormatException.h"
namespace storm { namespace storm {
namespace expressions { namespace expressions {
@ -251,6 +249,9 @@ namespace storm {
storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Module createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const; storm::prism::Module createRenamedModule(std::string const& newModuleName, std::string const& oldModuleName, std::map<std::string, std::string> const& renaming, GlobalProgramInformation& globalProgramInformation) const;
storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const; storm::prism::Program createProgram(GlobalProgramInformation const& globalProgramInformation) const;
// An error handler function.
phoenix::function<SpiritErrorHandler> handler;
}; };
} // namespace parser } // namespace parser
} // namespace storm } // namespace storm

34
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<typename T1, typename T2, typename T3, typename T4>
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_ */

5
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 // 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). // 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()) { for (auto const& constant : this->getConstants()) {
if (constant.isDefined()) { if (constant.isDefined()) {
if (constant.getExpression().containsVariable(undefinedConstantVariables)) { if (constant.getExpression().containsVariable(undefinedConstantVariables)) {
return false;
undefinedConstantVariables.insert(constant.getExpressionVariable());
} }
} }
} }

Loading…
Cancel
Save