From fb4657db2d2667ccdd9a8411422a6aeea46b3bd7 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 29 Sep 2016 12:18:54 +0200
Subject: [PATCH] added boolean variable declarations

Former-commit-id: cd170fab94476a9133c5da38266c9a6b9bcc83b5 [formerly 28713eaf6c5dc551a7ddcef1845a6045a8949547]
Former-commit-id: e86692a85756735ed4999dc718f7701e10c47c82
---
 src/parser/PgclParser.cpp | 20 +++++++++++++++++++-
 src/parser/PgclParser.h   |  2 ++
 2 files changed, 21 insertions(+), 1 deletion(-)

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<storm::pgcl::AssignmentStatement> 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<storm::pgcl::AssignmentStatement> 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<storm::pgcl::ObserveStatement> PgclParser::createObserveStatement(storm::pgcl::BooleanExpression const& condition) {
             std::shared_ptr<storm::pgcl::ObserveStatement> 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<Iterator, std::vector<std::shared_ptr<storm::pgcl::AssignmentStatement>>(), Skipper> variableDeclarations;
             qi::rule<Iterator, std::shared_ptr<storm::pgcl::AssignmentStatement>(), Skipper> integerDeclaration;
+            qi::rule<Iterator, std::shared_ptr<storm::pgcl::AssignmentStatement>(), Skipper> booleanDeclaration;
             qi::rule<Iterator, storm::expressions::Variable(), Skipper> 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<storm::pgcl::AssignmentStatement> createAssignmentStatement(std::string const& variableName, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& assignedExpression);
             std::shared_ptr<storm::pgcl::AssignmentStatement> createIntegerDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
+            std::shared_ptr<storm::pgcl::AssignmentStatement> createBooleanDeclarationStatement(std::string const& variableName, storm::expressions::Expression const& assignedExpression);
             std::shared_ptr<storm::pgcl::ObserveStatement> createObserveStatement(storm::pgcl::BooleanExpression const& condition);
             std::shared_ptr<storm::pgcl::IfStatement> createIfElseStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& if_body, boost::optional<std::vector<std::shared_ptr<storm::pgcl::Statement> > > const& else_body);
             std::shared_ptr<storm::pgcl::LoopStatement> createLoopStatement(storm::pgcl::BooleanExpression const& condition, std::vector<std::shared_ptr<storm::pgcl::Statement> > const& body);