From 22c644b42ced8c70552f738e8543adc2b80820e7 Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@gmail.com>
Date: Sun, 24 May 2020 11:03:30 -0700
Subject: [PATCH] more trace messages in counterexample generation

---
 .../counterexamples/SMTMinimalLabelSetGenerator.h      | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
index 4d4dd9629..64be9e83d 100644
--- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -1506,9 +1506,9 @@ namespace storm {
              * Also returns the Labelsets of the sub-model.
              */
             static std::pair<std::shared_ptr<storm::models::sparse::Model<T>>, std::vector<storm::storage::FlatSet<uint_fast64_t>>> restrictModelToLabelSet(storm::models::sparse::Model<T> const& model,  storm::storage::FlatSet<uint_fast64_t> const& filterLabelSet, boost::optional<uint64_t> absorbState = boost::none) {
-
                 bool customRowGrouping = model.isOfType(storm::models::ModelType::Mdp);
-                
+                STORM_LOG_TRACE("Restrict model to label set " <<  storm::storage::toString(filterLabelSet));
+
                 std::vector<storm::storage::FlatSet<uint_fast64_t>> resultLabelSet;
                 storm::storage::SparseMatrixBuilder<T> transitionMatrixBuilder(0, model.getTransitionMatrix().getColumnCount(), 0, true, customRowGrouping, model.getTransitionMatrix().getRowGroupCount());
 
@@ -1522,6 +1522,8 @@ namespace storm {
 
                         // If the choice is valid, copy over all its elements.
                         if (choiceValid) {
+                            STORM_LOG_TRACE("Choice " << choice << " has a valid label set " <<  storm::storage::toString(choiceLabelSet));
+
                             if (!stateHasValidChoice && customRowGrouping) {
                                 transitionMatrixBuilder.newRowGroup(currentRow);
                             }
@@ -1563,14 +1565,16 @@ namespace storm {
 
                 std::vector<T> allStatesResult;
                 
-                STORM_LOG_DEBUG("Invoking model checker.");
+                STORM_LOG_DEBUG("Invoking model checker on model with " << model.getNumberOfStates() << " states and " << model.getNumberOfTransitions() << " transitions.");
                 if (model.isOfType(storm::models::ModelType::Dtmc)) {
                     if (rewardName == boost::none) {
                         results.push_back(storm::utility::zero<T>());
                         allStatesResult = storm::modelchecker::helper::SparseDtmcPrctlHelper<T>::computeUntilProbabilities(env, false, model.getTransitionMatrix(), model.getBackwardTransitions(), phiStates, psiStates, false);
                         for (auto state : model.getInitialStates()) {
+                            STORM_LOG_TRACE("Found probability " << allStatesResult[state]);
                             results.back() = std::max(results.back(), allStatesResult[state]);
                         }
+                        STORM_LOG_TRACE("Final probability " << results.back());
                     } else {
                         for (auto const &rewName : rewardName.get()) {
                             results.push_back(storm::utility::zero<T>());