From dc0be79172e9bc5e16a3412cca78c4213cd24c92 Mon Sep 17 00:00:00 2001 From: dehnert Date: Sun, 20 Oct 2013 21:17:26 +0200 Subject: [PATCH] Improved elimination of solutions in which the target states are not even reachable. Former-commit-id: f3d917ef7bfade2965e0e11d9fae96c39c85df65 --- .../MILPMinimalLabelSetGenerator.h | 2 +- .../SMTMinimalCommandSetGenerator.h | 57 ++++++++++++------- 2 files changed, 37 insertions(+), 22 deletions(-) diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h index fd619e18d..4c6628bdd 100644 --- a/src/counterexamples/MILPMinimalLabelSetGenerator.h +++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h @@ -195,7 +195,7 @@ namespace storm { */ static std::pair createGurobiEnvironmentAndModel() { GRBenv* env = nullptr; - int error = GRBloadenv(&env, "storm_gurobi.log"); + int error = GRBloadenv(&env, ""); if (error || env == NULL) { LOG4CPLUS_ERROR(logger, "Could not initialize Gurobi (" << GRBgeterrormsg(env) << ")."); throw storm::exceptions::InvalidStateException() << "Could not initialize Gurobi (" << GRBgeterrormsg(env) << ")."; diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index 8338846e0..5d442ba9f 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -129,16 +129,7 @@ namespace storm { relevancyInformation.relevantLabels = remainingLabels; } -// std::vector> guaranteedLabels = storm::utility::counterexamples::getGuaranteedLabelSets(labeledMdp, psiStates, relevancyInformation.relevantLabels); -// for (auto state : relevancyInformation.relevantStates) { -// std::cout << "state " << state << " ##########################################################" << std::endl; -// for (auto label : guaranteedLabels[state]) { -// std::cout << label << ", "; -// } -// std::cout << std::endl; -// } - - std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."; + std::cout << "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels." << std::endl; LOG4CPLUS_DEBUG(logger, "Found " << relevancyInformation.relevantLabels.size() << " relevant and " << relevancyInformation.knownLabels.size() << " known labels."); return relevancyInformation; @@ -952,7 +943,7 @@ namespace storm { return getUsedLabelSet(context, solver.get_model(), variableInformation); } - static void analyzeBadSolution(z3::context& context, z3::solver& solver, storm::models::Mdp const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& psiStates, std::set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { + static void analyzeBadSolution(z3::context& context, z3::solver& solver, storm::models::Mdp const& subMdp, storm::models::Mdp const& originalMdp, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::set const& commandSet, VariableInformation& variableInformation, RelevancyInformation const& relevancyInformation) { storm::storage::BitVector reachableStates(subMdp.getNumberOfStates()); // Initialize the stack for the DFS. @@ -1004,18 +995,35 @@ namespace storm { throw storm::exceptions::InvalidStateException() << "Target must be unreachable for this analysis."; } + storm::storage::BitVector statesThatCanReachTargetStates = storm::utility::graph::performProbGreater0E(subMdp, subMdp.getBackwardTransitions(), phiStates, psiStates); + std::vector> guaranteedLabelSets = storm::utility::counterexamples::getGuaranteedLabelSets(originalMdp, statesThatCanReachTargetStates, relevancyInformation.relevantLabels); + std::vector> const& choiceLabeling = originalMdp.getChoiceLabeling(); - std::set cutLabels; + std::set> cutLabels; + uint_fast64_t numberOfBorderStates = 0; for (auto state : reachableStates) { + bool isBorderState = false; for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { if (!storm::utility::set::isSubsetOf(choiceLabeling[currentChoice], commandSet)) { + isBorderState = true; + + std::set currentLabelSet; for (auto label : choiceLabeling[currentChoice]) { if (commandSet.find(label) == commandSet.end()) { - cutLabels.insert(label); + currentLabelSet.insert(label); } } + std::set notTakenImpliedChoices; + std::set_difference(guaranteedLabelSets[state].begin(), guaranteedLabelSets[state].end(), commandSet.begin(), commandSet.end(), std::inserter(notTakenImpliedChoices, notTakenImpliedChoices.begin())); + currentLabelSet.insert(notTakenImpliedChoices.begin(), notTakenImpliedChoices.end()); + + cutLabels.insert(currentLabelSet); } } + + if (isBorderState) { + ++numberOfBorderStates; + } } std::vector formulae; @@ -1024,12 +1032,18 @@ namespace storm { for (auto label : unknownReachableLabels) { formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); } - for (auto cutLabel : cutLabels) { - formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel))); + for (auto const& cutLabelSet : cutLabels) { + z3::expr cube = context.bool_val(true); + for (auto cutLabel : cutLabelSet) { + cube = cube && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(cutLabel)); + } + + formulae.push_back(cube); } LOG4CPLUS_DEBUG(logger, "Asserting reachability implications."); +// std::cout << "reachability implications:" << std::endl; // for (auto e : formulae) { // std::cout << e << ", "; // } @@ -1142,24 +1156,25 @@ namespace storm { maximalReachabilityProbability = std::max(maximalReachabilityProbability, result[state]); } - if (maximalReachabilityProbability <= probabilityThreshold) { + if (maximalReachabilityProbability < probabilityThreshold) { if (maximalReachabilityProbability == 0) { ++zeroProbabilityCount; // If there was no target state reachable, analyze the solution and guide the solver into the // right direction. - analyzeBadSolution(context, solver, subMdp, labeledMdp, psiStates, commandSet, variableInformation, relevancyInformation); + analyzeBadSolution(context, solver, subMdp, labeledMdp, phiStates, psiStates, commandSet, variableInformation, relevancyInformation); + } else { + // In case we have not yet exceeded the given threshold, we have to rule out the current solution. + ruleOutSolution(context, solver, commandSet, variableInformation); } - // In case we have not yet exceeded the given threshold, we have to rule out the current solution. - ruleOutSolution(context, solver, commandSet, variableInformation); } else { done = true; } ++iterations; endTime = std::chrono::high_resolution_clock::now(); - if (std::chrono::duration_cast(endTime - iterationTimer).count() > 5) { - std::cout << "Checked " << iterations << " models in " << std::chrono::duration_cast(endTime - startTime).count() << "s (out of which " << zeroProbabilityCount << " could not reach the target states). Current command set size is " << commandSet.size() << std::endl; + if (std::chrono::duration_cast(endTime - iterationTimer).count() >= 5) { + std::cout << "Checked " << iterations << " models in " << std::chrono::duration_cast(endTime - startTime).count() << "s (out of which " << zeroProbabilityCount << " could not reach the target states). Current command set size is " << commandSet.size() << "." << std::endl; iterationTimer = std::chrono::high_resolution_clock::now(); } } while (!done);