From 9a5a6d72c6ec049b5823556b15e8ef8aaa8a808c Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 28 Oct 2019 22:39:16 +0100 Subject: [PATCH] Moved some cex code into counterexample module --- src/storm-cli-utilities/model-handling.h | 13 +- .../counterexamples/GuaranteedLabelSet.h | 125 +++++++++++++++++ .../counterexamples/HighLevelCounterexample.h | 3 +- .../MILPMinimalLabelSetGenerator.h | 22 ++- .../SMTMinimalLabelSetGenerator.h | 16 +-- .../CounterexampleGeneratorSettings.cpp | 34 +++-- .../modules/CounterexampleGeneratorSettings.h | 23 +++- src/storm/settings/modules/CoreSettings.cpp | 8 -- src/storm/settings/modules/CoreSettings.h | 17 --- src/storm/utility/counterexamples.h | 128 ------------------ 10 files changed, 194 insertions(+), 195 deletions(-) create mode 100644 src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h delete mode 100644 src/storm/utility/counterexamples.h diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 996d1fdc1..9d4306b48 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -268,12 +268,14 @@ namespace storm { storm::builder::BuilderOptions options(createFormulasToRespect(input.properties), input.model.get()); options.setBuildChoiceLabels(buildSettings.isBuildChoiceLabelsSet()); options.setBuildStateValuations(buildSettings.isBuildStateValuationsSet()); + bool buildChoiceOrigins = false; if (storm::settings::manager().hasModule(storm::settings::modules::CounterexampleGeneratorSettings::moduleName)) { auto counterexampleGeneratorSettings = storm::settings::getModule(); - options.setBuildChoiceOrigins(counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet()); - } else { - options.setBuildChoiceOrigins(false); + if (counterexampleGeneratorSettings.isCounterexampleSet()) { + buildChoiceOrigins = counterexampleGeneratorSettings.isMinimalCommandSetGenerationSet(); + } } + options.setBuildChoiceOrigins(buildChoiceOrigins); options.setAddOutOfBoundsState(buildSettings.isBuildOutOfBoundsStateSet()); if (buildSettings.isBuildFullModelSet()) { options.clearTerminalStates(); @@ -929,6 +931,7 @@ namespace storm { void processInputWithValueTypeAndDdlib(SymbolicInput const& input) { auto coreSettings = storm::settings::getModule(); auto abstractionSettings = storm::settings::getModule(); + auto counterexampleSettings = storm::settings::getModule(); // For several engines, no model building step is performed, but the verification is started right away. storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine(); @@ -941,11 +944,9 @@ namespace storm { std::shared_ptr model = buildPreprocessExportModelWithValueTypeAndDdlib(input, engine); if (model) { - if (coreSettings.isCounterexampleSet()) { - auto ioSettings = storm::settings::getModule(); + if (counterexampleSettings.isCounterexampleSet()) { generateCounterexamples(model, input); } else { - auto ioSettings = storm::settings::getModule(); verifyModel(model, input, coreSettings); } } diff --git a/src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h b/src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h new file mode 100644 index 000000000..da1696517 --- /dev/null +++ b/src/storm-counterexamples/counterexamples/GuaranteedLabelSet.h @@ -0,0 +1,125 @@ +#pragma once + +#include +#include + +#include "storm/exceptions/InvalidArgumentException.h" +#include "storm/models/sparse/Model.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" + +namespace storm { + namespace counterexamples { + + /*! + * Computes a set of labels that is executed along all paths from any state to a target state. + * + * @param labelSet the considered label sets (a label set is assigned to each choice) + * + * @return The set of labels that is visited on all paths from any state to a target state. + */ + template + std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { + STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); + + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); + + // Now we compute the set of labels that is present on all paths from the initial to the target states. + std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); + + std::queue worklist; + storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); + storm::storage::BitVector markedStates(model.getNumberOfStates()); + + // Initially, put all predecessors of target states in the worklist and empty the analysis information them. + for (auto state : psiStates) { + analysisInformation[state] = storm::storage::FlatSet(); + for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { + if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { + worklist.push(predecessorEntry.getColumn()); + statesInWorkList.set(predecessorEntry.getColumn()); + markedStates.set(state); + } + } + } + + uint_fast64_t iters = 0; + while (!worklist.empty()) { + ++iters; + uint_fast64_t const& currentState = worklist.front(); + + size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); + + // Iterate over the successor states for all choices and compute new analysis information. + for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { + bool modifiedChoice = false; + + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (markedStates.get(entry.getColumn())) { + modifiedChoice = true; + break; + } + } + + // If we can reach the target state with this choice, we need to intersect the current + // analysis information with the union of the new analysis information of the target state + // and the choice labels. + if (modifiedChoice) { + for (auto const& entry : transitionMatrix.getRow(currentChoice)) { + if (markedStates.get(entry.getColumn())) { + storm::storage::FlatSet tmpIntersection; + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); + analysisInformation[currentState] = std::move(tmpIntersection); + } + } + } + } + + // If the analysis information changed, we need to update it and put all the predecessors of this + // state in the worklist. + if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { + for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { + // Only put the predecessor in the worklist if it's not already a target state. + if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { + worklist.push(predecessorEntry.getColumn()); + statesInWorkList.set(predecessorEntry.getColumn()); + } + } + markedStates.set(currentState, true); + } else { + markedStates.set(currentState, false); + } + + worklist.pop(); + statesInWorkList.set(currentState, false); + } + + return analysisInformation; + } + + /*! + * Computes a set of labels that is executed along all paths from an initial state to a target state. + * + * @param labelSet the considered label sets (a label set is assigned to each choice) + * + * @return The set of labels that is executed on all paths from an initial state to a target state. + */ + template + storm::storage::FlatSet getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); + + storm::storage::FlatSet knownLabels(relevantLabels); + storm::storage::FlatSet tempIntersection; + for (auto initialState : model.getInitialStates()) { + std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); + std::swap(knownLabels, tempIntersection); + } + + return knownLabels; + } + + } // namespace counterexample +} // namespace storm diff --git a/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h index 27fe981c0..4ce432a8f 100644 --- a/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h +++ b/src/storm-counterexamples/counterexamples/HighLevelCounterexample.h @@ -1,7 +1,6 @@ #pragma once -#include "Counterexample.h" - +#include "storm-counterexamples/counterexamples/Counterexample.h" #include "storm/storage/SymbolicModelDescription.h" namespace storm { diff --git a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h index a2e6de197..d7186c95c 100644 --- a/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h @@ -2,9 +2,16 @@ #include +#include "storm-counterexamples/counterexamples/GuaranteedLabelSet.h" +#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" + #include "storm/models/sparse/Mdp.h" #include "storm/logic/Formulas.h" #include "storm/storage/prism/Program.h" +#include "storm/storage/sparse/PrismChoiceOrigins.h" +#include "storm/storage/sparse/JaniChoiceOrigins.h" +#include "storm/storage/BoostTypes.h" #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h" #include "storm/modelchecker/prctl/helper/SparseMdpPrctlHelper.h" #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h" @@ -13,23 +20,12 @@ #include "storm/exceptions/InvalidPropertyException.h" #include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/InvalidStateException.h" - #include "storm/solver/MinMaxLinearEquationSolver.h" - -#include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" - +#include "storm/solver/LpSolver.h" #include "storm/utility/graph.h" -#include "storm/utility/counterexamples.h" #include "storm/utility/solver.h" -#include "storm/solver/LpSolver.h" - -#include "storm/storage/sparse/PrismChoiceOrigins.h" -#include "storm/storage/sparse/JaniChoiceOrigins.h" -#include "storm/storage/BoostTypes.h" - #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/GeneralSettings.h" -#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" namespace storm { @@ -167,7 +163,7 @@ namespace storm { } // Finally, determine the set of labels that are known to be taken. - result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, result.allRelevantLabels); + result.knownLabels = storm::counterexamples::getGuaranteedLabelSet(mdp, labelSets, psiStates, result.allRelevantLabels); STORM_LOG_DEBUG("Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels."); return result; diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 9a66982b0..66e27fa78 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -3,10 +3,11 @@ #include #include -#include "storm/solver/Z3SmtSolver.h" - +#include "storm-counterexamples/counterexamples/GuaranteedLabelSet.h" #include "storm-counterexamples/counterexamples/HighLevelCounterexample.h" +#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" +#include "storm/solver/Z3SmtSolver.h" #include "storm/storage/prism/Program.h" #include "storm/storage/expressions/Expression.h" #include "storm/storage/sparse/PrismChoiceOrigins.h" @@ -17,13 +18,10 @@ #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h" #include "storm/settings/SettingsManager.h" #include "storm/settings/modules/CoreSettings.h" -#include "storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h" - +#include "storm/utility/cli.h" #include "storm/utility/macros.h" #include "storm/exceptions/NotSupportedException.h" -#include "storm/utility/counterexamples.h" -#include "storm/utility/cli.h" namespace storm { @@ -165,7 +163,7 @@ namespace storm { } // Compute the set of labels that are known to be taken in any case. - relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); + relevancyInformation.knownLabels = storm::counterexamples::getGuaranteedLabelSet(model, labelSets, psiStates, relevancyInformation.relevantLabels); if (!relevancyInformation.knownLabels.empty()) { storm::storage::FlatSet remainingLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(remainingLabels, remainingLabels.end())); @@ -1349,7 +1347,7 @@ namespace storm { storm::storage::FlatSet locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); STORM_LOG_DEBUG("Found " << reachableLabels.size() << " reachable labels and " << reachableStates.getNumberOfSetBits() << " reachable states."); // Search for states on the border of the reachable state space, i.e. states that are still reachable @@ -1466,7 +1464,7 @@ namespace storm { storm::storage::FlatSet locallyRelevantLabels; std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin())); - std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); + std::vector> guaranteedLabelSets = storm::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels); // Search for states for which we could enable another option and possibly improve the reachability probability. std::set> cutLabels; diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp index 27a2c1120..b0de2ca79 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp @@ -13,30 +13,45 @@ namespace storm { namespace modules { const std::string CounterexampleGeneratorSettings::moduleName = "counterexample"; - const std::string CounterexampleGeneratorSettings::minimalCommandSetOptionName = "mincmd"; + const std::string CounterexampleGeneratorSettings::counterexampleOptionName = "counterexample"; + const std::string CounterexampleGeneratorSettings::counterexampleOptionShortName = "cex"; + const std::string CounterexampleGeneratorSettings::counterexampleTypeOptionName = "cextype"; + const std::string CounterexampleGeneratorSettings::minimalCommandMethodOptionName = "mincmdmethod"; 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/edge set. Note that this requires the model to be given in a symbolic format.").setIsAdvanced() - .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, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build()); + std::vector cextype = {"mincmd"}; + this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleTypeOptionName, false, "Generates a counterexample of the given type if the given PRCTL formula is not satisfied by the model.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("type", "The type of the counterexample to compute.").setDefaultValueString("mincmd").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(cextype)).build()).build()); + std::vector method = {"maxsat", "milp"}; + this->addOption(storm::settings::OptionBuilder(moduleName, minimalCommandMethodOptionName, true, "Sets which method is used to derive the counterexample in terms of a minimal command/edge set.").setIsAdvanced() + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("method", "The name of the method to use.").setDefaultValueString("maxsat").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(method)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, encodeReachabilityOptionName, true, "Sets whether to encode reachability for MAXSAT-based counterexample generation.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, schedulerCutsOptionName, true, "Sets whether to add the scheduler cuts for MILP-based counterexample generation.").setIsAdvanced().build()); this->addOption(storm::settings::OptionBuilder(moduleName, noDynamicConstraintsOptionName, true, "Disables the generation of dynamic constraints in the MAXSAT-based counterexample generation.").setIsAdvanced().build()); } - + + bool CounterexampleGeneratorSettings::isCounterexampleSet() const { + return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); + } + + bool CounterexampleGeneratorSettings::isCounterexampleTypeSet() const { + return this->getOption(counterexampleTypeOptionName).getHasOptionBeenSet(); + } + bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const { - return this->getOption(minimalCommandSetOptionName).getHasOptionBeenSet(); + return this->getOption(counterexampleTypeOptionName).getArgumentByName("type").getValueAsString() == "mincmd"; } bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const { - return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "milp"; + return this->getOption(minimalCommandMethodOptionName).getArgumentByName("method").getValueAsString() == "milp"; } bool CounterexampleGeneratorSettings::isUseMaxSatBasedMinimalCommandSetGenerationSet() const { - return this->getOption(minimalCommandSetOptionName).getArgumentByName("method").getValueAsString() == "maxsat"; + return this->getOption(minimalCommandMethodOptionName).getArgumentByName("method").getValueAsString() == "maxsat"; } bool CounterexampleGeneratorSettings::isEncodeReachabilitySet() const { @@ -52,8 +67,9 @@ namespace storm { } bool CounterexampleGeneratorSettings::check() const { + STORM_LOG_THROW(isCounterexampleSet() || !isCounterexampleTypeSet(), storm::exceptions::InvalidSettingsException, "Counterexample type was set but counterexample flag '-cex' is missing."); // Ensure that the model was given either symbolically or explicitly. - STORM_LOG_THROW(!isMinimalCommandSetGenerationSet() || storm::settings::getModule().isPrismInputSet() || storm::settings::getModule().isJaniInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM/JANI format."); + STORM_LOG_THROW(!isCounterexampleSet() || !isMinimalCommandSetGenerationSet() || storm::settings::getModule().isPrismInputSet() || storm::settings::getModule().isJaniInputSet(), storm::exceptions::InvalidSettingsException, "For the generation of a minimal command set, the model has to be specified in the PRISM/JANI format."); if (isMinimalCommandSetGenerationSet()) { STORM_LOG_WARN_COND(isUseMaxSatBasedMinimalCommandSetGenerationSet() || !isEncodeReachabilitySet(), "Encoding reachability is only available for the MaxSat-based minimal command set generation, so selecting it has no effect."); diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h index bdb0813a6..2e8fe1388 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h @@ -16,9 +16,23 @@ namespace storm { * Creates a new set of counterexample settings. */ CounterexampleGeneratorSettings(); - + + /*! + * Retrieves whether the counterexample option was set. + * + * @return True if the counterexample option was set. + */ + bool isCounterexampleSet() const; + + /*! + * Retrieves whether the type of counterexample was set. + * + * @return True if the type of the counterexample was set. + */ + bool isCounterexampleTypeSet() const; + /*! - * Retrieves whether the option to generate a minimal command set was set. + * Retrieves whether the option to generate a minimal command set counterexample was set. * * @return True iff a minimal command set counterexample is to be generated. */ @@ -70,7 +84,10 @@ namespace storm { private: // Define the string names of the options as constants. - static const std::string minimalCommandSetOptionName; + static const std::string counterexampleOptionName; + static const std::string counterexampleOptionShortName; + static const std::string counterexampleTypeOptionName; + static const std::string minimalCommandMethodOptionName; static const std::string encodeReachabilityOptionName; static const std::string schedulerCutsOptionName; static const std::string noDynamicConstraintsOptionName; diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp index c29f037ec..bc9ea87fb 100644 --- a/src/storm/settings/modules/CoreSettings.cpp +++ b/src/storm/settings/modules/CoreSettings.cpp @@ -20,8 +20,6 @@ namespace storm { namespace modules { const std::string CoreSettings::moduleName = "core"; - const std::string CoreSettings::counterexampleOptionName = "counterexample"; - const std::string CoreSettings::counterexampleOptionShortName = "cex"; const std::string CoreSettings::eqSolverOptionName = "eqsolver"; const std::string CoreSettings::lpSolverOptionName = "lpsolver"; const std::string CoreSettings::smtSolverOptionName = "smtsolver"; @@ -35,8 +33,6 @@ namespace storm { const std::string CoreSettings::intelTbbOptionShortName = "tbb"; CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) { - this->addOption(storm::settings::OptionBuilder(moduleName, counterexampleOptionName, false, "Generates a counterexample for the given PRCTL formulas if not satisfied by the model.").setShortName(counterexampleOptionShortName).build()); - std::vector engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"}; this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName) .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build()); @@ -62,10 +58,6 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, intelTbbOptionName, false, "Sets whether to use Intel TBB (if Storm was built with support for TBB).").setShortName(intelTbbOptionShortName).build()); } - bool CoreSettings::isCounterexampleSet() const { - return this->getOption(counterexampleOptionName).getHasOptionBeenSet(); - } - storm::solver::EquationSolverType CoreSettings::getEquationSolver() const { std::string equationSolverName = this->getOption(eqSolverOptionName).getArgumentByName("name").getValueAsString(); if (equationSolverName == "gmm++") { diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h index b475a2326..405fad91f 100644 --- a/src/storm/settings/modules/CoreSettings.h +++ b/src/storm/settings/modules/CoreSettings.h @@ -36,21 +36,6 @@ namespace storm { */ CoreSettings(); - /*! - * Retrieves whether the counterexample option was set. - * - * @return True if the counterexample option was set. - */ - bool isCounterexampleSet() const; - - /*! - * Retrieves the name of the file to which the counterexample is to be written if the counterexample - * option was set. - * - * @return The name of the file to which the counterexample is to be written. - */ - std::string getCounterexampleFilename() const; - /*! * Retrieves the selected equation solver. * @@ -150,8 +135,6 @@ namespace storm { Engine engine; // Define the string names of the options as constants. - static const std::string counterexampleOptionName; - static const std::string counterexampleOptionShortName; static const std::string eqSolverOptionName; static const std::string lpSolverOptionName; static const std::string smtSolverOptionName; diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h deleted file mode 100644 index 6705e40f7..000000000 --- a/src/storm/utility/counterexamples.h +++ /dev/null @@ -1,128 +0,0 @@ -#ifndef STORM_UTILITY_COUNTEREXAMPLE_H_ -#define STORM_UTILITY_COUNTEREXAMPLE_H_ - -#include -#include - -#include "storm/storage/sparse/PrismChoiceOrigins.h" - -namespace storm { - namespace utility { - namespace counterexamples { - - /*! - * Computes a set of labels that is executed along all paths from any state to a target state. - * - * @param labelSet the considered label sets (a label set is assigned to each choice) - * - * @return The set of labels that is visited on all paths from any state to a target state. - */ - template - std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { - STORM_LOG_THROW(model.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); - - // Get some data from the model for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); - storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); - - // Now we compute the set of labels that is present on all paths from the initial to the target states. - std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); - - std::queue worklist; - storm::storage::BitVector statesInWorkList(model.getNumberOfStates()); - storm::storage::BitVector markedStates(model.getNumberOfStates()); - - // Initially, put all predecessors of target states in the worklist and empty the analysis information them. - for (auto state : psiStates) { - analysisInformation[state] = storm::storage::FlatSet(); - for (auto const& predecessorEntry : backwardTransitions.getRow(state)) { - if (predecessorEntry.getColumn() != state && !statesInWorkList.get(predecessorEntry.getColumn()) && !psiStates.get(predecessorEntry.getColumn())) { - worklist.push(predecessorEntry.getColumn()); - statesInWorkList.set(predecessorEntry.getColumn()); - markedStates.set(state); - } - } - } - - uint_fast64_t iters = 0; - while (!worklist.empty()) { - ++iters; - uint_fast64_t const& currentState = worklist.front(); - - size_t analysisInformationSizeBefore = analysisInformation[currentState].size(); - - // Iterate over the successor states for all choices and compute new analysis information. - for (uint_fast64_t currentChoice = nondeterministicChoiceIndices[currentState]; currentChoice < nondeterministicChoiceIndices[currentState + 1]; ++currentChoice) { - bool modifiedChoice = false; - - for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (markedStates.get(entry.getColumn())) { - modifiedChoice = true; - break; - } - } - - // If we can reach the target state with this choice, we need to intersect the current - // analysis information with the union of the new analysis information of the target state - // and the choice labels. - if (modifiedChoice) { - for (auto const& entry : transitionMatrix.getRow(currentChoice)) { - if (markedStates.get(entry.getColumn())) { - storm::storage::FlatSet tmpIntersection; - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), analysisInformation[entry.getColumn()].begin(), analysisInformation[entry.getColumn()].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); - std::set_intersection(analysisInformation[currentState].begin(), analysisInformation[currentState].end(), labelSets[currentChoice].begin(), labelSets[currentChoice].end(), std::inserter(tmpIntersection, tmpIntersection.begin())); - analysisInformation[currentState] = std::move(tmpIntersection); - } - } - } - } - - // If the analysis information changed, we need to update it and put all the predecessors of this - // state in the worklist. - if (analysisInformation[currentState].size() != analysisInformationSizeBefore) { - for (auto const& predecessorEntry : backwardTransitions.getRow(currentState)) { - // Only put the predecessor in the worklist if it's not already a target state. - if (!psiStates.get(predecessorEntry.getColumn()) && !statesInWorkList.get(predecessorEntry.getColumn())) { - worklist.push(predecessorEntry.getColumn()); - statesInWorkList.set(predecessorEntry.getColumn()); - } - } - markedStates.set(currentState, true); - } else { - markedStates.set(currentState, false); - } - - worklist.pop(); - statesInWorkList.set(currentState, false); - } - - return analysisInformation; - } - - /*! - * Computes a set of labels that is executed along all paths from an initial state to a target state. - * - * @param labelSet the considered label sets (a label set is assigned to each choice) - * - * @return The set of labels that is executed on all paths from an initial state to a target state. - */ - template - storm::storage::FlatSet getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); - - storm::storage::FlatSet knownLabels(relevantLabels); - storm::storage::FlatSet tempIntersection; - for (auto initialState : model.getInitialStates()) { - std::set_intersection(knownLabels.begin(), knownLabels.end(), guaranteedLabels[initialState].begin(), guaranteedLabels[initialState].end(), std::inserter(tempIntersection, tempIntersection.end())); - std::swap(knownLabels, tempIntersection); - } - - return knownLabels; - } - - } // namespace counterexample - } // namespace utility -} // namespace storm - -#endif /* STORM_UTILITY_COUNTEREXAMPLE_H_ */