From a04bdd9b970e51bd28e1b31330199a77dfdddd8a Mon Sep 17 00:00:00 2001 From: dehnert Date: Sat, 22 Dec 2012 19:41:01 +0100 Subject: [PATCH] Fixed a few bugs. --- src/modelChecker/EigenDtmcPrctlModelChecker.h | 2 +- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 10 ++++++++-- src/storage/SquareSparseMatrix.h | 2 +- 3 files changed, 10 insertions(+), 4 deletions(-) diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index 9a1760292..f17f87def 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -51,7 +51,7 @@ public: mrmc::storage::SquareSparseMatrix 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* eigenMatrix = tmpMatrix.toEigenSparseMatrix(); diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index cd693da78..83036e3bf 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -49,7 +49,7 @@ public: mrmc::storage::SquareSparseMatrix 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* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); @@ -59,9 +59,15 @@ public: mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. + std::vector* swap = nullptr; + std::vector* tmpResult = new std::vector(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; diff --git a/src/storage/SquareSparseMatrix.h b/src/storage/SquareSparseMatrix.h index cbb56f196..b14e31dd2 100644 --- a/src/storage/SquareSparseMatrix.h +++ b/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 {