Good old const correctness added to all pgcl structs.

Former-commit-id: 387e3f7206 [formerly 5d53a2e8d3]
Former-commit-id: d4a7f36efd

src/storage/pgcl/AbstractStatementVisitor.h

@@ -1,9 +1,4 @@
-//
-// Created by Lukas Westhofen on 22.04.15.
-//
-
-#ifndef STORM_ABSTRACTSTATEVISITOR_H
-#define STORM_ABSTRACTSTATEVISITOR_H
+#pragma once 
 
 namespace storm {
     namespace pgcl {
@@ -20,14 +15,13 @@ namespace storm {
         public:
             // Those functions need to be implemented for every possible
             // statement instantiation.
-            virtual void visit(class AssignmentStatement&) = 0;
-            virtual void visit(class ObserveStatement&) = 0;
-            virtual void visit(class IfStatement&) = 0;
-            virtual void visit(class LoopStatement&) = 0;
-            virtual void visit(class NondeterministicBranch&) = 0;
-            virtual void visit(class ProbabilisticBranch&) = 0;
+            virtual void visit(class AssignmentStatement const&) = 0;
+            virtual void visit(class ObserveStatement const&) = 0;
+            virtual void visit(class IfStatement const&) = 0;
+            virtual void visit(class LoopStatement const&) = 0;
+            virtual void visit(class NondeterministicBranch const&) = 0;
+            virtual void visit(class ProbabilisticBranch const&) = 0;
         };
     }
 }
 
-#endif //STORM_ABSTRACTSTATEVISITOR_H

src/storage/pgcl/AssignmentStatement.cpp

@@ -13,25 +13,17 @@ namespace storm {
             variable(variable), expression(expression) {
         }
         
-        boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& AssignmentStatement::getExpression() {
+        boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& AssignmentStatement::getExpression() const {
             return this->expression;
         }
 
-        storm::expressions::Variable const& AssignmentStatement::getVariable() {
+        storm::expressions::Variable const& AssignmentStatement::getVariable() const {
             return this->variable;
         }
 
         void AssignmentStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
             visitor.visit(*this);
         }
-
-        std::size_t AssignmentStatement::getNumberOfOutgoingTransitions() {
-            if(this->expression.which() == 1) {
-                return boost::get<storm::pgcl::UniformExpression>(this->expression).getEnd() - boost::get<storm::pgcl::UniformExpression>(this->expression).getBegin() + 1;
-            } else {
-                return 1;
-            }
-        }
     }
 }
 

src/storage/pgcl/AssignmentStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   AssignmentStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:42
- */
-
-#ifndef ASSIGNMENTSTATEMENT_H
-#define	ASSIGNMENTSTATEMENT_H
+#pragma once
 
 #include "src/storage/pgcl/SimpleStatement.h"
 #include "src/storage/pgcl/UniformExpression.h"
@@ -34,18 +26,17 @@ namespace storm {
             AssignmentStatement(storm::expressions::Variable const& variable, boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& expression);
             AssignmentStatement(const AssignmentStatement& orig) = default;
             virtual ~AssignmentStatement() = default;
-            std::size_t getNumberOfOutgoingTransitions();
-            void accept(class AbstractStatementVisitor&);
+            void accept(AbstractStatementVisitor&);
             /**
              * Returns the right hand expression of the assignemnt.
              * @return The expression of the assignment.
              */
-            boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& getExpression();
+            boost::variant<storm::expressions::Expression, storm::pgcl::UniformExpression> const& getExpression() const;
             /**
              * Returns the left hand variable of the assignemnt.
              * @return The variable to which the expression is assigned.
              */
-            storm::expressions::Variable const& getVariable();
+            storm::expressions::Variable const& getVariable() const;
         private:
             /// Represents the variable of our assignment statement.
             storm::expressions::Variable variable;
@@ -54,6 +45,3 @@ namespace storm {
         };
     }
 }
-
-#endif	/* ASSIGNMENTSTATEMENT_H */
-

src/storage/pgcl/Block.cpp

@@ -20,10 +20,18 @@ namespace storm {
             return this->sequenceOfStatements.begin();
         }
         
+        const_iterator PgclBlock::begin() const {
+            return this->sequenceOfStatements.begin();
+        }
+        
         iterator PgclBlock::end() {
             return this->sequenceOfStatements.end();
         }
         
