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

src/formula/AP.h

@@ -89,8 +89,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(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkAP(this);
 	}
 
 private:

src/formula/And.h

@@ -141,8 +141,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->checkAnd(this);
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+		return modelChecker.checkAnd(this);
 	}
 
 private:

src/formula/BoundedUntil.h

@@ -167,8 +167,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->checkBoundedUntil(this);
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkBoundedUntil(this);
 	}
 
 private:

src/formula/Next.h

@@ -112,8 +112,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->checkNext(this);
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkNext(this);
 	}
 
 private:

src/formula/Not.h

@@ -105,8 +105,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->checkNot(this);
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkNot(this);
 	}
 
 private:

src/formula/Or.h

@@ -140,8 +140,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->checkOr(this);
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkOr(this);
 	}
 
 private:

src/formula/PCTLPathFormula.h

@@ -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(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
 };
 
 } //namespace formula

src/formula/PCTLStateFormula.h

@@ -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(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) = 0;
 };
 
 } //namespace formula

src/formula/ProbabilisticOperator.h

@@ -10,7 +10,7 @@
 
 #include "PCTLStateFormula.h"
 #include "PCTLPathFormula.h"
-#include "misc/const_templates.h"
+#include "utility/const_templates.h"
 
 namespace mrmc {
 
@@ -40,8 +40,8 @@ public:
 	 * Empty constructor
 	 */
 	ProbabilisticOperator() {
-		upper = mrmc::misc::constGetZero(&upper);
-		lower = mrmc::misc::constGetZero(&lower);
+		upper = mrmc::utility::constGetZero(upper);
+		lower = mrmc::utility::constGetZero(lower);
 		pathFormula = NULL;
 	}
 
@@ -151,8 +151,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->checkProbabilisticOperator(this);
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkProbabilisticOperator(this);
 	}
 
 private:

src/formula/Until.h

@@ -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(mrmc::modelChecker::DtmcPrctlModelChecker<T>& modelChecker) {
+	  return modelChecker.checkUntil(this);
 	}
 
 private:

src/modelChecker/DtmcPrctlModelChecker.cpp

@@ -6,27 +6,3 @@
  */
 
 #include "DtmcPrctlModelChecker.h"
-
-namespace mrmc {
-
-namespace modelChecker {
-
-template<class T>
-DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* dtmc) {
-   this->dtmc = dtmc;
-}
-
-template<class T>
-DtmcPrctlModelChecker<T>::~DtmcPrctlModelChecker() {
-   delete this->dtmc;
-}
-
-template<class T>
-DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
-	this->dtmc = new mrmc::models::Dtmc<T>(modelChecker->getDtmc());
-}
-
-
-} //namespace modelChecker
-
-} //namespace mrmc

src/modelChecker/DtmcPrctlModelChecker.h

@@ -60,19 +60,25 @@ public:
 	 *
 	 * @param Dtmc The dtmc model which is checked.
 	 */
-	explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* Dtmc);
+	explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* dtmc) {
+	   this->dtmc = dtmc;
+	}
 
 	/*!
 	 * Copy constructor
 	 *
 	 * @param modelChecker The model checker that is copied.
 	 */
-	explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker);
+	explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+		this->dtmc = new mrmc::models::Dtmc<T>(modelChecker->getDtmc());
+	}
 
 	/*!
 	 * Destructor
 	 */
-	virtual ~DtmcPrctlModelChecker();
+	virtual ~DtmcPrctlModelChecker() {
+	   delete this->dtmc;
+	}
 
 	/*!
 	 * @returns A reference to the dtmc of the model checker.
@@ -95,7 +101,9 @@ public:
 	 * @param ap A string representing an atomic proposition.
 	 * @returns The set of states labeled with the atomic proposition ap.
 	 */
