Moved some cex code into counterexample module

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);
                     }
                 }

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

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 {

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;

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;

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.");

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;

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++") {

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;

src/storm/utility/counterexamples.h

@@ -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_ */