From cc7b31db6249dfb8e5899fbb79de1efcffbc78e2 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 14:59:53 +0200 Subject: [PATCH] Created factory method for the creation of the Prctl model checkers --- src/storm.cpp | 35 ++++++++++++++++++++++++++++------- 1 file changed, 28 insertions(+), 7 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index 1dad607d1..f332c5329 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -141,6 +141,26 @@ void cleanUp() { // nothing here } +/*! + * 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::Mdp& mdp) { + //TODO: Add support for different libraries (read from settings) + return new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); +} + +/*! + * 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::Dtmc& dtmc) { + //TODO: Add support for different libraries (read from settings) + return new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); +} + /*! * Calls the check method of a model checker for all PRCTL formulas in a given list. * @@ -170,10 +190,11 @@ void checkMdp(std::shared_ptr> mdp) { storm::parser::PrctlFileParser fileParser; std::list*> formulaList = fileParser.parseFormulas(s->getString("prctl")); - //TODO: Add support for different model checkers (selected by settings) - storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); + storm::modelchecker::AbstractModelChecker* mc = createPrctlModelChecker(*mdp); - checkPrctlFormulasAgainstModel(formulaList, mc); + checkPrctlFormulasAgainstModel(formulaList, *mc); + + delete mc; } if(s->isSet("csl")) { @@ -188,16 +209,16 @@ void checkMdp(std::shared_ptr> mdp) { void checkDtmc(std::shared_ptr> dtmc) { dtmc->printModelInformationToStream(std::cout); storm::settings::Settings* s = storm::settings::instance(); - LOG4CPLUS_INFO(logger, "lalala"); if (s->isSet("prctl")) { LOG4CPLUS_INFO(logger, "Parsing prctl file"+ s->getString("prctl")); storm::parser::PrctlFileParser fileParser; std::list*> formulaList = fileParser.parseFormulas(s->getString("prctl")); - //TODO: Add support for different model checkers (selected by settings) - storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); + storm::modelchecker::AbstractModelChecker* mc = createPrctlModelChecker(*dtmc); + + checkPrctlFormulasAgainstModel(formulaList, *mc); - checkPrctlFormulasAgainstModel(formulaList, mc); + delete mc; } if(s->isSet("csl")) {