-	virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0;
+	virtual mrmc::storage::BitVector* getStatesLabeledWith(std::string ap) {
+		return dtmc->getLabeledStates(ap);
+	}
 
 	/*!
 	 * Multiplies the matrix with a given vector; the result again is a vector.
@@ -112,7 +120,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 checkStateFormula(mrmc::formula::PCTLStateFormula<T>* formula) {
+	virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula<T>& formula) {
 		return formula->check(this);
 	}
 
@@ -122,7 +130,13 @@ 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(mrmc::formula::And<T>* formula) = 0;
+	virtual mrmc::storage::BitVector* checkAnd(mrmc::formula::And<T>& formula) {
+		mrmc::storage::BitVector* result = check(formula.getLeft());
+		mrmc::storage::BitVector* right = check(formula.getRight());
+		(*result) &= (*right);
+		delete right;
+		return result;
+	}
 
 	/*!
 	 * The check method for a formula with an AP node as root in its formula tree
@@ -130,7 +144,9 @@ 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(mrmc::formula::AP<T>* formula) = 0;
+	virtual mrmc::storage::BitVector* checkAP(mrmc::formula::AP<T>& formula) {
+		return getStatesLabeledWith(formula.getAP());
+	}
 
 	/*!
 	 * The check method for a formula with a Not node as root in its formula tree
@@ -138,7 +154,11 @@ 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(mrmc::formula::Not<T>* formula) = 0;
+	virtual mrmc::storage::BitVector* checkNot(mrmc::formula::Not<T>& formula) {
+		mrmc::storage::BitVector* result = check(formula.getChild());
+		result->complement();
+		return result;
+	}
 
 	/*!
 	 * The check method for a state formula with an Or node as root in its formula tree
@@ -146,7 +166,13 @@ 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(mrmc::formula::Or<T>* formula) = 0;
+	virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or<T>& formula) {
+		mrmc::storage::BitVector* result = check(formula.getLeft());
+		mrmc::storage::BitVector* right = check(formula.getRight());
+		(*result) |= (*right);
+		delete right;
+		return result;
+	}
 
 	/*!
 	 * The check method for a state formula with a probabilistic operator node as root in its formula tree
@@ -154,7 +180,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(mrmc::formula::ProbabilisticOperator<T>* formula) = 0;
+	virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>& formula);
 
 	/*!
 	 * The check method for a path formula; Will infer the actual type of formula and delegate it
@@ -163,7 +189,7 @@ public:
 	 * @param formula The path formula to check
 	 * @returns for each state the probability that the path formula holds.
 	 */
-	virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula<T>* formula) {
+	virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula<T>& formula) {
 		return formula->check(this);
 	}
 
@@ -173,7 +199,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(mrmc::formula::BoundedUntil<T>* formula) = 0;
+	virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil<T>& formula) = 0;
 
 	/*!
 	 * The check method for a path formula with a Next operator node as root in its formula tree
@@ -181,7 +207,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(mrmc::formula::Next<T>* formula) = 0;
+	virtual std::vector<T> checkNext(mrmc::formula::Next<T>& formula) = 0;
 
 	/*!
 	 * The check method for a path formula with an Until operator node as root in its formula tree
@@ -189,7 +215,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(mrmc::formula::Until<T>* formula) = 0;
+	virtual std::vector<T> checkUntil(mrmc::formula::Until<T>& formula) = 0;
 
 private:
 	mrmc::models::Dtmc<T>* dtmc;

src/storage/SquareSparseMatrix.h

@@ -12,7 +12,7 @@
 #include "src/exceptions/file_IO_exception.h"
 #include "src/storage/BitVector.h"
 
-#include "src/misc/const_templates.h"
+#include "src/utility/const_templates.h"
 #include "Eigen/Sparse"
 #include "gmm/gmm_matrix.h"
 
@@ -658,12 +658,12 @@ public:
 		uint_fast64_t rowEnd = rowIndications[row + 1];
 
 		while (rowStart < rowEnd) {
-			valueStorage[rowStart] = mrmc::misc::constGetZero(valueStorage);
+			valueStorage[rowStart] = mrmc::utility::constGetZero(valueStorage[rowStart]);
 			++rowStart;
 		}
 
 		// Set the element on the diagonal to one.
-		diagonalStorage[row] = mrmc::misc::constGetOne(diagonalStorage);
+		diagonalStorage[row] = mrmc::utility::constGetOne(diagonalStorage[row]);
 		return true;
 	}
 

src/misc/const_templates.h → src/utility/const_templates.h

@@ -10,7 +10,7 @@
 
 namespace mrmc {
 
-namespace misc {
+namespace utility {
 
 /*!
  * Returns a constant value of 0 that is fit to the type it is being written to.
@@ -19,20 +19,19 @@ namespace misc {
  *
  * <b>Parameter</b>
  *
- * The parameter is a pointer which is used to infer the return type (So, if you want
- * the return value to be of type double, the parameter has to be of type double*).
- * In most cases, it is a good choice to use the address of the variable that is to be
- * set.
+ * The parameter is a reference which is used to infer the return type (So, if you want
+ * the return value to be of type double, the parameter has to be a double variable).
+ * In most cases, it is a good choice to use the the variable that is to be set.
  */
 template<typename _Scalar>
