From b0abbb5088a56588590aff80b89ec2f679d717d3 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 29 Oct 2019 18:42:50 +0100 Subject: [PATCH] Support for k-shortest path counterexamples --- CHANGELOG.md | 1 + src/storm-cli-utilities/model-handling.h | 26 +++++++-- .../api/counterexamples.cpp | 56 +++++++++++++++++-- .../api/counterexamples.h | 5 +- .../counterexamples/PathCounterexample.cpp | 40 +++++++++++++ .../counterexamples/PathCounterexample.h | 25 +++++++++ .../CounterexampleGeneratorSettings.cpp | 13 ++++- .../modules/CounterexampleGeneratorSettings.h | 17 +++++- src/storm/settings/modules/IOSettings.cpp | 2 +- 9 files changed, 170 insertions(+), 15 deletions(-) create mode 100644 src/storm-counterexamples/counterexamples/PathCounterexample.cpp create mode 100644 src/storm-counterexamples/counterexamples/PathCounterexample.h diff --git a/CHANGELOG.md b/CHANGELOG.md index c67e2e75c..88296152d 100644 --- a/CHANGELOG.md +++ b/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 `) diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 815332974..1dc8a2370 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -540,27 +540,41 @@ namespace storm { auto counterexampleSettings = storm::settings::getModule(); if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { - bool useMilp = counterexampleSettings.isUseMilpBasedMinimalCommandSetGenerationSet(); for (auto const& property : input.properties) { std::shared_ptr 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."); - counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as>(), property.getRawFormula()); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, + "Counterexample generation using MILP is currently only supported for MDPs."); + counterexample = storm::api::computeHighLevelCounterexampleMilp(input.model.get(), sparseModel->template as>(), + 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>(), property.getRawFormula()); + counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), + property.getRawFormula()); } else { - counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), property.getRawFormula()); + counterexample = storm::api::computeHighLevelCounterexampleMaxSmt(input.model.get(), sparseModel->template as>(), + property.getRawFormula()); } } watch.stop(); printCounterexample(counterexample, &watch); } + } else if (counterexampleSettings.isShortestPathGenerationSet()) { + for (auto const& property : input.properties) { + std::shared_ptr 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>(), property.getRawFormula(), counterexampleSettings.getShortestPathMaxK()); + watch.stop(); + printCounterexample(counterexample, &watch); + } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The selected counterexample formalism is unsupported."); } diff --git a/src/storm-counterexamples/api/counterexamples.cpp b/src/storm-counterexamples/api/counterexamples.cpp index 5652beba6..f0927c869 100644 --- a/src/storm-counterexamples/api/counterexamples.cpp +++ b/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 computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> mdp, std::shared_ptr const& formula) { + + std::shared_ptr + computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> mdp, + std::shared_ptr const& formula) { Environment env; return storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(env, symbolicModel, *mdp, formula); } - - std::shared_ptr computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> model, std::shared_ptr const& formula) { + + std::shared_ptr + computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> model, + std::shared_ptr const& formula) { Environment env; return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(env, symbolicModel, *model, formula); } - + + std::shared_ptr + computeKShortestPathCounterexample(std::shared_ptr> model, std::shared_ptr const& formula, size_t maxK) { + // Only accept formulas of the form "P 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(); + 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> modelchecker(*model); + + storm::logic::EventuallyFormula const& eventuallyFormula = subformula.asEventuallyFormula(); + std::unique_ptr subResult = modelchecker.check(env, eventuallyFormula.getSubformula()); + storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult(); + + auto generator = storm::utility::ksp::ShortestPathsGenerator(*model, subQualitativeResult.getTruthValuesVector()); + storm::counterexamples::PathCounterexample 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>(cex); + } + } } diff --git a/src/storm-counterexamples/api/counterexamples.h b/src/storm-counterexamples/api/counterexamples.h index 6a5984991..4e0a9f931 100644 --- a/src/storm-counterexamples/api/counterexamples.h +++ b/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 { @@ -9,6 +10,8 @@ namespace storm { std::shared_ptr computeHighLevelCounterexampleMilp(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> mdp, std::shared_ptr const& formula); std::shared_ptr computeHighLevelCounterexampleMaxSmt(storm::storage::SymbolicModelDescription const& symbolicModel, std::shared_ptr> model, std::shared_ptr const& formula); - + + std::shared_ptr computeKShortestPathCounterexample(std::shared_ptr> model, std::shared_ptr const& formula, size_t maxK); + } } diff --git a/src/storm-counterexamples/counterexamples/PathCounterexample.cpp b/src/storm-counterexamples/counterexamples/PathCounterexample.cpp new file mode 100644 index 000000000..5d8f18762 --- /dev/null +++ b/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 + PathCounterexample::PathCounterexample(std::shared_ptr> model) : model(model) { + // Intentionally left empty. + } + + template + void PathCounterexample::addPath(std::vector path, size_t k) { + if (k >= shortestPaths.size()) { + shortestPaths.resize(k); + } + shortestPaths[k-1] = path; + } + + template + void PathCounterexample::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; + } +} diff --git a/src/storm-counterexamples/counterexamples/PathCounterexample.h b/src/storm-counterexamples/counterexamples/PathCounterexample.h new file mode 100644 index 000000000..41543687d --- /dev/null +++ b/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 + class PathCounterexample : public Counterexample { + public: + PathCounterexample(std::shared_ptr> model); + + void addPath(std::vector path, size_t k); + + void writeToStream(std::ostream& out) const override; + + private: + std::shared_ptr> model; + std::vector> shortestPaths; + }; + + } +} diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp index b0de2ca79..752da88be 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.cpp +++ b/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 cextype = {"mincmd"}; + std::vector 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 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()); @@ -45,6 +48,14 @@ namespace storm { bool CounterexampleGeneratorSettings::isMinimalCommandSetGenerationSet() const { 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"; diff --git a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h index 2e8fe1388..4fa9e77e0 100644 --- a/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h +++ b/src/storm-counterexamples/settings/modules/CounterexampleGeneratorSettings.h @@ -37,7 +37,21 @@ namespace storm { * @return True iff a minimal command set counterexample is to be generated. */ 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; diff --git a/src/storm/settings/modules/IOSettings.cpp b/src/storm/settings/modules/IOSettings.cpp index edfc2eaae..98219969e 100644 --- a/src/storm/settings/modules/IOSettings.cpp +++ b/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());