Added option support to gmm++-based model checker. Removed junk code from mrmc.cpp.

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<gmm::csr_matrix<Type>>(*gmmxxMatrix), iter);
-				} else if (precond.compare("diagonal") == 0) {
+				} else if (precond == "diagonal") {
 					gmm::bicgstab(*gmmxxMatrix, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*gmmxxMatrix), iter);
-				} else if (precond.compare("ildlt") == 0) {
+				} else if (precond == "ildlt") {
 					gmm::bicgstab(*gmmxxMatrix, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*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<gmm::csr_matrix<Type>>(*gmmxxMatrix), s->get<unsigned>("restart"), iter);
-				} else if (precond.compare("diagonal") == 0) {
+				} else if (precond == "diagonal") {
 					gmm::gmres(*gmmxxMatrix, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*gmmxxMatrix), s->get<unsigned>("restart"), iter);
-				} else if (precond.compare("ildlt") == 0) {
+				} else if (precond == "ildlt") {
 					gmm::gmres(*gmmxxMatrix, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*gmmxxMatrix), s->get<unsigned>("restart"), iter);
-				} else if (precond.compare("none") == 0) {
+				} else if (precond == "none") {
 					gmm::gmres(*gmmxxMatrix, x, b, gmm::identity_matrix(), s->get<unsigned>("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<gmm::csr_matrix<Type>>(*gmmxxMatrix), iter);
-				} else if (precond.compare("diagonal") == 0) {
+				} else if (precond == "diagonal" == 0) {
 					gmm::qmr(*gmmxxMatrix, x, b, gmm::diagonal_precond<gmm::csr_matrix<Type>>(*gmmxxMatrix), iter);
-				} else if (precond.compare("ildlt") == 0) {
+				} else if (precond == "ildlt") {
 					gmm::qmr(*gmmxxMatrix, x, b, gmm::ildlt_precond<gmm::csr_matrix<Type>>(*gmmxxMatrix), iter);
-				} else if (precond.compare("none") == 0) {
+				} else if (precond == "none") {
 					gmm::qmr(*gmmxxMatrix, x, b, gmm::identity_matrix(), iter);
 				}
 			}

src/mrmc.cpp

@@ -76,10 +76,10 @@ int main(const int argc, const char* argv[]) {
 	try {
 		mrmc::settings::Settings::registerModule<mrmc::modelChecker::GmmxxDtmcPrctlModelChecker<double> >();
 		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<double> mc(dtmc);
-	mrmc::formula::AP<double>* trueFormula = new mrmc::formula::AP<double>(std::string("true"));
-	mrmc::formula::AP<double>* ap = new mrmc::formula::AP<double>(std::string("observe0Greater1"));
-	mrmc::formula::Until<double>* until = new mrmc::formula::Until<double>(trueFormula, ap);
-	
-	
-	try {
-		std::vector<double>* 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<double> mcG(dtmc);
-	mrmc::formula::AP<double>* trueFormulaG = new mrmc::formula::AP<double>(std::string("true"));
-	mrmc::formula::AP<double>* apG = new mrmc::formula::AP<double>(std::string("observe0Greater1"));
-	mrmc::formula::Until<double>* untilG = new mrmc::formula::Until<double>(trueFormulaG, apG);
-	std::vector<double>* 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;
 	}