Support for k-shortest path counterexamples

CHANGELOG.md

@@ -23,6 +23,7 @@ Version 1.3.x
 - DRN: Support for placeholder variables which allows to parse recurring rational functions only once.
 - Fixed sparse bisimulation of MDPs (which failed if all non-absorbing states in the quotient are initial).
 - Support for export of MTBDDs from Storm.
+- Support for k-shortest path counterexamples (arguments `-cex --cextype shortestpath`)
 - New settings module `transformation` for Markov chain transformations. Use `--help transformation` to get a list of available transformations.
 - Support for eliminating chains of Non-Markovian states in MAs via `--eliminate-chains`.
 - Export to dot format allows for maximal line width in states (argument `--dot-maxwidth <width>`)

src/storm-cli-utilities/model-handling.h

@@ -540,27 +540,41 @@ namespace storm {
             
             auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
             if (counterexampleSettings.isMinimalCommandSetGenerationSet()) {
-                
                 bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet();
                 for (auto const& property : input.properties) {
                     std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
                     printComputingCounterexample(property);
                     storm::utility::Stopwatch watch(true);
                     if (useMilp) {
-                        STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MILP is currently only supported for MDPs.");
+                        STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException,
-                        counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
+                                        "Counterexample generation using MILP is currently only supported for MDPs.");
+                        counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(),
+                                                                                        property.getRawFormula());
                     } else {
-                        STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
+                        STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp),
+                                        storm::exceptions::NotSupportedException, "Counterexample generation using MaxSAT is currently only supported for discrete-time models.");
 
                         if (sparseModel->isOfType(storm::models::ModelType::Dtmc)) {
-                            counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula());
+                            counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(),
+                                                                                              property.getRawFormula());
                         } else {
-                            counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(), property.getRawFormula());
+                            counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as<storm::models::sparse::Mdp<ValueType>>(),
+                                                                                              property.getRawFormula());
                         }
                     }
                     watch.stop();
                     printCounterexample(counterexample, &watch);
                 }
+            } else if (counterexampleSettings.isShortestPathGenerationSet()) {
+                for (auto const& property : input.properties) {
+                    std::shared_ptr<storm::counterexamples::Counterexample> counterexample;
+                    printComputingCounterexample(property);
+                    storm::utility::Stopwatch watch(true);
+                    STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc), storm::exceptions::NotSupportedException, "Counterexample generation using shortest paths is currently only supported for DTMCs.");
+                    counterexample = storm::api::computeKShortestPathCounterexample(sparseModel->template as<storm::models::sparse::Dtmc<ValueType>>(), property.getRawFormula(), counterexampleSettings.getShortestPathMaxK());
+                    watch.stop();
+                    printCounterexample(counterexample, &watch);
+                }
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported.");
             }

src/storm-counterexamples/api/counterexamples.cpp

@@ -1,19 +1,65 @@
 #include "storm-counterexamples/api/counterexamples.h"
 
 #include "storm/environment/Environment.h"
+#include "storm/utility/shortestPaths.h"
 
 namespace storm {
     namespace api {
 
-        std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        std::shared_ptr<storm::counterexamples::Counterexample>
+        computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Mdp<double>> mdp,
+                                           std::shared_ptr<storm::logic::Formula const> const& formula) {
             Environment env;
             return storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(env, symbolicModel, *mdp, formula);
         }
 
-        std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
+        std::shared_ptr<storm::counterexamples::Counterexample>
+        computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Model<double>> model,
+                                             std::shared_ptr<storm::logic::Formula const> const& formula) {
             Environment env;
             return storm::counterexamples::SMTMinimalLabelSetGenerator<double>::computeCounterexample(env, symbolicModel, *model, formula);
         }
 
