From 834cb269a6381403d3d3ec7988d61018f3972ea9 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Mon, 22 Apr 2013 17:03:29 +0200 Subject: [PATCH] Minor corrections in code --- src/formula/abstract/RewardNoBoundOperator.h | 2 +- src/parser/LtlParser.cpp | 191 +++++++++++++++++++ src/parser/LtlParser.h | 60 ++++++ 3 files changed, 252 insertions(+), 1 deletion(-) create mode 100644 src/parser/LtlParser.cpp create mode 100644 src/parser/LtlParser.h diff --git a/src/formula/abstract/RewardNoBoundOperator.h b/src/formula/abstract/RewardNoBoundOperator.h index fdcc2c3ef..7c2bc4fbd 100644 --- a/src/formula/abstract/RewardNoBoundOperator.h +++ b/src/formula/abstract/RewardNoBoundOperator.h @@ -77,7 +77,7 @@ public: /*! * Destructor */ - virtual ~RewardBoundOperator() { + virtual ~RewardNoBoundOperator() { // Intentionally left empty } diff --git a/src/parser/LtlParser.cpp b/src/parser/LtlParser.cpp new file mode 100644 index 000000000..2ee16bf40 --- /dev/null +++ b/src/parser/LtlParser.cpp @@ -0,0 +1,191 @@ +/* + * LtlParser.cpp + * + * Created on: 22.04.2013 + * Author: thomas + */ + +#include "LtlParser.h" + +#include "src/utility/OsDetection.h" +#include "src/utility/ConstTemplates.h" + +// If the parser fails due to ill-formed data, this exception is thrown. +#include "src/exceptions/WrongFormatException.h" + +// Used for Boost spirit. +#include +#include +#include + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +// Needed for file IO. +#include +#include +#include + + +// Some typedefs and namespace definitions to reduce code size. +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + + + +namespace storm { + +namespace parser { + +template +struct LtlParser::LtlGrammar : qi::grammar*(), Skipper > { + LtlGrammar() : LtlGrammar::base_type(start) { + freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))]; + + //This block defines rules for parsing state formulas + ltlFormula %= orFormula; + ltlFormula.name("state formula"); + orFormula = andFormula[qi::_val = qi::_1] > *(qi::lit("|") > andFormula)[qi::_val = + phoenix::new_>(qi::_val, qi::_1)]; + orFormula.name("state formula"); + andFormula = notFormula[qi::_val = qi::_1] > *(qi::lit("&") > notFormula)[qi::_val = + phoenix::new_>(qi::_val, qi::_1)]; + andFormula.name("state formula"); + notFormula = atomicLtlFormula[qi::_val = qi::_1] | (qi::lit("!") > atomicLtlFormula)[qi::_val = + phoenix::new_>(qi::_1)]; + notFormula.name("state formula"); + + //This block defines rules for "atomic" state formulas + //(Propositions, probabilistic/reward formulas, and state formulas in brackets) + atomicLtlFormula %= pathFormula | atomicProposition | qi::lit("(") >> ltlFormula >> qi::lit(")"); + atomicLtlFormula.name("state formula"); + atomicProposition = (freeIdentifierName)[qi::_val = + phoenix::new_>(qi::_1)]; + atomicProposition.name("state formula"); + /*probabilisticBoundOperator = ( + (qi::lit("P") >> qi::lit(">") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::GREATER, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit(">=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::GREATER_EQUAL, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit("<") >> qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::LESS, qi::_1, qi::_2)] | + (qi::lit("P") >> qi::lit("<=") > qi::double_ > qi::lit("[") > LtlFormula > qi::lit("]"))[qi::_val = + phoenix::new_ >(storm::formula::LESS_EQUAL, qi::_1, qi::_2)] + ); + probabilisticBoundOperator.name("state formula");*/ + + //This block defines rules for parsing formulas with noBoundOperators + /*noBoundOperator = (probabilisticNoBoundOperator | rewardNoBoundOperator); + noBoundOperator.name("no bound operator"); + probabilisticNoBoundOperator = (qi::lit("P") >> qi::lit("=") >> qi::lit("?") >> qi::lit("[") >> LtlFormula >> qi::lit("]"))[qi::_val = + phoenix::new_ >(qi::_1)]; + probabilisticNoBoundOperator.name("no bound operator");*/ + + //This block defines rules for parsing probabilistic path formulas + pathFormula = (boundedEventually | eventually | globally | boundedUntil | until); + pathFormula.name("ltl formula"); + boundedEventually = (qi::lit("F") >> qi::lit("<=") > qi::int_ > ltlFormula)[qi::_val = + phoenix::new_>(qi::_2, qi::_1)]; + boundedEventually.name("ltl formula"); + eventually = (qi::lit("F") > ltlFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + eventually.name("ltl formula"); + globally = (qi::lit("G") > ltlFormula)[qi::_val = + phoenix::new_ >(qi::_1)]; + globally.name("ltl formula"); + boundedUntil = (ltlFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") >> qi::lit("<=") > qi::int_ > ltlFormula) + [qi::_val = phoenix::new_>(phoenix::bind(&storm::formula::ltl::AbstractLtlFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_3, qi::_2)]; + boundedUntil.name("ltl formula"); + until = (ltlFormula[qi::_a = phoenix::construct>>(qi::_1)] >> qi::lit("U") > ltlFormula)[qi::_val = + phoenix::new_>(phoenix::bind(&storm::formula::ltl::AbstractLtlFormula::clone, phoenix::bind(&std::shared_ptr>::get, qi::_a)), qi::_2)]; + until.name("ltl formula"); + + start = ltlFormula; + start.name("LTL formula"); + } + + qi::rule*(), Skipper> start; + + qi::rule*(), Skipper> ltlFormula; + qi::rule*(), Skipper> atomicLtlFormula; + + qi::rule*(), Skipper> andFormula; + qi::rule*(), Skipper> atomicProposition; + qi::rule*(), Skipper> orFormula; + qi::rule*(), Skipper> notFormula; + //qi::rule*(), Skipper> probabilisticBoundOperator; + + //qi::rule*(), Skipper> noBoundOperator; + //qi::rule*(), Skipper> probabilisticNoBoundOperator; + + qi::rule*(), Skipper> pathFormula; + qi::rule*(), Skipper> boundedEventually; + qi::rule*(), Skipper> eventually; + qi::rule*(), Skipper> globally; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> boundedUntil; + qi::rule*(), qi::locals< std::shared_ptr>>, Skipper> until; + + qi::rule freeIdentifierName; + +}; + +} //namespace storm +} //namespace parser + + +storm::parser::LtlParser::LtlParser(std::string formulaString) { + // Prepare iterators to input. + BaseIteratorType stringIteratorBegin = formulaString.begin(); + BaseIteratorType stringIteratorEnd = formulaString.end(); + PositionIteratorType positionIteratorBegin(stringIteratorBegin, stringIteratorEnd, formulaString); + PositionIteratorType positionIteratorEnd; + + + // Prepare resulting intermediate representation of input. + storm::formula::ltl::AbstractLtlFormula* result_pointer = nullptr; + + LtlGrammar grammar; + + // Now, parse the formula from the given string + try { + qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space, result_pointer); + } catch(const qi::expectation_failure& e) { + // If the parser expected content different than the one provided, display information + // about the location of the error. + const boost::spirit::classic::file_position_base& pos = e.first.get_position(); + + // Construct the error message including a caret display of the position in the + // erroneous line. + std::stringstream msg; + msg << pos.file << ", line " << pos.line << ", column " << pos.column + << ": parse error: expected " << e.what_ << std::endl << "\t" + << e.first.get_currentline() << std::endl << "\t"; + int i = 0; + for (i = 0; i < pos.column; ++i) { + msg << "-"; + } + msg << "^"; + for (; i < 80; ++i) { + msg << "-"; + } + msg << std::endl; + + std::cerr << msg.str(); + + // Now propagate exception. + throw storm::exceptions::WrongFormatException() << msg.str(); + } + + // The syntax can be so wrong that no rule can be matched at all + // In that case, no expectation failure is thrown, but the parser just returns nullptr + // Then, of course the result is not usable, hence we throw a WrongFormatException, too. + if (result_pointer == nullptr) { + throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; + } + + formula = result_pointer; +} + diff --git a/src/parser/LtlParser.h b/src/parser/LtlParser.h new file mode 100644 index 000000000..423bf5d0a --- /dev/null +++ b/src/parser/LtlParser.h @@ -0,0 +1,60 @@ +/* + * LtlParser.h + * + * Created on: 22.04.2013 + * Author: thomas + */ + +#ifndef STORM_PARSER_LTLPARSER_H_ +#define STORM_PARSER_LTLPARSER_H_ + +#include "Parser.h" +#include "src/formula/Ltl.h" + +namespace storm { +namespace parser { + +class LtlParser: public storm::parser::Parser { +public: +public: + /*! + * Reads a LTL formula from its string representation and parses it into a formula tree, consisting of + * classes in the namespace storm::formula. + * + * If the string could not be parsed successfully, it will throw a wrongFormatException. + * + * @param formulaString The string representation of the formula + * @throw wrongFormatException If the input could not be parsed successfully + */ + LtlParser(std::string formulaString); + + /*! + * @return a pointer to the parsed formula object + */ + storm::formula::ltl::AbstractLtlFormula* getFormula() { + return this->formula; + } + + /*! + * Destructor + * + * Does not delete the parsed formula! + */ + virtual ~LtlParser() { + // Intentionally left empty + // The formula is not deleted with the parser. + } + +private: + storm::formula::ltl::AbstractLtlFormula* formula; + + /*! + * Struct for the Ltl grammar, that Boost::Spirit uses to parse the formulas. + */ + template + struct LtlGrammar; +}; + +} /* namespace parser */ +} /* namespace storm */ +#endif /* STORM_PARSER_LTLPARSER_H_ */