diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index 4aff07fae..8a8edb0e6 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -1322,6 +1322,24 @@ namespace storm { return getUsedLabelSet(*solver.getModel(), variableInformation); } + static void ruleOutSingleSolution(storm::solver::SmtSolver& solver, boost::container::flat_set const& labelSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + std::vector formulae; + + boost::container::flat_set unknownLabels; + std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLabels, unknownLabels.end())); + for (auto const& label : unknownLabels) { + formulae.emplace_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + } + boost::container::flat_set remainingLabels; + std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), labelSet.begin(), labelSet.end(), std::inserter(remainingLabels, remainingLabels.end())); + for (auto const& label : remainingLabels) { + formulae.emplace_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); + } + + STORM_LOG_DEBUG("Ruling out single solution."); + assertDisjunction(solver, formulae, *variableInformation.manager); + } + /*! * Analyzes the given sub-model that has a maximal reachability of zero (i.e. no psi states are reachable) and tries to construct assertions that aim to make at least one psi state reachable. * @@ -1618,6 +1636,19 @@ namespace storm { } public: + struct Options { + Options(bool checkThresholdFeasible = false) : checkThresholdFeasible(checkThresholdFeasible) { + auto const& settings = storm::settings::getModule(); + + encodeReachability = settings.isEncodeReachabilitySet(); + useDynamicConstraints = settings.isUseDynamicConstraintsSet(); + } + + bool checkThresholdFeasible; + bool encodeReachability; + bool useDynamicConstraints; + }; + /*! * Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi. * @@ -1627,10 +1658,9 @@ namespace storm { * @param psiStates A bit vector characterizing all psi states in the model. * @param probabilityThreshold The threshold that is to be achieved or exceeded. * @param strictBound Indicates whether the threshold needs to be achieved (true) or exceeded (false). - * @param checkThresholdFeasible If set, it is verified that the model can actually achieve/exceed the given probability value. If this check - * is made and fails, an exception is thrown. + * @param options A set of options for customization. */ - static boost::container::flat_set getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), bool checkThresholdFeasible = false, bool includeReachabilityEncoding = false) { + static boost::container::flat_set getMinimalLabelSet(Environment const& env, storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, double probabilityThreshold, bool strictBound, boost::container::flat_set const& dontCareLabels = boost::container::flat_set(), Options const& options = Options()) { #ifdef STORM_HAVE_Z3 // Set up all clocks used for time measurement. auto totalClock = std::chrono::high_resolution_clock::now(); @@ -1669,7 +1699,7 @@ namespace storm { // (1) Check whether its possible to exceed the threshold if checkThresholdFeasible is set. double maximalReachabilityProbability = 0; - if (checkThresholdFeasible) { + if (options.checkThresholdFeasible) { maximalReachabilityProbability = computeMaximalReachabilityProbability(env, model, phiStates, psiStates); STORM_LOG_THROW((strictBound && maximalReachabilityProbability >= probabilityThreshold) || (!strictBound && maximalReachabilityProbability > probabilityThreshold), storm::exceptions::InvalidArgumentException, "Given probability threshold " << probabilityThreshold << " can not be " << (strictBound ? "achieved" : "exceeded") << " in model with maximal reachability probability of " << maximalReachabilityProbability << "."); @@ -1684,7 +1714,7 @@ namespace storm { std::unique_ptr solver = std::make_unique(*manager); // (4) Create the variables for the relevant commands. - VariableInformation variableInformation = createVariables(manager, model, psiStates, relevancyInformation, includeReachabilityEncoding); + VariableInformation variableInformation = createVariables(manager, model, psiStates, relevancyInformation, options.encodeReachability); STORM_LOG_DEBUG("Created variables."); // (5) Now assert an adder whose result variables can later be used to constrain the nummber of label @@ -1697,7 +1727,7 @@ namespace storm { STORM_LOG_DEBUG("Asserting cuts."); assertCuts(symbolicModel, model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted cuts."); - if (includeReachabilityEncoding) { + if (options.encodeReachability) { assertReachabilityCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } @@ -1749,15 +1779,22 @@ namespace storm { // Depending on whether the threshold was successfully achieved or not, we proceed by either analyzing the bad solution or stopping the iteration process. analysisClock = std::chrono::high_resolution_clock::now(); if ((strictBound && maximalReachabilityProbability < probabilityThreshold) || (!strictBound && maximalReachabilityProbability <= probabilityThreshold)) { - if (maximalReachabilityProbability == 0) { + if (maximalReachabilityProbability == storm::utility::zero()) { ++zeroProbabilityCount; - - // If there was no target state reachable, analyze the solution and guide the solver into the right direction. - analyzeZeroProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + } + + if (options.useDynamicConstraints) { + if (maximalReachabilityProbability == storm::utility::zero()) { + // If there was no target state reachable, analyze the solution and guide the solver into the right direction. + analyzeZeroProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + } else { + // If the reachability probability was greater than zero (i.e. there is a reachable target state), but the probability was insufficient to exceed + // the given threshold, we analyze the solution and try to guide the solver into the right direction. + analyzeInsufficientProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + } } else { - // If the reachability probability was greater than zero (i.e. there is a reachable target state), but the probability was insufficient to exceed - // the given threshold, we analyze the solution and try to guide the solver into the right direction. - analyzeInsufficientProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + // Do not guide solver, just rule out current solution. + ruleOutSingleSolution(*solver, commandSet, variableInformation, relevancyInformation); } } else { done = true; @@ -1948,7 +1985,7 @@ namespace storm { // Delegate the actual computation work to the function of equal name. auto startTime = std::chrono::high_resolution_clock::now(); - auto labelSet = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, boost::container::flat_set(), true, storm::settings::getModule().isEncodeReachabilitySet()); + auto labelSet = getMinimalLabelSet(env, symbolicModel, model, phiStates, psiStates, threshold, strictBound, boost::container::flat_set(), true); auto endTime = std::chrono::high_resolution_clock::now(); std::cout << std::endl << "Computed minimal label set of size " << labelSet.size() << " in " << std::chrono::duration_cast(endTime - startTime).count() << "ms." << std::endl; diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp index b33a332df..2525f19b0 100644 --- a/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm/settings/modules/CounterexampleGeneratorSettings.cpp @@ -16,13 +16,15 @@ namespace storm { const std::string CounterexampleGeneratorSettings::minimalCommandSetOptionName = "mincmd"; const std::string CounterexampleGeneratorSettings::encodeReachabilityOptionName = "encreach"; const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts"; - + const std::string CounterexampleGeneratorSettings::noDynamicConstraintsOptionName = "nodyn"; + CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(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.") + this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandSetOptionName, true, "Computes a counterexample for the given model in terms of a minimal command/edge set. Note that this requires the model to be given in a symbolic format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "Sets which technique is used to derive the counterexample.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(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()); + this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").build()); } bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const { @@ -44,7 +46,11 @@ namespace storm { bool CounterexampleGeneratorSettings::isUseSchedulerCutsSet() const { return this->getOption(schedulerCutsOptionName).getHasOptionBeenSet(); } - + + bool CounterexampleGeneratorSettings::isUseDynamicConstraintsSet() const { + return !this->getOption(noDynamicConstraintsOptionName).getHasOptionBeenSet(); + } + bool CounterexampleGeneratorSettings::check() const { // Ensure that the model was given either symbolically or explicitly. STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule().isPrismInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM format."); diff --git a/src/storm/settings/modules/CounterexampleGeneratorSettings.h b/src/storm/settings/modules/CounterexampleGeneratorSettings.h index 03002c8f6..bdb0813a6 100644 --- a/src/storm/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/storm/settings/modules/CounterexampleGeneratorSettings.h @@ -56,6 +56,13 @@ namespace storm { */ bool isUseSchedulerCutsSet() const; + /*! + * Retrieves whether to use the dynamic constraints in the MAXSAT-based technique. + * + * @return True iff dynamic constraints are to be used. + */ + bool isUseDynamicConstraintsSet() const; + bool check() const override; // The name of the module. @@ -66,6 +73,7 @@ namespace storm { static const std::string minimalCommandSetOptionName; static const std::string encodeReachabilityOptionName; static const std::string schedulerCutsOptionName; + static const std::string noDynamicConstraintsOptionName; }; } // namespace modules