diff --git a/src/parser/read_lab_file.cpp b/src/parser/read_lab_file.cpp
index f61871ab9..d631cb215 100644
--- a/src/parser/read_lab_file.cpp
+++ b/src/parser/read_lab_file.cpp
@@ -53,7 +53,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
    FILE *P;
 
    //TODO (Thomas Heinemann): handle files with lines that are longer than BUFFER_SIZE
-   //TODO (Thomas Heinemann): Throw errors if fgets return NULL in the declaration.
+   //TODO (Thomas Heinemann): Throw errors if fgets return NULL in the declaration. (fixed by Philipp. Or?)
 
    char s[BUFFER_SIZE];              //String buffer
    char *saveptr = NULL;             //Buffer for strtok_r
@@ -64,14 +64,14 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
    if (P == NULL) {
       pantheios::log_ERROR("File could not be opened.");
       throw mrmc::exceptions::file_IO_exception();
+	  return NULL;
    }
 
-   if (fgets(s, BUFFER_SIZE, P)) {
-      if (strcmp(s, "#DECLARATION\n")) {
-         fclose(P);
-         pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing).");
-         throw mrmc::exceptions::wrong_file_format();
-      }
+   if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#DECLARATION\n")) {
+		fclose(P);
+		pantheios::log_ERROR("Wrong declaration section (\"#DECLARATION\" missing).");
+		throw mrmc::exceptions::wrong_file_format();
+		return NULL;
    }
 
 
@@ -104,6 +104,8 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
       } else {
          pantheios::log_ERROR("EOF in the declaration section");
          throw mrmc::exceptions::wrong_file_format();
+		 delete[] decl_buffer;
+		 return NULL;
       }
    } while (need_next_iteration);
 
@@ -132,17 +134,18 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
       result -> addProposition(proposition);
    }
 
+   // Free decl_buffer
+   delete[] decl_buffer;
 
 
    saveptr = NULL;                        //resetting save pointer for strtok_r
 
-   if (fgets(s, BUFFER_SIZE, P)) {
-      if (strcmp(s, "#END\n")) {
-         fclose(P);
-         delete result;
-         pantheios::log_ERROR("Wrong declaration section (\"#END\" missing).");
-         throw mrmc::exceptions::wrong_file_format();
-      }
+   if (!fgets(s, BUFFER_SIZE, P) || strcmp(s, "#END\n")) {
+		fclose(P);
+		delete result;
+		pantheios::log_ERROR("Wrong declaration section (\"#END\" missing).");
+		throw mrmc::exceptions::wrong_file_format();
+		return NULL;
    }
 
    while (fgets(s, BUFFER_SIZE, P)) {
@@ -157,6 +160,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
          delete result;
          pantheios::log_ERROR("Line assigning propositions does not start with a node number.");
          throw mrmc::exceptions::wrong_file_format();
+		 return NULL;
       }
       do {
          token = STRTOK_FUNC(NULL, sep, &saveptr);
@@ -169,9 +173,7 @@ mrmc::dtmc::labeling * read_lab_file(int node_count, const char * filename)
    }
 
    fclose(P);
-
    return result;
-
 }
 
 } //namespace parser
