From 4f36e7e431266c7f188c12e057bf2ef7df1996a6 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Thu, 31 Oct 2019 20:05:26 +0100
Subject: [PATCH] Check if counterexample exists for k-shortest path

---
 .../api/counterexamples.cpp                   | 33 +++++++++++++------
 1 file changed, 23 insertions(+), 10 deletions(-)

diff --git a/src/storm-counterexamples/api/counterexamples.cpp b/src/storm-counterexamples/api/counterexamples.cpp
index f0927c869..0230595e1 100644
--- a/src/storm-counterexamples/api/counterexamples.cpp
+++ b/src/storm-counterexamples/api/counterexamples.cpp
@@ -6,22 +6,22 @@
 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) {
+        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.");
@@ -33,7 +33,10 @@ namespace storm {
             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);
+            bool strictBound = (probabilityOperator.getComparisonType() == storm::logic::ComparisonType::Less);
+            STORM_LOG_THROW(model->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException,
+                            "k-shortest paths is only supported for models with a unique initial state.");
+            size_t initialState = *(model->getInitialStates().begin());
 
             // Perform model checking to get target states
             Environment env;
@@ -43,6 +46,16 @@ namespace storm {
             std::unique_ptr<storm::modelchecker::CheckResult> subResult = modelchecker.check(env, eventuallyFormula.getSubformula());
             storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
 
+            // Check if counterexample is even possible
+            storm::storage::BitVector phiStates(model->getNumberOfStates(), true);
+            auto results = storm::modelchecker::helper::SparseDtmcPrctlHelper<double>::computeUntilProbabilities(env, false, model->getTransitionMatrix(),
+                                                                                                                 model->getBackwardTransitions(), phiStates,
+                                                                                                                 subQualitativeResult.getTruthValuesVector(), true);
+            double reachProb = results.at(initialState);
+            STORM_LOG_THROW((reachProb > threshold) || (strictBound && reachProb >= threshold), storm::exceptions::InvalidArgumentException,
+                            "Given probability threshold " << threshold << " cannot be " << (strictBound ? "achieved" : "exceeded")
+                                                           << " in model with maximal reachability probability of " << reachProb << ".");
+
             auto generator = storm::utility::ksp::ShortestPathsGenerator<double>(*model, subQualitativeResult.getTruthValuesVector());
             storm::counterexamples::PathCounterexample<double> cex(model);
             double probability = 0;
@@ -51,7 +64,7 @@ namespace storm {
                 cex.addPath(generator.getPathAsList(k), k);
                 probability += generator.getDistance(k);
                 // Check if accumulated probability mass is already enough
-                if ((probability >= threshold && !strictBound) || (probability > threshold)) {
+                if ((probability > threshold) || (strictBound && probability >= threshold && strictBound)) {
                     thresholdExceeded = true;
                     break;
                 }