From c54283cef27ba00dc649a2e5ce76ed981bab9a12 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Dec 2012 17:58:49 +0100 Subject: [PATCH 1/9] 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: "); From a9129c00c75bef4036cccbbf0529de8594349e9f Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 13 Dec 2012 22:03:22 +0100 Subject: [PATCH 2/9] new exception Created BaseException that can act as a stringstream. You can do the following: throw BaseException() << "some error " << variable << " foo"; Changed InvalidSettings to use BaseException, using this new syntax in Settings. --- src/exceptions/BaseException.h | 40 ++++++++++++++++++++++++++++++++ src/exceptions/InvalidSettings.h | 29 ++++------------------- src/mrmc.cpp | 4 +++- src/utility/settings.cpp | 18 +++++--------- src/utility/settings.h | 2 +- 5 files changed, 55 insertions(+), 38 deletions(-) create mode 100644 src/exceptions/BaseException.h diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h new file mode 100644 index 000000000..1f61c8338 --- /dev/null +++ b/src/exceptions/BaseException.h @@ -0,0 +1,40 @@ +#ifndef BASEEXCEPTION_H_ +#define BASEEXCEPTION_H_ + +#include +#include + +namespace mrmc { +namespace exceptions { + +class BaseException : public std::exception +{ + public: + BaseException() : exception() {} + BaseException(const BaseException& cp) + : exception(cp), stream(cp.stream.str()) + { + } + + ~BaseException() throw() { } + + template + BaseException& operator<<(const T& var) + { + this->stream << var; + return *this; + } + + virtual const char* what() const throw() + { + return this->stream.str().c_str(); + } + + private: + std::stringstream stream; +}; + +} // namespace exceptions +} // namespace mrmc + +#endif // BASEEXCEPTION_H_ diff --git a/src/exceptions/InvalidSettings.h b/src/exceptions/InvalidSettings.h index 8244c6d4c..2e34a7419 100644 --- a/src/exceptions/InvalidSettings.h +++ b/src/exceptions/InvalidSettings.h @@ -1,35 +1,16 @@ -#ifndef MRMC_EXCEPTIONS_INVALID_SETTINGS_H_ -#define MRMC_EXCEPTIONS_INVALID_SETTINGS_H_ +#ifndef INVALIDSETTINGS_H_ +#define INVALIDSETTINGS_H_ -#include +#include "src/exceptions/BaseException.h" namespace mrmc { namespace exceptions { -//!This exception is thrown when a memory request can't be -//!fulfilled. -class InvalidSettings : public std::exception +class InvalidSettings : public BaseException { - public: -/* The Visual C++-Version of the exception class has constructors accepting - * a char*-constant; The GCC version does not have these - * - * As the "extended" constructor is used in the sparse matrix code, a dummy - * constructor is used under linux (which will ignore the parameter) - */ -#ifdef _WIN32 - InvalidSettings() : exception("::mrmc::InvalidSettings"){} - InvalidSettings(const char * const s): exception(s) {} -#else - InvalidSettings() : exception() {} - InvalidSettings(const char * const s): exception() {} - -#endif - virtual const char* what() const throw() - { return "mrmc::InvalidSettings"; } }; } // namespace exceptions } // namespace mrmc -#endif // MRMC_EXCEPTIONS_INVALID_SETTINGS_H_ +#endif // INVALIDSETTINGS_H_ diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 42a954cef..2b21f1cc6 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -75,8 +75,10 @@ int main(const int argc, const char* argv[]) { try { s = mrmc::settings::newInstance(argc, argv, nullptr); - } catch (mrmc::exceptions::InvalidSettings&) { + } catch (mrmc::exceptions::InvalidSettings& e) { + LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what()); LOG4CPLUS_FATAL(logger, "Could not recover from settings error, terminating."); + std::cout << "Could not recover from settings error: " << e.what() << std::endl; std::cout << std::endl << mrmc::settings::help; delete s; return 1; diff --git a/src/utility/settings.cpp b/src/utility/settings.cpp index 748bc931a..94aba1f15 100644 --- a/src/utility/settings.cpp +++ b/src/utility/settings.cpp @@ -7,6 +7,8 @@ #include "src/utility/settings.h" +#include "src/exceptions/BaseException.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" extern log4cplus::Logger logger; @@ -107,27 +109,19 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) } catch (bpo::required_option e) { - std::cerr << "Required option: " << e.what() << std::endl; - LOG4CPLUS_ERROR(logger, "Required option: " << e.what()); - throw mrmc::exceptions::InvalidSettings(); + throw mrmc::exceptions::InvalidSettings() << "Required option missing"; } catch (bpo::validation_error e) { - std::cerr << "Validation failed: " << e.what() << std::endl; - LOG4CPLUS_ERROR(logger, "Validation failed: " << e.what()); - throw mrmc::exceptions::InvalidSettings(); + throw mrmc::exceptions::InvalidSettings() << "Validation failed: " << e.what(); } catch (bpo::invalid_command_line_syntax e) { - std::cerr << "Invalid command line syntax: " << e.what() << std::endl; - LOG4CPLUS_ERROR(logger, "Invalid command line syntax: " << e.what()); - throw mrmc::exceptions::InvalidSettings(); + throw mrmc::exceptions::InvalidSettings() << e.what(); } catch (bpo::error e) { - std::cerr << e.what() << std::endl; - LOG4CPLUS_ERROR(logger, "Unknown error: " << e.what()); - throw mrmc::exceptions::InvalidSettings(); + throw mrmc::exceptions::InvalidSettings() << e.what(); } } diff --git a/src/utility/settings.h b/src/utility/settings.h index 842074655..0d634697f 100644 --- a/src/utility/settings.h +++ b/src/utility/settings.h @@ -52,7 +52,7 @@ namespace settings { */ template const T& get(const std::string &name) const { - if (this->vm.count(name) == 0) throw mrmc::exceptions::InvalidSettings(); + if (this->vm.count(name) == 0) throw mrmc::exceptions::InvalidSettings() << "Could not read option " << name << "."; return this->vm[name].as(); } From cc1441ce26860159d2b4e9ce4859d6584bc12f37 Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 13 Dec 2012 22:21:13 +0100 Subject: [PATCH 3/9] fixed wrong return type of operator<<() for BaseException. Templates FTW! --- src/exceptions/BaseException.h | 5 +++-- src/exceptions/InvalidSettings.h | 2 +- src/mrmc.cpp | 2 +- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/exceptions/BaseException.h b/src/exceptions/BaseException.h index 1f61c8338..cfba4218e 100644 --- a/src/exceptions/BaseException.h +++ b/src/exceptions/BaseException.h @@ -7,6 +7,7 @@ namespace mrmc { namespace exceptions { +template class BaseException : public std::exception { public: @@ -19,10 +20,10 @@ class BaseException : public std::exception ~BaseException() throw() { } template - BaseException& operator<<(const T& var) + E& operator<<(const T& var) { this->stream << var; - return *this; + return * dynamic_cast(this); } virtual const char* what() const throw() diff --git a/src/exceptions/InvalidSettings.h b/src/exceptions/InvalidSettings.h index 2e34a7419..0ac7b14b8 100644 --- a/src/exceptions/InvalidSettings.h +++ b/src/exceptions/InvalidSettings.h @@ -6,7 +6,7 @@ namespace mrmc { namespace exceptions { -class InvalidSettings : public BaseException +class InvalidSettings : public BaseException { }; diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 2b21f1cc6..757fc44d9 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -75,7 +75,7 @@ int main(const int argc, const char* argv[]) { try { s = mrmc::settings::newInstance(argc, argv, nullptr); - } catch (mrmc::exceptions::InvalidSettings& e) { + } catch (mrmc::exceptions::InvalidSettings e) { LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what()); LOG4CPLUS_FATAL(logger, "Could not recover from settings error, terminating."); std::cout << "Could not recover from settings error: " << e.what() << std::endl; From 2a6228af718c6e8a03feec0cb9f743173483b395 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Dec 2012 22:25:23 +0100 Subject: [PATCH 4/9] Added some options to Gmmxx-Modelchecker. DO NOT PULL FOR THE TIME BEING AS THERE IS A PROBLEM WITH THE OPTIONS. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 50 +++++++++++++++++++ src/mrmc.cpp | 3 +- 2 files changed, 52 insertions(+), 1 deletion(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index d654bff81..ff332b566 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -13,6 +13,9 @@ #include "src/solver/GraphAnalyzer.h" #include "src/utility/vector.h" +#include "src/exceptions/InvalidSettings.h" +#include + #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -167,6 +170,53 @@ public: return result; } + + /*! + * Returns the name of this module. + * @return The name of this module. + */ + static std::string getModuleName() { + return "gmm++"; + } + + /*! + * Returns a trigger such that if the option "matrixlib" is set to "gmm++", this model checker + * is to be used. + * @return An option trigger for this module. + */ + static std::pair getOptionTrigger() { + return std::pair("matrixlib", "gmm++"); + } + + /*! + * Registers all options associated with the gmm++ matrix library. + */ + static void putOptions(boost::program_options::options_description* desc) { + desc->add_options()("lemethod", boost::program_options::value()->default_value("bicgstab")->notifier(&validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, gmres, qmr}."); + desc->add_options()("lemethod", boost::program_options::value()->default_value(10000), "Sets the maximal number of iterations used for linear equation solving."); + desc->add_options()("precond", boost::program_options::value()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioner used for linear equation solving. Must be in {ilu, diagonal, ildlt}."); + desc->add_options()("restart", boost::program_options::value()->default_value(40), "Sets the number of iterations after which gmres is restarted."); + } + + /*! + * Validates whether the given lemethod matches one of the available ones. + * Throws an exception of type InvalidSettings in case the selected method is illegal. + */ + static void validateLeMethod(const std::string& lemethod) { + if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0 && lemethod.compare("gmres") != 0) { + throw exceptions::InvalidSettings(); + } + } + + /*! + * Validates whether the given preconditioner matches one of the available ones. + * Throws an exception of type InvalidSettings in case the selected preconditioner is illegal. + */ + static void validatePreconditioner(const std::string& preconditioner) { + if (preconditioner.compare("ilu") != 0 && preconditioner.compare("diagonal") != 0 && preconditioner.compare("ildlt") != 0) { + throw exceptions::InvalidSettings(); + } + } }; } //namespace modelChecker diff --git a/src/mrmc.cpp b/src/mrmc.cpp index 6f2caed40..063d2643c 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -62,7 +62,7 @@ void setUpConsoleLogging() { int main(const int argc, const char* argv[]) { setUpFileLogging(); - mrmc::settings::Settings* s = NULL; + mrmc::settings::Settings* s = nullptr; LOG4CPLUS_INFO(logger, "This is the Markov Reward Model Checker (MRMC) by i2 of RWTH Aachen University."); @@ -74,6 +74,7 @@ int main(const int argc, const char* argv[]) { LOG4CPLUS_INFO(logger, "MRMC command invoked " << commandStream.str()); try { + mrmc::settings::Settings::registerModule >(); s = mrmc::settings::newInstance(argc, argv, nullptr); } catch (mrmc::exceptions::InvalidSettings& e) { LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what()); From 331d3c7a1157bdeb9ee9a7c7482801ea21e3f7dd Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 13 Dec 2012 22:34:36 +0100 Subject: [PATCH 5/9] fixing invalid read iterators just don't survive an erase... --- src/utility/settings.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/utility/settings.cpp b/src/utility/settings.cpp index 94aba1f15..525f9a02f 100644 --- a/src/utility/settings.cpp +++ b/src/utility/settings.cpp @@ -74,6 +74,8 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) // Perform first parse run this->firstRun(argc, argv, filename); + // Buffer for items to be deleted + std::list< std::pair< std::string, std::string > > deleteQueue; // Check module triggers for (auto it : Settings::modules) { @@ -83,11 +85,12 @@ Settings::Settings(const int argc, const char* argv[], const char* filename) if (this->vm[trigger.first].as().compare(trigger.second) == 0) { Settings::desc->add(*it.second); - Settings::modules.erase(trigger); + deleteQueue.push_back(trigger); } } - } + for (auto it : deleteQueue) Settings::modules.erase(it); + // Stop if help is set if (this->vm.count("help") > 0) From e802942be2ed4940e7a8c8dc3edc5108fde4b80c Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 13 Dec 2012 23:09:04 +0100 Subject: [PATCH 6/9] fixing memory leaks. only log4cplus left... --- src/modelChecker/EigenDtmcPrctlModelChecker.h | 1 + src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 1 + src/mrmc.cpp | 8 +++++--- src/utility/settings.cpp | 2 +- src/utility/settings.h | 6 +++--- 5 files changed, 11 insertions(+), 7 deletions(-) diff --git a/src/modelChecker/EigenDtmcPrctlModelChecker.h b/src/modelChecker/EigenDtmcPrctlModelChecker.h index 7be98d772..4730ab9cc 100644 --- a/src/modelChecker/EigenDtmcPrctlModelChecker.h +++ b/src/modelChecker/EigenDtmcPrctlModelChecker.h @@ -157,6 +157,7 @@ public: // Transform the submatric matrix to the eigen format to use its solvers Eigen::SparseMatrix* eigenSubMatrix = submatrix->toEigenSparseMatrix(); + delete submatrix; // 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 diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index ff332b566..f98c169da 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -127,6 +127,7 @@ public: // Transform the submatrix to the gmm++ format to use its solvers. gmm::csr_matrix* gmmxxMatrix = submatrix->toGMMXXSparseMatrix(); + delete submatrix; // 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 diff --git a/src/mrmc.cpp b/src/mrmc.cpp index d01191f00..aa9767b29 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -115,9 +115,10 @@ int main(const int argc, const char* argv[]) { mrmc::formula::AP* ap = new mrmc::formula::AP(std::string("observe0Greater1")); mrmc::formula::Until* until = new mrmc::formula::Until(trueFormula, ap); - std::vector* eigenResult = NULL; + try { - eigenResult = mc.checkPathFormula(*until); + std::vector* eigenResult = mc.checkPathFormula(*until); + delete eigenResult; } catch (mrmc::exceptions::NoConvergence& nce) { // solver did not converge LOG4CPLUS_ERROR(logger, "EigenDtmcPrctlModelChecker did not converge with " << nce.getIterationCount() << " of max. " << nce.getMaxIterationCount() << "Iterations!"); @@ -130,7 +131,8 @@ int main(const int argc, const char* argv[]) { mrmc::formula::AP* trueFormulaG = new mrmc::formula::AP(std::string("true")); mrmc::formula::AP* apG = new mrmc::formula::AP(std::string("observe0Greater1")); mrmc::formula::Until* untilG = new mrmc::formula::Until(trueFormulaG, apG); - std::vector* gmmResult = mcG.checkPathFormula(*untilG); + std::vector* vec = mcG.checkPathFormula(*untilG); + delete vec; delete untilG; /* diff --git a/src/utility/settings.cpp b/src/utility/settings.cpp index 525f9a02f..1a03cc98d 100644 --- a/src/utility/settings.cpp +++ b/src/utility/settings.cpp @@ -27,7 +27,7 @@ std::unique_ptr mrmc::settings::Settings::desc = nullp std::string mrmc::settings::Settings::binaryName = ""; mrmc::settings::Settings* mrmc::settings::Settings::inst = nullptr; -std::map< std::pair, bpo::options_description* > mrmc::settings::Settings::modules; +std::map< std::pair, std::shared_ptr > mrmc::settings::Settings::modules; /*! * The constructor fills the option descriptions, parses the diff --git a/src/utility/settings.h b/src/utility/settings.h index 0d634697f..d7387392d 100644 --- a/src/utility/settings.h +++ b/src/utility/settings.h @@ -113,9 +113,9 @@ namespace settings { // build description name std::stringstream str; str << T::getModuleName() << " (" << trigger.first << " = " << trigger.second << ")"; - bpo::options_description* desc = new bpo::options_description(str.str()); + std::shared_ptr desc = std::shared_ptr(new bpo::options_description(str.str())); // but options - T::putOptions(desc); + T::putOptions(desc.get()); // store Settings::modules[ trigger ] = desc; } @@ -159,7 +159,7 @@ namespace settings { /*! * @brief Contains option descriptions for all modules. */ - static std::map< std::pair< std::string, std::string >, bpo::options_description* > modules; + static std::map< std::pair< std::string, std::string >, std::shared_ptr > modules; /*! * @brief option mapping. From d965595fbe79477849a7bcf9e87e24e4cb75d8d3 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Dec 2012 23:29:25 +0100 Subject: [PATCH 7/9] Evaluated given options in gmm++-based model checker. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 64 ++++++++++++++----- 1 file changed, 48 insertions(+), 16 deletions(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index f98c169da..25e87432a 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -8,13 +8,14 @@ #ifndef GMMXXDTMCPRCTLMODELCHECKER_H_ #define GMMXXDTMCPRCTLMODELCHECKER_H_ +#include + #include "src/models/Dtmc.h" #include "src/modelChecker/DtmcPrctlModelChecker.h" #include "src/solver/GraphAnalyzer.h" #include "src/utility/vector.h" -#include "src/exceptions/InvalidSettings.h" -#include +#include "src/utility/settings.h" #include "gmm/gmm_matrix.h" #include "gmm/gmm_iter_solvers.h" @@ -139,17 +140,48 @@ public: 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); - LOG4CPLUS_DEBUG(logger, "Done computing preconditioner."); + // Get the settings object to customize linear solving. + mrmc::settings::Settings* s = mrmc::settings::instance(); + // Prepare an iteration object that determines the accuracy, maximum number of iterations // and the like. - gmm::iteration iter(0.000001); + gmm::iteration iter(s->get("precision"), 0, s->get("lemaxiter")); // Now do the actual solving. LOG4CPLUS_INFO(logger, "Starting iterative solver."); - gmm::bicgstab(*gmmxxMatrix, x, b, P, iter); + const std::string& precond = s->getString("precond"); + if (s->getString("lemethod").compare("bicgstab") == 0) { + if (precond.compare("ilu")) { + gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); + } else if (precond.compare("diagonal") == 0) { + gmm::bicgstab(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); + } else if (precond.compare("ildlt") == 0) { + gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ildlt_precond>(*gmmxxMatrix), iter); + } else if (precond.compare("none") == 0) { + gmm::bicgstab(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); + } + // FIXME: gmres has been disabled, because it triggers gmm++ compilation errors + /* } else if (s->getString("lemethod").compare("gmres") == 0) { + if (precond.compare("ilu")) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), s->get("restart"), iter); + } else if (precond.compare("diagonal") == 0) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), s->get("restart"), iter); + } else if (precond.compare("ildlt") == 0) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::ildlt_precond>(*gmmxxMatrix), s->get("restart"), iter); + } else if (precond.compare("none") == 0) { + gmm::gmres(*gmmxxMatrix, x, b, gmm::identity_matrix(), s->get("restart"), iter); + } */ + } else if (s->getString("lemethod").compare("qmr") == 0) { + if (precond.compare("ilu")) { + gmm::qmr(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); + } else if (precond.compare("diagonal") == 0) { + gmm::qmr(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); + } else if (precond.compare("ildlt") == 0) { + gmm::qmr(*gmmxxMatrix, x, b, gmm::ildlt_precond>(*gmmxxMatrix), iter); + } else if (precond.compare("none") == 0) { + gmm::qmr(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); + } + } // Check if the solver converged and issue a warning otherwise. if (iter.converged()) { @@ -193,10 +225,10 @@ public: * Registers all options associated with the gmm++ matrix library. */ static void putOptions(boost::program_options::options_description* desc) { - desc->add_options()("lemethod", boost::program_options::value()->default_value("bicgstab")->notifier(&validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, gmres, qmr}."); - desc->add_options()("lemethod", boost::program_options::value()->default_value(10000), "Sets the maximal number of iterations used for linear equation solving."); - desc->add_options()("precond", boost::program_options::value()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioner used for linear equation solving. Must be in {ilu, diagonal, ildlt}."); - desc->add_options()("restart", boost::program_options::value()->default_value(40), "Sets the number of iterations after which gmres is restarted."); + desc->add_options()("lemethod", boost::program_options::value()->default_value("bicgstab")->notifier(&validateLeMethod), "Sets the method used for linear equation solving. Must be in {bicgstab, qmr}."); + desc->add_options()("lemaxiter", boost::program_options::value()->default_value(10000), "Sets the maximal number of iterations for iterative linear equation solving."); + desc->add_options()("precision", boost::program_options::value()->default_value(10e-6), "Sets the precision for iterative linear equation solving."); + desc->add_options()("precond", boost::program_options::value()->default_value("ilu")->notifier(&validatePreconditioner), "Sets the preconditioning technique for linear equation solving. Must be in {ilu, diagonal, ildlt, none}."); } /*! @@ -204,8 +236,8 @@ public: * Throws an exception of type InvalidSettings in case the selected method is illegal. */ static void validateLeMethod(const std::string& lemethod) { - if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0 && lemethod.compare("gmres") != 0) { - throw exceptions::InvalidSettings(); + if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0 != 0) { + throw exceptions::InvalidSettings() << "Argument " << lemethod << " for option 'lemethod' is invalid."; } } @@ -214,8 +246,8 @@ public: * Throws an exception of type InvalidSettings in case the selected preconditioner is illegal. */ static void validatePreconditioner(const std::string& preconditioner) { - if (preconditioner.compare("ilu") != 0 && preconditioner.compare("diagonal") != 0 && preconditioner.compare("ildlt") != 0) { - throw exceptions::InvalidSettings(); + if (preconditioner.compare("ilu") != 0 && preconditioner.compare("diagonal") != 0 && preconditioner.compare("ildlt") && preconditioner.compare("none") != 0) { + throw exceptions::InvalidSettings() << "Argument " << preconditioner << " for option 'precond' is invalid."; } } }; From b9d1eb28f1817b38854f101866fa1348cf4dc3bd Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 13 Dec 2012 23:38:14 +0100 Subject: [PATCH 8/9] Removed superfluous operator. --- src/modelChecker/GmmxxDtmcPrctlModelChecker.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 25e87432a..264e1b27c 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -236,7 +236,7 @@ public: * Throws an exception of type InvalidSettings in case the selected method is illegal. */ static void validateLeMethod(const std::string& lemethod) { - if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0 != 0) { + if (lemethod.compare("bicgstab") != 0 && lemethod.compare("qmr") != 0) { throw exceptions::InvalidSettings() << "Argument " << lemethod << " for option 'lemethod' is invalid."; } } From 25ee8f906ad3bd057724223f19220340455bd250 Mon Sep 17 00:00:00 2001 From: gereon Date: Thu, 13 Dec 2012 23:47:45 +0100 Subject: [PATCH 9/9] added a few words about the current state of the PRCTLParser --- src/parser/readPrctlFile.cpp | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) diff --git a/src/parser/readPrctlFile.cpp b/src/parser/readPrctlFile.cpp index e51890d3e..973132a55 100644 --- a/src/parser/readPrctlFile.cpp +++ b/src/parser/readPrctlFile.cpp @@ -89,6 +89,33 @@ namespace ws = *( space ); value %= ( double_ | int_ ); // double_ must be *before* int_ type = string("int") | string("double"); + + /* + * Todo: + * Use two arguments at one point in the code, e.g. do something like + * this->variables[ variable ] = value + * + * You can have local variables in rules, but somehow does not work. + * You can also (somehow) let a rule return some arbitrary class and let boost magically collect the arguments for the constructor. + * No idea how this can possibly work, did not get this to work. + * You can also generate a syntax tree and do this manually (-> utree)... somehow. + * + * Attention: spirit had some major upgrades in the last few releases. 1.48 already lacks some features that might be useful. + * + * The rules parse the const definitions of + * http://www.prismmodelchecker.org/manual/PropertySpecification/PropertiesFiles + * We actually do not need them, but the problems I described above are fairly generic. + * We will not be able to parse the formulas if we don't solve them... + * + * Example input: + * const int k = 7; + * const double T = 9; + * const double p = 0.01; + * + * Parser can be run via ./mrmc --test-prctl foo bar + * foo and bar are necessary, otherwise the option parser fails... + */ + varDef = string("const") >> ws >> type >> ws >>