diff --git a/src/parser/PgclParser.cpp b/src/parser/PgclParser.cpp index bfa708207..56bf4c0fe 100755 --- a/src/parser/PgclParser.cpp +++ b/src/parser/PgclParser.cpp @@ -75,7 +75,7 @@ namespace storm { qi::lit("}"))[qi::_val = phoenix::bind(&PgclParser::createProgram, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)]; sequenceOfStatements %= +(statement); - variableDeclarations %= qi::lit("var") >> qi::lit("{") >> +integerDeclaration >> qi::lit("}"); + variableDeclarations %= qi::lit("var") >> qi::lit("{") >> +(integerDeclaration | booleanDeclaration) >> qi::lit("}"); variableDeclarations.name("variable declarations"); // Statements @@ -86,6 +86,7 @@ namespace storm { // Simple statements doubleDeclaration = (qi::lit("double ") >> variableName)[qi::_val = phoenix::bind(&PgclParser::declareDoubleVariable, phoenix::ref(*this), qi::_1)]; integerDeclaration = (qi::lit("int ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createIntegerDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)]; + booleanDeclaration = (qi::lit("bool ") >> variableName >> qi::lit(":=") >> expression >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createBooleanDeclarationStatement, phoenix::ref(*this), qi::_1, qi::_2)]; assignmentStatement = (variableName >> qi::lit(":=") >> (expression | uniformExpression) >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createAssignmentStatement, phoenix::ref(*this), qi::_1, qi::_2)]; observeStatement = (qi::lit("observe") >> qi::lit("(") >> booleanCondition >> qi::lit(")") >> qi::lit(";"))[qi::_val = phoenix::bind(&PgclParser::createObserveStatement, phoenix::ref(*this), qi::_1)]; @@ -197,6 +198,23 @@ namespace storm { return newAssignment; } + std::shared_ptr PgclParser::createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression) { + storm::expressions::Variable variable; + if(!(*expressionManager).hasVariable(variableName)) { + variable = (*expressionManager).declareBooleanVariable(variableName); + this->identifiers_.add(variableName, variable.getExpression()); + } else { + // In case that a declaration already happened. + variable = (*expressionManager).getVariable(variableName); + STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Declaration of boolean variable " << variableName << " which was already declared previously."); + } + std::shared_ptr newAssignment(new storm::pgcl::AssignmentStatement(variable, assignedExpression)); + newAssignment->setLocationNumber(this->currentLocationNumber); + this->locationToStatement.insert(this->locationToStatement.begin() + this->currentLocationNumber, newAssignment); + currentLocationNumber++; + return newAssignment; + } + std::shared_ptr PgclParser::createObserveStatement(storm::pgcl::BooleanExpression const& condition) { std::shared_ptr observe(new storm::pgcl::ObserveStatement(condition)); this->observeCreated = true; diff --git a/src/parser/PgclParser.h b/src/parser/PgclParser.h index 7fd3ded71..a9b99ef09 100755 --- a/src/parser/PgclParser.h +++ b/src/parser/PgclParser.h @@ -76,6 +76,7 @@ namespace storm { qi::rule>(), Skipper> variableDeclarations; qi::rule(), Skipper> integerDeclaration; + qi::rule(), Skipper> booleanDeclaration; qi::rule doubleDeclaration; /// Denotes the invalid identifiers, which are later passed to the expression parser. @@ -141,6 +142,7 @@ namespace storm { storm::expressions::Variable declareDoubleVariable(std::string const& variableName); std::shared_ptr createAssignmentStatement(std::string const& variableName, boost::variant const& assignedExpression); std::shared_ptr createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression); + std::shared_ptr createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression); std::shared_ptr createObserveStatement(storm::pgcl::BooleanExpression const& condition); std::shared_ptr createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector > const& if_body, boost::optional > > const& else_body); std::shared_ptr createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector > const& body);