diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index 13bf696f2..208550067 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -23,9 +23,10 @@ namespace parser { class PrctlFileParser: public storm::parser::PrctlParser { public: /*! - * Reads the formula from the given file and parses it into the formula tree + * Reads the formula from the given file and parses it into a formula tree, consisting of + * classes in the namespace storm::formula. * - * If the contents of the file could not be parsed successfully, it will throw a wrongFileFormatException. + * If the contents of the file could not be parsed successfully, it will throw a wrongFormatException. * * @param filename The name of the file to parse * @throw wrongFormatException If the input could not be parsed successfully @@ -43,4 +44,5 @@ public: } /* namespace parser */ } /* namespace storm */ + #endif /* STORM_PARSER_PRCTLFILEPARSER_H_ */ diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp index 57b9f7f25..f827794f1 100644 --- a/src/parser/PrctlParser.cpp +++ b/src/parser/PrctlParser.cpp @@ -49,7 +49,7 @@ struct PrctlParser::PrctlGrammar : qi::grammar>(qi::_1)]; notFormula.name("state formula"); - //This block defines rules for atomic state formulas + //This block defines rules for "atomic" state formulas //(Propositions, probabilistic/reward formulas, and state formulas in brackets) atomicStateFormula %= probabilisticBoundOperator | rewardBoundOperator | atomicProposition | qi::lit("(") >> stateFormula >> qi::lit(")"); atomicStateFormula.name("state formula"); diff --git a/src/parser/PrctlParser.h b/src/parser/PrctlParser.h index ac8e0ef78..41771cf3d 100644 --- a/src/parser/PrctlParser.h +++ b/src/parser/PrctlParser.h @@ -22,7 +22,8 @@ class PrctlParser : Parser { public: /*! - * Reads a PRCTL formula from its string representation and parses it into the formula tree + * Reads a PRCTL 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. * @@ -43,18 +44,25 @@ class PrctlParser : Parser /*! * Empty constructor. * - * Some subclasses do not get a formula string as input (E.g. PrctlFileFormat), hence they should not + * Some subclasses do not get a formula string as input (E.g. PrctlFileParser), hence they should not * call the usual constructor of this class. * - * However, this constructor should never be called directly (only as constructor of the super class), - * as it will not parse anything (and formula will point to nullptr then), so it is protected. + * However, this constructor should never be called directly (only during construction of an object of + * a subclass), as it will not parse anything (and formula will point to nullptr then); hence, it is + * protected. */ PrctlParser() { formula = nullptr; } /*! - * Parses a formula and stores the result in the field "formula" + * Does the actual parsing. + * + * Is to be called once in a constructor, and never from any other location. + * The function is not included in the constructor, as sub classes may use constructors + * that calculate the string representation of the formula (e.g. read it from a file), hence they + * cannot hand it over to a constructor of this class. + * * @param formula The string representation of the formula to parse */ void parse(std::string formula);