Merge branch 'master' of https://sselab.de/lab9/private/git/MRMC/

Conflicts:
	src/storage/SquareSparseMatrix.h
(resolved by sticking to the version of master branch)

src/formula/AP.h

@@ -38,18 +38,6 @@ public:
 		this->ap = ap;
 	}
 
-	/*!
-	 * Constructor
-	 *
-	 * Creates a new atomic proposition leaf, with the label AP
-	 *
-	 * @param ap The string representing the atomic proposition
-	 */
-	AP(char* ap) {
-	 //TODO: Does that really work?
-		this->ap = ap;
-	}
-
 	/*!
 	 * Destructor.
 	 * At this time, empty...
@@ -59,7 +47,7 @@ public:
 	/*!
 	 * @returns the name of the atomic proposition
 	 */
-	const std::string& getAP() {
+	const std::string& getAP() const {
 		return ap;
 	}
 
@@ -67,7 +55,7 @@ public:
 	 * @returns a string representation of the leaf.
 	 *
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		return getAP();
 	}
 
@@ -76,7 +64,7 @@ public:
 	 *
 	 * @returns a new AP-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 	  return new AP(ap);
 	}
 
@@ -89,8 +77,8 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
-	  return modelChecker.checkAP(this);
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+	  return modelChecker.checkAP(*this);
 	}
 
 private:

src/formula/And.h

@@ -91,21 +91,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " && ";
@@ -121,7 +121,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		And<T>* result = new And();
 		if (this->left != NULL) {
 		  result->setLeft(left->clone());
@@ -141,7 +141,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 		return modelChecker.checkAnd(this);
 	}
 

src/formula/BoundedUntil.h

@@ -97,21 +97,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns the maximally allowed number of steps for the bounded until operator
 	 */
