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

CMakeLists.txt

@@ -24,7 +24,7 @@ endif()
 
 #Configurations for GCC
 if(CMAKE_COMPILER_IS_GNUCC) 
-    set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -pedantic")
+    set (CMAKE_CXX_FLAGS "-std=c++0x -Wall -Werror -pedantic")
     
     # Turn on popcnt instruction if possible
     if (USE_POPCNT)

src/models/atomic_propositions_labeling.h

@@ -58,7 +58,7 @@ public:
 	 * @param state_count The number of states of the model.
 	 * @param ap_count The number of atomic propositions.
 	 */
-	AtomicPropositionsLabeling(const uint_fast32_t state_count,	const uint_fast32_t ap_count)
+	AtomicPropositionsLabeling(const uint_fast32_t state_count, const uint_fast32_t ap_count)
 			: state_count(state_count), ap_count(ap_count), aps_current(0) {
 		this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count];
 		for (uint_fast32_t i = 0; i < ap_count; ++i) {
@@ -78,8 +78,7 @@ public:
 			  name_to_labeling_map(atomic_propositions_labeling.name_to_labeling_map) {
 		this->single_labelings = new SingleAtomicPropositionLabeling*[ap_count];
 		for (uint_fast32_t i = 0; i < ap_count; ++i) {
-			this->single_labelings[i] = new SingleAtomicPropositionLabeling(
-					*atomic_propositions_labeling.single_labelings[i]);
+			this->single_labelings[i] = new SingleAtomicPropositionLabeling(*atomic_propositions_labeling.single_labelings[i]);
 		}
 	}
 
@@ -89,7 +88,6 @@ public:
 	 */
 	virtual ~AtomicPropositionsLabeling() {
 		// delete all the single atomic proposition labelings in the map
-		MAP<std::string, SingleAtomicPropositionLabeling*>::iterator it;
 		for (uint_fast32_t i = 0; i < ap_count; ++i) {
 			delete this->single_labelings[i];
 			this->single_labelings[i] = NULL;

src/models/backward_transitions.h

@@ -35,43 +35,47 @@ public:
 	 * @param transition_matrix The (0-based) matrix representing the transition
 	 * relation.
 	 */
-	BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transitionMatrix)
-			: numberOfStates(transitionMatrix->getRowCount()),
-			  numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
-		this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
+	BackwardTransitions(mrmc::sparse::StaticSparseMatrix<T>* transitionMatrix) {
+		numberOfNonZeroTransitions = transitionMatrix->getNonZeroEntryCount();
 		this->predecessor_list = new uint_fast64_t[numberOfNonZeroTransitions];
+		
+		numberOfStates = transitionMatrix->getRowCount();
+		this->state_indices_list = new uint_fast64_t[numberOfStates + 1];
 
 		// First, we need to count how many backward transitions each state has.
 		// NOTE: We disregard the diagonal here, as we only consider "true"
 		// predecessors.
-		for (uint_fast64_t i = 0; i <= numberOfStates; i++) {
+		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
 			for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
 				this->state_indices_list[*rowIt + 1]++;
 			}
 		}
 
 		// Now compute the accumulated offsets.
-		for (uint_fast64_t i = 1; i <= numberOfStates; i++) {
+		for (uint_fast64_t i = 1; i < numberOfStates; i++) {
 			this->state_indices_list[i] = this->state_indices_list[i - 1] + this->state_indices_list[i];
 		}
 
 		// Put a sentinel element at the end of the indices list. This way,
 		// for each state i the range of indices can be read off between
 		// state_indices_list[i] and state_indices_list[i + 1].
-		this->state_indices_list[numberOfStates + 1] = numberOfNonZeroTransitions;
+		this->state_indices_list[numberOfStates] = numberOfNonZeroTransitions;
 
 		// Create an array that stores the next index for each state. Initially
 		// this corresponds to the previously computed accumulated offsets.
-		uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates + 1];
-		memcpy(next_state_index_list, state_indices_list, (numberOfStates + 1) * sizeof(uint_fast64_t));
+		uint_fast64_t* next_state_index_list = new uint_fast64_t[numberOfStates];
+		memcpy(next_state_index_list, state_indices_list, numberOfStates * sizeof(uint_fast64_t));
 
 		// Now we are ready to actually fill in the list of predecessors for
 		// every state. Again, we start by considering all but the last row.
-		for (uint_fast64_t i = 0; i <= numberOfStates; i++) {
+		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
 			for (auto rowIt = transitionMatrix->beginConstColumnNoDiagIterator(i); rowIt != transitionMatrix->endConstColumnNoDiagIterator(i); ++rowIt) {
 				this->predecessor_list[next_state_index_list[*rowIt]++] = i;
 			}
 		}
+
+		// Now we can dispose of the auxiliary array.
+		delete[] next_state_index_list;
 	}
 
 	//! Destructor
@@ -79,10 +83,10 @@ public:
 	 * Destructor. Frees the internal storage.
 	 */
 	~BackwardTransitions() {
-		if (this->predecessor_list != NULL) {
+		if (this->predecessor_list != nullptr) {
 			delete[] this->predecessor_list;
 		}
-		if (this->state_indices_list != NULL) {
+		if (this->state_indices_list != nullptr) {
 			delete[] this->state_indices_list;
 		}
 	}

src/models/dtmc.h

@@ -55,6 +55,20 @@ public:
 		pantheios::log_DEBUG("Copy constructor of DTMC invoked.");
 	}
 
+	//! Destructor
+	/*!
+	 * Destructor. Frees the matrix and labeling associated with this DTMC.
+	 *
+	 */
+	~Dtmc() {
+		if (this->probability_matrix != nullptr) {
+			delete this->probability_matrix;
+		}
+		if (this->state_labeling != nullptr) {
+			delete this->state_labeling;
+		}
+	}
+
 	/*!
 	 * Returns the state space size of the DTMC.
 	 * @return The size of the state space of the DTMC.

src/mrmc-cpp.cpp

@@ -42,11 +42,12 @@ int main(const int argc, const char* argv[]) {
 	
 	try
 	{
-		s = new mrmc::settings::Settings(argc, argv, NULL);
+		s = new mrmc::settings::Settings(argc, argv, nullptr);
 	}
 	catch (mrmc::exceptions::InvalidSettings)
 	{
 		std::cout << "Could not recover from settings error, terminating." << std::endl;
+		delete s;
 		return 1;
 	}
 	
@@ -65,7 +66,9 @@ int main(const int argc, const char* argv[]) {
 	mrmc::models::AtomicPropositionsLabeling* labeling = mrmc::parser::read_lab_file(probMatrix->getRowCount(), s->getString("labfile").c_str());
 	mrmc::models::Dtmc<double> dtmc(probMatrix, labeling);
 
-
+	if (s != nullptr) {
+		delete s;
+	}
 
 	return 0;
 }

src/parser/read_lab_file.cpp

@@ -25,9 +25,12 @@
 #	define STRTOK_FUNC strtok_r
 #endif
 
+// Only disable the warning if we are not using GCC, because
+// GCC does not know this pragma and raises a warning 
+#ifndef __GNUG__
 // Disable C4996 - This function or variable may be unsafe.
 #pragma warning(disable:4996)
-
+#endif
 
 namespace mrmc {
 
@@ -150,7 +153,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
 
    while (fgets(s, BUFFER_SIZE, P)) {
       char * token = NULL;
-      uint_fast32_t node = 0;
+      unsigned int node = 0;
       /* First token has to be a number identifying the node,
        * hence it is treated differently from the other tokens.
        */
@@ -167,7 +170,7 @@ mrmc::models::AtomicPropositionsLabeling * read_lab_file(int node_count, const c
          if (token == NULL) {
             break;
          }
-         result->addAtomicPropositionToState(token, node);
+         result->addAtomicPropositionToState(token, static_cast<uint_fast64_t>(node));
       } while (token != NULL);
 
    }

src/parser/read_tra_file.cpp

@@ -26,8 +26,12 @@ namespace mrmc {
 
 namespace parser{
 
+// Only disable the warning if we are not using GCC, because
+// GCC does not know this pragma and raises a warning 
+#ifndef __GNUG__
 // Disable C4996 - This function or variable may be unsafe.
 #pragma warning(disable:4996)
+#endif
 
 /*!
 * This method does the first pass through the .tra file and computes
@@ -46,7 +50,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
       throw exceptions::file_IO_exception ("make_first_pass: File not readable (this should be checked before calling this function!)");
    }
    char s[BUFFER_SIZE];                 //String buffer
-   uint_fast32_t rows=0, non_zero=0;
+   int rows=0, non_zero=0;
 
    //Reading No. of states
    if (fgets(s, BUFFER_SIZE, p) != NULL) {
@@ -69,7 +73,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
    //And increase number of transitions
    while (NULL != fgets( s, BUFFER_SIZE, p ))
    {
-      uint_fast32_t row=0, col=0;
+      int row=0, col=0;
       double val=0.0;
       if (sscanf( s, "%d%d%lf", &row, &col, &val ) != 3) {
          (void)fclose(p);
@@ -80,7 +84,7 @@ static uint_fast32_t make_first_pass(FILE* p) {
          --non_zero;
       }
    }
-   return non_zero;
+   return static_cast<uint_fast64_t>(non_zero);
 }
 
 
@@ -95,7 +99,8 @@ static uint_fast32_t make_first_pass(FILE* p) {
 sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	FILE *p = NULL;
 	char s[BUFFER_SIZE];
-	uint_fast32_t rows, non_zero;
+	uint_fast64_t non_zero = 0;
+	int rows = 0;
 	sparse::StaticSparseMatrix<double> *sp = NULL;
 
 	p = fopen(filename, "r");
@@ -121,7 +126,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	 * Note that the result is not used in this function as make_first_pass()
 	 * computes the relevant number (non_zero)
 	 */
-	uint_fast32_t nnz=0;
+	int nnz = 0;
 	if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) {
 		(void)fclose(p);
 		throw mrmc::exceptions::wrong_file_format();
@@ -135,7 +140,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 	 * Memory for diagonal elements is automatically allocated, hence only the number of non-diagonal
 	 * non-zero elements has to be specified (which is non_zero, computed by make_first_pass)
 	 */
-	sp = new sparse::StaticSparseMatrix<double>(rows + 1);
+	sp = new sparse::StaticSparseMatrix<double>(static_cast<uint_fast64_t>(rows) + 1);
 	if ( NULL == sp ) {
 		throw std::bad_alloc();
 		return NULL;
@@ -144,7 +149,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 
 	//Reading transitions (one per line) and saving the results in the matrix
 	while (NULL != fgets(s, BUFFER_SIZE, p )) {
-		uint_fast32_t row=0, col=0;
+		int row=0, col=0;
 		double val = 0.0;
 		if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) {
 			(void)fclose(p);
@@ -158,7 +163,7 @@ sparse::StaticSparseMatrix<double> * read_tra_file(const char * filename) {
 							" to position ",
 							pantheios::integer(row), " x ",
 							pantheios::integer(col));
-		sp->addNextValue(row,col,val);
+		sp->addNextValue(static_cast<uint_fast64_t>(row),static_cast<uint_fast64_t>(col),static_cast<uint_fast64_t>(val));
 	}
 
 	(void)fclose(p);

src/reward/reward_model.h

@@ -27,7 +27,7 @@ class RewardModel {
 	typedef const DataClass& crDataClass;
 
 	public:
-		RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : null_value(null_value), state_count(state_count) {
+		RewardModel(const uint_fast32_t state_count, const DataClass& null_value) : state_count(state_count), null_value(null_value) {
 
 			this->reward_vector = new VectorImpl<DataClass, std::allocator<DataClass>>(this->state_count);
 			// init everything to zero

src/sparse/static_sparse_matrix.h

@@ -47,7 +47,7 @@ public:
 	 * @see hasError()
 	 */
 	enum MatrixStatus {
-		Error = -1, UnInitialized = 0, Initialized = 1, ReadReady = 2,
+		Error = -1, UnInitialized = 0, Initialized = 1, ReadReady = 2
 	};
 
 	//! Constructor
@@ -56,11 +56,7 @@ public:
 	 * @param rows The number of rows of the matrix
 	 */
 	StaticSparseMatrix(uint_fast64_t rows)
-			: internalStatus(MatrixStatus::UnInitialized),
-			  currentSize(0), lastRow(0), valueStorage(nullptr),
-			  diagonalStorage(nullptr), columnIndications(nullptr),
-			  rowIndications(nullptr), rowCount(rows), nonZeroEntryCount(0) { }
-
+			: rowCount(rows), nonZeroEntryCount(0), valueStorage(nullptr), diagonalStorage(nullptr), columnIndications(nullptr), rowIndications(nullptr), internalStatus(MatrixStatus::UnInitialized), currentSize(0), lastRow(0) { }
 	//! Copy Constructor
 	/*!
 	 * Copy Constructor. Performs a deep copy of the given sparse matrix.
@@ -322,7 +318,7 @@ public:
 			// Fill in the missing entries in the row_indications array.
 			// (Can happen because of empty rows at the end.)
 			if (lastRow != rowCount) {
-				for (uint_fast64_t i = lastRow + 1; i <= rowCount; ++i) {
+				for (uint_fast64_t i = lastRow + 1; i < rowCount; ++i) {
 					rowIndications[i] = currentSize;
 				}
 			}
@@ -331,7 +327,7 @@ public:
 			// array. This eases iteration work, as now the indices of row i
 			// are always between row_indications[i] and row_indications[i + 1],
 			// also for the first and last row.
-			rowIndications[rowCount + 1] = nonZeroEntryCount;
+			rowIndications[rowCount] = nonZeroEntryCount;
 
 			setState(MatrixStatus::ReadReady);
 		}