From bb37bc49f285474b234fdb6017722bca8fb927a2 Mon Sep 17 00:00:00 2001 From: gereon Date: Wed, 10 Apr 2013 18:58:59 +0200 Subject: [PATCH] Compiling version of PrismParser. --- src/parser/PrismParser.cpp | 429 +++--------------- src/parser/PrismParser.h | 111 ++++- .../PrismParser/BooleanExpressionGrammar.cpp | 55 +++ .../PrismParser/BooleanExpressionGrammar.h | 66 +++ .../ConstBooleanExpressionGrammar.cpp | 32 ++ .../ConstBooleanExpressionGrammar.h | 49 ++ .../ConstIntegerExpressionGrammar.cpp | 30 ++ .../ConstIntegerExpressionGrammar.h | 38 ++ src/parser/PrismParser/Includes.h | 35 ++ .../PrismParser/IntegerExpressionGrammar.cpp | 46 ++ .../PrismParser/IntegerExpressionGrammar.h | 61 +++ src/parser/PrismParser/UtilityGrammars.h | 69 +++ src/parser/PrismParser/VariableState.h | 96 ++++ 13 files changed, 745 insertions(+), 372 deletions(-) create mode 100644 src/parser/PrismParser/BooleanExpressionGrammar.cpp create mode 100644 src/parser/PrismParser/BooleanExpressionGrammar.h create mode 100644 src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp create mode 100644 src/parser/PrismParser/ConstBooleanExpressionGrammar.h create mode 100644 src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp create mode 100644 src/parser/PrismParser/ConstIntegerExpressionGrammar.h create mode 100644 src/parser/PrismParser/Includes.h create mode 100644 src/parser/PrismParser/IntegerExpressionGrammar.cpp create mode 100644 src/parser/PrismParser/IntegerExpressionGrammar.h create mode 100644 src/parser/PrismParser/UtilityGrammars.h create mode 100644 src/parser/PrismParser/VariableState.h diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index 8930f251e..e1aaacaab 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -7,6 +7,11 @@ #include "PrismParser.h" #include "src/utility/OsDetection.h" +#include "src/parser/PrismParser/VariableState.h" +#include "src/parser/PrismParser/IntegerExpressionGrammar.h" +#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" +#include "src/parser/PrismParser/BooleanExpressionGrammar.h" +#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFileFormatException.h" @@ -35,41 +40,25 @@ namespace storm { namespace parser { -using namespace storm::ir; -using namespace storm::ir::expressions; - -// The Boost spirit grammar used for parsing the input. -template -struct PrismParser::PrismGrammar : qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { - - /* - * The constructor of the grammar. It defines all rules of the grammar and the corresponding - * semantic actions that take care of constructing the intermediate representation during - * parsing. - * - * Note: The grammar takes care of some semantic checks already. For example, in places - * where we necessarily require a constant expression, this is enforced by not allowing - * variables as subexpressions. Also, variable names are by definition unique and it is - * ensured that variables and constants are properly declared. - * TODO: It should be ensured that updates of a command only refer to variables of the - * current module. - */ - PrismGrammar() : PrismGrammar::base_type(start), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) { +PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start) { + + this->state = std::shared_ptr(new storm::parser::prism::VariableState()); + storm::parser::prism::IntegerExpressionGrammar intExpr(this->state); + storm::parser::prism::ConstIntegerExpressionGrammar constIntExpr(this->state); + storm::parser::prism::BooleanExpressionGrammar boolExpr(this->state); + storm::parser::prism::ConstBooleanExpressionGrammar constBoolExpr(this->state); + // This rule defines all identifiers that have not been previously used. - identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&PrismGrammar::isIdentifier, this, qi::_1) ]; + identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isIdentifier, this->state.get(), qi::_1) ]; identifierName.name("identifier"); - freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&PrismGrammar::isFreeIdentifier, this, qi::_1) ]; + freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isFreeIdentifier, this->state.get(), qi::_1) ]; freeIdentifierName.name("unused identifier"); // This block defines all literal expressions. booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; booleanLiteralExpression.name("boolean literal"); - integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; - integerLiteralExpression.name("integer literal"); doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; doubleLiteralExpression.name("double literal"); - literalExpression %= (booleanLiteralExpression | integerLiteralExpression | doubleLiteralExpression); - literalExpression.name("literal"); // This block defines all expressions that are variables. @@ -80,38 +69,11 @@ struct PrismParser::PrismGrammar : qi::grammarstate->booleanConstants_ | booleanLiteralExpression); booleanConstantExpression.name("boolean constant or literal"); - integerConstantExpression %= (integerConstants_ | integerLiteralExpression); - integerConstantExpression.name("integer constant or literal"); - doubleConstantExpression %= (doubleConstants_ | doubleLiteralExpression); + doubleConstantExpression %= (this->state->doubleConstants_ | doubleLiteralExpression); doubleConstantExpression.name("double constant or literal"); - constantExpression %= (booleanConstantExpression | integerConstantExpression | doubleConstantExpression); - constantExpression.name("constant or literal"); - - // This block defines all expressions of integral type. - atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression); - atomicIntegerExpression.name("integer expression"); - integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))]; - integerMultExpression.name("integer expression"); - integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]]; - integerPlusExpression.name("integer expression"); - integerExpression %= integerPlusExpression; - integerExpression.name("integer expression"); - - // This block defines all expressions of integral type that are by syntax constant. That is, they are evaluable given the values for all constants. - constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); - constantAtomicIntegerExpression.name("constant integer expression"); - constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))]; - constantIntegerMultExpression.name("constant integer expression"); - constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]]; - constantIntegerPlusExpression.name("constant integer expression"); - constantIntegerExpression %= constantIntegerPlusExpression; - constantIntegerExpression.name("constant integer expression"); // This block defines all expressions of type double that are by syntax constant. That is, they are evaluable given the values for all constants. constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); @@ -123,48 +85,16 @@ struct PrismParser::PrismGrammar : qi::grammar> relations_ >> integerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; - relativeExpression.name("relative expression"); - atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression); - atomicBooleanExpression.name("boolean expression"); - notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, UnaryBooleanFunctionExpression::NOT))]; - notExpression.name("boolean expression"); - andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))]; - andExpression.name("boolean expression"); - orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::OR))]; - orExpression.name("boolean expression"); - booleanExpression %= orExpression; - booleanExpression.name("boolean expression"); - - // This block defines all expressions of type boolean that are by syntax constant. That is, they are evaluable given the values for all constants. - constantRelativeExpression = (constantIntegerExpression >> relations_ >> constantIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; - constantRelativeExpression.name("constant boolean expression"); - constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); - constantAtomicBooleanExpression.name("constant boolean expression"); - constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, UnaryBooleanFunctionExpression::NOT))]; - constantNotExpression.name("constant boolean expression"); - constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))]; - constantAndExpression.name("constant boolean expression"); - constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::OR))]; - constantOrExpression.name("constant boolean expression"); - constantBooleanExpression %= constantOrExpression; - constantBooleanExpression.name("constant boolean expression"); - - // This block defines the general root of all expressions. Most of the time, however, you may want to start with a more specialized rule. - expression %= (booleanExpression | integerExpression | constantDoubleExpression); - expression.name("expression"); - // This block defines all entities that are needed for parsing labels. - labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> booleanExpression >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2)), phoenix::bind(labelNames_.add, qi::_1, qi::_1)]; + labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> boolExpr >> qi::lit(";"))[phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_2)), phoenix::bind(this->state->labelNames_.add, qi::_1, qi::_1)]; labelDefinition.name("label declaration"); labelDefinitionList %= *labelDefinition(qi::_r1); labelDefinitionList.name("label declaration list"); // This block defines all entities that are needed for parsing a reward model. - stateRewardDefinition = (booleanExpression > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + stateRewardDefinition = (boolExpr > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; stateRewardDefinition.name("state reward definition"); - transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > boolExpr > qi::lit(":") > constantDoubleExpression > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; transitionRewardDefinition.name("transition reward definition"); rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > freeIdentifierName > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))[phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_a, qi::_b)))]; rewardDefinition.name("reward definition"); @@ -172,50 +102,45 @@ struct PrismParser::PrismGrammar : qi::grammarstate->booleanVariableNames_; booleanVariableName.name("boolean variable"); - integerVariableName %= integerVariableNames_; + integerVariableName %= this->state->integerVariableNames_; integerVariableName.name("integer variable"); - commandName %= commandNames_; + commandName %= this->state->commandNames_; commandName.name("command name"); - unassignedLocalBooleanVariableName %= localBooleanVariables_ - assignedLocalBooleanVariables_; + unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); - unassignedLocalIntegerVariableName %= localIntegerVariables_ - assignedLocalIntegerVariables_; + unassignedLocalIntegerVariableName %= this->state->localIntegerVariables_ - this->state->assignedLocalIntegerVariables_; unassignedLocalIntegerVariableName.name("unassigned local integer variable"); // This block defines all entities that are needed for parsing a single command. - assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > integerExpression > qi::lit(")"))[phoenix::bind(assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > booleanExpression > qi::lit(")"))[phoenix::bind(assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))]; + assignmentDefinition = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > intExpr > qi::lit(")"))[phoenix::bind(this->state->assignedLocalIntegerVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))] | (qi::lit("(") > unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > boolExpr > qi::lit(")"))[phoenix::bind(this->state->assignedLocalBooleanVariables_.add, qi::_1, qi::_1), phoenix::insert(qi::_r1, phoenix::construct>(qi::_1, phoenix::construct(qi::_1, qi::_2)))]; assignmentDefinition.name("assignment"); assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&"; assignmentDefinitionList.name("assignment list"); - updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b)]; + updateDefinition = (constantDoubleExpression > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedLocalBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedLocalIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b)]; updateDefinition.name("update"); updateListDefinition = +updateDefinition % "+"; updateListDefinition.name("update list"); - commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > booleanExpression > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; + commandDefinition = (qi::lit("[") > -((freeIdentifierName[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]) > qi::lit("]") > boolExpr > qi::lit("->") > updateListDefinition > qi::lit(";"))[qi::_val = phoenix::construct(qi::_a, qi::_2, qi::_3)]; commandDefinition.name("command"); // This block defines all entities that are needed for parsing variable definitions. - booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constBoolExpr[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ - phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), - phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextBooleanVariableIndex))), - qi::_a = phoenix::construct>(phoenix::new_(BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)), - phoenix::bind(booleanVariables_.add, qi::_1, qi::_a), - phoenix::bind(booleanVariableNames_.add, qi::_1, qi::_1), - phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), - phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1 + //qi::_a = phoenix::bind(&VariableState::addBooleanVariable, *this->state.get(), qi::_1), + qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addBooleanVariable, *this->state, qi::_1, qi::_b), + phoenix::push_back(qi::_r1, phoenix::construct(qi::_a, phoenix::val(qi::_1), qi::_b)), + phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, qi::_a)), + phoenix::bind(this->state->localBooleanVariables_.add, qi::_1, qi::_1) ]; booleanVariableDefinition.name("boolean variable declaration"); - integerVariableDefinition = (freeIdentifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") > constIntExpr > qi::lit("..") > constIntExpr > qi::lit("]") > -(qi::lit("init") > constIntExpr[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ - phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), - phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), - qi::_a = phoenix::construct>(phoenix::new_(BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3)), - phoenix::bind(integerVariables_.add, qi::_1, qi::_a), - phoenix::bind(integerVariableNames_.add, qi::_1, qi::_1), - phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), - phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1 + qi::_a = phoenix::bind(&storm::parser::prism::VariableState::addIntegerVariable, *this->state, qi::_1, qi::_2, qi::_3, qi::_b), + phoenix::push_back(qi::_r1, phoenix::construct(qi::_a, qi::_1, qi::_2, qi::_3, qi::_b)), + phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, qi::_a)), + phoenix::bind(this->state->localIntegerVariables_.add, qi::_1, qi::_1) ]; integerVariableDefinition.name("integer variable declaration"); variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3) | integerVariableDefinition(qi::_r2, qi::_r4)); @@ -223,42 +148,44 @@ struct PrismParser::PrismGrammar : qi::grammar> freeIdentifierName - [phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] + [phoenix::clear(phoenix::ref(this->state->localBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->localIntegerVariables_))] >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) [ - phoenix::bind(moduleNames_.add, qi::_1, qi::_1), + phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2), - phoenix::bind(moduleMap_.add, qi::_1, qi::_val) + phoenix::bind(this->state->moduleMap_.add, qi::_1, qi::_val) ]; Module const * (qi::symbols::*moduleFinder)(const std::string&) const = &qi::symbols::find; moduleDefinition.name("module"); moduleRenaming = (qi::lit("module") >> freeIdentifierName >> qi::lit("=") - > moduleNames_ > qi::lit("[") > *( + > this->state->moduleNames_ > qi::lit("[") > *( (identifierName > qi::lit("=") > identifierName >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct>(qi::_1, qi::_2))] ) > qi::lit("]") > qi::lit("endmodule")) [ - phoenix::bind(moduleNames_.add, qi::_1, qi::_1), - qi::_val = phoenix::construct(*phoenix::bind(moduleFinder, moduleMap_, qi::_2), qi::_1, qi::_a, VariableAdder(this)), - phoenix::bind(moduleMap_.add, qi::_1, qi::_val) + phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1), + qi::_val = phoenix::construct(*phoenix::bind(moduleFinder, this->state->moduleMap_, qi::_2), qi::_1, qi::_a, this->state), + phoenix::bind(this->state->moduleMap_.add, qi::_1, qi::_val) ]; moduleRenaming.name("renamed module"); moduleDefinitionList %= +(moduleDefinition | moduleRenaming); moduleDefinitionList.name("module list"); - + + integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + integerLiteralExpression.name("integer literal"); // This block defines all entities that are needed for parsing constant definitions. - definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > qi::lit(";"))[phoenix::bind(booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> freeIdentifierName >> qi::lit("=") > booleanLiteralExpression > 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") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > qi::lit(";"))[phoenix::bind(integerConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> freeIdentifierName >> qi::lit("=") > integerLiteralExpression > 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]; definedIntegerConstantDefinition.name("defined integer constant declaration"); - definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > doubleLiteralExpression > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; definedDoubleConstantDefinition.name("defined double constant declaration"); - undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; + undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); - undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(integerConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; + undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedIntegerConstantDefinition.name("undefined integer constant declaration"); - undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(allConstantNames_.add, qi::_1, qi::_1)]; + undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > freeIdentifierName > qi::lit(";"))[qi::_a = phoenix::construct>(phoenix::new_(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedDoubleConstantDefinition.name("undefined double constant declaration"); definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition); definedConstantDefinition.name("defined constant declaration"); @@ -274,248 +201,19 @@ struct PrismParser::PrismGrammar : qi::grammar lower, const std::shared_ptr upper, const std::shared_ptr init) const { - std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, grammar->nextIntegerVariableIndex, name, lower, upper)); - grammar->integerVariables_.add(name, varExpr); - grammar->integerVariableNames_.add(name, name); - grammar->nextIntegerVariableIndex++; - return grammar->nextIntegerVariableIndex-1; - } - - uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) const { - std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, grammar->nextBooleanVariableIndex, name)); - grammar->integerVariables_.add(name, varExpr); - grammar->integerVariableNames_.add(name, name); - grammar->nextBooleanVariableIndex++; - return grammar->nextBooleanVariableIndex-1; - } - }; - - void prepareForSecondRun() { + void PrismParser::PrismGrammar::prepareForSecondRun() { // Clear constants. - integerConstants_.clear(); - booleanConstants_.clear(); - doubleConstants_.clear(); - allConstantNames_.clear(); - // Reset variable indices. - nextIntegerVariableIndex = 0; - nextBooleanVariableIndex = 0; - // Clear module names - moduleNames_.clear(); + storm::parser::prism::IntegerExpressionGrammar intExpr(this->state); + storm::parser::prism::ConstIntegerExpressionGrammar constIntExpr(this->state); + + this->state->prepareForSecondRun(); // Override variable expressions: only allow declared variables. - integerVariableExpression %= integerVariables_; + integerVariableExpression %= this->state->integerVariables_; integerVariableExpression.name("integer variable"); - booleanVariableExpression %= booleanVariables_; + booleanVariableExpression %= this->state->booleanVariables_; booleanVariableExpression.name("boolean variable"); - - // Override variable definition: don't register variables again globally. - booleanVariableDefinition = (identifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > constantBooleanExpression) > qi::lit(";")) - [ - phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextBooleanVariableIndex), phoenix::val(qi::_1), qi::_b)), - phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextBooleanVariableIndex))), - qi::_a = phoenix::construct>(phoenix::new_(BaseExpression::bool_, phoenix::ref(nextBooleanVariableIndex), qi::_1)), - phoenix::bind(localBooleanVariables_.add, qi::_1, qi::_1), - phoenix::ref(nextBooleanVariableIndex) = phoenix::ref(nextBooleanVariableIndex) + 1 - ]; - booleanVariableDefinition.name("boolean variable declaration"); - - integerVariableDefinition = (identifierName > qi::lit(":") > qi::lit("[") > constantIntegerExpression > qi::lit("..") > constantIntegerExpression > qi::lit("]") > -(qi::lit("init") > constantIntegerExpression) > qi::lit(";")) - [ - phoenix::push_back(qi::_r1, phoenix::construct(phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3, qi::_b)), - phoenix::insert(qi::_r2, phoenix::construct>(qi::_1, phoenix::ref(nextIntegerVariableIndex))), - qi::_a = phoenix::construct>(phoenix::new_(BaseExpression::int_, phoenix::ref(nextIntegerVariableIndex), qi::_1, qi::_2, qi::_3)), - phoenix::bind(localIntegerVariables_.add, qi::_1, qi::_1), - phoenix::ref(nextIntegerVariableIndex) = phoenix::ref(nextIntegerVariableIndex) + 1 - ]; - integerVariableDefinition.name("integer variable declaration"); } - - // The starting point of the grammar. - qi::rule>, std::map>, std::map>, std::map, std::map>>, Skipper> start; - qi::rule modelTypeDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; - qi::rule(), Skipper> moduleDefinitionList; - - // Rules for module definition. - qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; - qi::rule>, Skipper> moduleRenaming; - - // Rules for variable definitions. - qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; - qi::rule&, std::map&), qi::locals, std::shared_ptr>, Skipper> booleanVariableDefinition; - qi::rule&, std::map&), qi::locals, std::shared_ptr>, Skipper> integerVariableDefinition; - - // Rules for command definitions. - qi::rule, Skipper> commandDefinition; - qi::rule(), Skipper> updateListDefinition; - qi::rule, std::map>, Skipper> updateDefinition; - qi::rule&, std::map&), Skipper> assignmentDefinitionList; - qi::rule&, std::map&), Skipper> assignmentDefinition; - - // Rules for variable/command names. - qi::rule integerVariableName; - qi::rule booleanVariableName; - qi::rule commandName; - qi::rule unassignedLocalBooleanVariableName; - qi::rule unassignedLocalIntegerVariableName; - - // Rules for reward definitions. - qi::rule&), Skipper> rewardDefinitionList; - qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; - qi::rule stateRewardDefinition; - qi::rule, Skipper> transitionRewardDefinition; - - // Rules for label definitions. - qi::rule>&), Skipper> labelDefinitionList; - qi::rule>&), Skipper> labelDefinition; - - // Rules for constant definitions. - qi::rule(), Skipper> constantDefinition; - qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; - qi::rule(), Skipper> definedConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; - qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; - qi::rule(), Skipper> definedBooleanConstantDefinition; - qi::rule(), Skipper> definedIntegerConstantDefinition; - qi::rule(), Skipper> definedDoubleConstantDefinition; - - qi::rule freeIdentifierName; - qi::rule identifierName; - - // The starting point for arbitrary expressions. - qi::rule(), Skipper> expression; - - // Rules with boolean result type. - qi::rule(), Skipper> booleanExpression; - qi::rule(), Skipper> orExpression; - qi::rule(), Skipper> andExpression; - qi::rule(), Skipper> notExpression; - qi::rule(), Skipper> atomicBooleanExpression; - qi::rule(), Skipper> relativeExpression; - qi::rule(), Skipper> constantBooleanExpression; - qi::rule(), Skipper> constantOrExpression; - qi::rule(), Skipper> constantAndExpression; - qi::rule(), Skipper> constantNotExpression; - qi::rule(), Skipper> constantAtomicBooleanExpression; - qi::rule(), Skipper> constantRelativeExpression; - - // Rules with integer result type. - qi::rule(), Skipper> integerExpression; - qi::rule(), qi::locals, Skipper> integerPlusExpression; - qi::rule(), Skipper> integerMultExpression; - qi::rule(), Skipper> atomicIntegerExpression; - qi::rule(), Skipper> constantIntegerExpression; - qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; - qi::rule(), Skipper> constantIntegerMultExpression; - qi::rule(), Skipper> constantAtomicIntegerExpression; - - // Rules with double result type. - qi::rule(), Skipper> constantDoubleExpression; - qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; - qi::rule(), qi::locals, Skipper> constantDoubleMultExpression; - qi::rule(), Skipper> constantAtomicDoubleExpression; - - // Rules for variable recognition. - qi::rule(), Skipper> variableExpression; - qi::rule(), Skipper> booleanVariableExpression; - qi::rule(), Skipper> booleanVariableCreatorExpression; - qi::rule(), Skipper> integerVariableExpression; - qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; - - // Rules for constant recognition. - qi::rule(), Skipper> constantExpression; - qi::rule(), Skipper> booleanConstantExpression; - qi::rule(), Skipper> integerConstantExpression; - qi::rule(), Skipper> doubleConstantExpression; - - // Rules for literal recognition. - qi::rule(), Skipper> literalExpression; - qi::rule(), Skipper> booleanLiteralExpression; - qi::rule(), Skipper> integerLiteralExpression; - qi::rule(), Skipper> doubleLiteralExpression; - - // A structure defining the keywords that are not allowed to be chosen as identifiers. - struct keywordsStruct : qi::symbols { - keywordsStruct() { - add - ("dtmc", 1) - ("ctmc", 2) - ("mdp", 3) - ("ctmdp", 4) - ("const", 5) - ("int", 6) - ("bool", 7) - ("module", 8) - ("endmodule", 9) - ("rewards", 10) - ("endrewards", 11) - ("true", 12) - ("false", 13) - ; - } - } keywords_; - - // A structure mapping the textual representation of a model type to the model type - // representation of the intermediate representation. - struct modelTypeStruct : qi::symbols { - modelTypeStruct() { - add - ("dtmc", Program::ModelType::DTMC) - ("ctmc", Program::ModelType::CTMC) - ("mdp", Program::ModelType::MDP) - ("ctmdp", Program::ModelType::CTMDP) - ; - } - } modelType_; - - // A structure mapping the textual representation of a binary relation to the representation - // of the intermediate representation. - struct relationalOperatorStruct : qi::symbols { - relationalOperatorStruct() { - add - ("=", BinaryRelationExpression::EQUAL) - ("<", BinaryRelationExpression::LESS) - ("<=", BinaryRelationExpression::LESS_OR_EQUAL) - (">", BinaryRelationExpression::GREATER) - (">=", BinaryRelationExpression::GREATER_OR_EQUAL) - ; - } - } relations_; - - // Used for indexing the variables. - uint_fast64_t nextBooleanVariableIndex; - uint_fast64_t nextIntegerVariableIndex; - - // Structures mapping variable and constant names to the corresponding expression nodes of - // the intermediate representation. - struct qi::symbols> integerVariables_, booleanVariables_; - struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; - struct qi::symbols moduleMap_; - - // A structure representing the identity function over identifier names. - struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, - localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; -}; /*! * Opens the given file for parsing, invokes the helper function to parse the actual content and @@ -564,13 +262,14 @@ std::shared_ptr PrismParser::parse(std::istream& inputStream // In order to instantiate the grammar, we have to pass the type of the skipping parser. // As this is more complex, we let Boost figure out the actual type for us. - PrismGrammar> *(qi::char_ - qi::eol) >> qi::eol)> grammar; + PrismGrammar grammar; try { // Now parse the content using phrase_parse in order to be able to supply a skipping parser. // First run. qi::phrase_parse(positionIteratorBegin, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); grammar.prepareForSecondRun(); result = std::shared_ptr(new storm::ir::Program()); + std::cout << "Now we start the second run..." << std::endl; // Second run. qi::phrase_parse(positionIteratorBegin2, positionIteratorEnd, grammar, boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol, *result); std::cout << "Here is the parsed grammar: " << std::endl << result->toString() << std::endl; diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 1fca04c55..86b7eb4d7 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -10,6 +10,9 @@ // All classes of the intermediate representation are used. #include "src/ir/IR.h" +#include "src/parser/PrismParser/Includes.h" +#include "src/parser/PrismParser/UtilityGrammars.h" +#include "src/parser/PrismParser/VariableState.h" // Used for file input. #include @@ -19,6 +22,9 @@ namespace storm { namespace parser { +using namespace storm::ir; +using namespace storm::ir::expressions; + /*! * This class parses the format of the PRISM model checker into an intermediate representation. */ @@ -32,6 +38,104 @@ public: */ std::shared_ptr parseFile(std::string const& filename) const; + /*! + * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of + * the input that complies with the PRISM syntax. + */ + class PrismGrammar : public qi::grammar>, std::map>, std::map>, std::map, std::map>>, Skipper> { + public: + PrismGrammar(); + void prepareForSecondRun(); + + private: + + std::shared_ptr state; + + // The starting point of the grammar. + qi::rule>, std::map>, std::map>, std::map, std::map>>, Skipper> start; + qi::rule modelTypeDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> constantDefinitionList; + qi::rule(), Skipper> moduleDefinitionList; + + // Rules for module definition. + qi::rule, std::vector, std::map, std::map>, Skipper> moduleDefinition; + qi::rule>, Skipper> moduleRenaming; + + // Rules for variable definitions. + qi::rule&, std::vector&, std::map&, std::map&), Skipper> variableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> booleanVariableDefinition; + qi::rule&, std::map&), qi::locals>, Skipper> integerVariableDefinition; + + // Rules for command definitions. + qi::rule, Skipper> commandDefinition; + qi::rule(), Skipper> updateListDefinition; + qi::rule, std::map>, Skipper> updateDefinition; + qi::rule&, std::map&), Skipper> assignmentDefinitionList; + qi::rule&, std::map&), Skipper> assignmentDefinition; + + // Rules for variable/command names. + qi::rule integerVariableName; + qi::rule booleanVariableName; + qi::rule commandName; + qi::rule unassignedLocalBooleanVariableName; + qi::rule unassignedLocalIntegerVariableName; + + // Rules for reward definitions. + qi::rule&), Skipper> rewardDefinitionList; + qi::rule&), qi::locals, std::vector>, Skipper> rewardDefinition; + qi::rule stateRewardDefinition; + qi::rule, Skipper> transitionRewardDefinition; + + // Rules for label definitions. + qi::rule>&), Skipper> labelDefinitionList; + qi::rule>&), Skipper> labelDefinition; + + // Rules for constant definitions. + qi::rule(), Skipper> integerLiteralExpression; + qi::rule(), Skipper> constantDefinition; + qi::rule>&, std::map>&, std::map>&), Skipper> undefinedConstantDefinition; + qi::rule(), Skipper> definedConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedBooleanConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedIntegerConstantDefinition; + qi::rule>&), qi::locals>, Skipper> undefinedDoubleConstantDefinition; + qi::rule(), Skipper> definedBooleanConstantDefinition; + qi::rule(), Skipper> definedIntegerConstantDefinition; + qi::rule(), Skipper> definedDoubleConstantDefinition; + + qi::rule freeIdentifierName; + qi::rule identifierName; + + // The starting point for arbitrary expressions. + qi::rule(), Skipper> expression; + // Rules with double result type. + qi::rule(), Skipper> constantDoubleExpression; + qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; + qi::rule(), qi::locals, Skipper> constantDoubleMultExpression; + qi::rule(), Skipper> constantAtomicDoubleExpression; + + // Rules for variable recognition. + qi::rule(), Skipper> booleanVariableExpression; + qi::rule(), Skipper> booleanVariableCreatorExpression; + qi::rule(), Skipper> integerVariableExpression; + qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; + + // Rules for constant recognition. + qi::rule(), Skipper> constantExpression; + qi::rule(), Skipper> booleanConstantExpression; + qi::rule(), Skipper> integerConstantExpression; + qi::rule(), Skipper> doubleConstantExpression; + + // Rules for literal recognition. + qi::rule(), Skipper> literalExpression; + qi::rule(), Skipper> booleanLiteralExpression; + qi::rule(), Skipper> doubleLiteralExpression; + + storm::parser::prism::keywordsStruct keywords_; + storm::parser::prism::modelTypeStruct modelType_; + storm::parser::prism::relationalOperatorStruct relations_; + + }; + private: /*! * Parses the given input stream into the intermediate representation assuming it complies with @@ -41,13 +145,6 @@ private: * @return a shared pointer to the intermediate representation of the PRISM file. */ std::shared_ptr parse(std::istream& inputStream, std::string const& filename) const; - - /*! - * The Boost spirit grammar for the PRISM language. Returns the intermediate representation of - * the input that complies with the PRISM syntax. - */ - template - struct PrismGrammar; }; } // namespace parser diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.cpp b/src/parser/PrismParser/BooleanExpressionGrammar.cpp new file mode 100644 index 000000000..3ad148c08 --- /dev/null +++ b/src/parser/PrismParser/BooleanExpressionGrammar.cpp @@ -0,0 +1,55 @@ +#include "BooleanExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + +BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr& state) + : BooleanExpressionGrammar::base_type(booleanExpression), state(state) { + + IntegerExpressionGrammar intExpr(this->state); + + // This rule defines all identifiers that have not been previously used. + identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isIdentifier, this->state.get(), qi::_1) ]; + identifierName.name("identifier"); + freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&storm::parser::prism::VariableState::isFreeIdentifier, this->state.get(), qi::_1) ]; + freeIdentifierName.name("unused identifier"); + + // This block defines all literal expressions. + booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + booleanLiteralExpression.name("boolean literal"); + + + // This block defines all expressions that are variables. + std::shared_ptr boolvarexpr = std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "bool", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); + booleanVariableExpression = identifierName[qi::_val = boolvarexpr]; + booleanVariableExpression.name("boolean variable"); + + // This block defines all atomic expressions that are constant, i.e. literals and constants. + booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression); + booleanConstantExpression.name("boolean constant or literal"); + + // This block defines all expressions of type boolean. + relativeExpression = (intExpr >> relations_ >> intExpr)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; + relativeExpression.name("relative expression"); + atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | booleanConstantExpression); + atomicBooleanExpression.name("boolean expression"); + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, UnaryBooleanFunctionExpression::NOT))]; + notExpression.name("boolean expression"); + andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))]; + andExpression.name("boolean expression"); + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::OR))]; + orExpression.name("boolean expression"); + booleanExpression %= orExpression; + booleanExpression.name("boolean expression"); + + // This block defines auxiliary entities that are used to check whether a certain variable exist. + booleanVariableName %= this->state->booleanVariableNames_; + booleanVariableName.name("boolean variable"); + unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; + unassignedLocalBooleanVariableName.name("unassigned local boolean variable"); + } + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.h b/src/parser/PrismParser/BooleanExpressionGrammar.h new file mode 100644 index 000000000..db5ad0951 --- /dev/null +++ b/src/parser/PrismParser/BooleanExpressionGrammar.h @@ -0,0 +1,66 @@ +/* + * File: BooleanExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 6:27 PM + */ + +#ifndef BOOLEANEXPRESSIONGRAMMAR_H +#define BOOLEANEXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" +#include "IntegerExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + +class BooleanExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +public: + BooleanExpressionGrammar(std::shared_ptr& state); + +private: + // Rules for variable/command names. + qi::rule integerVariableName; + qi::rule booleanVariableName; + qi::rule unassignedLocalBooleanVariableName; + qi::rule unassignedLocalIntegerVariableName; + + qi::rule freeIdentifierName; + qi::rule identifierName; + + // The starting point for arbitrary expressions. + qi::rule(), Skipper> expression; + + // Rules with boolean result type. + qi::rule(), Skipper, Skipper> booleanExpression; + qi::rule(), Skipper> orExpression; + qi::rule(), Skipper> andExpression; + qi::rule(), Skipper> notExpression; + qi::rule(), Skipper> atomicBooleanExpression; + qi::rule(), Skipper> relativeExpression; + + // Rules for variable recognition. + qi::rule(), Skipper> booleanVariableExpression; + qi::rule(), Skipper> booleanVariableCreatorExpression; + + // Rules for constant recognition. + qi::rule(), Skipper> booleanConstantExpression; + + // Rules for literal recognition. + qi::rule(), Skipper> booleanLiteralExpression; + + // A structure mapping the textual representation of a binary relation to the representation + // of the intermediate representation. + storm::parser::prism::relationalOperatorStruct relations_; + + std::shared_ptr state; +}; + + +} +} +} + +#endif /* BOOLEANEXPRESSIONGRAMMAR_H */ diff --git a/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp b/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp new file mode 100644 index 000000000..53a5f5a96 --- /dev/null +++ b/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp @@ -0,0 +1,32 @@ +#include "ConstBooleanExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + + ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr& state) + : ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), state(state) { + + ConstIntegerExpressionGrammar constIntExpr(this->state); + + booleanLiteralExpression = qi::bool_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + booleanLiteralExpression.name("boolean literal"); + booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression); + booleanConstantExpression.name("boolean constant or literal"); + constantRelativeExpression = (constIntExpr >> relations_ >> constIntExpr)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, qi::_3, qi::_2))]; + constantRelativeExpression.name("constant boolean expression"); + constantAtomicBooleanExpression %= (constantRelativeExpression | qi::lit("(") >> constantBooleanExpression >> qi::lit(")") | booleanLiteralExpression | booleanConstantExpression); + constantAtomicBooleanExpression.name("constant boolean expression"); + constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_1, UnaryBooleanFunctionExpression::NOT))]; + constantNotExpression.name("constant boolean expression"); + constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::AND))]; + constantAndExpression.name("constant boolean expression"); + constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::construct>(phoenix::new_(qi::_val, qi::_1, BinaryBooleanFunctionExpression::OR))]; + constantOrExpression.name("constant boolean expression"); + constantBooleanExpression %= constantOrExpression; + constantBooleanExpression.name("constant boolean expression"); + } +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/ConstBooleanExpressionGrammar.h b/src/parser/PrismParser/ConstBooleanExpressionGrammar.h new file mode 100644 index 000000000..24166035e --- /dev/null +++ b/src/parser/PrismParser/ConstBooleanExpressionGrammar.h @@ -0,0 +1,49 @@ +/* + * File: ConstBooleanExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 6:34 PM + */ + +#ifndef CONSTBOOLEANEXPRESSIONGRAMMAR_H +#define CONSTBOOLEANEXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "ConstIntegerExpressionGrammar.h" +#include "VariableState.h" +#include "UtilityGrammars.h" + +namespace storm { +namespace parser { +namespace prism { + +class ConstBooleanExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +public: + ConstBooleanExpressionGrammar(std::shared_ptr& state); + +private: + + qi::rule(), Skipper> booleanLiteralExpression; + qi::rule(), Skipper> booleanConstantExpression; + qi::rule(), Skipper> relativeExpression; + qi::rule(), Skipper, Skipper> constantBooleanExpression; + qi::rule(), Skipper> constantOrExpression; + qi::rule(), Skipper> constantAndExpression; + qi::rule(), Skipper> constantNotExpression; + qi::rule(), Skipper> constantAtomicBooleanExpression; + qi::rule(), Skipper> constantRelativeExpression; + + + storm::parser::prism::relationalOperatorStruct relations_; + + std::shared_ptr state; + +}; + + +} +} +} + +#endif /* CONSTBOOLEANEXPRESSIONGRAMMAR_H */ + diff --git a/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp b/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp new file mode 100644 index 000000000..ef9d8c91f --- /dev/null +++ b/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp @@ -0,0 +1,30 @@ +#include "ConstIntegerExpressionGrammar.h" + + +namespace storm { +namespace parser { +namespace prism { + +ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr& state) + : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), state(state) { + + integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + integerLiteralExpression.name("integer literal"); + integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); + integerConstantExpression.name("integer constant or literal"); + + constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression); + constantAtomicIntegerExpression.name("constant integer expression"); + constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))]; + constantIntegerMultExpression.name("constant integer expression"); + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]]; + constantIntegerPlusExpression.name("constant integer expression"); + constantIntegerExpression %= constantIntegerPlusExpression; + constantIntegerExpression.name("constant integer expression"); + + +} + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/ConstIntegerExpressionGrammar.h b/src/parser/PrismParser/ConstIntegerExpressionGrammar.h new file mode 100644 index 000000000..2c1a3420c --- /dev/null +++ b/src/parser/PrismParser/ConstIntegerExpressionGrammar.h @@ -0,0 +1,38 @@ +/* + * File: ConstIntegerExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 6:02 PM + */ + +#ifndef CONSTINTEGEREXPRESSIONGRAMMAR_H +#define CONSTINTEGEREXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" + +namespace storm { +namespace parser { +namespace prism { + +class ConstIntegerExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +public: + ConstIntegerExpressionGrammar(std::shared_ptr& state); + +private: + qi::rule(), Skipper> integerLiteralExpression; + qi::rule(), Skipper> integerConstantExpression; + qi::rule(), Skipper, Skipper> constantIntegerExpression; + qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; + qi::rule(), Skipper> constantIntegerMultExpression; + qi::rule(), Skipper> constantAtomicIntegerExpression; + + std::shared_ptr state; +}; + + +} +} +} + +#endif /* CONSTINTEGEREXPRESSIONGRAMMAR_H */ diff --git a/src/parser/PrismParser/Includes.h b/src/parser/PrismParser/Includes.h new file mode 100644 index 000000000..39eb5a450 --- /dev/null +++ b/src/parser/PrismParser/Includes.h @@ -0,0 +1,35 @@ +/* + * File: BoostIncludes.h + * Author: nafur + * + * Created on April 10, 2013, 4:46 PM + */ + +#ifndef BOOSTINCLUDES_H +#define BOOSTINCLUDES_H + +// Used for Boost spirit. +#include +#include +#include + +// Include headers for spirit iterators. Needed for diagnostics and input stream iteration. +#include +#include + +namespace qi = boost::spirit::qi; +namespace phoenix = boost::phoenix; + +typedef std::string::const_iterator BaseIteratorType; +typedef boost::spirit::classic::position_iterator2 PositionIteratorType; +typedef PositionIteratorType Iterator; +typedef BOOST_TYPEOF(boost::spirit::ascii::space | qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol) Skipper; + +#include "src/ir/IR.h" +using namespace storm::ir; +using namespace storm::ir::expressions; + +#include "UtilityGrammars.h" + +#endif /* BOOSTINCLUDES_H */ + diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.cpp b/src/parser/PrismParser/IntegerExpressionGrammar.cpp new file mode 100644 index 000000000..1d4c2cd19 --- /dev/null +++ b/src/parser/PrismParser/IntegerExpressionGrammar.cpp @@ -0,0 +1,46 @@ +#include "IntegerExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + +IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr& state) + : IntegerExpressionGrammar::base_type(integerExpression), state(state) { + + // This rule defines all identifiers that have not been previously used. + identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ]; + identifierName.name("identifier"); + + // This block defines all literal expressions. + integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + integerLiteralExpression.name("integer literal"); + + // This block defines all expressions that are variables. + std::shared_ptr intvarexpr = std::shared_ptr(new VariableExpression(BaseExpression::int_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); + integerVariableExpression = identifierName[qi::_val = intvarexpr]; + integerVariableExpression.name("integer variable"); + + // This block defines all atomic expressions that are constant, i.e. literals and constants. + integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); + integerConstantExpression.name("integer constant or literal"); + + // This block defines all expressions of integral type. + atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | integerConstantExpression); + atomicIntegerExpression.name("integer expression"); + integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression)[qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES))]; + integerMultExpression.name("integer expression"); + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::int_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]]; + integerPlusExpression.name("integer expression"); + integerExpression %= integerPlusExpression; + integerExpression.name("integer expression"); +} + +void IntegerExpressionGrammar::prepareForSecondRun() { + // Override variable expressions: only allow declared variables. + integerVariableExpression %= this->state->integerVariables_; + integerVariableExpression.name("integer variable"); +} + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.h b/src/parser/PrismParser/IntegerExpressionGrammar.h new file mode 100644 index 000000000..7a240809b --- /dev/null +++ b/src/parser/PrismParser/IntegerExpressionGrammar.h @@ -0,0 +1,61 @@ +/* + * File: IntegerExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 4:39 PM + */ + +#ifndef INTEGEREXPRESSIONGRAMMAR_H +#define INTEGEREXPRESSIONGRAMMAR_H + +#include "src/ir/IR.h" +#include "VariableState.h" +#include "Includes.h" + +#include + +namespace storm { +namespace parser { +namespace prism { + +class IntegerExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +public: + IntegerExpressionGrammar(std::shared_ptr& state); + void prepareForSecondRun(); + +private: + + qi::rule identifierName; + + // The starting point for arbitrary expressions. + qi::rule(), Skipper> expression; + + // Rules with integer result type. + qi::rule(), Skipper, Skipper> integerExpression; + qi::rule(), qi::locals, Skipper> integerPlusExpression; + qi::rule(), Skipper> integerMultExpression; + qi::rule(), Skipper> atomicIntegerExpression; + qi::rule(), Skipper> constantIntegerExpression; + qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; + qi::rule(), Skipper> constantIntegerMultExpression; + qi::rule(), Skipper> constantAtomicIntegerExpression; + + // Rules for variable recognition. + qi::rule(), Skipper> integerVariableExpression; + qi::rule(), qi::locals>, Skipper> integerVariableCreatorExpression; + + // Rules for constant recognition. + qi::rule(), Skipper> integerConstantExpression; + + // Rules for literal recognition. + qi::rule(), Skipper> integerLiteralExpression; + + std::shared_ptr state; +}; + +} +} +} + +#endif /* INTEGEREXPRESSIONGRAMMAR_H */ + diff --git a/src/parser/PrismParser/UtilityGrammars.h b/src/parser/PrismParser/UtilityGrammars.h new file mode 100644 index 000000000..e6c7e9707 --- /dev/null +++ b/src/parser/PrismParser/UtilityGrammars.h @@ -0,0 +1,69 @@ +/* + * File: Keywords.h + * Author: nafur + * + * Created on April 10, 2013, 6:03 PM + */ + +#ifndef KEYWORDS_H +#define KEYWORDS_H + +#include "Includes.h" + +namespace storm { +namespace parser { +namespace prism { + +// A structure defining the keywords that are not allowed to be chosen as identifiers. + struct keywordsStruct : qi::symbols { + keywordsStruct() { + add + ("dtmc", 1) + ("ctmc", 2) + ("mdp", 3) + ("ctmdp", 4) + ("const", 5) + ("int", 6) + ("bool", 7) + ("module", 8) + ("endmodule", 9) + ("rewards", 10) + ("endrewards", 11) + ("true", 12) + ("false", 13) + ; + } + }; + + // A structure mapping the textual representation of a model type to the model type + // representation of the intermediate representation. + struct modelTypeStruct : qi::symbols { + modelTypeStruct() { + add + ("dtmc", Program::ModelType::DTMC) + ("ctmc", Program::ModelType::CTMC) + ("mdp", Program::ModelType::MDP) + ("ctmdp", Program::ModelType::CTMDP) + ; + } + }; + + // A structure mapping the textual representation of a binary relation to the representation + // of the intermediate representation. + struct relationalOperatorStruct : qi::symbols { + relationalOperatorStruct() { + add + ("=", BinaryRelationExpression::EQUAL) + ("<", BinaryRelationExpression::LESS) + ("<=", BinaryRelationExpression::LESS_OR_EQUAL) + (">", BinaryRelationExpression::GREATER) + (">=", BinaryRelationExpression::GREATER_OR_EQUAL) + ; + } + }; + +} +} +} +#endif /* KEYWORDS_H */ + diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h new file mode 100644 index 000000000..dd8fb0d80 --- /dev/null +++ b/src/parser/PrismParser/VariableState.h @@ -0,0 +1,96 @@ +/* + * File: VariableState.h + * Author: nafur + * + * Created on April 10, 2013, 4:43 PM + */ + +#ifndef VARIABLESTATE_H +#define VARIABLESTATE_H + +#include "src/ir/IR.h" +#include "Includes.h" + +namespace storm { +namespace parser { +namespace prism { + +using namespace storm::ir; +using namespace storm::ir::expressions; + +struct VariableState : public storm::ir::VariableAdder { + + public: + VariableState() + : keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) + { + } + + keywordsStruct keywords; + + // Used for indexing the variables. + uint_fast64_t nextBooleanVariableIndex; + uint_fast64_t nextIntegerVariableIndex; + + // Structures mapping variable and constant names to the corresponding expression nodes of + // the intermediate representation. + struct qi::symbols> integerVariables_, booleanVariables_; + struct qi::symbols> integerConstants_, booleanConstants_, doubleConstants_; + struct qi::symbols moduleMap_; + + // A structure representing the identity function over identifier names. + struct variableNamesStruct : qi::symbols { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_, + localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; + + uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) { + std::shared_ptr res = this->booleanVariables_.at(name); + if (res != nullptr) { + return res->getVariableIndex(); + } + std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, this->nextBooleanVariableIndex, name)); + this->booleanVariables_.add(name, varExpr); + this->booleanVariableNames_.add(name, name); + this->nextBooleanVariableIndex++; + return this->nextBooleanVariableIndex-1; + } + + uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) { + std::shared_ptr res = this->integerVariables_.at(name); + if (res != nullptr) { + return res->getVariableIndex(); + } + std::shared_ptr varExpr = std::shared_ptr(new VariableExpression(storm::ir::expressions::BaseExpression::int_, this->nextIntegerVariableIndex, name, lower, upper)); + this->integerVariables_.add(name, varExpr); + this->integerVariableNames_.add(name, name); + this->nextIntegerVariableIndex++; + return this->nextIntegerVariableIndex-1; + } + + bool isFreeIdentifier(std::string& s) const { + if (this->integerVariableNames_.find(s) != nullptr) return false; + if (this->allConstantNames_.find(s) != nullptr) return false; + if (this->labelNames_.find(s) != nullptr) return false; + if (this->moduleNames_.find(s) != nullptr) return false; + if (this->keywords.find(s) != nullptr) return false; + return true; + } + bool isIdentifier(std::string& s) const { + if (this->allConstantNames_.find(s) != nullptr) return false; + if (this->keywords.find(s) != nullptr) return false; + return true; + } + + void prepareForSecondRun() { + integerConstants_.clear(); + booleanConstants_.clear(); + doubleConstants_.clear(); + allConstantNames_.clear(); + } +}; + +} +} +} + +#endif /* VARIABLESTATE_H */ +