-	uint_fast64_t getBound() {
+	uint_fast64_t getBound() const {
 		return bound;
 	}
 
@@ -127,7 +127,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " U<=";
@@ -145,7 +145,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() {
+	virtual PCTLPathFormula<T>* clone() const {
 		BoundedUntil<T>* result = new BoundedUntil();
 		result->setBound(bound);
 		if (left != NULL) {
@@ -167,7 +167,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkBoundedUntil(this);
 	}
 

src/formula/Formulas.h

@@ -0,0 +1,23 @@
+/*
+ * Formulas.h
+ *
+ *  Created on: 06.12.2012
+ *      Author: chris
+ */
+
+#ifndef FORMULAS_H_
+#define FORMULAS_H_
+
+#include "And.h"
+#include "AP.h"
+#include "BoundedUntil.h"
+#include "Next.h"
+#include "Not.h"
+#include "Or.h"
+#include "PCTLformula.h"
+#include "PCTLPathFormula.h"
+#include "PCTLStateFormula.h"
+#include "ProbabilisticOperator.h"
+#include "Until.h"
+
+#endif /* FORMULAS_H_ */

src/formula/Next.h

@@ -65,7 +65,7 @@ public:
 	/*!
 	 * @returns the child node
 	 */
-	PCTLStateFormula<T>& getChild() {
+	const PCTLStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -80,7 +80,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += " X ";
 		result += child->toString();
@@ -95,7 +95,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() {
+	virtual PCTLPathFormula<T>* clone() const {
 		Next<T>* result = new Next<T>();
 		if (child != NULL) {
 			result->setChild(child);
@@ -112,7 +112,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkNext(this);
 	}
 

src/formula/Not.h

@@ -60,7 +60,7 @@ public:
 	/*!
 	 * @returns The child node
 	 */
-	PCTLStateFormula<T>& getChild() {
+	const PCTLStateFormula<T>& getChild() const {
 		return *child;
 	}
 
@@ -75,7 +75,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "!";
 		result += child->toString();
 		return result;
@@ -88,7 +88,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		Not<T>* result = new Not<T>();
 		if (child != NULL) {
 			result->setChild(child);
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkNot(this);
 	}
 

src/formula/Or.h

@@ -90,21 +90,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " || ";
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		Or<T>* result = new Or();
 		if (this->left != NULL) {
 		  result->setLeft(left->clone());
@@ -140,7 +140,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkOr(this);
 	}
 

src/formula/PCTLPathFormula.h

@@ -42,7 +42,7 @@ public:
 	 * @note This function is not implemented in this class.
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() = 0;
+	virtual PCTLPathFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
@@ -55,7 +55,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
+	virtual std::vector<T>* check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace formula

src/formula/PCTLStateFormula.h

@@ -42,7 +42,7 @@ public:
 	 * @note This function is not implemented in this class.
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() = 0;
+	virtual PCTLStateFormula<T>* clone() const = 0;
 
 	/*!
 	 * Calls the model checker to check this formula.
@@ -55,7 +55,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace formula

src/formula/PCTLformula.h

@@ -38,7 +38,7 @@ public:
 	 * @note This function is not implemented in this class.
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() = 0;
+	virtual std::string toString() const = 0;
 };
 
 } //namespace formula

src/formula/ProbabilisticOperator.h

@@ -73,21 +73,21 @@ public:
 	/*!
 	 * @returns the child node (representation of a PCTL path formula)
 	 */
-	PCTLPathFormula<T>& getPathFormula () {
+	const PCTLPathFormula<T>& getPathFormula () const {
 		return *pathFormula;
 	}
 
 	/*!
 	 * @returns the lower bound for the probability
 	 */
-	const T& getLowerBound() {
+	const T& getLowerBound() const {
 		return lower;
 	}
 
 	/*!
 	 * @returns the upper bound for the probability
 	 */
-	const T& getUpperBound() {
+	const T& getUpperBound() const {
 		return upper;
 	}
 
@@ -114,7 +114,7 @@ public:
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += " P[";
 		result += lower;
@@ -133,7 +133,7 @@ public:
 	 *
 	 * @returns a new AND-object that is identical the called object.
 	 */
-	virtual PCTLStateFormula<T>* clone() {
+	virtual PCTLStateFormula<T>* clone() const {
 		ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
 		result->setInterval(lower, upper);
 		if (pathFormula != NULL) {
@@ -151,7 +151,7 @@ public:
 	 *
 	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
 	 */
-	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	virtual mrmc::storage::BitVector *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
 	  return modelChecker.checkProbabilisticOperator(this);
 	}
 

src/formula/Until.h

@@ -90,21 +90,21 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>& getLeft() {
+	const PCTLStateFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>& getRight() {
+	const PCTLStateFormula<T>& getRight() const {
 		return *right;
 	}
 
 	/*!
 	 * @returns a string representation of the formula
 	 */
-	virtual std::string toString() {
+	virtual std::string toString() const {
 		std::string result = "(";
 		result += left->toString();
 		result += " U ";
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @returns a new BoundedUntil-object that is identical the called object.
 	 */
-	virtual PCTLPathFormula<T>* clone() {
+	virtual PCTLPathFormula<T>* clone() const {
 		Until<T>* result = new Until();
 		if (left != NULL) {
 			result->setLeft(left->clone());
@@ -140,8 +140,8 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
-	  return modelChecker.checkUntil(this);
+	virtual std::vector<T> *check(const mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) const {
+	  return modelChecker.checkUntil(*this);
 	}
 
 private:

src/modelChecker/DtmcPrctlModelChecker.h

@@ -103,8 +103,8 @@ public:
 	 * @param formula The state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula<T>& formula) {
-		return formula.check(this);
+	virtual mrmc::storage::BitVector* checkStateFormula(const mrmc::formula::PCTLStateFormula<T>& formula) const {
+		return formula.check(*this);
 	}
 
 	/*!
@@ -113,9 +113,9 @@ public:
 	 * @param formula The And formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector* checkAnd(const mrmc::formula::And<T>& formula) {
-		mrmc::storage::BitVector* result = check(formula.getLeft());
-		mrmc::storage::BitVector* right = check(formula.getRight());
+	virtual mrmc::storage::BitVector* checkAnd(const mrmc::formula::And<T>& formula) const {
+		mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft());
+		mrmc::storage::BitVector* right = checkStateFormula(formula.getRight());
 		(*result) &= (*right);
 		delete right;
 		return result;
@@ -127,7 +127,12 @@ public:
 	 * @param formula The AP state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector* checkAP(const mrmc::formula::AP<T>& formula) {
+	virtual mrmc::storage::BitVector* checkAP(const mrmc::formula::AP<T>& formula) const {
+		if (formula.getAP().compare("true") == 0) {
+			return new mrmc::storage::BitVector(model->getNumberOfStates(), 1);
+		} else if (formula.getAP().compare("false") == 0) {
+			return new mrmc::storage::BitVector(model->getNumberOfStates());
+		}
 		return new mrmc::storage::BitVector(*model->getLabeledStates(formula.getAP()));
 	}
 
@@ -137,8 +142,8 @@ public:
 	 * @param formula The Not state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector* checkNot(const mrmc::formula::Not<T>& formula) {
-		mrmc::storage::BitVector* result = check(formula.getChild());
+	virtual mrmc::storage::BitVector* checkNot(const mrmc::formula::Not<T>& formula) const {
+		mrmc::storage::BitVector* result = checkStateFormula(formula.getChild());
 		result->complement();
 		return result;
 	}
@@ -149,9 +154,9 @@ public:
 	 * @param formula The Or state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector* checkOr(const mrmc::formula::Or<T>& formula) {
-		mrmc::storage::BitVector* result = check(formula.getLeft());
-		mrmc::storage::BitVector* right = check(formula.getRight());
+	virtual mrmc::storage::BitVector* checkOr(const mrmc::formula::Or<T>& formula) const {
+		mrmc::storage::BitVector* result = checkStateFormula(formula.getLeft());
+		mrmc::storage::BitVector* right = checkStateFormula(formula.getRight());
 		(*result) |= (*right);
 		delete right;
 		return result;
@@ -163,7 +168,7 @@ public:
 	 * @param formula The state formula to check
 	 * @returns The set of states satisfying the formula, represented by a bit vector
 	 */
-	virtual mrmc::storage::BitVector checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator<T>& formula);
+	virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator<T>& formula) const = 0;
 
 	/*!
 	 * The check method for a path formula; Will infer the actual type of formula and delegate it
@@ -172,8 +177,8 @@ public:
 	 * @param formula The path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<T>* checkPathFormula(const mrmc::formula::PCTLPathFormula<T>& formula) {
-		return formula.check(this);
+	virtual std::vector<T>* checkPathFormula(const mrmc::formula::PCTLPathFormula<T>& formula) const {
+		return formula.check(*this);
 	}
 
 	/*!
@@ -182,7 +187,7 @@ public:
 	 * @param formula The Bounded Until path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<T>* checkBoundedUntil(const mrmc::formula::BoundedUntil<T>& formula) = 0;
+	virtual std::vector<T>* checkBoundedUntil(const mrmc::formula::BoundedUntil<T>& formula) const = 0;
 
 	/*!
 	 * The check method for a path formula with a Next operator node as root in its formula tree
@@ -190,7 +195,7 @@ public:
 	 * @param formula The Next path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<T>* checkNext(const mrmc::formula::Next<T>& formula) = 0;
+	virtual std::vector<T>* checkNext(const mrmc::formula::Next<T>& formula) const = 0;
 
 	/*!
 	 * The check method for a path formula with an Until operator node as root in its formula tree
@@ -198,7 +203,7 @@ public:
 	 * @param formula The Until path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<T>* checkUntil(const mrmc::formula::Until<T>& formula) = 0;
+	virtual std::vector<T>* checkUntil(const mrmc::formula::Until<T>& formula) const = 0;
 
 private:
 	mrmc::models::Dtmc<T>* model;

src/modelChecker/GmmxxDtmcPrctlModelChecker.h

@@ -10,7 +10,8 @@
 
 #include "src/utility/vector.h"
 
-#include "src/models/dtmc.h"
+#include "src/models/Dtmc.h"
+#include "src/modelChecker/DtmcPrctlModelChecker.h"
 #include "src/solver/GraphAnalyzer.h"
 
 #include "gmm/gmm_matrix.h"
@@ -19,7 +20,7 @@
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
 
-log4cplus::Logger logger;
+extern log4cplus::Logger logger;
 
 namespace mrmc {
 
@@ -28,31 +29,46 @@ namespace modelChecker {
 /*
  * A model checking engine that makes use of the gmm++ backend.
  */
-template <class T>
-class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<T> {
+template <class Type>
+class GmmxxDtmcPrctlModelChecker : public DtmcPrctlModelChecker<Type> {
 
 public:
-	explicit GmmxxDtmcPrctlModelChecker(const mrmc::models::Dtmc<T>* dtmc) : DtmcPrctlModelChecker(dtmc) { }
+	explicit GmmxxDtmcPrctlModelChecker(mrmc::models::Dtmc<Type>& dtmc) : DtmcPrctlModelChecker<Type>(dtmc) { }
 
 	virtual ~GmmxxDtmcPrctlModelChecker() { }
 
-	virtual std::vector<T>* checkBoundedUntil(mrmc::formula::BoundedUntil<T>& formula) {
+	virtual mrmc::storage::BitVector* checkProbabilisticOperator(const mrmc::formula::ProbabilisticOperator<Type>& formula) const {
+		std::vector<Type>* probabilisticResult = this->checkPathFormula(formula.getPathFormula());
+
+		mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates());
+		Type lower = formula.getLowerBound();
+		Type upper = formula.getUpperBound();
+		for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) {
+			if ((*probabilisticResult)[i] >= lower && (*probabilisticResult)[i] <= upper) result->set(i, true);
+		}
+
+		delete probabilisticResult;
+
+		return result;
+	}
+
+	virtual std::vector<Type>* checkBoundedUntil(const mrmc::formula::BoundedUntil<Type>& formula) const {
 		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		mrmc::storage::BitVector* leftStates = this->check(formula.getLeft());
-		mrmc::storage::BitVector* rightStates = this->check(formula.getRight());
+		mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft());
+		mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
 
 		// Copy the matrix before we make any changes.
-		mrmc::storage::SquareSparseMatrix<T>* tmpMatrix(dtmc.getTransitionProbabilityMatrix());
+		mrmc::storage::SquareSparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
 
 		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
-		tmpMatrix.makeRowsAbsorbing((~leftStates & rightStates) | rightStates);
+		tmpMatrix.makeRowsAbsorbing((~*leftStates & *rightStates) | *rightStates);
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
 		gmm::csr_matrix<double>* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix();
 
 		// Create the vector with which to multiply.
-		std::vector<T>* result = new st::vector<T>(dtmc.getNumberOfStates());
-		mrmc::utility::setVectorValue(result, *rightStates, 1);
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
+		mrmc::utility::setVectorValues(result, *rightStates, static_cast<double>(1.0));
 
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
 		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
@@ -66,22 +82,22 @@ public:
 		return result;
 	}
 
-	virtual std::vector<T>* checkNext(const mrmc::formula::Next<T>& formula) {
+	virtual std::vector<Type>* checkNext(const mrmc::formula::Next<Type>& formula) const {
 		// First, we need to compute the states that satisfy the sub-formula of the next-formula.
-		mrmc::storage::BitVector* nextStates = this->check(formula.getChild());
+		mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<double>* gmmxxMatrix = dtmc.getTransitionProbabilityMatrix()->toGMMXXSparseMatrix();
+		gmm::csr_matrix<double>* gmmxxMatrix = this->getModel().getTransitionProbabilityMatrix()->toGMMXXSparseMatrix();
 
 		// Create the vector with which to multiply and initialize it correctly.
-		std::vector<T> x(dtmc.getNumberOfStates());
-		mrmc::utility::setVectorValue(x, nextStates, 1);
+		std::vector<Type> x(this->getModel().getNumberOfStates());
+		mrmc::utility::setVectorValues(&x, *nextStates, static_cast<double>(1.0));
 
 		// Delete not needed next states bit vector.
 		delete nextStates;
 
 		// Create resulting vector.
-		std::vector<T>* result = new std::vector<T>(dtmc.getNumberOfStates());
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
 
 		// Perform the actual computation.
 		gmm::mult(*gmmxxMatrix, x, *result);
@@ -91,17 +107,17 @@ public:
 		return result;
 	}
 
-	virtual std::vector<T>* checkUntil(const mrmc::formula::Until<T>& formula) {
+	virtual std::vector<Type>* checkUntil(const mrmc::formula::Until<Type>& formula) const {
 		// First, we need to compute the states that satisfy the sub-formulas of the until-formula.
-		mrmc::storage::BitVector* leftStates = this->check(formula.getLeft());
-		mrmc::storage::BitVector* rightStates = this->check(formula.getRight());
+		mrmc::storage::BitVector* leftStates = this->checkStateFormula(formula.getLeft());
+		mrmc::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
 
 		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
 		// all states that have probability 0 and 1 of satisfying the until-formula.
-		mrmc::storage::BitVector notExistsPhiUntilPsiStates(dtmc.getNumberOfStates());
-		mrmc::storage::BitVector alwaysPhiUntilPsiStates(dtmc.getNumberOfStates());
-		mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates<double>(dtmc, *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
-		notExistsPhiUntilPsiStates->complement();
+		mrmc::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
+		mrmc::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
+		mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
+		notExistsPhiUntilPsiStates.complement();
 
 		delete leftStates;
 		delete rightStates;
@@ -109,12 +125,15 @@ public:
 		LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states.");
 		LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states.");
 		mrmc::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates);
-		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " maybe states.");
+		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
+
+		// Create resulting vector and set values accordingly.
+		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
 
 		// Only try to solve system if there are states for which the probability is unknown.
 		if (maybeStates.getNumberOfSetBits() > 0) {
 			// Now we can eliminate the rows and columns from the original transition probability matrix.
-			mrmc::storage::SquareSparseMatrix<double>* submatrix = dtmc.getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
+			mrmc::storage::SquareSparseMatrix<double>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
 			// Converting the matrix to the form needed for the equation system. That is, we go from
 			// x = A*x + b to (I-A)x = b.
 			submatrix->convertToEquationSystem();
@@ -125,12 +144,12 @@ public:
 			// Initialize the x vector with 0.5 for each element. This is the initial guess for
 			// the iterative solvers. It should be safe as for all 'maybe' states we know that the
 			// probability is strictly larger than 0.
-			std::vector<T>* x = new std::vector<T>(maybeStates.getNumberOfSetBits(), 0.5);
+			std::vector<Type> x(maybeStates.getNumberOfSetBits(), Type(0.5));
 
 			// Prepare the right-hand side of the equation system. For entry i this corresponds to
 			// the accumulated probability of going from state i to some 'yes' state.
 			std::vector<double> b(maybeStates.getNumberOfSetBits());
-			dtmc.getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x);
+			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x);
 
 			// Set up the precondition of the iterative solver.
 			gmm::ilu_precond<gmm::csr_matrix<double>> P(*gmmxxMatrix);
@@ -139,24 +158,26 @@ public:
 			gmm::iteration iter(0.000001);
 
 			// Now do the actual solving.
-			LOG4CPLUS_INFO(logger, "Starting iterations...");
+			LOG4CPLUS_INFO(logger, "Starting iterative solver.");
 			gmm::bicgstab(*gmmxxMatrix, x, b, P, iter);
-			LOG4CPLUS_INFO(logger, "Done with iterations.");
+			LOG4CPLUS_INFO(logger, "Iterative solver converged.");
 
-			// Create resulting vector and set values accordingly.
-			std::vector<T>* result = new std::vector<T>(dtmc.getNumberOfStates());
-			mrmc::utility::setVectorValues<std::vector<T>>(result, maybeStates, x);
+			// Set values of resulting vector according to result.
+			mrmc::utility::setVectorValues<Type>(result, maybeStates, x);
 
-			// Delete temporary matrix and return result.
-			delete x;
+			// Delete temporary matrix.
 			delete gmmxxMatrix;
 		}
 
-		mrmc::utility::setVectorValue<std::vector<T>>(result, notExistsPhiUntilPsiStates, 0);
-		mrmc::utility::setVectorValue<std::vector<T>>(result, alwaysPhiUntilPsiStates, 1);
+		mrmc::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, static_cast<double>(0));
+		mrmc::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, static_cast<double>(1.0));
 
 		return result;
 	}
 };
 
+} //namespace modelChecker
+
+} //namespace mrmc
+
 #endif /* GMMXXDTMCPRCTLMODELCHECKER_H_ */

src/models/Dtmc.h

@@ -9,6 +9,7 @@
 #define DTMC_H_
 
 #include <ostream>
+#include <memory>
 
 #include "AtomicPropositionsLabeling.h"
 #include "GraphTransitions.h"
@@ -35,10 +36,8 @@ public:
 	 * @param stateLabeling The labeling that assigns a set of atomic
 	 * propositions to each state.
 	 */
-	Dtmc(mrmc::storage::SquareSparseMatrix<T>* probabilityMatrix, mrmc::models::AtomicPropositionsLabeling* stateLabeling)
-			: backwardTransitions(nullptr) {
-		this->probabilityMatrix = probabilityMatrix;
-		this->stateLabeling = stateLabeling;
+	Dtmc(std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> probabilityMatrix, std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling)
+			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), backwardTransitions(nullptr) {
 	}
 
 	//! Copy Constructor
@@ -58,12 +57,6 @@ public:
 	 * Destructor. Frees the matrix and labeling associated with this DTMC.
 	 */
 	~Dtmc() {
-		if (this->probabilityMatrix != nullptr) {
-			delete this->probabilityMatrix;
-		}
-		if (this->stateLabeling != nullptr) {
-			delete this->stateLabeling;
-		}
 		if (this->backwardTransitions != nullptr) {
 			delete this->backwardTransitions;
 		}
@@ -102,7 +95,7 @@ public:
 	 * @return A pointer to the matrix representing the transition probability
 	 * function.
 	 */
-	mrmc::storage::SquareSparseMatrix<T>* getTransitionProbabilityMatrix() const {
+	std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> getTransitionProbabilityMatrix() const {
 		return this->probabilityMatrix;
 	}
 
@@ -146,10 +139,10 @@ public:
 private:
 
 	/*! A matrix representing the transition probability function of the DTMC. */
-	mrmc::storage::SquareSparseMatrix<T>* probabilityMatrix;
+	std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> probabilityMatrix;
 
 	/*! The labeling of the states of the DTMC. */
-	mrmc::models::AtomicPropositionsLabeling* stateLabeling;
+	std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> stateLabeling;
 
 	/*!
 	 * A data structure that stores the predecessors for all states. This is

src/models/GraphTransitions.h

@@ -11,6 +11,7 @@
 #include "src/storage/SquareSparseMatrix.h"
 
 #include <algorithm>
+#include <memory>
 
 namespace mrmc {
 
@@ -38,7 +39,7 @@ public:
 	 * @param forward If set to true, this objects will store the graph structure
 	 * of the backwards transition relation.
 	 */
-	GraphTransitions(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix, bool forward)
+	GraphTransitions(std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionMatrix, bool forward)
 			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
 		if (forward) {
 			this->initializeForward(transitionMatrix);
@@ -86,7 +87,7 @@ private:
 	 * Initializes this graph transitions object using the forward transition
 	 * relation given by means of a sparse matrix.
 	 */
-	void initializeForward(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix) {
+	void initializeForward(std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionMatrix) {
 		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
 		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
 
@@ -108,7 +109,7 @@ private:
 	 * relation, whose forward transition relation is given by means of a sparse
 	 * matrix.
 	 */
-	void initializeBackward(mrmc::storage::SquareSparseMatrix<T>* transitionMatrix) {
+	void initializeBackward(std::shared_ptr<mrmc::storage::SquareSparseMatrix<T>> transitionMatrix) {
 		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions]();
 		this->stateIndications = new uint_fast64_t[numberOfStates + 1]();
 

src/mrmc.cpp

@@ -21,11 +21,13 @@
 #include "src/models/Dtmc.h"
 #include "src/storage/SquareSparseMatrix.h"
 #include "src/models/AtomicPropositionsLabeling.h"
+#include "src/modelChecker/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/readLabFile.h"
 #include "src/parser/readTraFile.h"
 #include "src/parser/readPrctlFile.h"
 #include "src/solver/GraphAnalyzer.h"
 #include "src/utility/settings.h"
+#include "src/formula/Formulas.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -102,6 +104,16 @@ int main(const int argc, const char* argv[]) {
 
 	dtmc.printModelInformationToStream(std::cout);
 
+	// Uncomment this if you want to see the first model checking procedure in action. :)
+	/*
+	mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double> mc(dtmc);
+	mrmc::formula::AP<double>* trueFormula = new mrmc::formula::AP<double>(std::string("true"));
+	mrmc::formula::AP<double>* ap = new mrmc::formula::AP<double>(std::string("observe0Greater1"));
+	mrmc::formula::Until<double>* until = new mrmc::formula::Until<double>(trueFormula, ap);
+	mc.checkPathFormula(*until);
+	delete until;
+	*/
+
 	if (s != nullptr) {
 		delete s;
 	}

src/parser/readLabFile.cpp

@@ -106,7 +106,7 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename)
 	/*
 	 *	create labeling object with given node and proposition count
 	 */
-	this->labeling = new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count);
+	this->labeling = std::shared_ptr<mrmc::models::AtomicPropositionsLabeling>(new mrmc::models::AtomicPropositionsLabeling(node_count, proposition_count));
 	
 	/*
 	 *	second run: add propositions and node labels to labeling

src/parser/readLabFile.h

@@ -6,6 +6,8 @@
 
 #include "src/parser/parser.h"
 
+#include <memory>
+
 namespace mrmc {
 namespace parser {
 
@@ -20,13 +22,13 @@ class LabParser : Parser
 	public:
 		LabParser(uint_fast64_t node_count, const char* filename);
 
-		mrmc::models::AtomicPropositionsLabeling* getLabeling()
+		std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> getLabeling()
 		{
 			return this->labeling;
 		}
 	
 	private:
-		mrmc::models::AtomicPropositionsLabeling* labeling;
+		std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> labeling;
 };
 
 } // namespace parser

src/parser/readTraFile.cpp

@@ -166,7 +166,7 @@ TraParser::TraParser(const char * filename)
 	 *	non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
 	LOG4CPLUS_INFO(logger, "Attempting to create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");
-	this->matrix = new mrmc::storage::SquareSparseMatrix<double>(maxnode + 1);
+	this->matrix = std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>>(new mrmc::storage::SquareSparseMatrix<double>(maxnode + 1));
 	if (this->matrix == NULL)
 	{
 		LOG4CPLUS_ERROR(logger, "Could not create matrix of size " << (maxnode+1) << " x " << (maxnode+1) << ".");

src/parser/readTraFile.h

@@ -5,6 +5,8 @@
 
 #include "src/parser/parser.h"
 
+#include <memory>
+
 namespace mrmc {
 namespace parser {
 	
@@ -20,13 +22,13 @@ class TraParser : Parser
 	public:
 		TraParser(const char* filename);
 		
-		mrmc::storage::SquareSparseMatrix<double>* getMatrix()
+		std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> getMatrix()
 		{
 			return this->matrix;
 		}
 	
 	private:
-		mrmc::storage::SquareSparseMatrix<double>* matrix;
+		std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix;
 		
 		uint_fast32_t firstPass(char* buf, uint_fast32_t &maxnode);
 	

src/storage/SquareSparseMatrix.h

@@ -71,8 +71,8 @@ public:
 	 * @param ssm A reference to the matrix to be copied.
 	 */
 	SquareSparseMatrix(const SquareSparseMatrix<T> &ssm)
-			: internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow),
-			  rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount) {
+			: rowCount(ssm.rowCount), nonZeroEntryCount(ssm.nonZeroEntryCount),
+			  internalStatus(ssm.internalStatus), currentSize(ssm.currentSize), lastRow(ssm.lastRow) {
 		LOG4CPLUS_WARN(logger, "Invoking copy constructor.");
 		// Check whether copying the matrix is safe.
 		if (!ssm.hasError()) {
@@ -454,7 +454,7 @@ public:
 	 * Checks whether the internal state of the matrix signals an error.
 	 * @return True iff the internal state of the matrix signals an error.
 	 */
-	bool hasError() {
+	bool hasError() const {
 		return (internalStatus == MatrixStatus::Error);
 	}
 
@@ -517,7 +517,7 @@ public:
 			// Then add the elements on the diagonal.
 			for (uint_fast64_t i = 0; i < rowCount; ++i) {
 				if (diagonalStorage[i] == 0) zeroCount++;
-				// tripletList.push_back(IntTriplet(i, i, diagonalStorage[i]));
+				tripletList.push_back(IntTriplet(i, i, diagonalStorage[i]));
 			}
 
 			// Let Eigen create a matrix from the given list of triplets.
@@ -663,11 +663,13 @@ public:
 
 	/*!
 	 * This function makes the rows given by the bit vector absorbing.
+	 * @param rows A bit vector indicating which rows to make absorbing.
+	 * @return True iff the operation was successful.
 	 */
 	bool makeRowsAbsorbing(const mrmc::storage::BitVector rows) {
 		bool result = true;
 		for (auto row : rows) {
-			result = result && makeRowAbsorbing(row);
+			result &= makeRowAbsorbing(row);
 		}
 
 		return result;
@@ -732,7 +734,7 @@ public:
 	void getConstrainedRowCountVector(const mrmc::storage::BitVector& rowConstraint, const mrmc::storage::BitVector& columnConstraint, std::vector<T>* resultVector) {
 		uint_fast64_t currentRowCount = 0;
 		for (auto row : rowConstraint) {
-			resultVector[currentRowCount++] = getConstrainedRowSum(row, columnConstraint);
+			(*resultVector)[currentRowCount++] = getConstrainedRowSum(row, columnConstraint);
 		}
 	}
 

src/utility/ioUtility.cpp

@@ -16,7 +16,7 @@ namespace mrmc {
 namespace utility {
 
 void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename) {
-   mrmc::storage::SquareSparseMatrix<double>* matrix = dtmc->getTransitionProbabilityMatrix();
+   std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> matrix(dtmc->getTransitionProbabilityMatrix());
    double* diagonal_storage = matrix->getDiagonalStoragePointer();
 
    std::ofstream file;

src/utility/vector.h

@@ -12,18 +12,18 @@ namespace mrmc {
 
 namespace utility {
 
-template<T>
-void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& positions, std::vector<T>* values) {
+template<class T>
+void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& positions, const std::vector<T> values) {
 	uint_fast64_t oldPosition = 0;
 	for (auto position : positions) {
-		vector[position] = values[oldPosition++];
+		(*vector)[position] = values[oldPosition++];
 	}
 }
 
-template<T>
-void setVectorValue(std::vector<T>* vector, const mrmc::storage::BitVector& positions, T value) {
+template<class T>
+void setVectorValues(std::vector<T>* vector, const mrmc::storage::BitVector& positions, T value) {
 	for (auto position : positions) {
-		vector[position] = value;
+		(*vector)[position] = value;
 	}
 }
 

test/parser/read_lab_file_test.cpp

@@ -12,6 +12,8 @@
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
 
+#include <memory>
+
 TEST(ReadLabFileTest, NonExistingFileTest) {
    //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
    ASSERT_THROW(mrmc::parser::LabParser(0,MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
@@ -19,12 +21,12 @@ TEST(ReadLabFileTest, NonExistingFileTest) {
 
 TEST(ReadLabFileTest, ParseTest) {
 	//This test is based on a test case from the original MRMC.
-	mrmc::models::AtomicPropositionsLabeling* labeling = NULL;
+	
 	
 	mrmc::parser::LabParser* parser;
 	//Parsing the file
 	ASSERT_NO_THROW(parser = new mrmc::parser::LabParser(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
-	labeling = parser->getLabeling();
+	std::shared_ptr<mrmc::models::AtomicPropositionsLabeling> labeling(parser->getLabeling());
 
 	//Checking whether all propositions are in the labelling
 
@@ -77,7 +79,6 @@ TEST(ReadLabFileTest, ParseTest) {
 		ASSERT_FALSE(labeling->stateHasAtomicProposition(smth,11));
 
 		//Deleting the labeling
-		delete labeling;
 		delete parser;
 	} else {
 		FAIL();

test/parser/read_tra_file_test.cpp

@@ -22,10 +22,9 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
 /* The following test case is based on one of the original MRMC test cases
  */
 TEST(ReadTraFileTest, ParseFileTest1) {
-	mrmc::storage::SquareSparseMatrix<double> *result = NULL;
 	mrmc::parser::TraParser* parser;
 	ASSERT_NO_THROW(parser = new mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
-	result = parser->getMatrix();
+	std::shared_ptr<mrmc::storage::SquareSparseMatrix<double>> result = parser->getMatrix();
 
 	if (result != NULL) {
 		double val = 0;
@@ -63,7 +62,6 @@ TEST(ReadTraFileTest, ParseFileTest1) {
 		ASSERT_TRUE(result->getValue(4,4,&val));
 		ASSERT_EQ(val,0);
 
-		delete result;
 		delete parser;
 	} else {
 		FAIL();