diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 0f7f877f1..4fa7a13d3 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -13,8 +13,6 @@ #include "modelchecker/GmmxxDtmcPrctlModelChecker.h" #include "modelchecker/GmmxxMdpPrctlModelChecker.h" -#include - namespace storm { namespace parser { @@ -41,13 +39,12 @@ std::list*> PrctlFileParser std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { - boost::algorithm::trim(line); - if ((line.length() == 0) || ((line[0] == '/') && (line[1] == '/'))) { - // ignore empty lines and lines starting with // - continue; - } PrctlParser parser(line); - result.push_back(parser.getFormula()); + if (!parser.parsedComment()) { + //lines containing comments will be skipped. + LOG4CPLUS_INFO(logger, "Parsed formula \"" + line + "\" into \"" + parser.getFormula()->toString() + "\""); + result.push_back(parser.getFormula()); + } } } diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 18f470660..446a6feb5 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -43,6 +43,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar"))[qi::_val = storm::property::GREATER] | (qi::lit("<="))[qi::_val = storm::property::LESS_EQUAL] | (qi::lit("<"))[qi::_val = storm::property::LESS]); + //Comment: Empty line or line starting with "//" comment = (qi::lit("//") >> *(qi::char_))[qi::_val = nullptr]; //This block defines rules for parsing state formulas @@ -70,7 +71,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar >(qi::_1, qi::_2, qi::_3, true)] | (qi::lit("P") >> qi::lit("max") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1, qi::_2, qi::_3, false)] | - (qi::lit("P") > comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = + (qi::lit("P") >> comparisonType > qi::double_ > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::new_ >(qi::_1, qi::_2, qi::_3)] ); @@ -142,11 +143,17 @@ struct PrctlParser::PrctlGrammar : qi::grammar>()]; - start = (comment | noBoundOperator | stateFormula) >> qi::eoi; + formula = (noBoundOperator | stateFormula); + formula.name("PRCTL formula"); + + start = (((formula) > (comment | qi::eps))[qi::_val = qi::_1] | + comment + ) > qi::eoi; start.name("PRCTL formula"); } qi::rule*(), Skipper> start; + qi::rule*(), Skipper> formula; qi::rule*(), Skipper> comment; qi::rule*(), Skipper> stateFormula; @@ -228,12 +235,5 @@ storm::parser::PrctlParser::PrctlParser(std::string formulaString) { 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 (positionIteratorBegin != positionIteratorEnd) { - throw storm::exceptions::WrongFormatException() << "Syntax error in formula"; - } - formula = result_pointer; } diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index 3778b862a..7e2b3d13d 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -38,6 +38,16 @@ class PrctlParser : Parser { return this->formula; } + /*! + * Checks whether the line which was parsed was a comment line; also returns true if the line was empty (as the semantics are + * the same) + * + * @return True if the parsed line consisted completely of a (valid) comment, false otherwise. + */ + bool parsedComment() { + return (formula == nullptr); + } + private: storm::property::prctl::AbstractPrctlFormula* formula;