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<storm::settings::modules::CounterexampleGeneratorSettings>();
- 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<storm::settings::modules::CoreSettings>();
auto abstractionSettings = storm::settings::getModule<storm::settings::modules::AbstractionSettings>();
+ auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
// 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<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
if (model) {
- if (coreSettings.isCounterexampleSet()) {
- auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+ if (counterexampleSettings.isCounterexampleSet()) {
generateCounterexamples<VerificationValueType>(model, input);
} else {
- auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
verifyModel<DdType, VerificationValueType>(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 <queue>
+#include <utility>
+
+#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<typename T>
+ std::vector<storm::storage::FlatSet<uint_fast64_t>> getGuaranteedLabelSets(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> 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<T> const& transitionMatrix = model.getTransitionMatrix();
+ std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
+ storm::storage::SparseMatrix<T> 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<storm::storage::FlatSet<uint_fast64_t>> analysisInformation(model.getNumberOfStates(), relevantLabels);
+
+ std::queue<uint_fast64_t> 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<uint_fast64_t>();
+ 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<uint_fast64_t> 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 <typename T>
+ storm::storage::FlatSet<uint_fast64_t> getGuaranteedLabelSet(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> const& relevantLabels) {
+ std::vector<storm::storage::FlatSet<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels);
+
+ storm::storage::FlatSet<uint_fast64_t> knownLabels(relevantLabels);
+ storm::storage::FlatSet<uint_fast64_t> 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 <chrono>
+#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 <queue>
#include <chrono>
-#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<uint_fast64_t> 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<uint_fast64_t> locallyRelevantLabels;
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin()));
- std::vector<storm::storage::FlatSet<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels);
+ std::vector<storm::storage::FlatSet<uint_fast64_t>> 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<uint_fast64_t> locallyRelevantLabels;
std::set_difference(relevancyInformation.relevantLabels.begin(), relevancyInformation.relevantLabels.end(), commandSet.begin(), commandSet.end(), std::inserter(locallyRelevantLabels, locallyRelevantLabels.begin()));
- std::vector<storm::storage::FlatSet<uint_fast64_t>> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalModel, originalLabelSets, statesThatCanReachTargetStates, locallyRelevantLabels);
+ std::vector<storm::storage::FlatSet<uint_fast64_t>> 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<storm::storage::FlatSet<uint_fast64_t>> 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<std::string> 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<std::string> 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<std::string> 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<storm::settings::modules::IOSettings>().isPrismInputSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().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<storm::settings::modules::IOSettings>().isPrismInputSet() || storm::settings::getModule<storm::settings::modules::IOSettings>().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<std::string> 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 <queue>
-#include <utility>
-
-#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 <typename T>
- std::vector<storm::storage::FlatSet<uint_fast64_t>> getGuaranteedLabelSets(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> 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<T> const& transitionMatrix = model.getTransitionMatrix();
- std::vector<uint_fast64_t> const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices();
- storm::storage::SparseMatrix<T> 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<storm::storage::FlatSet<uint_fast64_t>> analysisInformation(model.getNumberOfStates(), relevantLabels);
-
- std::queue<uint_fast64_t> 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<uint_fast64_t>();
- 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<uint_fast64_t> 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 <typename T>
- storm::storage::FlatSet<uint_fast64_t> getGuaranteedLabelSet(storm::models::sparse::Model<T> const& model, std::vector<storm::storage::FlatSet<uint_fast64_t>> const& labelSets, storm::storage::BitVector const& psiStates, storm::storage::FlatSet<uint_fast64_t> const& relevantLabels) {
- std::vector<storm::storage::FlatSet<uint_fast64_t>> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels);
-
- storm::storage::FlatSet<uint_fast64_t> knownLabels(relevantLabels);
- storm::storage::FlatSet<uint_fast64_t> 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_ */