diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index 81c20a68d..19b165f0a 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/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 const& labeledMdp, storm::property::prctl::AbstractPrctlFormula const* formulaPtr) { + static void computeCounterexample(storm::ir::Program const& program, storm::models::Mdp const& labeledMdp, storm::property::prctl::AbstractPrctlFormula 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(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. diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index e4c336a58..c2aa105ce 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/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(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. diff --git a/src/storm.cpp b/src/storm.cpp index 5c07c3c75..5d3a4c4f3 100644 --- a/src/storm.cpp +++ b/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* formulaPtr : formulaList) { if (useMILP) { - storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(*mdp, formulaPtr); + storm::counterexamples::MILPMinimalLabelSetGenerator::computeCounterexample(program, *mdp, formulaPtr); } else { storm::counterexamples::SMTMinimalCommandSetGenerator::computeCounterexample(program, constants, *mdp, formulaPtr); }