From 96086cb6d83f45dbc1dbfeaedcab9a992e4befe9 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 29 Sep 2014 18:54:48 +0200 Subject: [PATCH] Fixed a bug in the option system and MILP-based cex generator. Now everything should work for the demo. :) Former-commit-id: 3676ec70230357d9fcd892939ad65dd14fe3eaf0 --- .../MILPMinimalLabelSetGenerator.h | 41 ++++++++++--------- .../SMTMinimalCommandSetGenerator.h | 2 +- src/settings/ArgumentBase.cpp | 6 +++ src/settings/SettingsManager.cpp | 3 +- .../CounterexampleGeneratorSettings.cpp | 4 -- .../modules/CounterexampleGeneratorSettings.h | 8 ---- 6 files changed, 30 insertions(+), 34 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 20656b828..f3ea782dd 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -156,7 +156,6 @@ namespace storm { // Finally, determine the set of labels that are known to be taken. result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, result.allRelevantLabels); - std::cout << "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels." << std::endl; LOG4CPLUS_DEBUG(logger, "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels."); return result; @@ -948,7 +947,7 @@ namespace storm { if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; } - std::cout << "Maximal reachability in model determined to be " << maximalReachabilityProbability << "." << std::endl; + std::cout << std::endl << "Maximal reachability in model is " << maximalReachabilityProbability << "." << std::endl << std::endl; } // (2) Identify relevant and problematic states. @@ -987,19 +986,21 @@ namespace storm { * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested * formula can be either an unbounded until formula or an eventually formula. */ - static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr> const & formulaPtr) { - std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl; + static void computeCounterexample(storm::prism::Program const& program, storm::models::Mdp const& labeledMdp, std::shared_ptr> const& formula) { + std::cout << std::endl << "Generating minimal label counterexample for formula " << formula->toString() << std::endl; // First, we need to check whether the current formula is an Until-Formula. - auto probBoundFormula = std::dynamic_pointer_cast>(formulaPtr); - if (probBoundFormula == nullptr) { + std::shared_ptr> probBoundFormula = std::dynamic_pointer_cast>(formula); + if (probBoundFormula.get() == nullptr) { LOG4CPLUS_ERROR(logger, "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal formula " << probBoundFormula->toString() << " for counterexample generation."; } + + // Check whether we were given an upper bound, because counterexample generation is limited to this case. if (probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS && probBoundFormula->getComparisonOperator() != storm::properties::ComparisonType::LESS_EQUAL) { LOG4CPLUS_ERROR(logger, "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."); throw storm::exceptions::InvalidPropertyException() << "Illegal comparison operator in formula " << probBoundFormula->toString() << ". Only upper bounds are supported for counterexample generation."; } - bool strictBound = !(probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS); + bool strictBound = probBoundFormula->getComparisonOperator() == storm::properties::ComparisonType::LESS; // Now derive the probability threshold we need to exceed as well as the phi and psi states. Simultaneously, check whether the formula is of a valid shape. double bound = probBoundFormula->getBound(); @@ -1007,22 +1008,22 @@ namespace storm { storm::storage::BitVector phiStates; storm::storage::BitVector psiStates; storm::modelchecker::prctl::SparseMdpPrctlModelChecker modelchecker(labeledMdp); - try { - auto untilFormula = std::dynamic_pointer_cast>(pathFormula); - + + std::shared_ptr> untilFormula = std::dynamic_pointer_cast>(pathFormula); + if(untilFormula.get() != nullptr) { phiStates = untilFormula->getLeft()->check(modelchecker); psiStates = untilFormula->getRight()->check(modelchecker); - } catch (std::bad_cast const&) { + + } if (std::dynamic_pointer_cast>(pathFormula).get() != nullptr) { // If the nested formula was not an until formula, it remains to check whether it's an eventually formula. - try { - auto eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); - - phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); - psiStates = eventuallyFormula->getChild()->check(modelchecker); - } catch (std::bad_cast const&) { - // If the nested formula is neither an until nor a finally formula, we throw an exception. - throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."; - } + std::shared_ptr> eventuallyFormula = std::dynamic_pointer_cast>(pathFormula); + + phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true); + psiStates = eventuallyFormula->getChild()->check(modelchecker); + + } else { + // If the nested formula is neither an until nor a finally formula, we throw an exception. + throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation."; } // Delegate the actual computation work to the function of equal name. diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index c961f6fe1..2fe722951 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -1660,7 +1660,7 @@ namespace storm { if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { throw storm::exceptions::InvalidArgumentException() << "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."; } - std::cout << "Maximal reachability in model determined to be " << maximalReachabilityProbability << "." << std::endl; + std::cout << std::endl << "Maximal reachability in model determined is " << maximalReachabilityProbability << "." << std::endl; } // (2) Identify all states and commands that are relevant, because only these need to be considered later. diff --git a/src/settings/ArgumentBase.cpp b/src/settings/ArgumentBase.cpp index 79c1b574b..93b3169e6 100644 --- a/src/settings/ArgumentBase.cpp +++ b/src/settings/ArgumentBase.cpp @@ -30,6 +30,12 @@ namespace storm { return t; } + template <> + std::string ArgumentBase::convertFromString(std::string const& valueAsString, bool& conversionSuccessful) { + conversionSuccessful = true; + return valueAsString; + } + template <> bool ArgumentBase::convertFromString(std::string const& s, bool& ok) { static const std::string lowerTrueString = "true"; diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp index de54de36d..d8b9284d9 100644 --- a/src/settings/SettingsManager.cpp +++ b/src/settings/SettingsManager.cpp @@ -302,7 +302,8 @@ namespace storm { // Now set the provided argument values one by one. for (uint_fast64_t i = 0; i < argumentCache.size(); ++i) { ArgumentBase& argument = option->getArgument(i); - argument.setFromStringValue(argumentCache[i]); + bool conversionOk = argument.setFromStringValue(argumentCache[i]); + STORM_LOG_THROW(conversionOk, storm::exceptions::OptionParserException, "Conversion of value of argument '" << argument.getName() << "' to its type failed."); } // In case there are optional arguments that were not set, we set them to their default value. diff --git a/src/settings/modules/CounterexampleGeneratorSettings.cpp b/src/settings/modules/CounterexampleGeneratorSettings.cpp index 17196a4bd..e2e29834d 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/settings/modules/CounterexampleGeneratorSettings.cpp @@ -14,7 +14,6 @@ namespace storm { CounterexampleGeneratorSettings::CounterexampleGeneratorSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) { std::vector techniques = {"maxsat", "milp"}; this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command set. Note that this requires the model to be given in a symbolic format.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The file containing the properties for which counterexamples are to be generated.").addValidationFunctionString(storm::settings::ArgumentValidators::existingReadableFileValidator()).build()) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample. Available are {milp, maxsat}").setDefaultValueString("maxsat").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(techniques)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based minimal command counterexample generation.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based minimal command counterexample generation.").build()); @@ -24,9 +23,6 @@ namespace storm { return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet(); } - std::string CounterexampleGeneratorSettings::minimalCommandSetPropertyFilename() const { - return this->getOption(minimalCommandSetOptionName).getArgumentByName("filename").getValueAsString(); - } bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const { return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp"; diff --git a/src/settings/modules/CounterexampleGeneratorSettings.h b/src/settings/modules/CounterexampleGeneratorSettings.h index e6d2b6f7e..680224b5a 100644 --- a/src/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/settings/modules/CounterexampleGeneratorSettings.h @@ -26,14 +26,6 @@ namespace storm { */ bool isMinimalCommandGenerationSet() const; - /*! - * Retrieves the name of the file that contains the properties for which a minimal command set - * counterexample is to be generated if the option to generate such a counterexample was set. - * - * @return The name of the file that contains the properties. - */ - std::string minimalCommandSetPropertyFilename() const; - /*! * Retrieves whether the MILP-based technique is to be used to generate a minimal command set * counterexample.