From 32a32a70134b0ae29a35ed94f8ce3730a74eea26 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 16:19:10 +0200 Subject: [PATCH] Added extended model checker factory functions. As currently only gmm++ is usable as matrix library they are not really useful, but they can be easily extended in the future. --- src/storm.cpp | 36 +++++++++++++++++++++++++----------- 1 file changed, 25 insertions(+), 11 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index f332c5329..e7f7c6323 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -142,23 +142,35 @@ void cleanUp() { } /*! - * Factory style creation of new MDP model checker - * @param mdp The Dtmc that the model checker will check + * Factory style creation of new DTMC model checker + * @param dtmc The Dtmc that the model checker will check * @return */ -storm::modelchecker::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp& mdp) { - //TODO: Add support for different libraries (read from settings) - return new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); +storm::modelchecker::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc& dtmc) { + storm::settings::Settings* s = storm::settings::instance(); + if (s->getString("matrixlib") == "gmm++") { + return new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); + } + // The control flow should never reach this point, as there is a default setting for matrixlib (gmm++) + std::string message = "No matrix library suitable for DTMC model checking has been set"; + throw storm::exceptions::InvalidSettingsException() << message; + return nullptr; } /*! - * Factory style creation of new DTMC model checker - * @param dtmc The Dtmc that the model checker will check + * Factory style creation of new MDP model checker + * @param mdp The Dtmc that the model checker will check * @return */ -storm::modelchecker::AbstractModelChecker* createPrctlModelChecker(storm::models::Dtmc& dtmc) { - //TODO: Add support for different libraries (read from settings) - return new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); +storm::modelchecker::AbstractModelChecker* createPrctlModelChecker(storm::models::Mdp& mdp) { + storm::settings::Settings* s = storm::settings::instance(); + if (s->getString("matrixlib") == "gmm++") { + return new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); + } + // The control flow should never reach this point, as there is a default setting for matrixlib (gmm++) + std::string message = "No matrix library suitable for MDP model checking has been set"; + throw storm::exceptions::InvalidSettingsException() << message; + return nullptr; } /*! @@ -233,6 +245,9 @@ void check_main() { storm::settings::Settings* s = storm::settings::instance(); storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew")); + LOG4CPLUS_DEBUG(logger, s->getString("matrixlib")); + + switch (parser.getType()) { case storm::models::DTMC: LOG4CPLUS_INFO(logger, "Model was detected as DTMC"); @@ -269,7 +284,6 @@ int main(const int argc, const char* argv[]) { } setUp(); - try { LOG4CPLUS_INFO(logger, "StoRM was invoked.");