From cac8a50e90d519bc7fbf555ce37108c0144cabea Mon Sep 17 00:00:00 2001 From: dehnert Date: Wed, 9 Apr 2014 11:31:58 +0200 Subject: [PATCH] Further work on PRISM grammar (commit to switch workplace). Former-commit-id: 2969fe50a364096b5ac88e75eb9ff4130f627dd4 --- src/parser/prismparser/PrismGrammar.cpp | 22 +++++---- src/parser/prismparser/PrismGrammar.h | 60 ++++++++++++++++--------- 2 files changed, 52 insertions(+), 30 deletions(-) diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp index 7c81b31ce..d52f2b9ae 100644 --- a/src/parser/prismparser/PrismGrammar.cpp +++ b/src/parser/prismparser/PrismGrammar.cpp @@ -58,9 +58,21 @@ namespace storm { // Parse a model type. modelTypeDefinition = modelType_; modelTypeDefinition.name("model type"); + + programHeader = modelTypeDefinition[phoenix::bind(&GlobalProgramInformation::modelType, qi::_r1) = qi::_1] + > *( undefinedConstantDefinition(qi::_r1) + | definedConstantDefinition(qi::_r1) + | formulaDefinition(qi::_r1) + | globalVariableDefinition(qi::_r1) + ); + programHeader.name("program header"); + + // This block defines all entities that are needed for parsing global variable definitions. + globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true))); + globalVariableDefinitionList.name("global variable declaration list"); // This block defines all entities that are needed for parsing constant definitions. - definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=") > expression > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedBooleanConstantDefinition = ((qi::lit("const") >> qi::lit("bool") >> identifier >> qi::lit("=")) > expression > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedBooleanConstantDefinition.name("defined boolean constant declaration"); definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; @@ -77,13 +89,10 @@ namespace storm { definedConstantDefinition.name("defined constant definition"); undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); undefinedConstantDefinition.name("undefined constant definition"); - constantDefinitionList = *(undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3) | definedConstantDefinition(qi::_r4, qi::_r5, qi::_r6)); - constantDefinitionList.name("constant definition list"); // Parse the ingredients of a probabilistic program. start = (qi::eps > - modelTypeDefinition > - constantDefinitionList(qi::_a, qi::_b, qi::_c, qi::_d, qi::_e, qi::_f) > + programHeader(qi::_a) > formulaDefinitionList > globalVariableDefinitionList(qi::_d) > moduleDefinitionList > @@ -162,9 +171,6 @@ namespace storm { moduleDefinitionList %= +(moduleDefinition | moduleRenaming); moduleDefinitionList.name("module list"); - // This block defines all entities that are needed for parsing global variable definitions. - globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true))); - globalVariableDefinitionList.name("global variable declaration list"); constantBooleanFormulaDefinition = (qi::lit("formula") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstBooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->constantBooleanFormulas_.add, qi::_1, qi::_2)]; constantBooleanFormulaDefinition.name("constant boolean formula definition"); diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h index 77a5406fc..785c85e9f 100644 --- a/src/parser/prismparser/PrismGrammar.h +++ b/src/parser/prismparser/PrismGrammar.h @@ -16,6 +16,7 @@ namespace qi = boost::spirit::qi; namespace phoenix = boost::phoenix; +namespace prism = storm::prism; typedef std::string::const_iterator BaseIteratorType; typedef boost::spirit::classic::position_iterator2 PositionIteratorType; @@ -28,13 +29,32 @@ typedef boost::spirit::unused_type Unused; #include "src/storage/prism/Program.h" #include "src/storage/expressions/Expression.h" -using namespace storm::prism; using namespace storm::expressions; namespace storm { namespace parser { namespace prism { - class PrismGrammar : public qi::grammar, std::set, std::set, std::map, std::map, std::map, std::map>, Skipper> { + class GlobalProgramInformation { + public: + // Default construct the header information. + GlobalProgramInformation() = default; + + // Members for all essential information that needs to be collected. + prism::Program::ModelType modelType; + std::set undefinedBooleanConstants; + std::set undefinedIntegerConstants; + std::set undefinedDoubleConstants; + std::map definedBooleanConstants; + std::map definedIntegerConstants; + std::map definedDoubleConstants; + std::map formulas; + std::map globalBooleanVariables; + std::map globalIntegerVariables; + std::map modules; + std::map rewardModels; + }; + + class PrismGrammar : public qi::grammar, Skipper> { public: /*! * Default constructor that creates an empty and functional grammar. @@ -43,30 +63,29 @@ namespace storm { private: // The starting point of the grammar. - // The locals are used for: (a) undefined boolean constants, (b) undefined integer constants, (c) undefined double constants, (d) defined boolean constants, (e) defined integer constants, (f) defined double constants, (g) module name to module map - qi::rule, std::set, std::set, std::map, std::map, std::map, std::map>, Skipper> start; + qi::rule, Skipper> start; // Rules for model type. qi::rule modelTypeDefinition; - // Rules for constant definitions. - qi::rule&, std::set&, std::set&, std::map&, std::map&, std::map&), Skipper> constantDefinitionList; - qi::rule&, std::set&, std::set&), Skipper> undefinedConstantDefinition; - qi::rule&, std::map&, std::map&), Skipper> definedConstantDefinition; - qi::rule&), Skipper> undefinedBooleanConstantDefinition; - qi::rule&), Skipper> undefinedIntegerConstantDefinition; - qi::rule&), Skipper> undefinedDoubleConstantDefinition; - qi::rule&), Skipper> definedBooleanConstantDefinition; - qi::rule&), Skipper> definedIntegerConstantDefinition; - qi::rule&), Skipper> definedDoubleConstantDefinition; + // Rules for parsing the program header. + qi::rule programHeader; + qi::rule undefinedConstantDefinition; + qi::rule definedConstantDefinition; + qi::rule undefinedBooleanConstantDefinition; + qi::rule undefinedIntegerConstantDefinition; + qi::rule undefinedDoubleConstantDefinition; + qi::rule definedBooleanConstantDefinition; + qi::rule definedIntegerConstantDefinition; + qi::rule definedDoubleConstantDefinition; // Rules for global variable definitions. - qi::rule&, std::map), Skipper> globalVariableDefinitionList; + qi::rule globalVariableDefinition; // Rules for modules definition. qi::rule(), Skipper> moduleDefinitionList; qi::rule, std::map>, Skipper> moduleDefinition; - qi::rule&), qi::locals>, Skipper> moduleRenaming; + qi::rule, Skipper> moduleRenaming; // Rules for variable definitions. qi::rule&, std::map&), Skipper> variableDefinition; @@ -81,18 +100,15 @@ namespace storm { qi::rule assignmentDefinition; // Rules for reward definitions. - qi::rule(), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule, std::vector>, Skipper> rewardModelDefinition; qi::rule stateRewardDefinition; qi::rule transitionRewardDefinition; // Rules for label definitions. - qi::rule(), Skipper> labelDefinitionList; - qi::rule&), Skipper> labelDefinition; + qi::rule labelDefinition; // Rules for formula definitions. - qi::rule(), Skipper> formulaDefinitionList; - qi::rule&), Skipper> formulaDefinition; + qi::rule formulaDefinition; // Rules for identifier parsing. qi::rule identifier;