+        std::shared_ptr<storm::counterexamples::Counterexample>
+        computeKShortestPathCounterexample(std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula, size_t maxK) {
+            // Only accept formulas of the form "P </<= x [F target]
+            STORM_LOG_THROW(formula->isProbabilityOperatorFormula(), storm::exceptions::InvalidPropertyException,
+                            "Counterexample generation does not support this kind of formula. Expecting a probability operator as the outermost formula element.");
+            storm::logic::ProbabilityOperatorFormula const& probabilityOperator = formula->asProbabilityOperatorFormula();
+            STORM_LOG_THROW(probabilityOperator.hasBound(), storm::exceptions::InvalidPropertyException, "Counterexample generation only supports bounded formulas.");
+            STORM_LOG_THROW(!storm::logic::isLowerBound(probabilityOperator.getComparisonType()), storm::exceptions::InvalidPropertyException,
+                            "Counterexample generation only supports upper bounds.");
+            double threshold = probabilityOperator.getThresholdAs<double>();
+            storm::logic::Formula const& subformula = formula->asOperatorFormula().getSubformula();
+            STORM_LOG_THROW(subformula.isEventuallyFormula(), storm::exceptions::InvalidPropertyException,
+                            "Path formula is required to be of the form 'F psi' for counterexample generation.");
+            bool strictBound = (probabilityOperator.getComparisonType() == storm::logic::ComparisonType::Greater);
+
+            // Perform model checking to get target states
+            Environment env;
+            storm::modelchecker::SparsePropositionalModelChecker<storm::models::sparse::Model<double>> modelchecker(*model);
+
+            storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula();
+            std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
+            storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
+
+            auto generator = storm::utility::ksp::ShortestPathsGenerator<double>(*model, subQualitativeResult.getTruthValuesVector());
+            storm::counterexamples::PathCounterexample<double> cex(model);
+            double probability = 0;
+            bool thresholdExceeded = false;
+            for (size_t k = 1; k <= maxK; ++k) {
+                cex.addPath(generator.getPathAsList(k), k);
+                probability += generator.getDistance(k);
+                // Check if accumulated probability mass is already enough
+                if ((probability >= threshold && !strictBound) || (probability > threshold)) {
+                    thresholdExceeded = true;
+                    break;
+                }
+            }
+            STORM_LOG_WARN_COND(thresholdExceeded, "Aborted computation because maximal number of paths was reached. Probability threshold is not yet exceeded.");
+
+            return std::make_shared<storm::counterexamples::PathCounterexample<double>>(cex);
+        }
+
     }
 }

src/storm-counterexamples/api/counterexamples.h

@@ -2,6 +2,7 @@
 
 #include "storm-counterexamples/counterexamples/MILPMinimalLabelSetGenerator.h"
 #include "storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h"
+#include "storm-counterexamples/counterexamples/PathCounterexample.h"
 
 namespace storm {
     namespace api {
@@ -10,5 +11,7 @@ namespace storm {
         
         std::shared_ptr<storm::counterexamples::Counterexample> computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula);
 
+        std::shared_ptr<storm::counterexamples::Counterexample> computeKShortestPathCounterexample(std::shared_ptr<storm::models::sparse::Model<double>> model, std::shared_ptr<storm::logic::Formula const> const& formula, size_t maxK);
+
     }
 }

src/storm-counterexamples/counterexamples/PathCounterexample.cpp

@@ -0,0 +1,40 @@
+#include "storm-counterexamples/counterexamples/PathCounterexample.h"
+
+#include "storm/utility/export.h"
+
+namespace storm {
+    namespace counterexamples {
+
+        template<typename ValueType>
+        PathCounterexample<ValueType>::PathCounterexample(std::shared_ptr<storm::models::sparse::Model<ValueType>> model) : model(model) {
+            // Intentionally left empty.
+        }
+
+        template<typename ValueType>
+        void PathCounterexample<ValueType>::addPath(std::vector<storage::sparse::state_type> path, size_t k) {
+            if (k >= shortestPaths.size()) {
+                shortestPaths.resize(k);
+            }
+            shortestPaths[k-1] = path;
+        }
+
+        template<typename ValueType>
+        void PathCounterexample<ValueType>::writeToStream(std::ostream& out) const {
+            out << "Shortest path counterexample with k = " << shortestPaths.size() << " paths: " << std::endl;
+            for (size_t i = 0; i < shortestPaths.size(); ++i) {
+                out << i+1 << "-shortest path: " << std::endl;
+                for (auto it = shortestPaths[i].rbegin(); it != shortestPaths[i].rend(); ++it) {
+                    out << "\tstate " << *it;
+                    if (model->hasStateValuations()) {
+                        out << ": "<< model->getStateValuations().getStateInfo(*it);
+                    }
+                    out << ": {";
+                    storm::utility::outputFixedWidth(out, model->getLabelsOfState(*it), 0);
+                    out << "}" << std::endl;
+                }
+            }
+        }
+
+        template class PathCounterexample<double>;
+    }
+}

src/storm-counterexamples/counterexamples/PathCounterexample.h

@@ -0,0 +1,25 @@
+#pragma once
+
+#include "storm-counterexamples/counterexamples/Counterexample.h"
+
+#include "storm/models/sparse/Model.h"
+
+namespace storm {
+    namespace counterexamples {
+
+        template<typename ValueType>
+        class PathCounterexample : public Counterexample {
+        public:
+            PathCounterexample(std::shared_ptr<storm::models::sparse::Model<ValueType>> model);
+
+            void addPath(std::vector<storage::sparse::state_type> path, size_t k);
+
+            void writeToStream(std::ostream& out) const override;
+
+        private:
+            std::shared_ptr<storm::models::sparse::Model<ValueType>> model;
+            std::vector<std::vector<storage::sparse::state_type>> shortestPaths;
+        };
+        
+    }
+}

