From a98310a7236d6044f5443b4bb7320e6554148df4 Mon Sep 17 00:00:00 2001 From: masawei Date: Sat, 26 Oct 2013 17:02:27 +0200 Subject: [PATCH] Some code revisions. Former-commit-id: 639afbe825f778048db24cf9c7b8c3cb80d8432d --- src/storm.cpp | 93 +++++++++++++++++++++++------------- src/utility/StormOptions.cpp | 2 +- 2 files changed, 62 insertions(+), 33 deletions(-) diff --git a/src/storm.cpp b/src/storm.cpp index d0c4289ab..9c2e33177 100644 --- a/src/storm.cpp +++ b/src/storm.cpp @@ -1,3 +1,4 @@ + /* * STORM - a C++ Rebuild of MRMC * @@ -288,6 +289,63 @@ bool checkForCounterExampleGeneration(storm::property::prctl::AbstractPrctlFormu } } +/*! + * Handles the counterexample generation control. + */ + void generateCounterExample(storm::parser::AutoParser parser) { + //Differentiate between model types. + if(parser.getType() != storm::models::DTMC) { + LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); + return; + } + + storm::models::Dtmc model = *parser.getModel>(); + LOG4CPLUS_INFO(logger, "Model is a DTMC."); + + // Test for and get PRCTL formulas. + storm::settings::Settings* s = storm::settings::Settings::getInstance(); + + if (!s->isSet("prctl")) { + LOG4CPLUS_ERROR(logger, "No PRCTL formula file specified."); + return; + } + + // Get specified PRCTL formulas. + std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); + LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); + std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); + + // Test for each formula if a counterexample can be generated for it. + for (auto formula : formulaList) { + + // First check if it is a formula type for which a counterexample can be generated. + if (dynamic_cast const*>(formula) == nullptr) { + LOG4CPLUS_ERROR(logger, "Unexpected kind of formula. Expected a state formula."); + delete formula; + continue; + } + + storm::property::prctl::AbstractStateFormula const& stateForm = static_cast const&>(*formula); + + // Now check if the model does not satisfy the formula. + // That is if there is at least one initial state of the model that does not. + storm::storage::BitVector result = stateForm.check(*createPrctlModelChecker(model)); + if((result & model.getInitialStates()).getNumberOfSetBits() == model.getInitialStates().getNumberOfSetBits()) { + LOG4CPLUS_ERROR(logger, "Formula is satisfied. Can not generate counterexample."); + delete formula; + continue; + } + + //Generate counterexample + storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), stateForm); + + //Output counterexample + //TODO: Write output. + + delete formula; + } + } + /*! * Main entry point. */ @@ -329,39 +387,10 @@ int main(const int argc, const char* argv[]) { storm::parser::AutoParser parser(chosenTransitionSystemFile, chosenLabelingFile, chosenStateRewardsFile, chosenTransitionRewardsFile); //Should there be a counterexample generated in case the formula is not satisfied? - if(s->isSet("subSys")) { + if(s->isSet("counterExample")) { - //Differentiate between model types. - if(parser.getType() == storm::models::DTMC) { - LOG4CPLUS_INFO(logger, "Model is a DTMC."); - - if (s->isSet("prctl")) { - // Get specified PRCTL formulas. - std::string const chosenPrctlFile = s->getOptionByLongName("prctl").getArgument(0).getValueAsString(); - LOG4CPLUS_INFO(logger, "Parsing prctl file: " << chosenPrctlFile << "."); - std::list*> formulaList = storm::parser::PrctlFileParser(chosenPrctlFile); - - // Test for each formula if a counterexample can be generated for it. - for (auto formula : formulaList) { - if(checkForCounterExampleGeneration(*formula, *parser.getModel>())) { - //Generate counterexample - storm::counterexamples::PathBasedSubsystemGenerator::computeCriticalSubsystem(*parser.getModel>(), static_cast const&>(*formula)); - - //Output counterexample - //TODO: Write output. - - } else { - LOG4CPLUS_INFO(logger, "No counterexample generated for PRCTL formula: " << formula->toString()); - } - - delete formula; - } - } else { - LOG4CPLUS_ERROR(logger, "No PRCTL formula specified."); - } - } else { - LOG4CPLUS_ERROR(logger, "Counterexample generation for the selected model type is not supported."); - } + generateCounterExample(parser); + } else { // Determine which engine is to be used to choose the right model checker. LOG4CPLUS_DEBUG(logger, s->getOptionByLongName("matrixLibrary").getArgument(0).getValueAsString()); diff --git a/src/utility/StormOptions.cpp b/src/utility/StormOptions.cpp index 7eec103f5..35d9215c2 100644 --- a/src/utility/StormOptions.cpp +++ b/src/utility/StormOptions.cpp @@ -12,7 +12,7 @@ bool storm::utility::StormOptions::optionsRegistered = storm::settings::Settings settings->addOption(storm::settings::OptionBuilder("StoRM Main", "prctl", "", "Evaluates the PRCTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("prctlFileName", "The path and name of the File to read PRCTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "csl", "", "Evaluates the CSL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("cslFileName", "The path and name of the File to read CSL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "ltl", "", "Evaluates the LTL Formulas given in the File").addArgument(storm::settings::ArgumentBuilder::createStringArgument("ltlFileName", "The path and name of the File to read LTL Formulas from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); - settings->addOption(storm::settings::OptionBuilder("StoRM Main", "subSys", "", "Generate subsystem as counterexample if given formula is not satisfied").build()); + settings->addOption(storm::settings::OptionBuilder("StoRM Main", "counterExample", "", "Generate a counterexample if given formula is not satisfied").build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "transitionRewards", "", "If specified, the model will have these transition rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("transitionRewardsFileName", "The path and name of the File to read the Transition Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "stateRewards", "", "If specified, the model will have these state rewards").addArgument(storm::settings::ArgumentBuilder::createStringArgument("stateRewardsFileName", "The path and name of the File to read the State Rewards from").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()).build()); settings->addOption(storm::settings::OptionBuilder("StoRM Main", "fixDeadlocks", "", "Insert Self-Loops for States with no outgoing transitions").build());