diff --git a/src/parser/read_tra_file.cpp b/src/parser/read_tra_file.cpp
index 8c2d12a95..72dcea77e 100644
--- a/src/parser/read_tra_file.cpp
+++ b/src/parser/read_tra_file.cpp
@@ -93,79 +93,79 @@ 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;
-   sparse::StaticSparseMatrix<double> *sp = NULL;
-
-   p = fopen(filename, "r");
-   if(p==NULL) {
-      pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
-      throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
-   }
-   non_zero = make_first_pass(p);
-
-   //Set file reader back to the beginning
-   rewind(p);
-
-   //Reading No. of states
-   if (fgets(s, BUFFER_SIZE, p) != NULL) {
-      if (sscanf( s, "STATES %d", &rows) == 0) {
-         pantheios::log_WARNING(pantheios::integer(rows));
-         (void)fclose(p);
-         throw mrmc::exceptions::wrong_file_format();
-      }
-   }
-
-   /* Reading No. of transitions
-    * Note that the result is not used in this function as make_first_pass()
-    * computes the relevant number (non_zero)
-    */
-   if (fgets(s, BUFFER_SIZE, p) != NULL) {
-      uint_fast32_t nnz=0;
-      if (sscanf( s, "TRANSITIONS %d", &nnz) == 0) {
-         (void)fclose(p);
-         throw mrmc::exceptions::wrong_file_format();
-      }
-   }
+	FILE *p = NULL;
+	char s[BUFFER_SIZE];
+	uint_fast32_t rows, non_zero;
+	sparse::StaticSparseMatrix<double> *sp = NULL;
+
+	p = fopen(filename, "r");
+	if(p == NULL) {
+		pantheios::log_ERROR("File ", filename, " was not readable (Does it exist?)");
+		throw exceptions::file_IO_exception("mrmc::read_tra_file: Error opening file! (Does it exist?)");
+		return NULL;
+	}
+	non_zero = make_first_pass(p);
+
+	//Set file reader back to the beginning
+	rewind(p);
+
+	//Reading No. of states
+	if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "STATES %d", &rows) == 0)) {
+		pantheios::log_WARNING(pantheios::integer(rows));
+		(void)fclose(p);
+		throw mrmc::exceptions::wrong_file_format();
+		return NULL;
+	}
+
+	/* Reading No. of transitions
+	 * 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;
+	if ((fgets(s, BUFFER_SIZE, p) == NULL) || (sscanf(s, "TRANSITIONS %d", &nnz) == 0)) {
+		(void)fclose(p);
+		throw mrmc::exceptions::wrong_file_format();
+		return NULL;
+	}
 
    pantheios::log_DEBUG("Creating matrix with ",
                         pantheios::integer(rows), " rows and ",
                         pantheios::integer(non_zero), " Non-Zero-Elements");
-   /* Creating matrix
-    * 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,non_zero);
-   sp->initialize();
-   if ( NULL == sp ) {
-      throw std::bad_alloc();
-      return NULL;
-      }
-
-   //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;
-      double val = 0.0;
-      if (sscanf( s, "%d%d%lf", &row, &col, &val) != 3) {
-         delete sp;
-         (void)fclose(p);
-         throw mrmc::exceptions::wrong_file_format();
-      }
-      pantheios::log_DEBUG("Write value ",
-                           pantheios::real(val),
-                           " to position ",
-                           pantheios::integer(row), " x ",
-                           pantheios::integer(col));
-      sp->addNextValue(row,col,val);
-   }
-
-   (void)fclose(p);
-
-   pantheios::log_DEBUG("Finalizing Matrix");
-   sp->finalize();
-   return sp;
+	/* Creating matrix
+	 * 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,non_zero);
+	if ( NULL == sp ) {
+		throw std::bad_alloc();
+		return NULL;
+	}
+	sp->initialize();
+
+	//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;
+		double val = 0.0;
+		if (sscanf(s, "%d%d%lf", &row, &col, &val) != 3) {
+			(void)fclose(p);
+			throw mrmc::exceptions::wrong_file_format();
+			// Delete Matrix to free allocated memory
+			delete sp;
+			return NULL;
+		}
+		pantheios::log_DEBUG("Write value ",
+							pantheios::real(val),
+							" to position ",
+							pantheios::integer(row), " x ",
+							pantheios::integer(col));
+		sp->addNextValue(row,col,val);
+	}
+
+	(void)fclose(p);
+
+	pantheios::log_DEBUG("Finalizing Matrix");
+	sp->finalize();
+	return sp;
 }
 
 } //namespace parser
diff --git a/src/sparse/static_sparse_matrix.h b/src/sparse/static_sparse_matrix.h
index b3b3f71b5..4177d06ee 100644
--- a/src/sparse/static_sparse_matrix.h
+++ b/src/sparse/static_sparse_matrix.h
@@ -26,13 +26,31 @@ namespace sparse {
 template <class T>
 class StaticSparseMatrix {
  public:
-		
+	//! Status enum
+	/*!
+		An Enum representing the internal state of the Matrix. 
+		After creating the Matrix using the Constructor, the Object is in state UnInitialized. After calling initialize(), that state changes to Initialized and after all entries have been entered and finalize() has been called, to ReadReady.
+		Should a critical error occur in any of the former functions, the state will change to Error.
+		@see getState()
+		@see isReadReady()
+		@see isInitialized()
+		@see hasError()
+	 */
+	 enum MatrixStatus {
+		Error = -1,
+		UnInitialized = 0,
+		Initialized = 1,
+		ReadReady = 2,
+	 };
+
+
 	//! Constructor
 	 /*!
 		\param rows Row-Count and therefore column-count of the symmetric matrix
 		\param non_zero_entries The exact count of entries that will be submitted through addNextValue *excluding* those on the diagonal (A_{i,j} with i = j)
 	 */
 	StaticSparseMatrix(uint_fast32_t rows, uint_fast32_t non_zero_entries) {
+		setState(MatrixStatus::UnInitialized);
 		current_size = 0;
 		storage_size = 0;
 		
@@ -48,6 +66,7 @@ class StaticSparseMatrix {
 	}
 
 	~StaticSparseMatrix() {
+		setState(MatrixStatus::UnInitialized);
 		if (value_storage != NULL) {
 			//free(value_storage);
 			delete[] value_storage;
@@ -68,7 +87,7 @@ class StaticSparseMatrix {
 
 	//! Getter for saving matrix entry A_{row,col} to target
 	/*!
-		Getter function for the matrix. 
+		Getter function for the matrix. This function does not check the internal status for errors for performance reasons.
 		\param row 1-based index of the requested row
 		\param col 1-based index of the requested column
 		\param target pointer to where the result will be stored
@@ -109,36 +128,42 @@ class StaticSparseMatrix {
 		Mandatory initialization of the matrix, must be called before using any other member function.
 	 */
 	void initialize() {
-
-		if (row_count == 0) {
+		if (internal_status != MatrixStatus::UnInitialized) {
+			pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid state for status flag != 0 (is ", pantheios::integer(internal_status)," - Already initialized?");
+			throw mrmc::exceptions::invalid_state("StaticSparseMatrix::initialize: Invalid state for status flag != 0 - Already initialized?");
+			triggerErrorState();
+		} else if (row_count == 0) {
 			pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid_argument for row_count = 0");
 			throw mrmc::exceptions::invalid_argument("mrmc::StaticSparseMatrix::initialize: Matrix with 0 rows is not reasonable");
-		}
-
-		if (((row_count * row_count) - row_count) < non_zero_entry_count) {
+			triggerErrorState();
+		} else if (((row_count * row_count) - row_count) < non_zero_entry_count) {
 			pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing invalid_argument: More non-zero entries than entries in target matrix");
 			throw mrmc::exceptions::invalid_argument("mrmc::StaticSparseMatrix::initialize: More non-zero entries than entries in target matrix");
-		}
-
-		storage_size = non_zero_entry_count;
-		last_row = 0;
+			triggerErrorState();
+		} else {
+			storage_size = non_zero_entry_count;
+			last_row = 0;
 
-		//value_storage = static_cast<T*>(calloc(storage_size, sizeof(*value_storage)));
-		value_storage = new (std::nothrow) T[storage_size]();
+			//value_storage = static_cast<T*>(calloc(storage_size, sizeof(*value_storage)));
+			value_storage = new (std::nothrow) T[storage_size]();
 
-		//column_indications = static_cast<uint_fast32_t*>(calloc(storage_size, sizeof(*column_indications)));
-		column_indications = new (std::nothrow) uint_fast32_t[storage_size]();
+			//column_indications = static_cast<uint_fast32_t*>(calloc(storage_size, sizeof(*column_indications)));
+			column_indications = new (std::nothrow) uint_fast32_t[storage_size]();
 
-		//row_indications = static_cast<uint_fast32_t*>(calloc(row_count + 1, sizeof(*row_indications)));
-		row_indications = new (std::nothrow) uint_fast32_t[row_count + 1]();
+			//row_indications = static_cast<uint_fast32_t*>(calloc(row_count + 1, sizeof(*row_indications)));
+			row_indications = new (std::nothrow) uint_fast32_t[row_count + 1]();
 
-		// row_count + 1 so that access with 1-based indices can be direct without the overhead of a -1 each time
-		//diagonal_storage = static_cast<T*>(calloc(row_count + 1, sizeof(*diagonal_storage)));
-		diagonal_storage = new (std::nothrow) T[row_count + 1]();
+			// row_count + 1 so that access with 1-based indices can be direct without the overhead of a -1 each time
+			//diagonal_storage = static_cast<T*>(calloc(row_count + 1, sizeof(*diagonal_storage)));
+			diagonal_storage = new (std::nothrow) T[row_count + 1]();
 		
-		if ((value_storage == NULL) || (column_indications == NULL) || (row_indications == NULL) || (diagonal_storage == NULL)) {
-			pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing bad_alloc: memory allocation failed");
-			throw std::bad_alloc();
+			if ((value_storage == NULL) || (column_indications == NULL) || (row_indications == NULL) || (diagonal_storage == NULL)) {
+				pantheios::log_ERROR("StaticSparseMatrix::initialize: Throwing bad_alloc: memory allocation failed");
+				throw std::bad_alloc();
+				triggerErrorState();
+			} else {
+				setState(MatrixStatus::Initialized);
+			}
 		}
 	}
 
@@ -151,6 +176,7 @@ class StaticSparseMatrix {
 		if ((row > row_count) || (col > row_count) || (row == 0) || (col == 0)) {
 			pantheios::log_ERROR("StaticSparseMatrix::addNextValue: Throwing out_of_range: row or col not in 1 .. rows");
 			throw mrmc::exceptions::out_of_range("mrmc::StaticSparseMatrix::addNextValue: row or col not in 1 .. rows");
+			triggerErrorState();
 		}
 		
 		if (row == col) {
@@ -172,18 +198,25 @@ class StaticSparseMatrix {
 	}
 
 	void finalize() {
-		if (storage_size != current_size) {
+		if (!isInitialized()) {
+			pantheios::log_ERROR("StaticSparseMatrix::finalize: Throwing invalid state for internal state not Initialized (is ", pantheios::integer(internal_status)," - Already finalized?");
+			throw mrmc::exceptions::invalid_state("StaticSparseMatrix::finalize: Invalid state for internal state not Initialized - Already finalized?");
+			triggerErrorState();
+		} else if (storage_size != current_size) {
 			pantheios::log_ERROR("StaticSparseMatrix::finalize: Throwing invalid_state: Wrong call count for addNextValue");
 			throw mrmc::exceptions::invalid_state("mrmc::StaticSparseMatrix::finalize: Wrong call count for addNextValue");
-		}
-
-		if (last_row != row_count) {
-			for (uint_fast32_t i = last_row; i < row_count; ++i) {
-				row_indications[i] = current_size;
+			triggerErrorState();
+		} else {
+			if (last_row != row_count) {
+				for (uint_fast32_t i = last_row; i < row_count; ++i) {
+					row_indications[i] = current_size;
+				}
 			}
-		}
 
-		row_indications[row_count] = storage_size;
+			row_indications[row_count] = storage_size;
+
+			setState(MatrixStatus::ReadReady);
+		}
 	}
 
 	uint_fast32_t getRowCount() const {
@@ -194,29 +227,52 @@ class StaticSparseMatrix {
 		return value_storage;
 	}
 
-	Eigen::SparseMatrix<T> toEigenSparseMatrix() {
-		typedef Eigen::Triplet<double> ETd;
-		std::vector<ETd> tripletList;
-		tripletList.reserve(non_zero_entry_count + row_count);
-
-		uint_fast32_t row_start;
-		uint_fast32_t row_end;
-		for (uint_fast32_t row = 1; row <= row_count; ++row) {
-			row_start	= row_indications[row - 1];
-			row_end		= row_indications[row];
-			while (row_start < row_end) {
-				tripletList.push_back(ETd(row - 1, column_indications[row_start] - 1, value_storage[row_start]));
-				++row_start;
-			}
-		}
-		for (uint_fast32_t i = 1; i <= row_count; ++i) {
-			tripletList.push_back(ETd(i, i, diagonal_storage[i]));
-		}
+	bool isReadReady() {
+		return (internal_status == MatrixStatus::ReadReady);
+	}
+
+	bool isInitialized() {
+		return (internal_status == MatrixStatus::Initialized || internal_status == MatrixStatus::ReadReady);
+	}
+
+	MatrixStatus getState() {
+		return internal_status;
+	}
 
+	bool hasError() {
+		return (internal_status == MatrixStatus::Error);
+	}
+
+	Eigen::SparseMatrix<T> toEigenSparseMatrix() {
 		Eigen::SparseMatrix<T> mat(row_count, row_count);
-		mat.setFromTriplets(tripletList.begin(), tripletList.end());
-		mat.makeCompressed();
 
+		if (!isReadReady()) {
+			pantheios::log_ERROR("StaticSparseMatrix::toEigenSparseMatrix: Throwing invalid state for internal state not ReadReady (is ", pantheios::integer(internal_status),").");
+			throw mrmc::exceptions::invalid_state("StaticSparseMatrix::toEigenSparseMatrix: Invalid state for internal state not ReadReady.");
+			triggerErrorState();
+		} else {
+			typedef Eigen::Triplet<double> ETd;
+			std::vector<ETd> tripletList;
+			tripletList.reserve(non_zero_entry_count + row_count);
+
+			uint_fast32_t row_start;
+			uint_fast32_t row_end;
+			for (uint_fast32_t row = 1; row <= row_count; ++row) {
+				row_start	= row_indications[row - 1];
+				row_end		= row_indications[row];
+				while (row_start < row_end) {
+					tripletList.push_back(ETd(row - 1, column_indications[row_start] - 1, value_storage[row_start]));
+					++row_start;
+				}
+			}
+			for (uint_fast32_t i = 1; i <= row_count; ++i) {
+				tripletList.push_back(ETd(i, i, diagonal_storage[i]));
+			}
+
+			mat.setFromTriplets(tripletList.begin(), tripletList.end());
+			mat.makeCompressed();
+		}
+		
 		return mat;
 	}
 
@@ -237,6 +293,22 @@ class StaticSparseMatrix {
 	uint_fast32_t* column_indications;
 	/*! Array containing the row boundaries of valueStorage */
 	uint_fast32_t* row_indications;
+
+	/*! Internal status enum, 0 for constructed, 1 for initialized and 2 for finalized, -1 on errors */
+	MatrixStatus internal_status;
+
+	/*! Sets the internal status to Error */
+	void triggerErrorState() {
+		setState(MatrixStatus::Error);
+	}
+
+	/*! 
+		Sets the internal status to new_state iff the current state is not the Error state.
+		@param new_state the new state to be switched to
+	*/
+	void setState(const MatrixStatus new_state) {
+		internal_status = (internal_status == MatrixStatus::Error) ? internal_status : new_state;
+	}
 };
 
 } // namespace sparse
diff --git a/test/parser/read_lab_file_test.cpp b/test/parser/read_lab_file_test.cpp
index 925952625..b2ee34ce3 100644
--- a/test/parser/read_lab_file_test.cpp
+++ b/test/parser/read_lab_file_test.cpp
@@ -18,63 +18,65 @@ TEST(ReadLabFileTest, NonExistingFileTest) {
 }
 
 TEST(ReadLabFileTest, ParseTest) {
-   //This test is based on a test case from the original MRMC.
-   mrmc::dtmc::labeling* labeling;
-
-   //Parsing the file
-   ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
-
-   //Checking whether all propositions are in the labelling
-
-   char phi[] = "phi", psi[] = "psi", smth[] = "smth";
-
-   ASSERT_TRUE(labeling->containsProposition(phi));
-   ASSERT_TRUE(labeling->containsProposition(psi));
-   ASSERT_TRUE(labeling->containsProposition(smth));
-
-   //Testing whether all and only the correct nodes are labeled with "phi"
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,1));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,2));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,3));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,5));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,7));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,9));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,10));
-   ASSERT_TRUE(labeling->nodeHasProposition(phi,11));
-
-   ASSERT_FALSE(labeling->nodeHasProposition(phi,4));
-   ASSERT_FALSE(labeling->nodeHasProposition(phi,6));
-
-   //Testing whether all and only the correct nodes are labeled with "psi"
-   ASSERT_TRUE(labeling->nodeHasProposition(psi,6));
-   ASSERT_TRUE(labeling->nodeHasProposition(psi,7));
-   ASSERT_TRUE(labeling->nodeHasProposition(psi,8));
-
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,1));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,2));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,3));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,4));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,5));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,9));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,10));
-   ASSERT_FALSE(labeling->nodeHasProposition(psi,11));
-
-   //Testing whether all and only the correct nodes are labeled with "smth"
-   ASSERT_TRUE(labeling->nodeHasProposition(smth,4));
-   ASSERT_TRUE(labeling->nodeHasProposition(smth,5));
-
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,1));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,2));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,3));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,6));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,7));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,8));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,9));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,10));
-   ASSERT_FALSE(labeling->nodeHasProposition(smth,11));
-
-   //Deleting the labeling
-   delete labeling;
+	//This test is based on a test case from the original MRMC.
+	mrmc::dtmc::labeling* labeling = NULL;
+
+	//Parsing the file
+	ASSERT_NO_THROW(labeling = mrmc::parser::read_lab_file(12, MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
+
+	//Checking whether all propositions are in the labelling
+
+	char phi[] = "phi", psi[] = "psi", smth[] = "smth";
+
+	if (labeling != NULL) {
+		ASSERT_TRUE(labeling->containsProposition(phi));
+		ASSERT_TRUE(labeling->containsProposition(psi));
+		ASSERT_TRUE(labeling->containsProposition(smth));
+
+		//Testing whether all and only the correct nodes are labeled with "phi"
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,1));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,2));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,3));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,5));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,7));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,9));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,10));
+		ASSERT_TRUE(labeling->nodeHasProposition(phi,11));
+
+		ASSERT_FALSE(labeling->nodeHasProposition(phi,4));
+		ASSERT_FALSE(labeling->nodeHasProposition(phi,6));
+
+		//Testing whether all and only the correct nodes are labeled with "psi"
+		ASSERT_TRUE(labeling->nodeHasProposition(psi,6));
+		ASSERT_TRUE(labeling->nodeHasProposition(psi,7));
+		ASSERT_TRUE(labeling->nodeHasProposition(psi,8));
+
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,1));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,2));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,3));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,4));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,5));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,9));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,10));
+		ASSERT_FALSE(labeling->nodeHasProposition(psi,11));
+
+		//Testing whether all and only the correct nodes are labeled with "smth"
+		ASSERT_TRUE(labeling->nodeHasProposition(smth,4));
+		ASSERT_TRUE(labeling->nodeHasProposition(smth,5));
+
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,1));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,2));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,3));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,6));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,7));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,8));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,9));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,10));
+		ASSERT_FALSE(labeling->nodeHasProposition(smth,11));
+
+		//Deleting the labeling
+		delete labeling;
+	}
 }
 
 TEST(ReadLabFileTest, WrongHeaderTest1) {
diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp
index fead6b563..e2eed9787 100644
--- a/test/parser/read_tra_file_test.cpp
+++ b/test/parser/read_tra_file_test.cpp
@@ -22,45 +22,47 @@ TEST(ReadTraFileTest, NonExistingFileTest) {
 /* The following test case is based on one of the original MRMC test cases
  */
 TEST(ReadTraFileTest, ParseFileTest1) {
-   pantheios::log_INFORMATIONAL("Started ParseFileTest1");
-   mrmc::sparse::StaticSparseMatrix<double> *result;
-   ASSERT_NO_THROW(result = mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
+	pantheios::log_INFORMATIONAL("Started ParseFileTest1");
+	mrmc::sparse::StaticSparseMatrix<double> *result = NULL;
+	ASSERT_NO_THROW(result = mrmc::parser::read_tra_file(MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/csl_general_input_01.tra"));
 
-   double val = 0;
-   ASSERT_TRUE(result->getValue(1,1,&val));
-   ASSERT_EQ(val,0.080645161290322580645161290322581);
+	if (result != NULL) {
+		double val = 0;
+		ASSERT_TRUE(result->getValue(1,1,&val));
+		ASSERT_EQ(val,0.080645161290322580645161290322581);
 
-   ASSERT_TRUE(result->getValue(1,2,&val));
-   ASSERT_EQ(val,0.080645161290322580645161290322581);
+		ASSERT_TRUE(result->getValue(1,2,&val));
+		ASSERT_EQ(val,0.080645161290322580645161290322581);
 
-   //Transition 1->3 was not set in the file, so it is not to appear in the matrix!
-   ASSERT_FALSE(result->getValue(1,3,&val));
-   ASSERT_EQ(val,0);
+		//Transition 1->3 was not set in the file, so it is not to appear in the matrix!
+		ASSERT_FALSE(result->getValue(1,3,&val));
+		ASSERT_EQ(val,0);
 
-   ASSERT_TRUE(result->getValue(2,1,&val));
-   ASSERT_EQ(val,0.04032258064516129032258064516129);
+		ASSERT_TRUE(result->getValue(2,1,&val));
+		ASSERT_EQ(val,0.04032258064516129032258064516129);
 
-   ASSERT_TRUE(result->getValue(2,2,&val));
-   ASSERT_EQ(val,0.04032258064516129032258064516129);
+		ASSERT_TRUE(result->getValue(2,2,&val));
+		ASSERT_EQ(val,0.04032258064516129032258064516129);
 
-   ASSERT_TRUE(result->getValue(2,3,&val));
-   ASSERT_EQ(val,0.04032258064516129032258064516129);
+		ASSERT_TRUE(result->getValue(2,3,&val));
+		ASSERT_EQ(val,0.04032258064516129032258064516129);
 
-   ASSERT_TRUE(result->getValue(2,4,&val));
-   ASSERT_EQ(val,0.04032258064516129032258064516129);
+		ASSERT_TRUE(result->getValue(2,4,&val));
+		ASSERT_EQ(val,0.04032258064516129032258064516129);
 
-   ASSERT_TRUE(result->getValue(3,2,&val));
-   ASSERT_EQ(val,0.0806451612903225806451612903225812);
+		ASSERT_TRUE(result->getValue(3,2,&val));
+		ASSERT_EQ(val,0.0806451612903225806451612903225812);
 
-   ASSERT_TRUE(result->getValue(3,3,&val));
-   ASSERT_EQ(val,0);
+		ASSERT_TRUE(result->getValue(3,3,&val));
+		ASSERT_EQ(val,0);
 
-   ASSERT_TRUE(result->getValue(3,4,&val));
-   ASSERT_EQ(val,0.080645161290322580645161290322581);
+		ASSERT_TRUE(result->getValue(3,4,&val));
+		ASSERT_EQ(val,0.080645161290322580645161290322581);
 
-   ASSERT_TRUE(result->getValue(4,4,&val));
-   ASSERT_EQ(val,0);
-   delete result;
+		ASSERT_TRUE(result->getValue(4,4,&val));
+		ASSERT_EQ(val,0);
+		delete result;
+	}
 }
 
 TEST(ReadTraFileTest, WrongFormatTestHeader1) {