From 4591dba631111f31a65a5252b1ab622f70d91f0b Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 21 Dec 2017 18:46:34 +0100 Subject: [PATCH] made maxsat-based counterexample generation be applicable to DTMCs and MDPs --- resources/examples/testfiles/dtmc/die.pm | 2 +- src/storm-cli-utilities/model-handling.h | 13 ++++++---- src/storm/api/counterexamples.cpp | 4 ++-- src/storm/api/counterexamples.h | 2 +- .../SMTMinimalLabelSetGenerator.h | 11 +++++---- .../models/sparse/NondeterministicModel.h | 6 ++--- src/storm/utility/counterexamples.h | 24 +++++++++---------- 7 files changed, 34 insertions(+), 28 deletions(-) diff --git a/resources/examples/testfiles/dtmc/die.pm b/resources/examples/testfiles/dtmc/die.pm index 1873bb8c1..e41139001 100644 --- a/resources/examples/testfiles/dtmc/die.pm +++ b/resources/examples/testfiles/dtmc/die.pm @@ -1,5 +1,5 @@ // Knuth's model of a fair die using only fair coins -mdp +dtmc module die diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h index 8cf964ca5..4180bdc33 100644 --- a/src/storm-cli-utilities/model-handling.h +++ b/src/storm-cli-utilities/model-handling.h @@ -373,8 +373,7 @@ namespace storm { STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::NotSupportedException, "Counterexample generation is currently only supported for sparse models."); auto sparseModel = model->as>(); - STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for MDPs."); - auto mdp = sparseModel->template as>(); + STORM_LOG_THROW(sparseModel->isOfType(storm::models::ModelType::Dtmc) || sparseModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "Counterexample is currently only supported for discrete-time models."); auto counterexampleSettings = storm::settings::getModule(); if (counterexampleSettings.isMinimalCommandSetGenerationSet()) { @@ -387,9 +386,15 @@ namespace storm { printComputingCounterexample(property); storm::utility::Stopwatch watch(true); if (useMilp) { - counterexample = storm::api::computePrismHighLevelCounterexampleMilp(program, mdp, 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::computePrismHighLevelCounterexampleMilp(program, sparseModel->template as>(), property.getRawFormula()); } else { - counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, mdp, property.getRawFormula()); + 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::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as>(), property.getRawFormula()); + } else { + counterexample = storm::api::computePrismHighLevelCounterexampleMaxSmt(program, sparseModel->template as>(), property.getRawFormula()); + } } watch.stop(); printCounterexample(counterexample, &watch); diff --git a/src/storm/api/counterexamples.cpp b/src/storm/api/counterexamples.cpp index 98c2f07bf..483dc57d4 100644 --- a/src/storm/api/counterexamples.cpp +++ b/src/storm/api/counterexamples.cpp @@ -10,9 +10,9 @@ namespace storm { return storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(env, program, *mdp, formula); } - std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula) { + std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula) { Environment env; - return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(env, program, *mdp, formula); + return storm::counterexamples::SMTMinimalLabelSetGenerator::computeCounterexample(env, program, *model, formula); } } diff --git a/src/storm/api/counterexamples.h b/src/storm/api/counterexamples.h index d8f3d1ddd..6481c4efd 100644 --- a/src/storm/api/counterexamples.h +++ b/src/storm/api/counterexamples.h @@ -8,7 +8,7 @@ namespace storm { std::shared_ptr computePrismHighLevelCounterexampleMilp(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula); - std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> mdp, std::shared_ptr const& formula); + std::shared_ptr computePrismHighLevelCounterexampleMaxSmt(storm::prism::Program const& program, std::shared_ptr> model, std::shared_ptr const& formula); } } diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h index e659209a3..5ad54a0f5 100644 --- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h @@ -119,7 +119,7 @@ namespace storm { // Retrieve some references for convenient access. storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = model.getNondeterministicChoiceIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now traverse all choices of all relevant states and check whether there is a successor target state. // If so, the associated labels become relevant. Also, if a choice of a relevant state has at least one @@ -1374,7 +1374,7 @@ namespace storm { } storm::storage::SparseMatrix const& transitionMatrix = subModel.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = subModel.getNondeterministicChoiceIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now determine which states and labels are actually reachable. boost::container::flat_set reachableLabels; @@ -1498,7 +1498,7 @@ namespace storm { } storm::storage::SparseMatrix const& transitionMatrix = subModel.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = subModel.getNondeterministicChoiceIndices(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); // Now determine which states and labels are actually reachable. boost::container::flat_set reachableLabels; @@ -1821,10 +1821,10 @@ namespace storm { auto startTime = std::chrono::high_resolution_clock::now(); // Create sub-model that only contains the choices allowed by the given command set. - storm::models::sparse::Model subModel = restrictModelToLabelSet(model, commandSet).first; + std::shared_ptr> subModel = restrictModelToLabelSet(model, commandSet).first; // Then determine all prob0E(psi) states that are reachable in the sub-model. - storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subModel.getTransitionMatrix(), subModel.getInitialStates(), phiStates, psiStates); + storm::storage::BitVector reachableProb0EStates = storm::utility::graph::getReachableStates(subModel->getTransitionMatrix(), subModel->getInitialStates(), phiStates, psiStates); // Create a queue of reachable prob0E(psi) states so we can check which commands need to be added // to give them a strategy that avoids psi states. @@ -1887,6 +1887,7 @@ namespace storm { } static boost::container::flat_set computeCounterexampleCommandSet(Environment const& env, storm::prism::Program program, storm::models::sparse::Model const& model, std::shared_ptr const& formula) { + STORM_LOG_THROW(model.isOfType(storm::models::ModelType::Dtmc) || model.isOfType(storm::models::ModelType::Mdp), storm::exceptions::NotSupportedException, "MaxSAT-based counterexample generation is supported only for discrete-time models."); std::cout << std::endl << "Generating minimal label counterexample for formula " << *formula << std::endl; 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."); diff --git a/src/storm/models/sparse/NondeterministicModel.h b/src/storm/models/sparse/NondeterministicModel.h index 2274e137a..ac8603e7f 100644 --- a/src/storm/models/sparse/NondeterministicModel.h +++ b/src/storm/models/sparse/NondeterministicModel.h @@ -19,10 +19,8 @@ namespace storm { * The base class of sparse nondeterministic models. */ template> - class NondeterministicModel: public Model { + class NondeterministicModel : public Model { public: - - /*! * Constructs a model from the given data. * @@ -39,6 +37,8 @@ namespace storm { */ std::vector const& getNondeterministicChoiceIndices() const; + using Model::getNumberOfChoices; + /*! * @param state State for which we want to know how many choices it has * diff --git a/src/storm/utility/counterexamples.h b/src/storm/utility/counterexamples.h index ec20c20cb..1ff429a5d 100644 --- a/src/storm/utility/counterexamples.h +++ b/src/storm/utility/counterexamples.h @@ -18,20 +18,20 @@ namespace storm { * @return The set of labels that is visited on all paths from any state to a target state. */ template - std::vector> getGuaranteedLabelSets(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { - STORM_LOG_THROW(mdp.getNumberOfChoices() == labelSets.size(), storm::exceptions::InvalidArgumentException, "The given number of labels does not match the number of choices."); + std::vector> getGuaranteedLabelSets(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set 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 MDP for convenient access. - storm::storage::SparseMatrix const& transitionMatrix = mdp.getTransitionMatrix(); - std::vector const& nondeterministicChoiceIndices = mdp.getNondeterministicChoiceIndices(); - storm::storage::SparseMatrix backwardTransitions = mdp.getBackwardTransitions(); + // Get some data from the model for convenient access. + storm::storage::SparseMatrix const& transitionMatrix = model.getTransitionMatrix(); + std::vector const& nondeterministicChoiceIndices = transitionMatrix.getRowGroupIndices(); + storm::storage::SparseMatrix backwardTransitions = model.getBackwardTransitions(); // Now we compute the set of labels that is present on all paths from the initial to the target states. - std::vector> analysisInformation(mdp.getNumberOfStates(), relevantLabels); + std::vector> analysisInformation(model.getNumberOfStates(), relevantLabels); std::queue worklist; - storm::storage::BitVector statesInWorkList(mdp.getNumberOfStates()); - storm::storage::BitVector markedStates(mdp.getNumberOfStates()); + 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) { @@ -108,12 +108,12 @@ namespace storm { * @return The set of labels that is executed on all paths from an initial state to a target state. */ template - boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Mdp const& mdp, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { - std::vector> guaranteedLabels = getGuaranteedLabelSets(mdp, labelSets, psiStates, relevantLabels); + boost::container::flat_set getGuaranteedLabelSet(storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, boost::container::flat_set const& relevantLabels) { + std::vector> guaranteedLabels = getGuaranteedLabelSets(model, labelSets, psiStates, relevantLabels); boost::container::flat_set knownLabels(relevantLabels); boost::container::flat_set tempIntersection; - for (auto initialState : mdp.getInitialStates()) { + 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); }