diff --git a/src/storage/pgcl/Block.cpp b/src/storage/pgcl/Block.cpp
new file mode 100644
index 000000000..f2bbab4d8
--- /dev/null
+++ b/src/storage/pgcl/Block.cpp
@@ -0,0 +1,84 @@
+#include "Block.h"
+#include "StatementPrinterVisitor.h"
+#include <typeinfo>
+
+namespace storm {
+ namespace pgcl {
+
+
+ PgclBlock::PgclBlock(vector const &statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve)
+ : sequenceOfStatements(statements),
+ expressions(expressions),
+ loop(hasLoop),
+ nondet(hasNondet),
+ observe(hasObserve)
+ {
+
+ }
+
+ iterator PgclBlock::begin() {
+ return this->sequenceOfStatements.begin();
+ }
+
+ iterator PgclBlock::end() {
+ return this->sequenceOfStatements.end();
+ }
+
+ bool PgclBlock::empty() {
+ return this->sequenceOfStatements.empty();
+ }
+
+ element PgclBlock::front() {
+ return this->sequenceOfStatements.front();
+ }
+
+ element PgclBlock::back() {
+ return this->sequenceOfStatements.back();
+ }
+
+ unsigned long PgclBlock::size() {
+ return this->sequenceOfStatements.size();
+ }
+
+ element PgclBlock::at(size_type n) {
+ return this->sequenceOfStatements.at(n);
+ }
+
+ iterator PgclBlock::insert(iterator position, const element& statement) {
+ return this->sequenceOfStatements.insert(position, statement);
+ }
+
+ void PgclBlock::clear() {
+ this->sequenceOfStatements.clear();
+ }
+
+ std::shared_ptr<storm::expressions::ExpressionManager> PgclBlock::getExpressionManager() {
+ return this->expressions;
+ }
+
+ std::vector<storm::expressions::Variable> PgclBlock::getParameters() {
+ return this->parameters;
+ }
+
+ bool PgclBlock::hasParameters() const {
+ return !(this->parameters.empty());
+ }
+
+ bool PgclBlock::hasObserve() const {
+ return this->observe;
+ }
+
+ bool PgclBlock::hasNondet() const {
+ return this->nondet;
+ }
+
+ bool PgclBlock::hasLoop() const {
+ return this->loop;
+ }
+
+ iterator PgclBlock::find(element &statement) {
+ return std::find(this->sequenceOfStatements.begin(), this->sequenceOfStatements.end(), statement);
+ }
+
+ }
+}
\ No newline at end of file
diff --git a/src/storage/pgcl/Block.h b/src/storage/pgcl/Block.h
new file mode 100644
index 000000000..ab7638bfd
--- /dev/null
+++ b/src/storage/pgcl/Block.h
@@ -0,0 +1,119 @@
+#pragma once
+
+#include <vector>
+#include "src/storage/pgcl/Statement.h"
+#include "src/storage/pgcl/StatementPrinterVisitor.h"
+#include "src/storage/expressions/ExpressionManager.h"
+
+namespace storm {
+ namespace pgcl {
+
+ typedef std::shared_ptr<storm::pgcl::Statement> element;
+ typedef std::vector<element> vector;
+ typedef std::vector<element>::iterator iterator;
+ typedef std::vector<element>::const_iterator const_iterator;
+ typedef std::vector<element>::size_type size_type;
+
+ /**
+ * This class represents a complete and functional PGCL program. It
+ * contains an expression manager which keeps track of the current
+ * identifiers and variable valuations. Other than that, it basically
+ * wraps a std::vector of program statements and is intended to be used
+ * as such.
+ */
+ class PgclBlock {
+ public:
+ PgclBlock() = default;
+ /**
+ * Does the same as the beforementioned constructor, but sets the
+ * location to statement vector to the empty vector. This
+ * constructor should be used for sub-programs, for which the
+ * location to statement relation doesn't make much sense.
+ * @param statements The sequence of statements representing the
+ * program.
+ * @param expressions The manager responsible for the expressions
+ * and variables of the program.
+ * @param hasLoop Whether the program contains a loop
+ * @param hasNondet Whether the program contains a nondeterministic
+ * statement.
+ * @param hasParam Whether the program is parameterized.
+ */
+ PgclBlock(vector const& statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve);
+ PgclBlock(const PgclBlock & orig) = default;
+ PgclBlock & operator=(PgclBlock const& other) = default;
+ iterator begin();
+ iterator end();
+ element front();
+ element back();
+ unsigned long size();
+ element at(size_type n);
+ iterator insert(iterator position, const element& statement);
+ iterator find(element& statement);
+ void clear();
+ bool empty();
+
+ /**
+ * Returns the list of parameters of the PGCL program.
+ */
+ std::vector<storm::expressions::Variable> getParameters();
+ /**
+ * Returns the expression manager of the PGCL program, which is
+ * responsible for managing all expressions and variables of the
+ * the program and all its subprograms.
+ * @return The expression manager of the program.
+ */
+ std::shared_ptr<storm::expressions::ExpressionManager> getExpressionManager();
+ /**
+ * Returns true if the program contains a loop statement.
+ * @return True if the program has a loop.
+ */
+ bool hasLoop() const;
+ /**
+ * Returns true if the program contains a nondeterministic
+ * statement.
+ * @return True if the program has a nondeterministic statement.
+ */
+ bool hasNondet() const;
+ /**
+ * Returns true if the program contains an observe statement.
+ * @return True if the program has an observe statement.
+ */
+ bool hasObserve() const;
+ /**
+ * Returns true if the program is parameterized.
+ * @return True if the program has at least one parameter.
+ */
+ bool hasParameters() const;
+
+ protected:
+ /**
+ * We are basically wrapping a std::vector which represents the
+ * ordered single statements of the program.
+ */
+ vector sequenceOfStatements;
+ /**
+ * Stores the parameters a.k.a. free variables of the PGCL program.
+ */
+ std::vector<storm::expressions::Variable> parameters;
+ /**
+ * Handles the expressions and variables for the whole program.
+ * The expressions of every subprogram are also handled by this
+ * manager. We are using a shared pointer since all subprograms
+ * are referring to that expression manager, too.
+ */
+ std::shared_ptr<storm::expressions::ExpressionManager> expressions;
+ /**
+ * Boolean variables to save some properties of the PGCL program.
+ * They are later on used by the model builder to possibly
+ * construct simpler models (e.g. if no loops, params and nondets
+ * are used, a DTMC suffices).
+ * The values are set to true if the PGCL parser hits a loop resp.
+ * nondet resp. observe resp. parameter statement.
+ */
+ bool loop = false;
+ bool nondet = false;
+ bool observe = false;
+ bool top = false;
+ };
+ }
+}
diff --git a/src/storage/pgcl/BranchStatement.cpp b/src/storage/pgcl/BranchStatement.cpp
index 4acd6a55a..a3bc318d9 100755
--- a/src/storage/pgcl/BranchStatement.cpp
+++ b/src/storage/pgcl/BranchStatement.cpp
@@ -10,11 +10,11 @@
namespace storm {
namespace pgcl {
- std::shared_ptr<storm::pgcl::PgclProgram> BranchStatement::getLeftBranch() {
+ std::shared_ptr<storm::pgcl::PgclBlock> BranchStatement::getLeftBranch() {
return this->leftBranch;
}
- std::shared_ptr<storm::pgcl::PgclProgram> BranchStatement::getRightBranch() {
+ std::shared_ptr<storm::pgcl::PgclBlock> BranchStatement::getRightBranch() {
return this->rightBranch;
}
diff --git a/src/storage/pgcl/BranchStatement.h b/src/storage/pgcl/BranchStatement.h
index bd390e2f3..ee0ef5286 100755
--- a/src/storage/pgcl/BranchStatement.h
+++ b/src/storage/pgcl/BranchStatement.h
@@ -30,15 +30,15 @@ namespace storm {
* Returns the left branch of the statement.
* @return The left branch PGCL program.
*/
- std::shared_ptr<storm::pgcl::PgclProgram> getLeftBranch();
+ std::shared_ptr<storm::pgcl::PgclBlock> getLeftBranch();
/**
* Returns the right branch of the statement.
* @return The right branch PGCL program.
*/
- std::shared_ptr<storm::pgcl::PgclProgram> getRightBranch();
+ std::shared_ptr<storm::pgcl::PgclBlock> getRightBranch();
protected:
- std::shared_ptr<storm::pgcl::PgclProgram> leftBranch;
- std::shared_ptr<storm::pgcl::PgclProgram> rightBranch;
+ std::shared_ptr<storm::pgcl::PgclBlock> leftBranch;
+ std::shared_ptr<storm::pgcl::PgclBlock> rightBranch;
};
}
}
diff --git a/src/storage/pgcl/IfStatement.cpp b/src/storage/pgcl/IfStatement.cpp
index 7e62a96ab..64dc88607 100755
--- a/src/storage/pgcl/IfStatement.cpp
+++ b/src/storage/pgcl/IfStatement.cpp
@@ -10,20 +10,20 @@
namespace storm {
namespace pgcl {
- IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body) :
+ IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body) :
ifBody(body), condition(condition) {
}
- IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& ifBody, std::shared_ptr<storm::pgcl::PgclProgram> const& elseBody) :
+ IfStatement::IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& ifBody, std::shared_ptr<storm::pgcl::PgclBlock> const& elseBody) :
ifBody(ifBody), elseBody(elseBody), condition(condition) {
this->hasElseBody = true;
}
- std::shared_ptr<storm::pgcl::PgclProgram> IfStatement::getIfBody() {
+ std::shared_ptr<storm::pgcl::PgclBlock> IfStatement::getIfBody() {
return this->ifBody;
}
- std::shared_ptr<storm::pgcl::PgclProgram> IfStatement::getElseBody() {
+ std::shared_ptr<storm::pgcl::PgclBlock> IfStatement::getElseBody() {
if(this->elseBody) {
return this->elseBody;
} else {
diff --git a/src/storage/pgcl/IfStatement.h b/src/storage/pgcl/IfStatement.h
index 515fc7ecc..74bacac9b 100755
--- a/src/storage/pgcl/IfStatement.h
+++ b/src/storage/pgcl/IfStatement.h
@@ -29,14 +29,14 @@ namespace storm {
* @param condition The guard of the statement body.
* @param body The if body.
*/
- IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body);
+ IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body);
/**
* Creates an if statement with an if and an else body.
* @param condition The guard of the if body.
* @param ifBody The if body.
* @param elseBody The else body.
*/
- IfStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& ifBody, std::shared_ptr<storm::pgcl::PgclProgram> const& elseBody);
+ 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();
@@ -45,13 +45,13 @@ namespace storm {
* Returns the if body of the if statement.
* @return The if body.
*/
- std::shared_ptr<storm::pgcl::PgclProgram> getIfBody();
+ std::shared_ptr<storm::pgcl::PgclBlock> getIfBody();
/**
* Returns the else body of the if statement, if present. Otherwise
* it throws an excpetion.
* @return The else body.
*/
- std::shared_ptr<storm::pgcl::PgclProgram> getElseBody();
+ std::shared_ptr<storm::pgcl::PgclBlock> getElseBody();
/**
* Returns true iff the if statement has an else body.
*/
@@ -63,9 +63,9 @@ namespace storm {
storm::pgcl::BooleanExpression& getCondition();
private:
/// The if body is again a PGCL program.
- std::shared_ptr<storm::pgcl::PgclProgram> ifBody;
+ std::shared_ptr<storm::pgcl::PgclBlock> ifBody;
/// The else body is again a PGCL program.
- std::shared_ptr<storm::pgcl::PgclProgram> elseBody;
+ std::shared_ptr<storm::pgcl::PgclBlock> elseBody;
/// Memorizes if an else body was set. Set to false by default.
bool hasElseBody = false;
/// Saves the guard of the if statement.
diff --git a/src/storage/pgcl/LoopStatement.cpp b/src/storage/pgcl/LoopStatement.cpp
index b61b7cede..cdeff443c 100755
--- a/src/storage/pgcl/LoopStatement.cpp
+++ b/src/storage/pgcl/LoopStatement.cpp
@@ -10,11 +10,11 @@
namespace storm {
namespace pgcl {
- LoopStatement::LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body) :
+ LoopStatement::LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclBlock> const& body) :
body(body), condition(condition) {
}
- std::shared_ptr<storm::pgcl::PgclProgram> LoopStatement::getBody() {
+ std::shared_ptr<storm::pgcl::PgclBlock> LoopStatement::getBody() {
return this->body;
}
diff --git a/src/storage/pgcl/LoopStatement.h b/src/storage/pgcl/LoopStatement.h
index 57196021e..096a6e50a 100755
--- a/src/storage/pgcl/LoopStatement.h
+++ b/src/storage/pgcl/LoopStatement.h
@@ -27,7 +27,7 @@ namespace storm {
* @param condition The guard of the loop.
* @param body The body of the loop.
*/
- LoopStatement(storm::pgcl::BooleanExpression const& condition, std::shared_ptr<storm::pgcl::PgclProgram> const& body);
+ 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();
@@ -36,7 +36,7 @@ namespace storm {
* Returns the loop body program.
* @return The loop body program.
*/
- std::shared_ptr<storm::pgcl::PgclProgram> getBody();
+ std::shared_ptr<storm::pgcl::PgclBlock> getBody();
/**
* Returns the guard of the loop.
* @return The boolean condition of the loop.
@@ -44,7 +44,7 @@ namespace storm {
storm::pgcl::BooleanExpression& getCondition();
private:
/// Represents the loop body.
- std::shared_ptr<storm::pgcl::PgclProgram> body;
+ std::shared_ptr<storm::pgcl::PgclBlock> body;
/// Represents the loop guard.
storm::pgcl::BooleanExpression condition;
};
diff --git a/src/storage/pgcl/NondeterministicBranch.cpp b/src/storage/pgcl/NondeterministicBranch.cpp
index 5080fde2e..25b8d741a 100755
--- a/src/storage/pgcl/NondeterministicBranch.cpp
+++ b/src/storage/pgcl/NondeterministicBranch.cpp
@@ -10,7 +10,7 @@
namespace storm {
namespace pgcl {
- NondeterministicBranch::NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right) {
+ NondeterministicBranch::NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right) {
leftBranch = left;
rightBranch = right;
}
diff --git a/src/storage/pgcl/NondeterministicBranch.h b/src/storage/pgcl/NondeterministicBranch.h
index 18b8700d5..87ce9d1e7 100755
--- a/src/storage/pgcl/NondeterministicBranch.h
+++ b/src/storage/pgcl/NondeterministicBranch.h
@@ -25,7 +25,7 @@ namespace storm {
* @param left The left (first) subprogram of the branch.
* @param right The right (second) subprogram of the branch.
*/
- NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right);
+ NondeterministicBranch(std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right);
NondeterministicBranch(const NondeterministicBranch& orig) = default;
virtual ~NondeterministicBranch() = default;
void accept(class AbstractStatementVisitor&);
diff --git a/src/storage/pgcl/PgclProgram.cpp b/src/storage/pgcl/PgclProgram.cpp
index 1b9d6916a..4666a8ef8 100755
--- a/src/storage/pgcl/PgclProgram.cpp
+++ b/src/storage/pgcl/PgclProgram.cpp
@@ -1,108 +1,21 @@
-/*
- * File: PgclProgram.cpp
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:39
- */
-
#include "PgclProgram.h"
#include "StatementPrinterVisitor.h"
#include <typeinfo>
namespace storm {
namespace pgcl {
- PgclProgram::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, bool isTop) :
- sequenceOfStatements(statements),
- locationToStatement(locationToStatement),
- parameters(parameters),
- expressions(expressions),
- loop(hasLoop),
- nondet(hasNondet),
- observe(hasObserve),
- top(isTop) {
- }
-
- PgclProgram::PgclProgram(vector const &statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop) :
- sequenceOfStatements(statements),
- expressions(expressions),
- loop(hasLoop),
- nondet(hasNondet),
- observe(hasObserve),
- top(isTop) {
- }
-
- iterator PgclProgram::begin() {
- return this->sequenceOfStatements.begin();
- }
-
- iterator PgclProgram::end() {
- return this->sequenceOfStatements.end();
- }
-
- bool PgclProgram::empty() {
- return this->sequenceOfStatements.empty();
- }
-
- element PgclProgram::front() {
- return this->sequenceOfStatements.front();
- }
-
- element PgclProgram::back() {
- return this->sequenceOfStatements.back();
+ PgclProgram::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) :
+ PgclBlock(statements,
+ expressions, hasLoop, hasNondet, hasObserve),
+ locationToStatement(locationToStatement)
+ {
}
- unsigned long PgclProgram::size() {
- return this->sequenceOfStatements.size();
- }
-
- element PgclProgram::at(size_type n) {
- return this->sequenceOfStatements.at(n);
- }
-
- iterator PgclProgram::insert(iterator position, const element& statement) {
- return this->sequenceOfStatements.insert(position, statement);
- }
- void PgclProgram::clear() {
- this->sequenceOfStatements.clear();
- }
-
- std::shared_ptr<storm::expressions::ExpressionManager> PgclProgram::getExpressionManager() {
- return this->expressions;
- }
-
- std::vector<storm::expressions::Variable> PgclProgram::getParameters() {
- return this->parameters;
- }
-
- bool PgclProgram::hasParameters() const {
- return !(this->parameters.empty());
- }
-
- bool PgclProgram::hasObserve() const {
- return this->observe;
- }
-
- bool PgclProgram::hasNondet() const {
- return this->nondet;
- }
-
- bool PgclProgram::hasLoop() const {
- return this->loop;
- }
-
vector PgclProgram::getLocationToStatementVector() {
return this->locationToStatement;
}
- iterator PgclProgram::find(element &statement) {
- return std::find(this->sequenceOfStatements.begin(), this->sequenceOfStatements.end(), statement);
- }
-
- bool PgclProgram::isTop() const {
- return this->top;
- }
-
std::ostream& operator<<(std::ostream& stream, PgclProgram& program) {
storm::pgcl::StatementPrinterVisitor printer(stream);
for(iterator statement = program.begin(); statement != program.end(); statement++) {
diff --git a/src/storage/pgcl/PgclProgram.h b/src/storage/pgcl/PgclProgram.h
index acff0c7e1..6b3635d22 100755
--- a/src/storage/pgcl/PgclProgram.h
+++ b/src/storage/pgcl/PgclProgram.h
@@ -1,14 +1,7 @@
-/*
- * File: PgclProgram.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:39
- */
-
-#ifndef PGCLPROGRAM_H
-#define PGCLPROGRAM_H
+#pragma once
#include <vector>
+#include "Block.h"
#include "src/storage/pgcl/Statement.h"
#include "src/storage/pgcl/StatementPrinterVisitor.h"
#include "src/storage/expressions/ExpressionManager.h"
@@ -16,11 +9,6 @@
namespace storm {
namespace pgcl {
- typedef std::shared_ptr<storm::pgcl::Statement> element;
- typedef std::vector<element> vector;
- typedef std::vector<element>::iterator iterator;
- typedef std::vector<element>::const_iterator const_iterator;
- typedef std::vector<element>::size_type size_type;
/**
* This class represents a complete and functional PGCL program. It
@@ -29,7 +17,7 @@ namespace storm {
* wraps a std::vector of program statements and is intended to be used
* as such.
*/
- class PgclProgram {
+ class PgclProgram : public PgclBlock {
public:
PgclProgram() = default;
/**
@@ -48,114 +36,24 @@ namespace storm {
* statement.
* @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, bool isTop);
- /**
- * Does the same as the beforementioned constructor, but sets the
- * location to statement vector to the empty vector. This
- * constructor should be used for sub-programs, for which the
- * location to statement relation doesn't make much sense.
- * @param statements The sequence of statements representing the
- * program.
- * @param expressions The manager responsible for the expressions
- * and variables of the program.
- * @param hasLoop Whether the program contains a loop
- * @param hasNondet Whether the program contains a nondeterministic
- * statement.
- * @param hasParam Whether the program is parameterized.
- */
- PgclProgram(vector const& statements, std::shared_ptr<storm::expressions::ExpressionManager> expressions, bool hasLoop, bool hasNondet, bool hasObserve, bool isTop);
- PgclProgram(const PgclProgram & orig) = default;
- PgclProgram & operator=(PgclProgram const& other) = default;
- iterator begin();
- iterator end();
- element front();
- element back();
- unsigned long size();
- element at(size_type n);
- iterator insert(iterator position, const element& statement);
- iterator find(element& statement);
- void clear();
- bool empty();
+ 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;
+
/**
* Returns a vector that has the statement with location number i at
* its i-th position. This allows for O(1)-access of statements if
* only the location number is given.
*/
vector getLocationToStatementVector();
- /**
- * Returns the list of parameters of the PGCL program.
- */
- std::vector<storm::expressions::Variable> getParameters();
- /**
- * Returns the expression manager of the PGCL program, which is
- * responsible for managing all expressions and variables of the
- * the program and all its subprograms.
- * @return The expression manager of the program.
- */
- std::shared_ptr<storm::expressions::ExpressionManager> getExpressionManager();
- /**
- * Returns true if the program contains a loop statement.
- * @return True if the program has a loop.
- */
- bool hasLoop() const;
- /**
- * Returns true if the program contains a nondeterministic
- * statement.
- * @return True if the program has a nondeterministic statement.
- */
- bool hasNondet() const;
- /**
- * Returns true if the program contains an observe statement.
- * @return True if the program has an observe statement.
- */
- bool hasObserve() const;
- /**
- * Returns true if the program is parameterized.
- * @return True if the program has at least one parameter.
- */
- bool hasParameters() const;
- /**
- * Returns whether the program is no subprogram.
- * @return True if the program is no subprogram of another
- * program.
- */
- bool isTop() const;
+
private:
- /**
- * We are basically wrapping a std::vector which represents the
- * ordered single statements of the program.
- */
- vector sequenceOfStatements;
/**
* Contains the statement with location i at its i-th position.
* Imagine this as the "unrolled" sequence of statements, so the
* recursion is resolved here.
*/
vector locationToStatement;
- /**
- * Stores the parameters a.k.a. free variables of the PGCL program.
- */
- std::vector<storm::expressions::Variable> parameters;
- /**
- * Handles the expressions and variables for the whole program.
- * The expressions of every subprogram are also handled by this
- * manager. We are using a shared pointer since all subprograms
- * are referring to that expression manager, too.
- */
- std::shared_ptr<storm::expressions::ExpressionManager> expressions;
- /**
- * Boolean variables to save some properties of the PGCL program.
- * They are later on used by the model builder to possibly
- * construct simpler models (e.g. if no loops, params and nondets
- * are used, a DTMC suffices).
- * The values are set to true if the PGCL parser hits a loop resp.
- * nondet resp. observe resp. parameter statement.
- */
- bool loop = false;
- bool nondet = false;
- bool observe = false;
- bool top = false;
- };
+ };
/**
* Prints every statement of the program along with their location
* numbers.
@@ -166,5 +64,4 @@ namespace storm {
}
}
-#endif /* PGCLPROGRAM_H */
diff --git a/src/storage/pgcl/ProbabilisticBranch.cpp b/src/storage/pgcl/ProbabilisticBranch.cpp
index 795284932..1c0e0e773 100755
--- a/src/storage/pgcl/ProbabilisticBranch.cpp
+++ b/src/storage/pgcl/ProbabilisticBranch.cpp
@@ -10,7 +10,7 @@
namespace storm {
namespace pgcl {
- ProbabilisticBranch::ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right) :
+ ProbabilisticBranch::ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right) :
probability(probability) {
rightBranch = right;
leftBranch = left;
diff --git a/src/storage/pgcl/ProbabilisticBranch.h b/src/storage/pgcl/ProbabilisticBranch.h
index 669f3fb2a..29e058897 100755
--- a/src/storage/pgcl/ProbabilisticBranch.h
+++ b/src/storage/pgcl/ProbabilisticBranch.h
@@ -31,7 +31,7 @@ namespace storm {
* @param left The left (first) subprogram of the branch.
* @param right The right (second) subprogram of the branch.
*/
- ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclProgram> const& left, std::shared_ptr<storm::pgcl::PgclProgram> const& right);
+ ProbabilisticBranch(storm::expressions::Expression const& probability, std::shared_ptr<storm::pgcl::PgclBlock> const& left, std::shared_ptr<storm::pgcl::PgclBlock> const& right);
ProbabilisticBranch(const ProbabilisticBranch& orig) = default;
virtual ~ProbabilisticBranch() = default;
/**
diff --git a/src/storage/pgcl/Statement.cpp b/src/storage/pgcl/Statement.cpp
index 25aece4d4..8bbfcde4d 100755
--- a/src/storage/pgcl/Statement.cpp
+++ b/src/storage/pgcl/Statement.cpp
@@ -1,11 +1,5 @@
-/*
- * File: Statement.cpp
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:41
- */
-
#include "src/storage/pgcl/Statement.h"
+#include "Block.h"
namespace storm {
namespace pgcl {
@@ -41,21 +35,14 @@ namespace storm {
return false;
}
- void Statement::setParentProgram(std::shared_ptr<storm::pgcl::PgclProgram> parentProgram) {
- this->parentProgram = parentProgram;
- }
-
- boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > Statement::getParentProgram() {
- return this->parentProgram;
+ void Statement::setParentBlock(PgclBlock* b) {
+ this->parentBlock = b;
}
- void Statement::setParentStatement(std::shared_ptr<storm::pgcl::Statement> parentStatement) {
- this->parentStatement = parentStatement;
+ PgclBlock* Statement::getParentBlock() {
+ return this->parentBlock;
}
- boost::optional<std::shared_ptr<storm::pgcl::Statement> > Statement::getParentStatement() {
- return this->parentStatement;
- }
std::size_t Statement::getNumberOfOutgoingTransitions() {
return 1;
diff --git a/src/storage/pgcl/Statement.h b/src/storage/pgcl/Statement.h
index 6afee011e..9690cfe0e 100755
--- a/src/storage/pgcl/Statement.h
+++ b/src/storage/pgcl/Statement.h
@@ -1,12 +1,4 @@
-/*
- * File: Statement.h
- * Author: Lukas Westhofen
- *
- * Created on 11. April 2015, 17:41
- */
-
-#ifndef STATEMENT_H
-#define STATEMENT_H
+#pragma once
#include <cstdint>
#include <memory>
@@ -14,7 +6,7 @@
namespace storm {
namespace pgcl {
- class PgclProgram;
+ class PgclBlock;
/**
* A PGCL program consists of various statements. Statements can again
* save lists of statements as their children. To make life easier, the
@@ -80,27 +72,16 @@ namespace storm {
* Sets the parent program of the statement.
* @param parentProgram The parent program of the statement.
*/
- void setParentProgram(std::shared_ptr<storm::pgcl::PgclProgram> parentProgram);
+ void setParentBlock(PgclBlock* block);
/**
* Returns the parent program of the statement.
* @return The parent program of the statement.
*/
- boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > getParentProgram();
- /**
- * Sets the parent statement of the statement.
- * @param parentProgram The parent statement of the statement.
- */
- void setParentStatement(std::shared_ptr<storm::pgcl::Statement> parentStatement);
- /**
- * Returns the parent statement of the statement.
- * @return The parent statement of the statement.
- */
- boost::optional<std::shared_ptr<storm::pgcl::Statement> > getParentStatement();
+ PgclBlock* getParentBlock();
+
protected:
/// The parent program of the statement.
- boost::optional<std::shared_ptr<storm::pgcl::PgclProgram> > parentProgram;
- /// The parent program of the statement.
- boost::optional<std::shared_ptr<storm::pgcl::Statement> > parentStatement;
+ PgclBlock* parentBlock;
/// Represents the line number of the statement.
std::size_t lineNumber = 0;
/// Represents the unique statement location.
@@ -110,5 +91,4 @@ namespace storm {
};
}
}
-#endif /* STATEMENT_H */