Added some more output to counterexample generators for benchmarks.

Former-commit-id: 7e64b90de6

src/counterexamples/MILPMinimalLabelSetGenerator.h

@@ -20,6 +20,7 @@ extern "C" {
 #endif
 
 #include "src/models/Mdp.h"
+#include "src/ir/program.h"
 #include "src/exceptions/NotImplementedException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidStateException.h"
@@ -161,11 +162,11 @@ namespace storm {
                         }
                     }
                 }
-                LOG4CPLUS_DEBUG(logger, "Found " << result.allRelevantLabels.size() << " relevant labels.");
 
                 // Finally, determine the set of labels that are known to be taken.
                 result.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, result.allRelevantLabels);
-                LOG4CPLUS_DEBUG(logger, "Found " << result.knownLabels.size() << " known labels.");
+                std::cout << "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels." << std::endl;
+                LOG4CPLUS_DEBUG(logger, "Found " << result.allRelevantLabels.size() << " relevant labels and " << result.knownLabels.size() << " known labels.");
 
                 return result;
             }
@@ -1325,7 +1326,7 @@ namespace storm {
              * @param formulaPtr A pointer to a safety formula. The outermost operator must be a probabilistic bound operator with a strict upper bound. The nested
              * formula can be either an unbounded until formula or an eventually formula.
              */
-            static void computeCounterexample(storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
+            static void computeCounterexample(storm::ir::Program const& program, storm::models::Mdp<T> const& labeledMdp, storm::property::prctl::AbstractPrctlFormula<double> const* formulaPtr) {
 #ifdef STORM_HAVE_GUROBI
                 std::cout << std::endl << "Generating minimal label counterexample for formula " << formulaPtr->toString() << std::endl;
                 // First, we need to check whether the current formula is an Until-Formula.
@@ -1369,6 +1370,10 @@ namespace storm {
                 auto endTime = std::chrono::high_resolution_clock::now();
                 std::cout << std::endl << "Computed minimal label set of size " << usedLabelSet.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms." << std::endl;
 
+                std::cout << "Resulting program:" << std::endl;
+                storm::ir::Program restrictedProgram(program);
+                restrictedProgram.restrictCommands(usedLabelSet);
+                std::cout << restrictedProgram.toString() << std::endl;
                 std::cout << std::endl << "-------------------------------------------" << std::endl;
                 
                 // FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set.

src/counterexamples/SMTMinimalCommandSetGenerator.h

@@ -120,6 +120,7 @@ namespace storm {
                     }
                 }
                 
+                
                 // Compute the set of labels that are known to be taken in any case.
                 relevancyInformation.knownLabels = storm::utility::counterexamples::getGuaranteedLabelSet(labeledMdp, psiStates, relevancyInformation.relevantLabels);
                 if (!relevancyInformation.knownLabels.empty()) {
@@ -137,6 +138,8 @@ namespace storm {
 //                    std::cout << std::endl;
 //                }
                 
+                std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels.";
+
                 LOG4CPLUS_DEBUG(logger, "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels.");
                 return relevancyInformation;
             }
@@ -1215,6 +1218,10 @@ namespace storm {
                 auto endTime = std::chrono::high_resolution_clock::now();
                 std::cout << std::endl << "Computed minimal label set of size " << labelSetIterationPair.first.size() << " in " << std::chrono::duration_cast<std::chrono::milliseconds>(endTime - startTime).count() << "ms (" << labelSetIterationPair.second << " models tested)." << std::endl;
                 
+                std::cout << "Resulting program:" << std::endl;
+                storm::ir::Program restrictedProgram(program);
+                restrictedProgram.restrictCommands(labelSetIterationPair.first);
+                std::cout << restrictedProgram.toString() << std::endl;
                 std::cout << std::endl << "-------------------------------------------" << std::endl;
                 
                 // FIXME: Return the DTMC that results from applying the max scheduler in the MDP restricted to the computed label set.

src/storm.cpp

@@ -356,7 +356,7 @@ int main(const int argc, const char* argv[]) {
                 // Now generate the counterexamples for each formula.
                 for (storm::property::prctl::AbstractPrctlFormula<double>* formulaPtr : formulaList) {
                     if (useMILP) {
-                        storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(*mdp, formulaPtr);
+                        storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr);
                     } else {
                         storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr);
                     }