src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp

@@ -16,6 +16,7 @@ namespace storm {
             const std::string CounterexampleGeneratorSettings::counterexampleOptionName = "counterexample";
             const std::string CounterexampleGeneratorSettings::counterexampleOptionShortName = "cex";
             const std::string CounterexampleGeneratorSettings::counterexampleTypeOptionName = "cextype";
+            const std::string CounterexampleGeneratorSettings::shortestPathMaxKOptionName = "shortestpath-maxk";
             const std::string CounterexampleGeneratorSettings::minimalCommandMethodOptionName = "mincmdmethod";
             const std::string CounterexampleGeneratorSettings::encodeReachabilityOptionName = "encreach";
             const std::string CounterexampleGeneratorSettings::schedulerCutsOptionName = "schedcuts";
@@ -23,9 +24,11 @@ namespace storm {
 
             CounterexampleGeneratorSettings::CounterexampleGeneratorSettings() : ModuleSettings(moduleName) {
                 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"};
+                std::vector<std::string> cextype = {"mincmd", "shortestpath"};
                 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());
+                this->addOption(storm::settings::OptionBuilder(moduleName, shortestPathMaxKOptionName, false, "Maximal number K of shortest paths to generate.").setIsAdvanced()
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxk", "Upper bound on number of generated paths. Default value is 10.").setDefaultValueUnsignedInteger(10).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());
@@ -46,6 +49,14 @@ namespace storm {
                 return this->getOption(counterexampleTypeOptionName).getArgumentByName("type").getValueAsString() == "mincmd";
             }
 
+            bool CounterexampleGeneratorSettings::isShortestPathGenerationSet() const {
+                return this->getOption(counterexampleTypeOptionName).getArgumentByName("type").getValueAsString() == "shortestpath";
+            }
+
+            size_t CounterexampleGeneratorSettings::getShortestPathMaxK() const {
+                return this->getOption(shortestPathMaxKOptionName).getArgumentByName("maxk").getValueAsUnsignedInteger();
+            }
+            
             bool CounterexampleGeneratorSettings::isUseMilpBasedMinimalCommandSetGenerationSet() const {
                 return this->getOption(minimalCommandMethodOptionName).getArgumentByName("method").getValueAsString() == "milp";
             }

src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h

@@ -38,6 +38,20 @@ namespace storm {
                  */
                 bool isMinimalCommandSetGenerationSet() const;
 
+                /*!
+                 * Retrieves whether the option to generate a shortest path counterexample was set.
+                 *
+                 * @return True iff a shortest path counterexample is to be generated.
+                 */
+                bool isShortestPathGenerationSet() const;
+
+                /*!
+                 * Retrieves the maximal number K of shortest paths which should be generated.
+                 *
+                 * @return The upper bound on the number of shortest paths.
+                 */
+                size_t getShortestPathMaxK() const;
+
                 /*!
                  * Retrieves whether the MILP-based technique is to be used to generate a minimal command set
                  * counterexample.
@@ -87,6 +101,7 @@ namespace storm {
                 static const std::string counterexampleOptionName;
                 static const std::string counterexampleOptionShortName;
                 static const std::string counterexampleTypeOptionName;
+                static const std::string shortestPathMaxKOptionName;
                 static const std::string minimalCommandMethodOptionName;
                 static const std::string encodeReachabilityOptionName;
                 static const std::string schedulerCutsOptionName;

src/storm/settings/modules/IOSettings.cpp

@@ -54,7 +54,7 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportDotOptionName, false, "If given, the loaded model will be written to the specified file in the dot format.").setIsAdvanced()
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportDotMaxWidthOptionName, false, "The maximal width for labels in the dot format. For longer lines a linebreak is inserted. Value 0 represents no linebreaks.").setIsAdvanced()
-                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("width", "The maximal line width for the dot format.").setDefaultValueUnsignedInteger(0).build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("width", "The maximal line width for the dot format. Default is 0 meaning no linebreaks.").setDefaultValueUnsignedInteger(0).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportJaniDotOptionName, false, "If given, the loaded jani model will be written to the specified file in the dot format.").setIsAdvanced()
                                         .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the file to which the model is to be written.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportCdfOptionName, false, "Exports the cumulative density function for reward bounded properties into a .csv file.").setIsAdvanced().setShortName(exportCdfOptionShortName).addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to an existing directory where the cdf files will be stored.").build()).build());