diff --git a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h index 264e1b27c..8d2af9f2a 100644 --- a/src/modelChecker/GmmxxDtmcPrctlModelChecker.h +++ b/src/modelChecker/GmmxxDtmcPrctlModelChecker.h @@ -150,35 +150,48 @@ public: // Now do the actual solving. LOG4CPLUS_INFO(logger, "Starting iterative solver."); const std::string& precond = s->getString("precond"); + if (precond == "ilu") { + LOG4CPLUS_INFO(logger, "Using ILU preconditioner."); + } else if (precond == "diagonal") { + LOG4CPLUS_INFO(logger, "Using diagonal preconditioner."); + } else if (precond == "ildlt") { + LOG4CPLUS_INFO(logger, "Using ILDLT preconditioner."); + } else if (precond == "none") { + LOG4CPLUS_INFO(logger, "Using no preconditioner."); + } + if (s->getString("lemethod").compare("bicgstab") == 0) { + LOG4CPLUS_INFO(logger, "Using BiCGStab method."); if (precond.compare("ilu")) { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); - } else if (precond.compare("diagonal") == 0) { + } else if (precond == "diagonal") { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); - } else if (precond.compare("ildlt") == 0) { + } else if (precond == "ildlt") { gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ildlt_precond>(*gmmxxMatrix), iter); - } else if (precond.compare("none") == 0) { + } else if (precond == "none") { 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) { + LOG4CPLUS_INFO(logger, "Using GMRES method."); if (precond.compare("ilu")) { gmm::gmres(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), s->get("restart"), iter); - } else if (precond.compare("diagonal") == 0) { + } else if (precond == "diagonal") { gmm::gmres(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), s->get("restart"), iter); - } else if (precond.compare("ildlt") == 0) { + } else if (precond == "ildlt") { gmm::gmres(*gmmxxMatrix, x, b, gmm::ildlt_precond>(*gmmxxMatrix), s->get("restart"), iter); - } else if (precond.compare("none") == 0) { + } else if (precond == "none") { gmm::gmres(*gmmxxMatrix, x, b, gmm::identity_matrix(), s->get("restart"), iter); } */ } else if (s->getString("lemethod").compare("qmr") == 0) { + LOG4CPLUS_INFO(logger, "Using QMR method."); if (precond.compare("ilu")) { gmm::qmr(*gmmxxMatrix, x, b, gmm::ilu_precond>(*gmmxxMatrix), iter); - } else if (precond.compare("diagonal") == 0) { + } else if (precond == "diagonal" == 0) { gmm::qmr(*gmmxxMatrix, x, b, gmm::diagonal_precond>(*gmmxxMatrix), iter); - } else if (precond.compare("ildlt") == 0) { + } else if (precond == "ildlt") { gmm::qmr(*gmmxxMatrix, x, b, gmm::ildlt_precond>(*gmmxxMatrix), iter); - } else if (precond.compare("none") == 0) { + } else if (precond == "none") { gmm::qmr(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter); } } diff --git a/src/mrmc.cpp b/src/mrmc.cpp index aa9767b29..7d334408c 100644 --- a/src/mrmc.cpp +++ b/src/mrmc.cpp @@ -76,10 +76,10 @@ int main(const int argc, const char* argv[]) { try { mrmc::settings::Settings::registerModule >(); s = mrmc::settings::newInstance(argc, argv, nullptr); - } catch (mrmc::exceptions::InvalidSettings e) { - LOG4CPLUS_FATAL(logger, "InvalidSettings error: " << e.what()); + } 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 << "Could not recover from settings error: " << e.what() << "." << std::endl; std::cout << std::endl << mrmc::settings::help; delete s; return 1; @@ -108,56 +108,6 @@ 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")); - mrmc::formula::Until* until = new mrmc::formula::Until(trueFormula, ap); - - - try { - 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!"); - return -1; - } - 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")); - mrmc::formula::Until* untilG = new mrmc::formula::Until(trueFormulaG, apG); - std::vector* vec = mcG.checkPathFormula(*untilG); - delete vec; - 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 { - LOG4CPLUS_INFO(logger, "Testing for different entries"); - for (unsigned int i = 0; i < eigenResult->size(); ++i) { - if (std::abs((eigenResult->at(i) - gmmResult->at(i))) > 0) { - LOG4CPLUS_ERROR(logger, "Warning: Eigen and GMM produced different results in entry " << i << " (Eigen: " << eigenResult->at(i) << ", Gmm: " << gmmResult->at(i) << ")!"); - } - if (eigenResult->at(i) != 0.0) { - LOG4CPLUS_INFO(logger, "Non zero entry " << eigenResult->at(i) << " at " << i); - } - } - } - */ - - /* - LOG4CPLUS_INFO(logger, "Result: "); - LOG4CPLUS_INFO(logger, "Entry : EigenResult at Entry : GmmResult at Entry"); - for (int i = 0; i < eigenResult->size(); ++i) { - LOG4CPLUS_INFO(logger, i << " : " << eigenResult->at(i) << " : " << gmmResult->at(i)); - }*/ - if (s != nullptr) { delete s; }