Merge.

CMakeLists.txt

@@ -171,3 +171,6 @@ configure_file (
   "${PROJECT_SOURCE_DIR}/mrmc-config.h.in"
   "${PROJECT_BINARY_DIR}/mrmc-config.h"
 )
+
+add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ./mrmc examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab)
+add_custom_target(memcheck-tests valgrind --leak-check=full --show-reachable=yes ./mrmc-tests)

src/formula/AP.h

@@ -59,7 +59,7 @@ public:
 	/*!
 	 * @returns the name of the atomic proposition
 	 */
-	std::string getAP() {
+	const std::string& getAP() {
 		return ap;
 	}
 

src/formula/And.h

@@ -91,15 +91,15 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>* getLeft() {
-		return left;
+	PCTLStateFormula<T>& getLeft() {
+		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>* getRight() {
-		return right;
+	PCTLStateFormula<T>& getRight() {
+		return *right;
 	}
 
 	/*!

src/formula/BoundedUntil.h

@@ -97,15 +97,15 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>* getLeft() {
-		return left;
+	PCTLStateFormula<T>& getLeft() {
+		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>* getRight() {
-		return right;
+	PCTLStateFormula<T>& getRight() {
+		return *right;
 	}
 
 	/*!

src/formula/Next.h

@@ -65,8 +65,8 @@ public:
 	/*!
 	 * @returns the child node
 	 */
-	PCTLStateFormula<T>* getChild() {
-		return child;
+	PCTLStateFormula<T>& getChild() {
+		return *child;
 	}
 
 	/*!

src/formula/Not.h

@@ -60,8 +60,8 @@ public:
 	/*!
 	 * @returns The child node
 	 */
-	PCTLStateFormula<T>* getChild() {
-		return child;
+	PCTLStateFormula<T>& getChild() {
+		return *child;
 	}
 
 	/*!

src/formula/Or.h

@@ -90,15 +90,15 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>* getLeft() {
-		return left;
+	PCTLStateFormula<T>& getLeft() {
+		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>* getRight() {
-		return right;
+	PCTLStateFormula<T>& getRight() {
+		return *right;
 	}
 
 	/*!

src/formula/ProbabilisticOperator.h

@@ -73,21 +73,21 @@ public:
 	/*!
 	 * @returns the child node (representation of a PCTL path formula)
 	 */
-	PCTLPathFormula<T>* getPathFormula () {
-		return pathFormula;
+	PCTLPathFormula<T>& getPathFormula () {
+		return *pathFormula;
 	}
 
 	/*!
 	 * @returns the lower bound for the probability
 	 */
-	T getLowerBound() {
+	const T& getLowerBound() {
 		return lower;
 	}
 
 	/*!
 	 * @returns the upper bound for the probability
 	 */
-	T getUpperBound() {
+	const T& getUpperBound() {
 		return upper;
 	}
 

src/formula/Until.h

@@ -90,15 +90,15 @@ public:
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	PCTLStateFormula<T>* getLeft() {
-		return left;
+	PCTLStateFormula<T>& getLeft() {
+		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	PCTLStateFormula<T>* getRight() {
-		return right;
+	PCTLStateFormula<T>& getRight() {
+		return *right;
 	}
 
 	/*!

src/models/AtomicPropositionsLabeling.h

@@ -10,25 +10,9 @@
 
 #include "src/storage/BitVector.h"
 #include <ostream>
-
-/* Map types: By default, the boost hash map is used.
- * If the macro USE_STD_MAP is defined, the default C++ class (std::map)
- * is used instead.
- */
-#ifdef USE_STD_MAP
-#  include <map>
-#  define MAP std::map
-#else
-#  ifdef USE_STD_UNORDERED_MAP
-#     include <unordered_map>
-#     define MAP std::unordered_map
-#  else
-#     include "boost/unordered_map.hpp"
-#     define MAP boost::unordered_map
-#  endif
-#endif
-
 #include <stdexcept>
+#include <unordered_map>
+#include <set>
 
 namespace mrmc {
 
@@ -230,7 +214,7 @@ private:
 	 * by mapping the name to a specific index in the array of all
 	 * individual labelings.
 	 */
-	MAP<std::string, uint_fast32_t> nameToLabelingMap;
+	std::unordered_map<std::string, uint_fast32_t> nameToLabelingMap;
 
 	/*!
 	 * Stores all individual labelings. To find the labeling associated with

src/mrmc.cpp

@@ -107,6 +107,9 @@ int main(const int argc, const char* argv[]) {
 		delete s;
 	}
 	
+	delete labparser.getLabeling();
+	delete traparser.getMatrix();
+
 	LOG4CPLUS_INFO(logger, "Nothing more to do, exiting.");
 
 	return 0;

src/parser/readLabFile.cpp

@@ -46,6 +46,7 @@ namespace parser {
  *	@return The pointer to the created labeling object.
  */
 LabParser::LabParser(uint_fast64_t node_count, const char * filename)
+	: labeling(nullptr)
 {
 	/*
 	 *	open file
@@ -124,7 +125,15 @@ LabParser::LabParser(uint_fast64_t node_count, const char * filename)
 		{
 			buf += cnt;
 			cnt = strcspn(buf, separator); // position of next separator
-			if (cnt > 0)
+			if (cnt >= sizeof(proposition))
+			{
+				/*
+				 *	if token is longer than our buffer, the following strncpy code might get risky...
+				 */
+				LOG4CPLUS_ERROR(logger, "Wrong file format in (" << filename << "). Atomic proposition with length > " << (sizeof(proposition)-1) << " was found.");
+				throw mrmc::exceptions::wrong_file_format();
+			}
+			else if (cnt > 0)
 			{
 				/*
 				 *	next token is: #DECLARATION: just skip it

src/parser/readLabFile.h

@@ -11,11 +11,15 @@ namespace parser {
 
 /*!
  *	@brief Load label file and return initialized AtomicPropositionsLabeling object.
+ *
+ *	Note that this class creates a new AtomicPropositionsLabeling object that can
+ *	be accessed via getLabeling(). However, it will not delete this object!
  */
 class LabParser : Parser
 {
 	public:
 		LabParser(uint_fast64_t node_count, const char* filename);
+
 		mrmc::models::AtomicPropositionsLabeling* getLabeling()
 		{
 			return this->labeling;

src/parser/readTraFile.cpp

@@ -118,6 +118,7 @@ uint_fast32_t TraParser::firstPass(char* buf, uint_fast32_t &maxnode)
  */
 
 TraParser::TraParser(const char * filename)
+	: matrix(nullptr)
 {
 	/*
 	*	enforce locale where decimal point is '.'

src/parser/readTraFile.h

@@ -11,6 +11,9 @@ namespace parser {
 /*!
  *	@brief	Load transition system from file and return initialized
  *	StaticSparseMatrix object.
+ *
+ *	Note that this class creates a new StaticSparseMatrix object that can be
+ *	accessed via getMatrix(). However, it does not delete this object!
  */
 class TraParser : Parser
 {

src/storage/BitVector.h

@@ -112,17 +112,17 @@ public:
 
 		if (initTrue) {
 			// Finally, create the full bucket array.
-			bucketArray = new uint64_t[bucketCount];
+			this->bucketArray = new uint64_t[bucketCount];
 
 			// Now initialize the values.
 			for (uint_fast64_t i = 0; i < bucketCount; ++i) {
-				bucketArray[i] = -1ll;
+				this->bucketArray[i] = -1ll;
 			}
 
 			truncateLastBucket();
 		} else {
 			// Finally, create the full bucket array.
-			bucketArray = new uint64_t[bucketCount]();
+			this->bucketArray = new uint64_t[bucketCount]();
 		}
 	}
 
@@ -134,7 +134,7 @@ public:
 	BitVector(const BitVector &bv) : bucketCount(bv.bucketCount), bitCount(bv.bitCount), endIterator(*this, bitCount, bitCount, false), truncateMask((1ll << (bitCount & mod64mask)) - 1ll) {
 		LOG4CPLUS_WARN(logger, "Invoking copy constructor.");
 		bucketArray = new uint64_t[bucketCount];
-		std::copy(bv.bucketArray, bv.bucketArray + bucketCount, bucketArray);
+		std::copy(bv.bucketArray, bv.bucketArray + this->bucketCount, this->bucketArray);
 	}
 
 	//! Destructor
@@ -142,8 +142,8 @@ public:
 	 * Destructor. Frees the underlying bucket array.
 	 */
 	~BitVector() {
-		if (bucketArray != nullptr) {
-			delete[] bucketArray;
+		if (this->bucketArray != nullptr) {
+			delete[] this->bucketArray;
 		}
 	}
 
@@ -178,7 +178,7 @@ public:
 		}
 
 		// Reserve a temporary array for copying.
-		uint_fast64_t* tempArray = new uint_fast64_t[newBucketCount];
+		uint64_t* tempArray = new uint64_t[newBucketCount];
 
 		// Copy over the elements from the old bit vector.
 		uint_fast64_t copySize = (newBucketCount <= bucketCount) ? newBucketCount : bucketCount;

src/storage/SquareSparseMatrix.h

@@ -112,19 +112,19 @@ public:
 	 */
 	~SquareSparseMatrix() {
 		setState(MatrixStatus::UnInitialized);
-		if (valueStorage != NULL) {
+		if (valueStorage != nullptr) {
 			//free(value_storage);
 			delete[] valueStorage;
 		}
-		if (columnIndications != NULL) {
+		if (columnIndications != nullptr) {
 			//free(column_indications);
 			delete[] columnIndications;
 		}
-		if (rowIndications != NULL) {
+		if (rowIndications != nullptr) {
 			//free(row_indications);
 			delete[] rowIndications;
 		}
-		if (diagonalStorage != NULL) {
+		if (diagonalStorage != nullptr) {
 			//free(diagonal_storage);
 			delete[] diagonalStorage;
 		}
@@ -507,7 +507,7 @@ public:
 			uint_fast64_t rowStart;
 			uint_fast64_t rowEnd;
 			uint_fast64_t zeroCount = 0;
-			for (uint_fast64_t row = 0; row <= rowCount; ++row) {
+			for (uint_fast64_t row = 0; row < rowCount; ++row) {
 				rowStart = rowIndications[row];
 				rowEnd = rowIndications[row + 1];
 				while (rowStart < rowEnd) {
@@ -518,7 +518,7 @@ public:
 			}
 
 			// Then add the elements on the diagonal.
-			for (uint_fast64_t i = 0; i <= rowCount; ++i) {
+			for (uint_fast64_t i = 0; i < rowCount; ++i) {
 				if (diagonalStorage[i] == 0) zeroCount++;
 				// tripletList.push_back(IntTriplet(i, i, diagonalStorage[i]));
 			}

test/storage/SquareSparseMatrixTest.cpp

@@ -157,6 +157,8 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_ColMajor_SparseMatrixTest)
 			ASSERT_EQ(target, row * 10 + col);
 		}
 	}
+	
+	delete ssm;
 }
 
 TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest) {
@@ -187,6 +189,8 @@ TEST(SquareSparseMatrixTest, ConversionFromDenseEigen_RowMajor_SparseMatrixTest)
 			ASSERT_EQ(target, row * 10 + col);
 		}
 	}
+	
+	delete ssm;
 }
 
 TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest) {
@@ -234,6 +238,8 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_ColMajor_SparseMatrixTest
 		ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target));
 		ASSERT_EQ(target, coeff.value());
 	}
+	
+	delete ssm;
 }
 
 TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
@@ -281,6 +287,8 @@ TEST(SquareSparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest
 		ASSERT_TRUE(ssm->getValue(coeff.row(), coeff.col(), &target));
 		ASSERT_EQ(target, coeff.value());
 	}
+	
+	delete ssm;
 }
 
 TEST(SquareSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest) {
@@ -311,4 +319,7 @@ TEST(SquareSparseMatrixTest, ConversionToSparseEigen_RowMajor_SparseMatrixTest)
 			ASSERT_EQ(values[row * 10 + col], esm->coeff(row, col));
 		}
 	}
+	
+	delete esm;
+	delete ssm;
 }