-static inline _Scalar constGetZero(_Scalar*) {
+static inline _Scalar constGetZero(_Scalar&) {
    return _Scalar(0);
 }
 
 /*! @cond TEMPLATE_SPECIALIZATION
  * (exclude the specializations from the documentation) */
 template <>
-inline int_fast32_t constGetZero(int_fast32_t*) {
+inline int_fast32_t constGetZero(int_fast32_t&) {
    return 0;
 }
 
@@ -40,7 +39,7 @@ inline int_fast32_t constGetZero(int_fast32_t*) {
  * Specialization of constGetZero for int_fast32_t
  */
 template <>
-inline double constGetZero(double*) {
+inline double constGetZero(double&) {
    return 0.0;
 }
 /*! @endcond */
@@ -52,30 +51,28 @@ inline double constGetZero(double*) {
  *
  * <b>Parameter</b>
  *
- * The parameter is a pointer which is used to infer the return type (So, if you want
- * the return value to be of type double, the parameter has to be of type double*).
- * In most cases, it is a good choice to use the address of the variable that is to be
- * set.
- */
+ * The parameter is a reference which is used to infer the return type (So, if you want
+ * the return value to be of type double, the parameter has to be a double variable).
+ * In most cases, it is a good choice to use the the variable that is to be set. */
 template<typename _Scalar>
-static inline _Scalar constGetOne(_Scalar*) {
+static inline _Scalar constGetOne(_Scalar&) {
    return _Scalar(1);
 }
 
 /*! @cond TEMPLATE_SPECIALIZATION
  * (exclude the specializations from the documentation) */
 template<>
-inline int_fast32_t constGetOne(int_fast32_t*) {
+inline int_fast32_t constGetOne(int_fast32_t&) {
    return 1;
 }
 
 template<>
-inline double constGetOne(double*) {
+inline double constGetOne(double&) {
    return 1.0;
 }
 /*! @endcond */
 
-} //namespace misc
+} //namespace utility
 
 } //namespace mrmc
 

src/utility/utility.cpp → src/utility/ioUtility.cpp

@@ -1,11 +1,11 @@
 /*
- * utility.cpp
+ * ioUtility.cpp
  *
  *  Created on: 17.10.2012
  *      Author: Thomas Heinemann
  */
 
-#include "src/utility/utility.h"
+#include "src/utility/ioUtility.h"
 #include "src/parser/readTraFile.h"
 #include "src/parser/readLabFile.h"
 

src/utility/utility.h → src/utility/ioUtility.h

@@ -1,5 +1,5 @@
 /*
- * utility.h
+ * ioUtility.h
  *
  *  Created on: 17.10.2012
  *      Author: Thomas Heinemann

test/parser/parse_dtmc_test.cpp

@@ -8,7 +8,7 @@
 
 #include "gtest/gtest.h"
 #include "mrmc-config.h"
-#include "src/utility/utility.h"
+#include "src/utility/ioUtility.h"
 
 TEST(ParseDtmcTest, parseAndOutput) {
 	mrmc::models::Dtmc<double>* myDtmc;

test/parser/read_tra_file_test.cpp

@@ -12,7 +12,7 @@
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
 
-#include "src/utility/utility.h"
+#include "src/utility/ioUtility.h"
 
 TEST(ReadTraFileTest, NonExistingFileTest) {
    //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)