diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h index ddba05ee7..2de2bfb28 100644 --- a/src/modelchecker/AbstractModelChecker.h +++ b/src/modelchecker/AbstractModelChecker.h @@ -116,6 +116,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 434adfed4..ed5f15a2b 100644 --- a/src/parser/PrctlFileParser.cpp +++ b/src/parser/PrctlFileParser.cpp @@ -16,69 +16,35 @@ 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*> 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()) { 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 */ diff --git a/src/storm.cpp b/src/storm.cpp index 19878d0a3..f02783319 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" @@ -108,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); @@ -139,322 +137,100 @@ 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; +/*! + * 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) { + 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; } -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; +/*! + * 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) { + 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; } -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; +/*! + * 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 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); +/*! + * 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")); - mc->check(*rewardFormula); - delete rewardFormula; + storm::modelchecker::AbstractModelChecker* mc = createPrctlModelChecker(*mdp); - electedFormula = new storm::property::prctl::Ap("elected"); - reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward(electedFormula); - rewardFormula = new storm::property::prctl::RewardNoBoundOperator(reachabilityRewardFormula, false); + checkPrctlFormulasAgainstModel(formulaList, *mc); - mc->check(*rewardFormula); - delete rewardFormula; + delete mc; + } - delete mc; + if(s->isSet("csl")) { + LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on MDPs."); + } } -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 checkDtmc(std::shared_ptr> dtmc) { + dtmc->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); + storm::modelchecker::AbstractModelChecker* mc = createPrctlModelChecker(*dtmc); - mc->check(*rewardFormula); - delete rewardFormula; + checkPrctlFormulasAgainstModel(formulaList, *mc); - delete mc; -} + delete mc; + } -/*! - * 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")); - - 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("csl")) { + LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs."); } } @@ -468,16 +244,46 @@ int main(const int argc, const char* argv[]) { printHeader(argc, argv); initializeLogger(); - if (!parseOptions(argc, argv)) { - return 0; - } - setUp(); + setUp(); try { LOG4CPLUS_INFO(logger, "StoRM was invoked."); - testChecking(); + // 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 d6e2f5bc3..9c2688f58 100644 --- a/src/utility/Settings.cpp +++ b/src/utility/Settings.cpp @@ -134,9 +134,11 @@ 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") + ("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/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); 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 ]