+        const_iterator PgclBlock::end() const {
+            return this->sequenceOfStatements.end();
+        }
+        
         bool PgclBlock::empty() {
             return this->sequenceOfStatements.empty();
         }
@@ -52,7 +60,7 @@ namespace storm {
             this->sequenceOfStatements.clear();
         }
         
-        std::shared_ptr<storm::expressions::ExpressionManager> PgclBlock::getExpressionManager() {
+        std::shared_ptr<storm::expressions::ExpressionManager> const&  PgclBlock::getExpressionManager() const  {
             return this->expressions;
         }
         

src/storage/pgcl/Block.h

@@ -42,7 +42,9 @@ namespace storm {
             PgclBlock(const PgclBlock & orig) = default;
             PgclBlock & operator=(PgclBlock const& other) = default;
             iterator begin();
+            const_iterator begin() const;
             iterator end();
+            const_iterator end() const;
             element front();
             element back();
             unsigned long size();
@@ -62,7 +64,8 @@ namespace storm {
              * the program and all its subprograms.
              * @return The expression manager of the program.
              */
-            std::shared_ptr<storm::expressions::ExpressionManager> getExpressionManager();
+            std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const;
+            
             /**
              * Returns true if the program contains a loop statement.
              * @return True if the program has a loop.
@@ -84,7 +87,7 @@ namespace storm {
              * @return True if the program has at least one parameter.
              */
             bool hasParameters() const;
-           
+            
         protected:
             /**
              * We are basically wrapping a std::vector which represents the
@@ -113,7 +116,6 @@ namespace storm {
             bool loop    = false;
             bool nondet  = false;
             bool observe = false;
-            bool top     = false;
         };
     }
 }

src/storage/pgcl/BooleanExpression.cpp

@@ -14,7 +14,7 @@ namespace storm {
             booleanExpression(booleanExpression) {
         }
         
-        storm::expressions::Expression& BooleanExpression::getBooleanExpression() {
+        storm::expressions::Expression const& BooleanExpression::getBooleanExpression() const {
             return this->booleanExpression;
         }
     }

src/storage/pgcl/BooleanExpression.h

@@ -31,7 +31,7 @@ namespace storm {
              * Returns the expression.
              * @return The expression of boolean type.
              */
-            storm::expressions::Expression& getBooleanExpression();
+            storm::expressions::Expression const& getBooleanExpression() const;
         private:
             storm::expressions::Expression booleanExpression;
         };

src/storage/pgcl/BranchStatement.cpp

@@ -10,16 +10,13 @@
 
 namespace storm {
     namespace pgcl {
-        std::shared_ptr<storm::pgcl::PgclBlock> BranchStatement::getLeftBranch() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& BranchStatement::getLeftBranch() const {
             return this->leftBranch;
         }
 
-        std::shared_ptr<storm::pgcl::PgclBlock> BranchStatement::getRightBranch() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& BranchStatement::getRightBranch() const {
             return this->rightBranch;
         }
 
-        std::size_t BranchStatement::getNumberOfOutgoingTransitions() {
-            return 2;
-        }
     }
 }

src/storage/pgcl/BranchStatement.h

@@ -1,12 +1,4 @@
-/* 
- * File:   BranchStatement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:42
- */
-
-#ifndef BRANCHSTATEMENT_H
-#define	BRANCHSTATEMENT_H
+#pragma once 
 
 #include "src/storage/pgcl/PgclProgram.h"
 #include "src/storage/pgcl/CompoundStatement.h"
@@ -25,22 +17,19 @@ namespace storm {
             BranchStatement(const BranchStatement& orig) = default;
             virtual ~BranchStatement() = default;
             virtual void accept(class AbstractStatementVisitor&) = 0;
-            std::size_t getNumberOfOutgoingTransitions();
             /**
              * Returns the left branch of the statement.
              * @return The left branch PGCL program.
              */
-            std::shared_ptr<storm::pgcl::PgclBlock> getLeftBranch();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getLeftBranch() const;
             /**
              * Returns the right branch of the statement.
              * @return The right branch PGCL program.
              */
-            std::shared_ptr<storm::pgcl::PgclBlock> getRightBranch();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getRightBranch() const;
         protected:
             std::shared_ptr<storm::pgcl::PgclBlock> leftBranch;
             std::shared_ptr<storm::pgcl::PgclBlock> rightBranch;
         };
     }
 }
