From b92260fed0c433769bef6e9ee559fa78fca3c7b9 Mon Sep 17 00:00:00 2001 From: gereon Date: Sat, 20 Apr 2013 01:18:17 +0200 Subject: [PATCH] A lot of work on PrismParser: * Created a distinct parser for each expression type and for identifiers * Removed all expression rules from PrismParser, using new parsers instead * Reduced excessive usage of boost::lambda, using semantic actions only for single calls * Moved actual state to new class (-> VariableState, whole two-run-logic can probably implemented there) * Much cleanup Work should be finished on expression parser, but not yet on prism parser... --- src/parser/PrismParser.cpp | 132 ++++++++---------- src/parser/PrismParser.h | 36 ++--- src/parser/PrismParser/BaseGrammar.h | 98 +++++++++++++ .../PrismParser/BooleanExpressionGrammar.cpp | 54 +++---- .../PrismParser/BooleanExpressionGrammar.h | 35 +---- .../ConstBooleanExpressionGrammar.cpp | 54 ++++--- .../ConstBooleanExpressionGrammar.h | 23 +-- .../ConstDoubleExpressionGrammar.cpp | 53 +++++++ .../ConstDoubleExpressionGrammar.h | 43 ++++++ .../ConstIntegerExpressionGrammar.cpp | 29 ++-- .../ConstIntegerExpressionGrammar.h | 11 +- src/parser/PrismParser/IdentifierGrammars.cpp | 23 +++ src/parser/PrismParser/IdentifierGrammars.h | 36 +++++ src/parser/PrismParser/Includes.h | 6 +- .../PrismParser/IntegerExpressionGrammar.cpp | 55 +++----- .../PrismParser/IntegerExpressionGrammar.h | 28 +--- .../{UtilityGrammars.h => Tokens.h} | 46 +++--- src/parser/PrismParser/VariableState.h | 90 +++++++++--- 18 files changed, 540 insertions(+), 312 deletions(-) create mode 100644 src/parser/PrismParser/BaseGrammar.h create mode 100644 src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp create mode 100644 src/parser/PrismParser/ConstDoubleExpressionGrammar.h create mode 100644 src/parser/PrismParser/IdentifierGrammars.cpp create mode 100644 src/parser/PrismParser/IdentifierGrammars.h rename src/parser/PrismParser/{UtilityGrammars.h => Tokens.h} (85%) diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp index e1aaacaab..e31e31b8a 100644 --- a/src/parser/PrismParser.cpp +++ b/src/parser/PrismParser.cpp @@ -6,12 +6,15 @@ */ #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" +#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" +#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" +#include "src/parser/PrismParser/IntegerExpressionGrammar.h" +#include "src/parser/PrismParser/VariableState.h" // If the parser fails due to ill-formed data, this exception is thrown. #include "src/exceptions/WrongFileFormatException.h" @@ -40,72 +43,44 @@ namespace storm { namespace parser { -PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start) { + void dump(const std::string& s) { + std::cerr << "Dump: " << s << std::endl; + } + /*void dump(const std::string& s, ) { + std::cerr << "Dump: " << s << std::endl; + }*/ + + std::shared_ptr addIntegerConstant(const std::string& name, const std::shared_ptr value, std::shared_ptr state) { + std::cerr << "addIntegerConstant: " << name << std::endl; + state->integerConstants_.add(name, value); + state->allConstantNames_.add(name, name); + return value; + } - 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); +PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type(start), state(new storm::parser::prism::VariableState()) { // 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 %= 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, 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 %= 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, 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"); - doubleLiteralExpression = qi::double_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; - doubleLiteralExpression.name("double 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))); - std::shared_ptr boolvarexpr = std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); - integerVariableExpression = identifierName[qi::_val = intvarexpr]; - integerVariableExpression.name("integer variable"); - 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"); - doubleConstantExpression %= (this->state->doubleConstants_ | doubleLiteralExpression); - doubleConstantExpression.name("double constant or literal"); - - // 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); - constantAtomicDoubleExpression.name("constant double expression"); - constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::double_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::TIMES)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::double_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::DIVIDE))]]; - constantDoubleMultExpression.name("constant double expression"); - constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression)[phoenix::if_(qi::_a) [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::double_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::PLUS)) ] .else_ [qi::_val = phoenix::construct>(phoenix::new_(BaseExpression::double_, qi::_val, qi::_1, BinaryNumericalFunctionExpression::MINUS))]]; - constantDoublePlusExpression.name("constant double expression"); - constantDoubleExpression %= constantDoublePlusExpression; - constantDoubleExpression.name("constant double expression"); - // This block defines all entities that are needed for parsing labels. - 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 = (qi::lit("label") >> -qi::lit("\"") >> freeIdentifierName >> -qi::lit("\"") >> qi::lit("=") >> prism::BooleanExpressionGrammar::instance(this->state) >> 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 = (boolExpr > qi::lit(":") > constantDoubleExpression >> qi::lit(";"))[qi::_val = phoenix::construct(qi::_1, qi::_2)]; + stateRewardDefinition = (prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) >> 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("]") > boolExpr > 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("]") > prism::BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > prism::ConstDoubleExpressionGrammar::instance(this->state) > 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"); rewardDefinitionList = *rewardDefinition(qi::_r1); rewardDefinitionList.name("reward definition list"); - // This block defines auxiliary entities that are used to check whether a certain variable exist. - booleanVariableName %= this->state->booleanVariableNames_; - booleanVariableName.name("boolean variable"); - integerVariableName %= this->state->integerVariableNames_; - integerVariableName.name("integer variable"); commandName %= this->state->commandNames_; commandName.name("command name"); unassignedLocalBooleanVariableName %= this->state->localBooleanVariables_ - this->state->assignedLocalBooleanVariables_; @@ -114,19 +89,23 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type 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("=") > 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 = (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > prism::IntegerExpressionGrammar::instance(this->state) > 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("=") > prism::BooleanExpressionGrammar::instance(this->state) > 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(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 = (prism::ConstDoubleExpressionGrammar::instance(this->state) > 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(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 = ( + qi::lit("[") > -( + (freeIdentifierName[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1] + ) > qi::lit("]") > prism::BooleanExpressionGrammar::instance(this->state) > 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") > constBoolExpr[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + booleanVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > prism::ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ //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), @@ -135,7 +114,10 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type phoenix::bind(this->state->localBooleanVariables_.add, qi::_1, qi::_1) ]; booleanVariableDefinition.name("boolean variable declaration"); - integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") > constIntExpr > qi::lit("..") > constIntExpr > qi::lit("]") > -(qi::lit("init") > constIntExpr[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) + + integerLiteralExpression = qi::int_[qi::_val = phoenix::construct>(phoenix::new_(qi::_1))]; + integerLiteralExpression.name("integer literal"); + integerVariableDefinition = (freeIdentifierName >> qi::lit(":") >> qi::lit("[") > integerLiteralExpression > qi::lit("..") > integerLiteralExpression > qi::lit("]") > -(qi::lit("init") > prism::ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct>(qi::_1)]) > qi::lit(";")) [ 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)), @@ -148,7 +130,7 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type // This block defines all entities that are needed for parsing a module. moduleDefinition = (qi::lit("module") >> freeIdentifierName - [phoenix::clear(phoenix::ref(this->state->localBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->localIntegerVariables_))] + [phoenix::bind(&prism::VariableState::startModule, *this->state)] >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule")) [ phoenix::bind(this->state->moduleNames_.add, qi::_1, qi::_1), @@ -172,14 +154,20 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type 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(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") >> freeIdentifierName >> qi::lit("=") > prism::ConstBooleanExpressionGrammar::instance(this->state) > 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(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2]; + definedIntegerConstantDefinition = ( + qi::lit("const") >> + qi::lit("int")[phoenix::bind(&dump, "const int")] >> + freeIdentifierName >> + qi::lit("=")[phoenix::bind(&dump, "const int = ")] >> + //constIntExpr.integerLiteralExpression[phoenix::bind(&dump, "const int = ")] >> + prism::ConstIntegerExpressionGrammar::instance(this->state)[phoenix::bind(&dump, "const int = ")] >> + qi::lit(";")[phoenix::bind(&dump, "const int = ;")] + )[ qi::_val = phoenix::bind(&addIntegerConstant, qi::_1, qi::_2, this->state) ]; definedIntegerConstantDefinition.name("defined integer constant declaration"); - 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 = (qi::lit("const") >> qi::lit("double") >> freeIdentifierName >> qi::lit("=") > prism::ConstDoubleExpressionGrammar::instance(this->state) > 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(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)]; undefinedBooleanConstantDefinition.name("undefined boolean constant declaration"); @@ -187,32 +175,28 @@ PrismParser::PrismGrammar::PrismGrammar() : PrismParser::PrismGrammar::base_type 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(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 %= (definedBooleanConstantDefinition[phoenix::bind(&dump, "")] | definedIntegerConstantDefinition[phoenix::bind(&dump, "")] | definedDoubleConstantDefinition[phoenix::bind(&dump, "")]); definedConstantDefinition.name("defined constant declaration"); undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3)); undefinedConstantDefinition.name("undefined constant declaration"); - constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)); + constantDefinitionList = *(definedConstantDefinition[phoenix::bind(&dump, "")] | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3)[phoenix::bind(&dump, "")]); constantDefinitionList.name("constant declaration list"); // This block defines all entities that are needed for parsing a program. modelTypeDefinition = modelType_; modelTypeDefinition.name("model type"); - start = (modelTypeDefinition > constantDefinitionList(qi::_a, qi::_b, qi::_c) > moduleDefinitionList > rewardDefinitionList(qi::_d) > labelDefinitionList(qi::_e))[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; + start = ( + modelTypeDefinition[phoenix::bind(&dump, "")] > + constantDefinitionList(qi::_a, qi::_b, qi::_c)[phoenix::bind(&dump, "")] > + moduleDefinitionList[phoenix::bind(&dump, "")] > + rewardDefinitionList(qi::_d)[phoenix::bind(&dump, "")] > + labelDefinitionList(qi::_e)[phoenix::bind(&dump, "")] + )[qi::_val = phoenix::construct(qi::_1, qi::_a, qi::_b, qi::_c, qi::_2, qi::_d, qi::_e)]; start.name("probabilistic program declaration"); } void PrismParser::PrismGrammar::prepareForSecondRun() { - // Clear constants. - 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 %= this->state->integerVariables_; - integerVariableExpression.name("integer variable"); - booleanVariableExpression %= this->state->booleanVariables_; - booleanVariableExpression.name("boolean variable"); } /*! diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h index 86b7eb4d7..a32487c78 100644 --- a/src/parser/PrismParser.h +++ b/src/parser/PrismParser.h @@ -11,8 +11,14 @@ // 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/Tokens.h" +#include "src/parser/PrismParser/IdentifierGrammars.h" #include "src/parser/PrismParser/VariableState.h" +#include "src/parser/PrismParser/ConstBooleanExpressionGrammar.h" +#include "src/parser/PrismParser/ConstDoubleExpressionGrammar.h" +#include "src/parser/PrismParser/ConstIntegerExpressionGrammar.h" +#include "src/parser/PrismParser/BooleanExpressionGrammar.h" +#include "src/parser/PrismParser/IntegerExpressionGrammar.h" // Used for file input. #include @@ -62,6 +68,7 @@ public: qi::rule>, Skipper> moduleRenaming; // Rules for variable definitions. + qi::rule(), Skipper> integerLiteralExpression; 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; @@ -74,8 +81,6 @@ public: 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; @@ -91,7 +96,6 @@ public: 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; @@ -102,34 +106,14 @@ public: qi::rule(), Skipper> definedIntegerConstantDefinition; qi::rule(), Skipper> definedDoubleConstantDefinition; - qi::rule freeIdentifierName; - qi::rule identifierName; + 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_; diff --git a/src/parser/PrismParser/BaseGrammar.h b/src/parser/PrismParser/BaseGrammar.h new file mode 100644 index 000000000..bcc5f3d44 --- /dev/null +++ b/src/parser/PrismParser/BaseGrammar.h @@ -0,0 +1,98 @@ +/* + * File: Keywords.h + * Author: nafur + * + * Created on April 10, 2013, 6:03 PM + */ + +#ifndef BASEGRAMMAR_H +#define BASEGRAMMAR_H + +#include "Includes.h" + +#include "VariableState.h" + +namespace storm { +namespace parser { +namespace prism { + + template + class BaseGrammar { + public: + BaseGrammar(std::shared_ptr& state) : state(state) {} + + static T& instance(std::shared_ptr& state = nullptr) { + if (BaseGrammar::instanceObject == nullptr) { + BaseGrammar::instanceObject = std::shared_ptr(new T(state)); + } + return *BaseGrammar::instanceObject; + } + + std::shared_ptr createBoolLiteral(const bool value) { + return std::shared_ptr(new BooleanLiteral(value)); + } + std::shared_ptr createDoubleLiteral(const double value) { + return std::shared_ptr(new DoubleLiteral(value)); + } + std::shared_ptr createIntLiteral(const int_fast64_t value) { + return std::shared_ptr(new IntegerLiteral(value)); + } + + std::shared_ptr createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right, BaseExpression::ReturnType type) { + if (addition) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::MINUS)); + } + } + std::shared_ptr createDoublePlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { + return this->createPlus(left, addition, right, BaseExpression::double_); + } + std::shared_ptr createIntPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { + return this->createPlus(left, addition, right, BaseExpression::int_); + } + + std::shared_ptr createIntMult(const std::shared_ptr left, const std::shared_ptr right) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, BinaryNumericalFunctionExpression::TIMES)); + } + std::shared_ptr createDoubleMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right) { + if (multiplication) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); + } + } + + std::shared_ptr createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right) { + return std::shared_ptr(new BinaryRelationExpression(left, right, relationType)); + } + std::shared_ptr createNot(std::shared_ptr child) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); + } + std::shared_ptr createAnd(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); + } + std::shared_ptr createOr(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); + } + std::shared_ptr getBoolVariable(const std::string name) { + return state->getBooleanVariable(name); + } + std::shared_ptr getIntVariable(const std::string name) { + return state->getIntegerVariable(name); + } + + protected: + std::shared_ptr state; + + private: + static std::shared_ptr instanceObject; + }; + + template + std::shared_ptr BaseGrammar::instanceObject; +} +} +} +#endif /* BASEGRAMMAR_H */ + diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.cpp b/src/parser/PrismParser/BooleanExpressionGrammar.cpp index 3ad148c08..101db9cce 100644 --- a/src/parser/PrismParser/BooleanExpressionGrammar.cpp +++ b/src/parser/PrismParser/BooleanExpressionGrammar.cpp @@ -1,53 +1,35 @@ #include "BooleanExpressionGrammar.h" +#include "IntegerExpressionGrammar.h" +#include "ConstBooleanExpressionGrammar.h" + namespace storm { namespace parser { namespace prism { BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr& state) - : BooleanExpressionGrammar::base_type(booleanExpression), state(state) { - - IntegerExpressionGrammar intExpr(this->state); + : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(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"); + booleanExpression %= orExpression; + booleanExpression.name("boolean expression"); + orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)]; + orExpression.name("boolean expression"); - // 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"); + andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)]; + andExpression.name("boolean expression"); - // 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"); + notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)]; + notExpression.name("boolean expression"); - // 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 %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state)); 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"); + relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; + relativeExpression.name("relative expression"); + + booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)]; + booleanVariableExpression.name("boolean variable"); } } diff --git a/src/parser/PrismParser/BooleanExpressionGrammar.h b/src/parser/PrismParser/BooleanExpressionGrammar.h index db5ad0951..9d14c5ec3 100644 --- a/src/parser/PrismParser/BooleanExpressionGrammar.h +++ b/src/parser/PrismParser/BooleanExpressionGrammar.h @@ -10,52 +10,29 @@ #include "Includes.h" #include "VariableState.h" -#include "IntegerExpressionGrammar.h" +#include "IdentifierGrammars.h" +#include "Tokens.h" + +#include namespace storm { namespace parser { namespace prism { -class BooleanExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +class BooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { 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, Unused> 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; }; diff --git a/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp b/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp index 53a5f5a96..203894638 100644 --- a/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp +++ b/src/parser/PrismParser/ConstBooleanExpressionGrammar.cpp @@ -1,31 +1,53 @@ #include "ConstBooleanExpressionGrammar.h" +#include "ConstIntegerExpressionGrammar.h" + namespace storm { namespace parser { namespace prism { + std::shared_ptr ConstBooleanExpressionGrammar::createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right) { + return std::shared_ptr(new BinaryRelationExpression(left, right, relationType)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createNot(std::shared_ptr child) { + return std::shared_ptr(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createAnd(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createOr(std::shared_ptr left, std::shared_ptr right) { + return std::shared_ptr(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR)); + } + std::shared_ptr ConstBooleanExpressionGrammar::createLiteral(const bool value) { + return std::shared_ptr(new BooleanLiteral(value)); + } ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr& state) - : ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), state(state) { + : ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) { - ConstIntegerExpressionGrammar constIntExpr(this->state); + constantBooleanExpression %= constantOrExpression; + constantBooleanExpression.name("constant boolean expression"); + + constantOrExpression = constantAndExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> constantAndExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createOr, this, qi::_val, qi::_1)]; + constantOrExpression.name("constant boolean expression"); + + constantAndExpression = constantNotExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> constantNotExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createAnd, this, qi::_val, qi::_1)]; + constantAndExpression.name("constant boolean expression"); + + constantNotExpression = constantAtomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> constantAtomicBooleanExpression)[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createNot, this, qi::_1)]; + constantNotExpression.name("constant boolean expression"); - 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"); + + constantRelativeExpression = (ConstIntegerExpressionGrammar::instance(this->state) >> relations_ >> ConstIntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)]; + constantRelativeExpression.name("constant boolean expression"); + + booleanConstantExpression %= (this->state->booleanConstants_ | booleanLiteralExpression); + booleanConstantExpression.name("boolean constant or literal"); + + booleanLiteralExpression = qi::bool_[qi::_val = phoenix::bind(&ConstBooleanExpressionGrammar::createLiteral, this, qi::_1)]; + booleanLiteralExpression.name("boolean literal"); } } } diff --git a/src/parser/PrismParser/ConstBooleanExpressionGrammar.h b/src/parser/PrismParser/ConstBooleanExpressionGrammar.h index 24166035e..4c8a5f7fb 100644 --- a/src/parser/PrismParser/ConstBooleanExpressionGrammar.h +++ b/src/parser/PrismParser/ConstBooleanExpressionGrammar.h @@ -9,35 +9,36 @@ #define CONSTBOOLEANEXPRESSIONGRAMMAR_H #include "Includes.h" -#include "ConstIntegerExpressionGrammar.h" #include "VariableState.h" -#include "UtilityGrammars.h" +#include "IdentifierGrammars.h" +#include "Tokens.h" namespace storm { namespace parser { namespace prism { -class ConstBooleanExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +class ConstBooleanExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { 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, Unused> constantBooleanExpression; qi::rule(), Skipper> constantOrExpression; qi::rule(), Skipper> constantAndExpression; qi::rule(), Skipper> constantNotExpression; qi::rule(), Skipper> constantAtomicBooleanExpression; qi::rule(), Skipper> constantRelativeExpression; - + qi::rule(), Skipper> booleanConstantExpression; + qi::rule(), Skipper> booleanLiteralExpression; storm::parser::prism::relationalOperatorStruct relations_; - std::shared_ptr state; - + std::shared_ptr createRelation(std::shared_ptr left, BinaryRelationExpression::RelationType relationType, std::shared_ptr right); + std::shared_ptr createNot(std::shared_ptr child); + std::shared_ptr createAnd(std::shared_ptr left, std::shared_ptr right); + std::shared_ptr createOr(std::shared_ptr left, std::shared_ptr right); + std::shared_ptr createLiteral(const bool value); }; diff --git a/src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp b/src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp new file mode 100644 index 000000000..e569d329c --- /dev/null +++ b/src/parser/PrismParser/ConstDoubleExpressionGrammar.cpp @@ -0,0 +1,53 @@ +#include "ConstDoubleExpressionGrammar.h" + +namespace storm { +namespace parser { +namespace prism { + + + std::shared_ptr ConstDoubleExpressionGrammar::createLiteral(double value) { + return std::shared_ptr(new DoubleLiteral(value)); + } + std::shared_ptr ConstDoubleExpressionGrammar::createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right) { + if (addition) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::PLUS)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::MINUS)); + } + } + std::shared_ptr ConstDoubleExpressionGrammar::createMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right) { + if (multiplication) { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES)); + } else { + return std::shared_ptr(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE)); + } + } + +ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr& state) + : ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) { + + constantDoubleExpression %= constantDoublePlusExpression; + constantDoubleExpression.name("constant double expression"); + + constantDoublePlusExpression %= constantDoubleMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantDoubleMultExpression) + [phoenix::bind(&ConstDoubleExpressionGrammar::createPlus, this, qi::_val, qi::_a, qi::_1)]; + constantDoublePlusExpression.name("constant double expression"); + + constantDoubleMultExpression %= constantAtomicDoubleExpression[qi::_val = qi::_1] >> *((qi::lit("*")[qi::_a = true] | qi::lit("/")[qi::_a = false]) >> constantAtomicDoubleExpression) + [phoenix::bind(&ConstDoubleExpressionGrammar::createMult, this, qi::_val, qi::_a, qi::_1)]; + constantDoubleMultExpression.name("constant double expression"); + + constantAtomicDoubleExpression %= (qi::lit("(") >> constantDoubleExpression >> qi::lit(")") | doubleConstantExpression); + constantAtomicDoubleExpression.name("constant double expression"); + + doubleConstantExpression %= (this->state->doubleConstants_ | doubleLiteralExpression); + doubleConstantExpression.name("double constant or literal"); + + doubleLiteralExpression = qi::double_[qi::_val = phoenix::bind(&ConstDoubleExpressionGrammar::createLiteral, this, qi::_1)]; + doubleLiteralExpression.name("double literal"); +} + + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/ConstDoubleExpressionGrammar.h b/src/parser/PrismParser/ConstDoubleExpressionGrammar.h new file mode 100644 index 000000000..9d70f9877 --- /dev/null +++ b/src/parser/PrismParser/ConstDoubleExpressionGrammar.h @@ -0,0 +1,43 @@ +/* + * File: ConstDoubleExpressionGrammar.h + * Author: nafur + * + * Created on April 10, 2013, 7:04 PM + */ + +#ifndef CONSTDOUBLEEXPRESSIONGRAMMAR_H +#define CONSTDOUBLEEXPRESSIONGRAMMAR_H + +#include "Includes.h" +#include "VariableState.h" +#include "IdentifierGrammars.h" + +namespace storm { +namespace parser { +namespace prism { + +class ConstDoubleExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { +public: + ConstDoubleExpressionGrammar(std::shared_ptr& state); + + +private: + qi::rule(), Skipper, Unused> constantDoubleExpression; + qi::rule(), qi::locals, Skipper> constantDoublePlusExpression; + qi::rule(), qi::locals, Skipper> constantDoubleMultExpression; + qi::rule(), Skipper> constantAtomicDoubleExpression; + qi::rule(), Skipper> doubleConstantExpression; + qi::rule(), Skipper> doubleLiteralExpression; + + std::shared_ptr createLiteral(double value); + std::shared_ptr createPlus(const std::shared_ptr left, bool addition, const std::shared_ptr right); + std::shared_ptr createMult(const std::shared_ptr left, bool multiplication, const std::shared_ptr right); +}; + + +} +} +} + +#endif /* CONSTDOUBLEEXPRESSIONGRAMMAR_H */ + diff --git a/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp b/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp index ef9d8c91f..233b4492a 100644 --- a/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp +++ b/src/parser/PrismParser/ConstIntegerExpressionGrammar.cpp @@ -1,27 +1,32 @@ #include "ConstIntegerExpressionGrammar.h" - namespace storm { namespace parser { namespace prism { + ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr& state) - : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), state(state) { + : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(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"); + constantIntegerExpression %= constantIntegerPlusExpression; + constantIntegerExpression.name("constant integer expression"); + + constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression) + [qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; + constantIntegerPlusExpression.name("constant integer expression"); + + constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression) + [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]; + constantIntegerMultExpression.name("constant integer expression"); 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"); + integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression); + integerConstantExpression.name("integer constant or literal"); + + integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)]; + integerLiteralExpression.name("integer literal"); } diff --git a/src/parser/PrismParser/ConstIntegerExpressionGrammar.h b/src/parser/PrismParser/ConstIntegerExpressionGrammar.h index 2c1a3420c..847892e10 100644 --- a/src/parser/PrismParser/ConstIntegerExpressionGrammar.h +++ b/src/parser/PrismParser/ConstIntegerExpressionGrammar.h @@ -10,24 +10,23 @@ #include "Includes.h" #include "VariableState.h" +#include "IdentifierGrammars.h" namespace storm { namespace parser { namespace prism { -class ConstIntegerExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +class ConstIntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { public: ConstIntegerExpressionGrammar(std::shared_ptr& state); private: - qi::rule(), Skipper> integerLiteralExpression; - qi::rule(), Skipper> integerConstantExpression; - qi::rule(), Skipper, Skipper> constantIntegerExpression; + qi::rule(), Skipper, Unused> constantIntegerExpression; qi::rule(), qi::locals, Skipper> constantIntegerPlusExpression; qi::rule(), Skipper> constantIntegerMultExpression; qi::rule(), Skipper> constantAtomicIntegerExpression; - - std::shared_ptr state; + qi::rule(), Skipper> integerConstantExpression; + qi::rule(), Skipper> integerLiteralExpression; }; diff --git a/src/parser/PrismParser/IdentifierGrammars.cpp b/src/parser/PrismParser/IdentifierGrammars.cpp new file mode 100644 index 000000000..552b6e2c0 --- /dev/null +++ b/src/parser/PrismParser/IdentifierGrammars.cpp @@ -0,0 +1,23 @@ +#include "IdentifierGrammars.h" + +namespace storm { +namespace parser { +namespace prism { + +IdentifierGrammar::IdentifierGrammar(std::shared_ptr& state) + : IdentifierGrammar::base_type(identifierName), BaseGrammar(state) { + + 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"); +} + +FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr& state) + : FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) { + + freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ]; + freeIdentifierName.name("identifier"); +} + +} +} +} \ No newline at end of file diff --git a/src/parser/PrismParser/IdentifierGrammars.h b/src/parser/PrismParser/IdentifierGrammars.h new file mode 100644 index 000000000..936ee732a --- /dev/null +++ b/src/parser/PrismParser/IdentifierGrammars.h @@ -0,0 +1,36 @@ +/* + * File: Keywords.h + * Author: nafur + * + * Created on April 10, 2013, 6:03 PM + */ + +#ifndef IDENTIFIERGRAMMARS_H +#define IDENTIFIERGRAMMARS_H + +#include "Includes.h" +#include "BaseGrammar.h" +#include "VariableState.h" + +namespace storm { +namespace parser { +namespace prism { + + class IdentifierGrammar : public qi::grammar, public BaseGrammar { + public: + IdentifierGrammar(std::shared_ptr& state); + private: + qi::rule identifierName; + }; + + class FreeIdentifierGrammar : public qi::grammar, public BaseGrammar { + public: + FreeIdentifierGrammar(std::shared_ptr& state); + private: + qi::rule freeIdentifierName; + }; +} +} +} +#endif /* IDENTIFIERGRAMMARS_H */ + diff --git a/src/parser/PrismParser/Includes.h b/src/parser/PrismParser/Includes.h index 39eb5a450..fe3418b2c 100644 --- a/src/parser/PrismParser/Includes.h +++ b/src/parser/PrismParser/Includes.h @@ -8,6 +8,8 @@ #ifndef BOOSTINCLUDES_H #define BOOSTINCLUDES_H +#define DEBUGPRISM + // Used for Boost spirit. #include #include @@ -24,12 +26,12 @@ 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; +typedef BOOST_TYPEOF(qi::lit("//") >> *(qi::char_ - qi::eol) >> qi::eol | boost::spirit::ascii::space) Skipper2; +typedef boost::spirit::unused_type Unused; #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 index 1d4c2cd19..89933aeb3 100644 --- a/src/parser/PrismParser/IntegerExpressionGrammar.cpp +++ b/src/parser/PrismParser/IntegerExpressionGrammar.cpp @@ -1,45 +1,30 @@ #include "IntegerExpressionGrammar.h" +#include "IdentifierGrammars.h" +#include "ConstIntegerExpressionGrammar.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"); -} + IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr& state) + : IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) { -void IntegerExpressionGrammar::prepareForSecondRun() { - // Override variable expressions: only allow declared variables. - integerVariableExpression %= this->state->integerVariables_; - integerVariableExpression.name("integer variable"); -} + integerExpression %= integerPlusExpression; + integerExpression.name("integer expression"); + + integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)]; + integerPlusExpression.name("integer expression"); + + integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]); + integerMultExpression.name("integer expression"); + + atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state)); + atomicIntegerExpression.name("integer expression"); + + integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)]; + integerVariableExpression.name("integer variable"); + } } } diff --git a/src/parser/PrismParser/IntegerExpressionGrammar.h b/src/parser/PrismParser/IntegerExpressionGrammar.h index 7a240809b..5c253e437 100644 --- a/src/parser/PrismParser/IntegerExpressionGrammar.h +++ b/src/parser/PrismParser/IntegerExpressionGrammar.h @@ -11,6 +11,7 @@ #include "src/ir/IR.h" #include "VariableState.h" #include "Includes.h" +#include "IdentifierGrammars.h" #include @@ -18,39 +19,16 @@ namespace storm { namespace parser { namespace prism { -class IntegerExpressionGrammar : public qi::grammar(), Skipper, Skipper> { +class IntegerExpressionGrammar : public qi::grammar(), Skipper, Unused>, public BaseGrammar { 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(), Skipper, Unused> 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; }; } diff --git a/src/parser/PrismParser/UtilityGrammars.h b/src/parser/PrismParser/Tokens.h similarity index 85% rename from src/parser/PrismParser/UtilityGrammars.h rename to src/parser/PrismParser/Tokens.h index e6c7e9707..cf0392f32 100644 --- a/src/parser/PrismParser/UtilityGrammars.h +++ b/src/parser/PrismParser/Tokens.h @@ -1,20 +1,33 @@ /* - * File: Keywords.h + * File: Tokens.h * Author: nafur * - * Created on April 10, 2013, 6:03 PM + * Created on April 19, 2013, 11:17 PM */ -#ifndef KEYWORDS_H -#define KEYWORDS_H - -#include "Includes.h" +#ifndef TOKENS_H +#define TOKENS_H namespace storm { namespace parser { namespace prism { -// A structure defining the keywords that are not allowed to be chosen as identifiers. + + // 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 defining the keywords that are not allowed to be chosen as identifiers. struct keywordsStruct : qi::symbols { keywordsStruct() { add @@ -34,20 +47,7 @@ namespace prism { ; } }; - - // 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 { @@ -61,9 +61,9 @@ namespace prism { ; } }; - } } } -#endif /* KEYWORDS_H */ + +#endif /* TOKENS_H */ diff --git a/src/parser/PrismParser/VariableState.h b/src/parser/PrismParser/VariableState.h index dd8fb0d80..1076d2764 100644 --- a/src/parser/PrismParser/VariableState.h +++ b/src/parser/PrismParser/VariableState.h @@ -10,6 +10,7 @@ #include "src/ir/IR.h" #include "Includes.h" +#include "Tokens.h" namespace storm { namespace parser { @@ -18,14 +19,15 @@ namespace prism { using namespace storm::ir; using namespace storm::ir::expressions; + struct VariableState : public storm::ir::VariableAdder { - public: - VariableState() - : keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) - { +public: + VariableState(bool firstRun = true) + : firstRun(firstRun), keywords(), nextBooleanVariableIndex(0), nextIntegerVariableIndex(0) { } + bool firstRun; keywordsStruct keywords; // Used for indexing the variables. @@ -43,30 +45,81 @@ struct VariableState : public storm::ir::VariableAdder { localBooleanVariables_, localIntegerVariables_, assignedLocalBooleanVariables_, assignedLocalIntegerVariables_; uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr init) { + std::cerr << "adding boolean variable " << name << std::endl; + if (firstRun) { + 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; + } else { + std::shared_ptr res = this->booleanVariables_.at(name); + if (res != nullptr) { + return res->getVariableIndex(); + } else { + std::cerr << "Variable " << name << " was not created in first run" << std::endl; + return 0; + } + } + } + + uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr lower, const std::shared_ptr upper, const std::shared_ptr init) { + std::cerr << "adding integer variable " << name << std::endl; + if (firstRun) { + 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; + } else { + std::shared_ptr res = this->integerVariables_.at(name); + if (res != nullptr) { + return res->getVariableIndex(); + } else { + std::cerr << "Variable " << name << " was not created in first run" << std::endl; + return 0; + } + } + } + + std::shared_ptr getBooleanVariable(const std::string& name) { + std::cerr << "getting boolen variable " << name << std::endl; std::shared_ptr res = this->booleanVariables_.at(name); if (res != nullptr) { - return res->getVariableIndex(); + return res; + } else { + if (firstRun) { + return std::shared_ptr(new VariableExpression(BaseExpression::bool_, std::numeric_limits::max(), "bool", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); + } else { + std::cerr << "Variable " << name << " was not created in first run" << std::endl; + return std::shared_ptr(nullptr); + } } - 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 getIntegerVariable(const std::string& name) { + std::cerr << "getting integer variable " << name << std::endl; std::shared_ptr res = this->integerVariables_.at(name); if (res != nullptr) { - return res->getVariableIndex(); + return res; + } else { + if (firstRun) { + return std::shared_ptr(new VariableExpression(BaseExpression::int_, std::numeric_limits::max(), "int", std::shared_ptr(nullptr), std::shared_ptr(nullptr))); + } else { + std::cerr << "Variable " << name << " was not created in first run" << std::endl; + return std::shared_ptr(nullptr); + } } - 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; + } + + void startModule() { + std::cerr << "starting new module" << std::endl; + this->localBooleanVariables_.clear(); + this->localIntegerVariables_.clear(); } bool isFreeIdentifier(std::string& s) const { + std::cerr << "Checking if " << s << " is free" << std::endl; if (this->integerVariableNames_.find(s) != nullptr) return false; if (this->allConstantNames_.find(s) != nullptr) return false; if (this->labelNames_.find(s) != nullptr) return false; @@ -75,16 +128,19 @@ struct VariableState : public storm::ir::VariableAdder { return true; } bool isIdentifier(std::string& s) const { + std::cerr << "Checking if " << s << " is identifier" << std::endl; if (this->allConstantNames_.find(s) != nullptr) return false; if (this->keywords.find(s) != nullptr) return false; return true; } void prepareForSecondRun() { + std::cerr << "starting second run" << std::endl; integerConstants_.clear(); booleanConstants_.clear(); doubleConstants_.clear(); allConstantNames_.clear(); + this->firstRun = false; } };