From 065ac8f659cd5c98ab7a9c94e430411654ea5111 Mon Sep 17 00:00:00 2001 From: Lanchid Date: Tue, 7 May 2013 14:27:09 +0200 Subject: [PATCH] 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();