-
-#endif	/* BRANCHSTATEMENT_H */

src/storage/pgcl/IfStatement.cpp

@@ -19,11 +19,11 @@ namespace storm {
             this->hasElseBody = true;
         }
 
-        std::shared_ptr<storm::pgcl::PgclBlock> IfStatement::getIfBody() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& IfStatement::getIfBody() const {
             return this->ifBody;
         }
 
-        std::shared_ptr<storm::pgcl::PgclBlock> IfStatement::getElseBody() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& IfStatement::getElseBody() const {
             if(this->elseBody) {
                 return this->elseBody;
             } else {
@@ -31,11 +31,11 @@ namespace storm {
             }
         }
         
-        bool IfStatement::hasElse() {
+        bool IfStatement::hasElse() const{
             return this->hasElseBody;
         }
         
-        storm::pgcl::BooleanExpression& IfStatement::getCondition() {
+        storm::pgcl::BooleanExpression const& IfStatement::getCondition() const {
             return this->condition;
         }
 
@@ -43,8 +43,5 @@ namespace storm {
             visitor.visit(*this);
         }
 
-        std::size_t IfStatement::getNumberOfOutgoingTransitions() {
-            return 1;
-        }
     }
 }

src/storage/pgcl/IfStatement.h

@@ -39,28 +39,27 @@ namespace storm {
             IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& ifBody, std::shared_ptr<storm::pgcl::PgclBlock> const& elseBody);
             IfStatement(const IfStatement& orig) = default;
             virtual ~IfStatement() = default;
-            std::size_t getNumberOfOutgoingTransitions();
             void accept(class AbstractStatementVisitor&);
             /**
              * Returns the if body of the if statement.
              * @return The if body.
              */
-            std::shared_ptr<storm::pgcl::PgclBlock> getIfBody();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getIfBody() const;
             /**
              * Returns the else body of the if statement, if present. Otherwise
              * it throws an excpetion.
              * @return The else body.
              */
-            std::shared_ptr<storm::pgcl::PgclBlock> getElseBody();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getElseBody() const;
             /**
              * Returns true iff the if statement has an else body.
              */
-            bool hasElse();
+            bool hasElse() const;
             /**
              * Returns the guard of the if statement.
              * @return The condition.
              */
-            storm::pgcl::BooleanExpression& getCondition();
+            storm::pgcl::BooleanExpression const& getCondition() const;
         private:
             /// The if body is again a PGCL program.
             std::shared_ptr<storm::pgcl::PgclBlock> ifBody;

src/storage/pgcl/LoopStatement.cpp

@@ -14,21 +14,17 @@ namespace storm {
             body(body), condition(condition) {
         }
 
-        std::shared_ptr<storm::pgcl::PgclBlock> LoopStatement::getBody() {
+        std::shared_ptr<storm::pgcl::PgclBlock> const& LoopStatement::getBody() const {
             return this->body;
         }
         
-        storm::pgcl::BooleanExpression& LoopStatement::getCondition() {
+        storm::pgcl::BooleanExpression const& LoopStatement::getCondition() const{
             return this->condition;
         }
 
         void LoopStatement::accept(storm::pgcl::AbstractStatementVisitor& visitor) {
             visitor.visit(*this);
         }
-
-        std::size_t LoopStatement::getNumberOfOutgoingTransitions() {
-            return 1;
-        }
     }
 }
 

src/storage/pgcl/LoopStatement.h

@@ -30,18 +30,17 @@ namespace storm {
             LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body);
             LoopStatement(const LoopStatement& orig) = default;
             virtual ~LoopStatement() = default;
-            std::size_t getNumberOfOutgoingTransitions();
             void accept(class AbstractStatementVisitor&);
             /**
              * Returns the loop body program.
              * @return The loop body program.
              */
-            std::shared_ptr<storm::pgcl::PgclBlock> getBody();
+            std::shared_ptr<storm::pgcl::PgclBlock> const& getBody() const;
             /**
              * Returns the guard of the loop.
              * @return The boolean condition of the loop.
              */
-            storm::pgcl::BooleanExpression& getCondition();
+            storm::pgcl::BooleanExpression const& getCondition() const;
         private:
             /// Represents the loop body.
             std::shared_ptr<storm::pgcl::PgclBlock> body;

src/storage/pgcl/NondeterministicBranch.cpp

@@ -19,7 +19,7 @@ namespace storm {
             visitor.visit(*this);
         }
 
-        bool NondeterministicBranch::isNondet() {
+        bool NondeterministicBranch::isNondet() const {
             return true;
         }
     }

src/storage/pgcl/NondeterministicBranch.h

@@ -29,7 +29,7 @@ namespace storm {
             NondeterministicBranch(const NondeterministicBranch& orig) = default;
             virtual ~NondeterministicBranch() = default;
             void accept(class AbstractStatementVisitor&);
-            bool isNondet();
+            bool isNondet() const;
         private:
         };
     }

src/storage/pgcl/ObserveStatement.cpp

@@ -17,13 +17,10 @@ namespace storm {
             visitor.visit(*this);
         }
 
-        storm::pgcl::BooleanExpression& ObserveStatement::getCondition() {
+        storm::pgcl::BooleanExpression const& ObserveStatement::getCondition() const {
             return this->condition;
         }
 
-        std::size_t ObserveStatement::getNumberOfOutgoingTransitions() {
-            return 1;
-        }
     }
 }
 

