From c54283cef27ba00dc649a2e5ce76ed981bab9a12 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Dec 2012 17:58:49 +0100 Subject: [PATCH] Merge. --- src/modelChecker/DtmcPrctlModelChecker.h | 8 ++- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 52 +++++++++++-------- src/mrmc.cpp | 4 ++ 3 files changed, 41 insertions(+), 23 deletions(-) diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h index fef616231..76aa00531 100644 --- a/src/modelChecker/DtmcPrctlModelChecker.h +++ b/src/modelChecker/DtmcPrctlModelChecker.h @@ -186,17 +186,23 @@ public: */ mrmc::storage::BitVector* checkProbabilisticIntervalOperator( const mrmc::formula::ProbabilisticIntervalOperator& formula) const { + // First, we need to compute the probability for satisfying the path formula for each state. std::vector* probabilisticResult = this->checkPathFormula(formula.getPathFormula()); + // Create resulting bit vector, which will hold the yes/no-answer for every state. mrmc::storage::BitVector* result = new mrmc::storage::BitVector(this->getModel().getNumberOfStates()); + + // Now, we can compute which states meet the bound specified in this operator, i.e. + // lie in the interval that was given along with this operator, and set the corresponding bits + // to true in the resulting vector. Type lower = formula.getLowerBound(); Type upper = formula.getUpperBound(); for (uint_fast64_t i = 0; i < this->getModel().getNumberOfStates(); ++i) { if ((*probabilisticResult)[i] >= lower && (*probabilisticResult)[i] <= upper) result->set(i, true); } + // Delete the probabilities computed for the states and return result. delete probabilisticResult; - return result; } diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 29057d95a..d654bff81 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -8,11 +8,10 @@ #ifndef GMMXXDTMCPRCTLMODELCHECKER_H_ #define GMMXXDTMCPRCTLMODELCHECKER_H_ -#include "src/utility/vector.h" - #include "src/models/Dtmc.h" #include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" +#include "src/utility/vector.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -46,24 +45,23 @@ 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(); + gmm::csr_matrix* gmmxxMatrix = tmpMatrix.toGMMXXSparseMatrix(); // Create the vector with which to multiply. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); + mrmc::utility::setVectorValues(result, *rightStates, static_cast(1.0)); // Now perform matrix-vector multiplication as long as we meet the bound of the formula. for (uint_fast64_t i = 0; i < formula.getBound(); ++i) { gmm::mult(*gmmxxMatrix, *result, *result); } - // Delete intermediate results. + // Delete intermediate results and return result. delete leftStates; delete rightStates; - return result; } @@ -72,19 +70,19 @@ public: mrmc::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild()); // Transform the transition probability matrix to the gmm++ format to use its arithmetic. - gmm::csr_matrix* gmmxxMatrix = this->getModel().getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = this->getModel().getTransitionProbabilityMatrix()->toGMMXXSparseMatrix(); // Create the vector with which to multiply and initialize it correctly. std::vector x(this->getModel().getNumberOfStates()); - mrmc::utility::setVectorValues(&x, *nextStates, static_cast(1.0)); + mrmc::utility::setVectorValues(&x, *nextStates, static_cast(1.0)); - // Delete not needed next states bit vector. + // Delete obsolete sub-result. delete nextStates; // Create resulting vector. std::vector* result = new std::vector(this->getModel().getNumberOfStates()); - // Perform the actual computation. + // Perform the actual computation, namely matrix-vector multiplication. gmm::mult(*gmmxxMatrix, x, *result); // Delete temporary matrix and return result. @@ -101,9 +99,10 @@ public: // all states that have probability 0 and 1 of satisfying the until-formula. mrmc::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates()); mrmc::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates()); - mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); + mrmc::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, ¬ExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates); notExistsPhiUntilPsiStates.complement(); + // Delete sub-results that are obsolete now. delete leftStates; delete rightStates; @@ -118,13 +117,13 @@ public: // Only try to solve system if there are states for which the probability is unknown. if (maybeStates.getNumberOfSetBits() > 0) { // Now we can eliminate the rows and columns from the original transition probability matrix. - mrmc::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); - // Converting the matrix to the form needed for the equation system. That is, we go from - // x = A*x + b to (I-A)x = b. + mrmc::storage::SquareSparseMatrix* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates); + // Converting the matrix from the fixpoint notation to the form needed for the equation + // system. That is, we go from x = A*x + b to (I-A)x = b. submatrix->convertToEquationSystem(); // Transform the submatrix to the gmm++ format to use its solvers. - gmm::csr_matrix* gmmxxMatrix = submatrix->toGMMXXSparseMatrix(); + gmm::csr_matrix* gmmxxMatrix = submatrix->toGMMXXSparseMatrix(); // Initialize the x vector with 0.5 for each element. This is the initial guess for // the iterative solvers. It should be safe as for all 'maybe' states we know that the @@ -133,11 +132,13 @@ public: // Prepare the right-hand side of the equation system. For entry i this corresponds to // the accumulated probability of going from state i to some 'yes' state. - std::vector b(maybeStates.getNumberOfSetBits()); - this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x); + std::vector b(maybeStates.getNumberOfSetBits()); + this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b); + LOG4CPLUS_DEBUG(logger, "Computing preconditioner."); // Set up the precondition of the iterative solver. - gmm::ilu_precond> P(*gmmxxMatrix); + gmm::ilu_precond> P(*gmmxxMatrix); + LOG4CPLUS_DEBUG(logger, "Done computing preconditioner."); // Prepare an iteration object that determines the accuracy, maximum number of iterations // and the like. gmm::iteration iter(0.000001); @@ -145,7 +146,13 @@ public: // Now do the actual solving. LOG4CPLUS_INFO(logger, "Starting iterative solver."); gmm::bicgstab(*gmmxxMatrix, x, b, P, iter); - LOG4CPLUS_INFO(logger, "Iterative solver converged."); + + // Check if the solver converged and issue a warning otherwise. + if (iter.converged()) { + LOG4CPLUS_INFO(logger, "Iterative solver converged after " << iter.get_iteration() << " iterations."); + } else { + LOG4CPLUS_WARN(logger, "Iterative solver did not converge."); + } // Set values of resulting vector according to result. mrmc::utility::setVectorValues(result, maybeStates, x); @@ -154,8 +161,9 @@ public: delete gmmxxMatrix; } - mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, static_cast(0)); - mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, static_cast(1.0)); + // Set values of resulting vector that are known exactly. + mrmc::utility::setVectorValues(result, notExistsPhiUntilPsiStates, static_cast(0)); + mrmc::utility::setVectorValues(result, alwaysPhiUntilPsiStates, static_cast(1.0)); return result; } diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 6d777c517..179877e78 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -111,6 +111,7 @@ int main(const int argc, const char* argv[]) { dtmc.printModelInformationToStream(std::cout); // Uncomment this if you want to see the first model checking procedure in action. :) + mrmc::modelChecker::EigenDtmcPrctlModelChecker mc(dtmc); mrmc::formula::AP* trueFormula = new mrmc::formula::AP(std::string("true")); mrmc::formula::AP* ap = new mrmc::formula::AP(std::string("observe0Greater1")); @@ -126,6 +127,7 @@ int main(const int argc, const char* argv[]) { } delete until; + mrmc::modelChecker::GmmxxDtmcPrctlModelChecker mcG(dtmc); mrmc::formula::AP* trueFormulaG = new mrmc::formula::AP(std::string("true")); mrmc::formula::AP* apG = new mrmc::formula::AP(std::string("observe0Greater1")); @@ -133,6 +135,7 @@ int main(const int argc, const char* argv[]) { std::vector* gmmResult = mcG.checkPathFormula(*untilG); delete untilG; + /* if (eigenResult->size() != gmmResult->size()) { LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results (Eigen: " << eigenResult->size() << ", Gmm: " << gmmResult->size() << ") in size!"); } else { @@ -146,6 +149,7 @@ int main(const int argc, const char* argv[]) { } } } + */ /* LOG4CPLUS_INFO(logger, "Result: ");