From 73900f1bbeb7da8ef662659b573376be32e1fcc6 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Tue, 7 Aug 2018 21:07:15 -0700 Subject: [PATCH] advanced stopping criteria for multi-counterexamples, additional measurements for cuts, an option to properly disable backward implications, and some cleaning --- .../SMTMinimalLabelSetGenerator.h | 215 +++++++++++------- 1 file changed, 128 insertions(+), 87 deletions(-) diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h index 74c973aa0..dd0ce03e9 100644 --- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h +++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h @@ -28,7 +28,20 @@ namespace storm { class Environment; namespace counterexamples { - + + /** + * Helper to avoid case disticinot between prism and jani + * Returns the number of edges/commands in a symbolic model description. + */ + size_t nrCommands(storm::storage::SymbolicModelDescription const& descr) { + if (descr.isJaniModel()) { + return descr.asJaniModel().getNumberOfEdges(); + } else { + assert(descr.isPrismModel()); + return descr.asPrismProgram().getNumberOfCommands(); + } + } + /*! * This class provides functionality to generate a minimal counterexample to a probabilistic reachability * property in terms of used labels. @@ -313,12 +326,18 @@ namespace storm { * @param context The Z3 context in which to build the expressions. * @param solver The solver to use for the satisfiability evaluation. */ - static void assertCuts(storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver) { + static std::chrono::milliseconds assertCuts(storm::storage::SymbolicModelDescription const& symbolicModel, storm::models::sparse::Model const& model, std::vector> const& labelSets, storm::storage::BitVector const& psiStates, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, storm::solver::SmtSolver& solver, bool addBackwardImplications) { // Walk through the model and // * identify labels enabled in initial states // * identify labels that can directly precede a given action // * identify labels that directly reach a target state // * identify labels that can directly follow a given action + auto assertCutsClock = std::chrono::high_resolution_clock::now(); + + // + if (addBackwardImplications) { + STORM_LOG_THROW(!symbolicModel.isJaniModel() || !symbolicModel.asJaniModel().usesAssignmentLevels(), storm::exceptions::NotSupportedException, "Counterexample generation with backward implications is not supported for indexed assignments"); + } boost::container::flat_set initialLabels; std::set> initialCombinations; @@ -334,6 +353,7 @@ namespace storm { storm::storage::BitVector const& initialStates = model.getInitialStates(); for (auto currentState : relevancyInformation.relevantStates) { + bool isInitial = initialStates.get(currentState); for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(currentState)) { // If the choice is a synchronization choice, we need to record it. @@ -344,7 +364,7 @@ namespace storm { } // If the state is initial, we need to add all the choice labels to the initial label set. - if (initialStates.get(currentState)) { + if (isInitial) { initialLabels.insert(labelSets[currentChoice].begin(), labelSets[currentChoice].end()); initialCombinations.insert(labelSets[currentChoice]); } @@ -378,6 +398,7 @@ namespace storm { for (auto const& successorEntry : transitionMatrix.getRow(predecessorChoice)) { if (successorEntry.getColumn() == currentState) { choiceTargetsCurrentState = true; + break; } } @@ -389,11 +410,10 @@ namespace storm { } } } - + // Store the found implications in a container similar to the preceding label sets. std::map, std::set>> backwardImplications; - - if (!symbolicModel.isJaniModel() || !symbolicModel.asJaniModel().usesAssignmentLevels()) { + if (addBackwardImplications) { // Create a new solver over the same variables as the given symbolic model description to use it for // determining the symbolic cuts. std::unique_ptr localSolver; @@ -587,8 +607,7 @@ namespace storm { // Iterate over all possible combinations of updates of the preceding command set. std::vector formulae; - bool done = false; - while (!done) { + while (true) { std::map currentVariableUpdateCombinationMap; for (auto const& updateIterator : iteratorVector) { for (auto const& variableUpdatePair : *updateIterator) { @@ -616,7 +635,7 @@ namespace storm { // If we had to reset all iterator to the start, we are done. if (k == 0) { - done = true; + break; } } @@ -722,85 +741,88 @@ namespace storm { assertDisjunction(solver, formulae, *variableInformation.manager); } } - - STORM_LOG_DEBUG("Asserting taken labels are followed and preceeded by another label if they are not a target label or an initial label, respectively."); - boost::container::flat_map, storm::expressions::Expression> labelSetToFormula; - for (auto const& labelSet : relevancyInformation.relevantLabelSets) { - storm::expressions::Expression labelSetFormula = variableInformation.manager->boolean(false); - // Compute the set of unknown labels on the left-hand side of the implication. - boost::container::flat_set unknownLhsLabels; - std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); - for (auto label : unknownLhsLabels) { - labelSetFormula = labelSetFormula || !variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); - } - - // Only build a constraint if the combination does not lead to a target state and - // no successor set is already known. - storm::expressions::Expression successorExpression; - if (targetCombinations.find(labelSet) == targetCombinations.end() && hasKnownSuccessor.find(labelSet) == hasKnownSuccessor.end()) { - successorExpression = variableInformation.manager->boolean(false); + if(addBackwardImplications) { - auto const& followingLabelSets = followingLabels.at(labelSet); + STORM_LOG_DEBUG("Asserting taken labels are followed and preceeded by another label if they are not a target label or an initial label, respectively."); + boost::container::flat_map, storm::expressions::Expression> labelSetToFormula; + for (auto const &labelSet : relevancyInformation.relevantLabelSets) { + storm::expressions::Expression labelSetFormula = variableInformation.manager->boolean(false); - for (auto const& followingSet : followingLabelSets) { - boost::container::flat_set tmpSet; - - // Check which labels of the current following set are not known. This set must be non-empty, because - // otherwise a successor combination would already be known and control cannot reach this point. - std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); - - // Construct an expression that enables all unknown labels of the current following set. - storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto label : tmpSet) { - conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + // Compute the set of unknown labels on the left-hand side of the implication. + boost::container::flat_set unknownLhsLabels; + std::set_difference(labelSet.begin(), labelSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(unknownLhsLabels, unknownLhsLabels.end())); + for (auto label : unknownLhsLabels) { + labelSetFormula = labelSetFormula || !variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + } + + // Only build a constraint if the combination does not lead to a target state and + // no successor set is already known. + storm::expressions::Expression successorExpression; + if (targetCombinations.find(labelSet) == targetCombinations.end() && hasKnownSuccessor.find(labelSet) == hasKnownSuccessor.end()) { + successorExpression = variableInformation.manager->boolean(false); + + auto const &followingLabelSets = followingLabels.at(labelSet); + + for (auto const &followingSet : followingLabelSets) { + boost::container::flat_set tmpSet; + + // Check which labels of the current following set are not known. This set must be non-empty, because + // otherwise a successor combination would already be known and control cannot reach this point. + std::set_difference(followingSet.begin(), followingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + + // Construct an expression that enables all unknown labels of the current following set. + storm::expressions::Expression conj = variableInformation.manager->boolean(true); + for (auto label : tmpSet) { + conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + } + successorExpression = successorExpression || conj; } - successorExpression = successorExpression || conj; + } else { + successorExpression = variableInformation.manager->boolean(true); } - } else { - successorExpression = variableInformation.manager->boolean(true); - } - // Constructed following cuts at this point. - - // Only build a constraint if the combination is no initial combination and no - // predecessor set is already known. - storm::expressions::Expression predecessorExpression; - if (initialCombinations.find(labelSet) == initialCombinations.end() && hasKnownPredecessor.find(labelSet) == hasKnownPredecessor.end()) { - predecessorExpression = variableInformation.manager->boolean(false); - + // Constructed following cuts at this point. + + // Only build a constraint if the combination is no initial combination and no + // predecessor set is already known. + storm::expressions::Expression predecessorExpression; + if (initialCombinations.find(labelSet) == initialCombinations.end() && hasKnownPredecessor.find(labelSet) == hasKnownPredecessor.end()) { + predecessorExpression = variableInformation.manager->boolean(false); + // std::cout << "labelSet" << std::endl; // for (auto const& e : labelSet) { // std::cout << e << ", "; // } // std::cout << std::endl; - auto const& preceedingLabelSets = backwardImplications.at(labelSet); + auto const &preceedingLabelSets = backwardImplications.at(labelSet); - for (auto const& preceedingSet : preceedingLabelSets) { - boost::container::flat_set tmpSet; - - // Check which labels of the current following set are not known. This set must be non-empty, because - // otherwise a predecessor combination would already be known and control cannot reach this point. - std::set_difference(preceedingSet.begin(), preceedingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); - - // Construct an expression that enables all unknown labels of the current following set. - storm::expressions::Expression conj = variableInformation.manager->boolean(true); - for (auto label : tmpSet) { - conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + for (auto const &preceedingSet : preceedingLabelSets) { + boost::container::flat_set tmpSet; + + // Check which labels of the current following set are not known. This set must be non-empty, because + // otherwise a predecessor combination would already be known and control cannot reach this point. + std::set_difference(preceedingSet.begin(), preceedingSet.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(tmpSet, tmpSet.end())); + + // Construct an expression that enables all unknown labels of the current following set. + storm::expressions::Expression conj = variableInformation.manager->boolean(true); + for (auto label : tmpSet) { + conj = conj && variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label)); + } + predecessorExpression = predecessorExpression || conj; } - predecessorExpression = predecessorExpression || conj; + } else { + predecessorExpression = variableInformation.manager->boolean(true); } - } else { - predecessorExpression = variableInformation.manager->boolean(true); + + labelSetFormula = labelSetFormula || (successorExpression && predecessorExpression); + + labelSetToFormula[labelSet] = labelSetFormula; } - - labelSetFormula = labelSetFormula || (successorExpression && predecessorExpression); - labelSetToFormula[labelSet] = labelSetFormula; - } - - for (auto const& labelSetFormula : labelSetToFormula) { - solver.add(labelSetFormula.second || getOtherSynchronizationEnabledFormula(labelSetFormula.first, synchronizingLabels, labelSetToFormula, variableInformation, relevancyInformation)); + for (auto const &labelSetFormula : labelSetToFormula) { + solver.add(labelSetFormula.second || getOtherSynchronizationEnabledFormula(labelSetFormula.first, synchronizingLabels, labelSetToFormula, variableInformation, relevancyInformation)); + } } STORM_LOG_DEBUG("Asserting synchronization cuts."); @@ -837,6 +859,9 @@ namespace storm { assertDisjunction(solver, formulae, *variableInformation.manager); } } + + auto endTime = std::chrono::high_resolution_clock::now(); + return std::chrono::duration_cast(endTime - assertCutsClock); } /*! @@ -1021,10 +1046,12 @@ namespace storm { */ static std::vector> createAdderPairs(VariableInformation const& variableInformation, std::vector> const& in) { std::vector> result; - - result.reserve(in.size() / 2 + in.size() % 2); - - for (uint_fast64_t index = 0; index < in.size() / 2; ++index) { + + + uint64_t maxIndex = in.size() / 2; + result.reserve(maxIndex + in.size() % 2); + + for (uint_fast64_t index = 0; index < maxIndex; ++index) { result.push_back(createAdder(variableInformation, in[2 * index], in[2 * index + 1])); } @@ -1586,9 +1613,11 @@ namespace storm { bool encodeReachability; bool useDynamicConstraints; bool silent = false; + bool addBackwardImplicationCuts = true; uint64_t continueAfterFirstCounterexampleUntil = 0; uint64_t maximumCounterexamples = 1; uint64_t multipleCounterexampleSizeCap = 100000000; + uint64_t maximumExtraIterations = 100000000; }; struct GeneratorStats { @@ -1596,8 +1625,11 @@ namespace storm { std::chrono::milliseconds solverTime; std::chrono::milliseconds modelCheckingTime; std::chrono::milliseconds analysisTime; + std::chrono::milliseconds cutTime; + uint64_t iterations; }; - + + /*! * Computes the minimal command set that is needed in the given model to exceed the given probability threshold for satisfying phi until psi. * @@ -1679,19 +1711,19 @@ namespace storm { // and subsequently relax that. variableInformation.adderVariables = assertAdder(*solver, variableInformation); variableInformation.auxiliaryVariables.push_back(assertLessOrEqualKRelaxed(*solver, variableInformation, 0)); - + + // As we are done with the setup at this point, stop the clock for the setup time. + totalSetupTime = std::chrono::high_resolution_clock::now() - setupTimeClock; + // (6) Add constraints that cut off a lot of suboptimal solutions. STORM_LOG_DEBUG("Asserting cuts."); - assertCuts(symbolicModel, model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); + stats.cutTime = assertCuts(symbolicModel, model, labelSets, psiStates, variableInformation, relevancyInformation, *solver, options.addBackwardImplicationCuts); STORM_LOG_DEBUG("Asserted cuts."); if (options.encodeReachability) { assertReachabilityCuts(model, labelSets, psiStates, variableInformation, relevancyInformation, *solver); STORM_LOG_DEBUG("Asserted reachability cuts."); } - - // As we are done with the setup at this point, stop the clock for the setup time. - totalSetupTime = std::chrono::high_resolution_clock::now() - setupTimeClock; - + // (7) Find the smallest set of commands that satisfies all constraints. If the probability of // satisfying phi until psi exceeds the given threshold, the set of labels is minimal and can be returned. // Otherwise, the current solution has to be ruled out and the next smallest solution is retrieved from @@ -1712,11 +1744,17 @@ namespace storm { uint_fast64_t lastSize = 0; uint_fast64_t iterations = 0; uint_fast64_t currentBound = 0; + uint64_t firstCounterexampleFound = 0; // The value is not queried before being set. std::vector maximalPropertyValue; uint_fast64_t zeroProbabilityCount = 0; - uint64_t smallestCounterexampleSize = model.getNumberOfChoices(); // Definitive u + size_t smallestCounterexampleSize = model.getNumberOfChoices(); // Definitive upper bound uint64_t progressDelay = storm::settings::getModule().getShowProgressDelay(); do { + ++iterations; + + if (result.size() > 0 && iterations > firstCounterexampleFound + options.maximumExtraIterations) { + break; + } STORM_LOG_DEBUG("Computing minimal command set."); solverClock = std::chrono::high_resolution_clock::now(); boost::optional> smallest = findSmallestCommandSet(*solver, variableInformation, currentBound); @@ -1781,19 +1819,21 @@ namespace storm { } } else { STORM_LOG_DEBUG("Found a counterexample."); + if (result.empty()) { + // If this is the first counterexample we find, we store when we found it. + firstCounterexampleFound = iterations; + } result.push_back(commandSet); if (options.maximumCounterexamples > result.size()) { STORM_LOG_DEBUG("Exclude counterexample for future."); ruleOutBiggerSolutions(*solver, commandSet, variableInformation, relevancyInformation); - } else { STORM_LOG_DEBUG("Stop searching for further counterexamples."); done = true; } - + smallestCounterexampleSize = std::min(smallestCounterexampleSize, commandSet.size()); } totalAnalysisTime += (std::chrono::high_resolution_clock::now() - analysisClock); - ++iterations; auto now = std::chrono::high_resolution_clock::now(); auto durationSinceLastMessage = std::chrono::duration_cast(now - timeOfLastMessage).count(); @@ -1816,6 +1856,7 @@ namespace storm { stats.setupTime = std::chrono::duration_cast(totalSetupTime); stats.modelCheckingTime = std::chrono::duration_cast(totalModelCheckingTime); stats.solverTime = std::chrono::duration_cast(totalSolverTime); + stats.iterations = iterations; if (storm::settings::getModule().isShowStatisticsSet()) { boost::container::flat_set allLabels;