src/storage/pgcl/ObserveStatement.h

@@ -28,13 +28,12 @@ namespace storm {
              */
             ObserveStatement(storm::pgcl::BooleanExpression const& condition);
             ObserveStatement(const ObserveStatement& orig) = default;
-            std::size_t getNumberOfOutgoingTransitions();
             virtual ~ObserveStatement() = default;
             /**
              * Returns the condition of the observe statement.
              * @return The boolean expression of the observe statement.
              */
-            storm::pgcl::BooleanExpression& getCondition();
+            storm::pgcl::BooleanExpression const& getCondition() const;
             void accept(class AbstractStatementVisitor&);
         private:
             /// Represents the assigned condition.

src/storage/pgcl/PgclProgram.cpp

@@ -15,6 +15,15 @@ namespace storm {
         vector PgclProgram::getLocationToStatementVector() {
             return this->locationToStatement;
         }
+        
+        std::vector<storm::expressions::Variable> PgclProgram::getVariables() const {
+            std::vector<storm::expressions::Variable> vars;
+            for(auto const& v : *(this->getExpressionManager())) {
+                vars.push_back(v.first);
+            }
+            
+            return vars;
+        }
 
         std::ostream& operator<<(std::ostream& stream, PgclProgram& program) {
             storm::pgcl::StatementPrinterVisitor printer(stream);

src/storage/pgcl/PgclProgram.h

@@ -37,7 +37,8 @@ namespace storm {
              * @param hasParam Whether the program is parameterized.
              */
             PgclProgram(vector const& statements, vector const& locationToStatement, std::vector<storm::expressions::Variable> const& parameters, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve);
-                        PgclProgram(const PgclProgram & orig) = default;
+            
+            PgclProgram(const PgclProgram & orig) = default;
             
             /**
              * Returns a vector that has the statement with location number i at
@@ -46,6 +47,8 @@ namespace storm {
              */
             vector getLocationToStatementVector();
             
+            std::vector<storm::expressions::Variable> getVariables() const;
+            
         private:
             /**
              * Contains the statement with location i at its i-th position.

src/storage/pgcl/ProbabilisticBranch.cpp

@@ -16,7 +16,7 @@ namespace storm {
             leftBranch = left;
         }
         
-        storm::expressions::Expression& ProbabilisticBranch::getProbability() {
+        storm::expressions::Expression const& ProbabilisticBranch::getProbability() const {
             return this->probability;
         }
 

src/storage/pgcl/ProbabilisticBranch.h

@@ -38,7 +38,7 @@ namespace storm {
              * Returns the expression representing the probability.
              * @return The expression representing the probability.
              */
-            storm::expressions::Expression& getProbability();
+            storm::expressions::Expression const& getProbability() const;
             void accept(class AbstractStatementVisitor&);
         private:
             /// The expression represents the probability of the branch.

src/storage/pgcl/Statement.cpp

@@ -11,11 +11,11 @@ namespace storm {
             this->lineNumber = lineNumber;
         }
 
-        std::size_t Statement::getLineNumber() {
+        std::size_t Statement::getLineNumber() const {
             return this->lineNumber;
         }
 
-        std::size_t Statement::getLocationNumber() {
+        std::size_t Statement::getLocationNumber() const {
             return this->locationNumber;
         }
 
@@ -23,7 +23,7 @@ namespace storm {
             this->locationNumber = locationNumber;
         }
 
-        bool Statement::isLast() {
+        bool Statement::isLast() const {
             return this->last;
         }
 
@@ -31,7 +31,7 @@ namespace storm {
             this->last = isLast;
         }
 
-        bool Statement::isNondet() {
+        bool Statement::isNondet() const {
             return false;
         }
 
@@ -44,7 +44,7 @@ namespace storm {
         }
 
 
-        std::size_t Statement::getNumberOfOutgoingTransitions() {
+        std::size_t Statement::getNumberOfOutgoingTransitions() const {
             return 1;
         }
     }

src/storage/pgcl/Statement.h

@@ -31,7 +31,7 @@ namespace storm {
              * was parsed from.
              * @return The line number of the statement.
              */
-            std::size_t getLineNumber();
+            std::size_t getLineNumber() const;
             /**
              * Sets the line number during the parsing process.
              * @param lineNumber The location number of the statement.
@@ -41,7 +41,7 @@ namespace storm {
              * Returns the unique location number of the statement.
              * @return The line number of the statement.
              */
-            std::size_t getLocationNumber();
+            std::size_t getLocationNumber() const;
             /**
              * Sets the unique location number of the statement.
              * @param lineNumber The location number of the statement.
@@ -52,7 +52,7 @@ namespace storm {
              * program.
              * @return true Whether the statement is the last statement.
              */
-            bool isLast();
+            bool isLast() const;
             /**
              * Sets the information whether the statement is the last of its
              * direct parent program.
@@ -62,11 +62,11 @@ namespace storm {
             /**
              * Returns wether the statements represents nondeterminism.
              */
-            virtual bool isNondet();
+            virtual bool isNondet() const;
             /**
              * Returns the number of transitions this statement will produce.
              */
-            virtual std::size_t getNumberOfOutgoingTransitions();
+            virtual std::size_t getNumberOfOutgoingTransitions() const;
             virtual void accept(class AbstractStatementVisitor&) = 0;
             /**
              * Sets the parent program of the statement.

src/storage/pgcl/StatementPrinterVisitor.cpp

@@ -16,7 +16,7 @@ namespace storm {
         StatementPrinterVisitor::StatementPrinterVisitor(std::ostream &stream) : stream(stream) {
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::AssignmentStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::AssignmentStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             if(statement.getExpression().which() == 0) {
                 storm::expressions::Expression const& expression = boost::get<storm::expressions::Expression>(statement.getExpression());
@@ -27,12 +27,12 @@ namespace storm {
             }
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::ObserveStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::ObserveStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "observe(" << statement.getCondition().getBooleanExpression() << ");" << std::endl;
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::IfStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::IfStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "if(" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
             int i = 1;
@@ -51,7 +51,7 @@ namespace storm {
             }
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::LoopStatement& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::LoopStatement const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "while(" << statement.getCondition().getBooleanExpression() << ") {" << std::endl;
             int i = 1;
@@ -62,7 +62,7 @@ namespace storm {
             this->stream << "}" << std::endl;
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::NondeterministicBranch& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::NondeterministicBranch const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "{" << std::endl;
             int i = 1;
@@ -78,7 +78,7 @@ namespace storm {
             this->stream << "}" << std::endl;
         }
 
-        void StatementPrinterVisitor::visit(storm::pgcl::ProbabilisticBranch& statement) {
+        void StatementPrinterVisitor::visit(storm::pgcl::ProbabilisticBranch const& statement) {
             this->stream << statement.getLocationNumber() << ": ";
             this->stream << "{" << std::endl;
             int i = 1;

src/storage/pgcl/StatementPrinterVisitor.h

@@ -24,12 +24,12 @@ namespace storm {
              * @param stream The stream to print to.
              */
             StatementPrinterVisitor(std::ostream& stream);
-            void visit(class AssignmentStatement&);
-            void visit(class ObserveStatement&);
-            void visit(class IfStatement&);
-            void visit(class LoopStatement&);
-            void visit(class NondeterministicBranch&);
-            void visit(class ProbabilisticBranch&);
+            void visit(AssignmentStatement const&);
+            void visit(ObserveStatement const&);
+            void visit(IfStatement const&);
+            void visit(LoopStatement const&);
+            void visit(NondeterministicBranch const&);
+            void visit(ProbabilisticBranch const&);
         private:
             std::ostream& stream;
         };