From 3b5602b94272463298d141703fc9a1c6bfd6a1cc Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 10:24:27 +0200 Subject: [PATCH 1/8] Reduction of functionality of fileParser: Only does the parsing, no checking --- src/parser/PrctlFileParser.cpp | 54 +++++----------------------------- src/parser/PrctlFileParser.h | 44 +++++++-------------------- 2 files changed, 18 insertions(+), 80 deletions(-) diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 434adfed4..f155a11cb 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -16,69 +16,29 @@ namespace storm { namespace parser { -PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Dtmc& dtmc, enum libraries library) { - //Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker: - storm::modelchecker::SparseDtmcPrctlModelChecker* modelChecker = nullptr; - switch(library) { - //case EIGEN: - //Eigen Model Checker is not completely implemented at the moment, thus using Eigen is not possible... - //Current behaviour: Fall back to GMMXX... - //modelChecker = new storm::modelchecker::EigenDtmcPrctlModelChecker(dtmc); - // break; - case GMMXX: - default: //Note: GMMXX is default, hence default branches here, too. - modelChecker = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); - break; - } - - //Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker: - check(filename, modelChecker); - delete modelChecker; -} - -PrctlFileParser::PrctlFileParser(std::string filename, storm::models::Mdp& mdp, enum libraries library) { - //Here ,the model checker which uses the correct library is created and a reference stored in the pointer modelChecker: - storm::modelchecker::SparseMdpPrctlModelChecker* modelChecker = nullptr; - switch(library) { - //case EIGEN: - //Eigen MDP Model Checker is not implemented yet - //Current behaviour: Fall back to GMMXX... - // break; - case GMMXX: - default: //Note: GMMXX is default, hence default branches here, too. - modelChecker = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); - break; - } - - //Now, the check function (which works on abstract model checkers) can parse the formulas and invoke the model checker: - check(filename, modelChecker); - delete modelChecker; +PrctlFileParser::PrctlFileParser() { + //Intentionally left empty } PrctlFileParser::~PrctlFileParser() { //intentionally left empty } -void PrctlFileParser::check(std::string filename, storm::modelchecker::AbstractModelChecker* modelChecker) { +std::list*> parseFormulas(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); + std::list*> result; while(!inputFileStream.eof()) { std::string line; //The while loop reads the input file line by line while (std::getline(inputFileStream, line)) { PrctlParser parser(line); - storm::property::prctl::AbstractStateFormula* stateFormula = dynamic_cast*>(parser.getFormula()); - if (stateFormula != nullptr) { - modelChecker->check(*stateFormula); - } - storm::property::prctl::AbstractNoBoundOperator* noBoundFormula = dynamic_cast*>(parser.getFormula()); - if (noBoundFormula != nullptr) { - modelChecker->check(*noBoundFormula); - } - delete parser.getFormula(); + result.push_back(parser.getFormula()); } } + + return result; } } /* namespace parser */ diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h index f82b62574..ee0987cfe 100644 --- a/src/parser/PrctlFileParser.h +++ b/src/parser/PrctlFileParser.h @@ -8,10 +8,9 @@ #ifndef STORM_PARSER_PRCTLFILEPARSER_H_ #define STORM_PARSER_PRCTLFILEPARSER_H_ -#include "models/Dtmc.h" -#include "models/Mdp.h" #include "formula/Prctl.h" -#include "modelchecker/AbstractModelChecker.h" + +#include namespace storm { namespace parser { @@ -25,46 +24,25 @@ namespace parser { */ class PrctlFileParser { public: - enum libraries { - GMMXX, - EIGEN - }; - /*! - * Reads a given file of formulas and checks each of these against a given DTMC. - * - * @param filename The name of the file to parse - * @param dtmc The DTMC model to check - * @param library Specifies the library that should perform the algebraic operations during model checking (default is GMMxx) - */ - PrctlFileParser(std::string filename, storm::models::Dtmc& dtmc, enum libraries library=GMMXX); - - /*! - * Reads a given file of formulas and checks each of these against a given MDP. - * - * @param filename The name of the file to parse - * @param mdp The MDP model to check - * @param library Specifies the library that should perform the algebraic operations during model checking (default is GMMxx, which at the moment also is the only implemented version...) + * Constructor */ - PrctlFileParser(std::string filename, storm::models::Mdp& mdp, enum libraries library=GMMXX); + PrctlFileParser(); -protected: /*! - * Does the actual checking. - * This procedure is equal for all model types (only the model checker is different, so it has to be created in - * different methods beforehand) + * Destructor. + * At this time, empty * - * @param filename The name of the file to parse - * @param modelChecker The model checker that checks the formula (has to know its model!) */ - void check(std::string filename, storm::modelchecker::AbstractModelChecker* modelChecker); + virtual ~PrctlFileParser(); /*! - * Destructor. - * At this time, empty + * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing. * + * @param filename + * @return The list of parsed formulas */ - virtual ~PrctlFileParser(); + std::list*> parseFormulas(std::string filename); }; } /* namespace parser */ From 5d3b9e5cc136e5bc667595805f16b211a50a1c22 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 11:38:17 +0200 Subject: [PATCH 2/8] Basic structure for central model checking method in storm.cpp --- src/parser/PrctlFileParser.cpp | 2 +- src/storm.cpp | 50 +++++++++++++++++++++++----------- src/utility/Settings.cpp | 3 ++ 3 files changed, 38 insertions(+), 17 deletions(-) diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index f155a11cb..50f0f5502 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -24,7 +24,7 @@ PrctlFileParser::~PrctlFileParser() { //intentionally left empty } -std::list*> parseFormulas(std::string filename) { +std::list*> PrctlFileParser::parseFormulas(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); std::list*> result; diff --git a/src/storm.cpp b/src/storm.cpp index abd7c04c2..8c940c0d2 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -31,6 +31,8 @@ #include "src/utility/ErrorHandling.h" #include "src/formula/Prctl.h" +#include "src/parser/PrctlFileParser.h" + #include "log4cplus/logger.h" #include "log4cplus/loggingmacros.h" #include "log4cplus/consoleappender.h" @@ -432,6 +434,18 @@ void testCheckingConsensus(storm::models::Mdp& mdp) { delete mc; } +/*! + * Check method for DTMCs + * @param dtmc Reference to the DTMC to check + */ +void checkDtmc(std::shared_ptr> dtmc) { + dtmc->printModelInformationToStream(std::cout); +} + +void checkMdp(std::shared_ptr> mdp) { + mdp->printModelInformationToStream(std::cout); +} + /*! * Simple testing procedure. */ @@ -439,22 +453,26 @@ void testChecking() { storm::settings::Settings* s = storm::settings::instance(); storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew")); - if (parser.getType() == storm::models::DTMC) { - std::shared_ptr> dtmc = parser.getModel>(); - dtmc->printModelInformationToStream(std::cout); - - // testCheckingDie(*dtmc); - // testCheckingCrowds(*dtmc); - // testCheckingSynchronousLeader(*dtmc, 6); - } else if (parser.getType() == storm::models::MDP) { - std::shared_ptr> mdp = parser.getModel>(); - mdp->printModelInformationToStream(std::cout); - - // testCheckingDice(*mdp); - // testCheckingAsynchLeader(*mdp); - // testCheckingConsensus(*mdp); - } else { - std::cout << "Input is neither a DTMC nor an MDP." << std::endl; + 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")); + + } + + + switch (parser.getType()) { + case storm::models::DTMC: + LOG4CPLUS_INFO(logger, "Model was detected as DTMC"); + checkDtmc(parser.getModel>()); + break; + case storm::models::MDP: + LOG4CPLUS_INFO(logger, "Model was detected as MDP"); + checkMdp(parser.getModel>()); + break; + default: + LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); + break; } } diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index d6e2f5bc3..d43a7b785 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -137,6 +137,9 @@ void Settings::initDescriptions() { ("test-prctl", bpo::value(), "name of prctl file") ("trafile", bpo::value()->required(), "name of the .tra file") ("labfile", bpo::value()->required(), "name of the .lab file") + ("prctl", bpo::value()->default_value(""), "text file containing prctl formulas") + ("csl", bpo::value()->default_value(""), "text file containing csl formulas") + ("ltl", bpo::value()->default_value(""), "text file containing ltl formulas") ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") From 6fca423152669e2123249ca180856733f57d25b0 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 13:16:11 +0200 Subject: [PATCH 3/8] Marked constants as unsigned to avoid comparison of signed and unsigned values --- test/functional/GmmxxDtmcPrctModelCheckerTest.cpp | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp index de47f60a3..aa2a014fa 100644 --- a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp +++ b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp @@ -81,8 +81,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) { std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 8607); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460); + ASSERT_EQ(dtmc->getNumberOfStates(), 8607u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u); storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); @@ -135,8 +135,8 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) { std::shared_ptr> dtmc = parser.getModel>(); - ASSERT_EQ(dtmc->getNumberOfStates(), 12400); - ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894); + ASSERT_EQ(dtmc->getNumberOfStates(), 12400u); + ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u); storm::modelchecker::GmmxxDtmcPrctlModelChecker mc(*dtmc); From 065ac8f659cd5c98ab7a9c94e430411654ea5111 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 14:27:09 +0200 Subject: [PATCH 4/8] Basic command line interface for SToRM --- src/modelchecker/AbstractModelChecker.h | 14 + src/parser/PrctlFileParser.cpp | 6 + src/storm.cpp | 353 ++++-------------------- 3 files changed, 75 insertions(+), 298 deletions(-) diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index 8de8863a4..f46e1999b 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -117,6 +117,20 @@ public: } } + /*! + * Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula) + * for all initial states, i.e. states that carry the atomic proposition "init". + * + * @param formula The formula to be checked. + */ + void check(storm::property::prctl::AbstractPrctlFormula const& formula) const { + if (dynamic_cast const*>(&formula) != nullptr) { + this->check(static_cast const&>(formula)); + } else if (dynamic_cast const*>(&formula) != nullptr) { + this->check(static_cast const&>(formula)); + } + } + /*! * Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e. * states that carry the atomic proposition "init". diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp index 50f0f5502..ed5f15a2b 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -27,6 +27,12 @@ PrctlFileParser::~PrctlFileParser() { std::list*> PrctlFileParser::parseFormulas(std::string filename) { // Open file std::ifstream inputFileStream(filename, std::ios::in); + + if (!inputFileStream.is_open()) { + std::string message = "Error while opening file "; + throw storm::exceptions::FileIoException() << message << filename; + } + std::list*> result; while(!inputFileStream.eof()) { diff --git a/src/storm.cpp b/src/storm.cpp index 8c940c0d2..1dad607d1 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -141,297 +141,44 @@ void cleanUp() { // nothing here } -void testCheckingDie(storm::models::Dtmc& dtmc) { - storm::modelchecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); - - storm::property::prctl::Ap* oneFormula = new storm::property::prctl::Ap("one"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(oneFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - mc->check(*probFormula); - delete probFormula; - - oneFormula = new storm::property::prctl::Ap("two"); - eventuallyFormula = new storm::property::prctl::Eventually(oneFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - mc->check(*probFormula); - delete probFormula; - - oneFormula = new storm::property::prctl::Ap("three"); - eventuallyFormula = new storm::property::prctl::Eventually(oneFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - mc->check(*probFormula); - delete probFormula; - - storm::property::prctl::Ap* done = new storm::property::prctl::Ap("done"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(done); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); - - mc->check(*rewardFormula); - delete rewardFormula; - delete mc; -} - -void testCheckingCrowds(storm::models::Dtmc& dtmc) { - storm::property::prctl::Ap* observe0Greater1Formula = new storm::property::prctl::Ap("observe0Greater1"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(observe0Greater1Formula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - storm::modelchecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); - mc->check(*probFormula); - delete probFormula; - - storm::property::prctl::Ap* observeIGreater1Formula = new storm::property::prctl::Ap("observeIGreater1"); - eventuallyFormula = new storm::property::prctl::Eventually(observeIGreater1Formula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - mc->check(*probFormula); - delete probFormula; - - storm::property::prctl::Ap* observeOnlyTrueSenderFormula = new storm::property::prctl::Ap("observeOnlyTrueSender"); - eventuallyFormula = new storm::property::prctl::Eventually(observeOnlyTrueSenderFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - mc->check(*probFormula); - delete probFormula; - - delete mc; -} - -void testCheckingSynchronousLeader(storm::models::Dtmc& dtmc, uint_fast64_t n) { - storm::property::prctl::Ap* electedFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(electedFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula); - - storm::modelchecker::GmmxxDtmcPrctlModelChecker* mc = new storm::modelchecker::GmmxxDtmcPrctlModelChecker(dtmc); - mc->check(*probFormula); - delete probFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::BoundedUntil* boundedUntilFormula = new storm::property::prctl::BoundedUntil(new storm::property::prctl::Ap("true"), electedFormula, n * 4); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedUntilFormula); - - mc->check(*probFormula); - delete probFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(electedFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula); - - mc->check(*rewardFormula); - delete rewardFormula; - - delete mc; -} - -void testCheckingDice(storm::models::Mdp& mdp) { - storm::property::prctl::Ap* twoFormula = new storm::property::prctl::Ap("two"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - storm::modelchecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); - - mc->check(*probFormula); - delete probFormula; - - - twoFormula = new storm::property::prctl::Ap("two"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("three"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("three"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("four"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("four"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("five"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("five"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("six"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - twoFormula = new storm::property::prctl::Ap("six"); - eventuallyFormula = new storm::property::prctl::Eventually(twoFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - storm::property::prctl::Ap* doneFormula = new storm::property::prctl::Ap("done"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(doneFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - - mc->check(*rewardFormula); - delete rewardFormula; - - doneFormula = new storm::property::prctl::Ap("done"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(doneFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - mc->check(*rewardFormula); - delete rewardFormula; - - delete mc; -} - -void testCheckingAsynchLeader(storm::models::Mdp& mdp) { - storm::property::prctl::Ap* electedFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(electedFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probMinFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - storm::modelchecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); - - mc->check(*probMinFormula); - delete probMinFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - eventuallyFormula = new storm::property::prctl::Eventually(electedFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probMaxFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probMaxFormula); - delete probMaxFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(electedFormula, 25); - probMinFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); - - mc->check(*probMinFormula); - delete probMinFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(electedFormula, 25); - probMaxFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); - - mc->check(*probMaxFormula); - delete probMaxFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(electedFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - - mc->check(*rewardFormula); - delete rewardFormula; - - electedFormula = new storm::property::prctl::Ap("elected"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(electedFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); - - mc->check(*rewardFormula); - delete rewardFormula; +/*! + * Calls the check method of a model checker for all PRCTL formulas in a given list. + * + * @param formulaList The list of PRCTL formulas + * @param mc the model checker + */ +void checkPrctlFormulasAgainstModel(std::list*>& formulaList, + storm::modelchecker::AbstractModelChecker const& mc) { + for ( auto formula : formulaList ) { + mc.check(*formula); - delete mc; + //TODO: Should that be done here or in a second iteration through the list? + delete formula; + } + formulaList.clear(); } -void testCheckingConsensus(storm::models::Mdp& mdp) { - storm::property::prctl::Ap* finishedFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::Eventually* eventuallyFormula = new storm::property::prctl::Eventually(finishedFormula); - storm::property::prctl::ProbabilisticNoBoundOperator* probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - storm::modelchecker::GmmxxMdpPrctlModelChecker* mc = new storm::modelchecker::GmmxxMdpPrctlModelChecker(mdp); - - mc->check(*probFormula); - delete probFormula; - - finishedFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::Ap* allCoinsEqual0Formula = new storm::property::prctl::Ap("all_coins_equal_0"); - storm::property::prctl::And* conjunctionFormula = new storm::property::prctl::And(finishedFormula, allCoinsEqual0Formula); - eventuallyFormula = new storm::property::prctl::Eventually(conjunctionFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - finishedFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::Ap* allCoinsEqual1Formula = new storm::property::prctl::Ap("all_coins_equal_1"); - conjunctionFormula = new storm::property::prctl::And(finishedFormula, allCoinsEqual1Formula); - eventuallyFormula = new storm::property::prctl::Eventually(conjunctionFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - finishedFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::Ap* agree = new storm::property::prctl::Ap("agree"); - storm::property::prctl::Not* notAgree = new storm::property::prctl::Not(agree); - conjunctionFormula = new storm::property::prctl::And(finishedFormula, notAgree); - eventuallyFormula = new storm::property::prctl::Eventually(conjunctionFormula); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(eventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - finishedFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::BoundedEventually* boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(finishedFormula, 50); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, true); - - mc->check(*probFormula); - delete probFormula; - - finishedFormula = new storm::property::prctl::Ap("finished"); - boundedEventuallyFormula = new storm::property::prctl::BoundedEventually(finishedFormula, 50); - probFormula = new storm::property::prctl::ProbabilisticNoBoundOperator(boundedEventuallyFormula, false); - - mc->check(*probFormula); - delete probFormula; - - finishedFormula = new storm::property::prctl::Ap("finished"); - storm::property::prctl::ReachabilityReward* reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(finishedFormula); - storm::property::prctl::RewardNoBoundOperator* rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, true); - - mc->check(*rewardFormula); - delete rewardFormula; +/*! + * Check method for DTMCs + * @param dtmc Reference to the DTMC to check + */ +void checkMdp(std::shared_ptr> mdp) { + mdp->printModelInformationToStream(std::cout); + storm::settings::Settings* s = storm::settings::instance(); + 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")); - finishedFormula = new storm::property::prctl::Ap("finished"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(finishedFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + //TODO: Add support for different model checkers (selected by settings) + storm::modelchecker::GmmxxMdpPrctlModelChecker mc(*mdp); - mc->check(*rewardFormula); - delete rewardFormula; + checkPrctlFormulasAgainstModel(formulaList, mc); + } - delete mc; + if(s->isSet("csl")) { + LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); + } } /*! @@ -440,26 +187,30 @@ void testCheckingConsensus(storm::models::Mdp& mdp) { */ void checkDtmc(std::shared_ptr> dtmc) { dtmc->printModelInformationToStream(std::cout); -} - -void checkMdp(std::shared_ptr> mdp) { - mdp->printModelInformationToStream(std::cout); -} - -/*! - * Simple testing procedure. - */ -void testChecking() { storm::settings::Settings* s = storm::settings::instance(); - storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew")); - + 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); + + checkPrctlFormulasAgainstModel(formulaList, mc); + } + + if(s->isSet("csl")) { + LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); } +} +/*! + * Simple testing procedure. + */ +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")); switch (parser.getType()) { case storm::models::DTMC: @@ -470,6 +221,12 @@ void testChecking() { LOG4CPLUS_INFO(logger, "Model was detected as MDP"); checkMdp(parser.getModel>()); break; + case storm::models::CTMC: + case storm::models::CTMDP: + // Continuous time model checking is not implemented yet + LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm."); + break; + case storm::models::Unknown: default: LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); break; @@ -495,7 +252,7 @@ int main(const int argc, const char* argv[]) { try { LOG4CPLUS_INFO(logger, "StoRM was invoked."); - testChecking(); + check_main(); cleanUp(); From d4f791e80df5bd8976c53078252e8a9d4435c64e Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 14:38:25 +0200 Subject: [PATCH 5/8] Removed default values for prctl, csl and ltl settings and added test formulas for the "die" test as prctl file --- src/utility/Settings.cpp | 6 +++--- test/functional/die/testFormulas.prctl | 4 ++++ 2 files changed, 7 insertions(+), 3 deletions(-) create mode 100644 test/functional/die/testFormulas.prctl diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index d43a7b785..9a9ab1120 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -137,9 +137,9 @@ void Settings::initDescriptions() { ("test-prctl", bpo::value(), "name of prctl file") ("trafile", bpo::value()->required(), "name of the .tra file") ("labfile", bpo::value()->required(), "name of the .lab file") - ("prctl", bpo::value()->default_value(""), "text file containing prctl formulas") - ("csl", bpo::value()->default_value(""), "text file containing csl formulas") - ("ltl", bpo::value()->default_value(""), "text file containing ltl formulas") + ("prctl", bpo::value(), "text file containing prctl formulas") + ("csl", bpo::value(), "text file containing csl formulas") + ("ltl", bpo::value(), "text file containing ltl formulas") ("transrew", bpo::value()->default_value(""), "name of transition reward file") ("staterew", bpo::value()->default_value(""), "name of state reward file") ("fix-deadlocks", "insert self-loops for states without outgoing transitions") diff --git a/test/functional/die/testFormulas.prctl b/test/functional/die/testFormulas.prctl new file mode 100644 index 000000000..8deea6c43 --- /dev/null +++ b/test/functional/die/testFormulas.prctl @@ -0,0 +1,4 @@ +P=? [ F one ] +P=? [ F two ] +P=? [ F three ] +R=? [ F done ] From cc7b31db6249dfb8e5899fbb79de1efcffbc78e2 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 14:59:53 +0200 Subject: [PATCH 6/8] 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")) { From 32a32a70134b0ae29a35ed94f8ce3730a74eea26 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 16:19:10 +0200 Subject: [PATCH 7/8] 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."); From 5279466644004da8dc0562ec148beaf6b589a75a Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 16:38:21 +0200 Subject: [PATCH 8/8] - Removed "test-prctl" option - Some restructuring in storm.cpp --- src/storm.cpp | 76 +++++++++++++++++++--------------------- src/utility/Settings.cpp | 1 - 2 files changed, 36 insertions(+), 41 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index e7f7c6323..4720e7016 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -110,10 +110,6 @@ bool parseOptions(const int argc, const char* argv[]) { std::cout << storm::settings::help; return false; } - if (s->isSet("test-prctl")) { - storm::parser::PrctlParser parser(s->getString("test-prctl").c_str()); - return false; - } if (s->isSet("verbose")) { logger.getAppender("mainConsoleAppender")->setThreshold(log4cplus::INFO_LOG_LEVEL); @@ -210,7 +206,7 @@ void checkMdp(std::shared_ptr> mdp) { } if(s->isSet("csl")) { - LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); + LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on MDPs."); } } @@ -238,37 +234,6 @@ void checkDtmc(std::shared_ptr> dtmc) { } } -/*! - * Simple testing procedure. - */ -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"); - checkDtmc(parser.getModel>()); - break; - case storm::models::MDP: - LOG4CPLUS_INFO(logger, "Model was detected as MDP"); - checkMdp(parser.getModel>()); - break; - case storm::models::CTMC: - case storm::models::CTMDP: - // Continuous time model checking is not implemented yet - LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm."); - break; - case storm::models::Unknown: - default: - LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); - break; - } -} - /*! * Main entry point. */ @@ -279,15 +244,46 @@ int main(const int argc, const char* argv[]) { printHeader(argc, argv); initializeLogger(); - if (!parseOptions(argc, argv)) { - return 0; - } + setUp(); try { LOG4CPLUS_INFO(logger, "StoRM was invoked."); - check_main(); + // Parse options + if (!parseOptions(argc, argv)) { + // If false is returned, the program execution is stopped here + // E.g. if the user asked to see the help text + return 0; + } + + // Now, the settings are receivd and the model is parsed. + 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")); + + + // Depending on the model type, the respective model checking procedure is chosen. + switch (parser.getType()) { + case storm::models::DTMC: + LOG4CPLUS_INFO(logger, "Model was detected as DTMC"); + checkDtmc(parser.getModel>()); + break; + case storm::models::MDP: + LOG4CPLUS_INFO(logger, "Model was detected as MDP"); + checkMdp(parser.getModel>()); + break; + case storm::models::CTMC: + case storm::models::CTMDP: + // Continuous time model checking is not implemented yet + LOG4CPLUS_ERROR(logger, "The model type you selected is not supported in this version of storm."); + break; + case storm::models::Unknown: + default: + LOG4CPLUS_ERROR(logger, "The model type could not be determined correctly."); + break; + } cleanUp(); diff --git a/src/utility/Settings.cpp b/src/utility/Settings.cpp index 9a9ab1120..9c2688f58 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -134,7 +134,6 @@ void Settings::initDescriptions() { ("debug", "be very verbose, intended for debugging") ("logfile,l", bpo::value(), "name of the log file") ("configfile,c", bpo::value(), "name of config file") - ("test-prctl", bpo::value(), "name of prctl file") ("trafile", bpo::value()->required(), "name of the .tra file") ("labfile", bpo::value()->required(), "name of the .lab file") ("prctl", bpo::value(), "text file containing prctl formulas")