Fixed a few bugs.

src/modelChecker/EigenDtmcPrctlModelChecker.h

@@ -51,7 +51,7 @@ public:
 		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 eigen format to use its arithmetic.
 		Eigen::SparseMatrix<Type, 1, int_fast32_t>* eigenMatrix = tmpMatrix.toEigenSparseMatrix();

src/modelChecker/GmmxxDtmcPrctlModelChecker.h

@@ -49,7 +49,7 @@ public:
 		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<Type>* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix();
@@ -59,9 +59,15 @@ public:
 		mrmc::utility::setVectorValues(result, *rightStates, static_cast<Type>(1.0));
 
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
+		std::vector<Type>* swap = nullptr;
+		std::vector<Type>* tmpResult = new std::vector<Type>(this->getModel().getNumberOfStates());
 		for (uint_fast64_t i = 0; i < formula.getBound(); ++i) {
-			gmm::mult(*gmmxxMatrix, *result, *result);
+			gmm::mult(*gmmxxMatrix, *result, *tmpResult);
+			swap = tmpResult;
+			tmpResult = result;
+			result = swap;
 		}
+		delete tmpResult;
 
 		// Delete intermediate results and return result.
 		delete leftStates;

src/storage/SquareSparseMatrix.h

@@ -76,7 +76,7 @@ public:
 			  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()) {
+		if (ssm.hasError()) {
 			LOG4CPLUS_ERROR(logger, "Trying to copy sparse matrix in error state.");
 			throw mrmc::exceptions::InvalidArgumentException("Trying to copy sparse matrix in error state.");
 		} else {