From e24c64e41ec05b414e222681b9a61e13fe80c9a2 Mon Sep 17 00:00:00 2001 From: dehnert Date: Mon, 21 Oct 2013 17:28:56 +0200 Subject: [PATCH] Refinement work on backward implications. Former-commit-id: 6f08189217ac5cb2b6c9220f6eee81b910583782 --- src/adapters/Z3ExpressionAdapter.h | 7 +- .../SMTMinimalCommandSetGenerator.h | 250 +++++++++++------- src/ir/Command.cpp | 4 + src/ir/Command.h | 7 + src/utility/IRUtility.h | 6 +- 5 files changed, 178 insertions(+), 96 deletions(-) diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h index d44bce569..e3864f4fc 100644 --- a/src/adapters/Z3ExpressionAdapter.h +++ b/src/adapters/Z3ExpressionAdapter.h @@ -39,10 +39,12 @@ namespace storm { expression->accept(this); z3::expr result = stack.top(); stack.pop(); + LOG4CPLUS_DEBUG(logger, "Returning " << result << "."); return result; } virtual void visit(ir::expressions::BinaryBooleanFunctionExpression* expression) { + LOG4CPLUS_DEBUG(logger, "Binary boolean function expression " << expression->toString() << "."); expression->getLeft()->accept(this); expression->getRight()->accept(this); @@ -98,6 +100,7 @@ namespace storm { } virtual void visit(ir::expressions::BinaryRelationExpression* expression) { + LOG4CPLUS_DEBUG(logger, "Binary boolean relation expression " << expression->toString() << "."); expression->getLeft()->accept(this); expression->getRight()->accept(this); @@ -170,7 +173,8 @@ namespace storm { } virtual void visit(ir::expressions::IntegerLiteralExpression* expression) { - stack.push(context.int_val(expression->getValueAsInt(nullptr))); + LOG4CPLUS_DEBUG(logger, "IntegerLiteralExpression " << expression->toString() << "."); + stack.push(context.int_val(expression->getValueAsInt(nullptr))); } virtual void visit(ir::expressions::UnaryBooleanFunctionExpression* expression) { @@ -204,6 +208,7 @@ namespace storm { } virtual void visit(ir::expressions::VariableExpression* expression) { + LOG4CPLUS_DEBUG(logger, "Variable " << expression->toString() << "."); stack.push(variableToExpressionMap.at(expression->getVariableName())); } diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h index f147ad6e2..a87653a71 100644 --- a/src/counterexamples/SMTMinimalCommandSetGenerator.h +++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h @@ -386,8 +386,9 @@ namespace storm { * @param solver The solver to use for the satisfiability evaluation. */ static void assertSymbolicCuts(storm::ir::Program const& program, storm::models::Mdp const& labeledMdp, VariableInformation const& variableInformation, RelevancyInformation const& relevancyInformation, z3::context& context, z3::solver& solver) { - std::map> precedingLabels; - std::set hasSynchronizingPredecessor; + + // A container storing the label sets that may precede a given label set. + std::map, std::set>> precedingLabelSets; // Get some data from the MDP for convenient access. storm::storage::SparseMatrix const& transitionMatrix = labeledMdp.getTransitionMatrix(); @@ -410,16 +411,7 @@ namespace storm { } if (choiceTargetsCurrentState) { - if (choiceLabeling.at(predecessorChoice).size() > 1) { - for (auto label : choiceLabeling.at(currentChoice)) { - hasSynchronizingPredecessor.insert(label); - } - } - for (auto labelToAdd : choiceLabeling[predecessorChoice]) { - for (auto labelForWhichToAdd : choiceLabeling[currentChoice]) { - precedingLabels[labelForWhichToAdd].insert(labelToAdd); - } - } + precedingLabelSets[choiceLabeling.at(currentChoice)].insert(choiceLabeling.at(predecessorChoice)); } } } @@ -467,108 +459,182 @@ namespace storm { initialStateExpression = initialStateExpression && (solverVariables.at(variable.getName()) == localContext.int_val(std::get<1>(*initialState).at(programVariableInformation.integerVariableToIndexMap.at(variable.getName())))); } - std::map> backwardImplications; + // Store the found implications in a container similar to the preceding label sets. + std::map, std::set>> backwardImplications; // Now check for possible backward cuts. - for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { - storm::ir::Module const& module = program.getModule(moduleIndex); + for (auto const& labelSetAndPrecedingLabelSetsPair : precedingLabelSets) { + + // Find out the commands for the currently considered label set. + std::vector> currentCommandVector; + for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { + storm::ir::Module const& module = program.getModule(moduleIndex); + + for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) { + storm::ir::Command const& command = module.getCommand(commandIndex); + + // If the current command is one of the commands we need to consider, store a reference to it in the container. + if (labelSetAndPrecedingLabelSetsPair.first.find(command.getGlobalIndex()) != labelSetAndPrecedingLabelSetsPair.first.end()) { + currentCommandVector.push_back(command); + } + } + } - for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) { - storm::ir::Command const& command = module.getCommand(commandIndex); + // Save the state of the solver so we can easily backtrack. + localSolver.push(); + + // Check if the command set is enabled in the initial state. + for (auto const& command : currentCommandVector) { + localSolver.add(expressionAdapter.translateExpression(command.get().getGuard())); + } + localSolver.add(initialStateExpression); + + z3::check_result checkResult = localSolver.check(); + localSolver.pop(); + localSolver.push(); - // If the label of the command is not relevant, skip it entirely. - if (relevancyInformation.relevantLabels.find(command.getGlobalIndex()) == relevancyInformation.relevantLabels.end()) continue; - - // If the label has a synchronizing predecessor, we also need to skip it, because the following - // procedure can only consider predecessors in isolation. - if(hasSynchronizingPredecessor.find(command.getGlobalIndex()) != hasSynchronizingPredecessor.end()) continue; - - // Save the state of the solver so we can easily backtrack. - localSolver.push(); + // If the solver reports unsat, then we know that the current selection is not enabled in the initial state. + if (checkResult == z3::unsat) { + LOG4CPLUS_DEBUG(logger, "Selection not enabled in initial state."); + std::unique_ptr guardConjunction; + if (currentCommandVector.size() == 1) { + guardConjunction = currentCommandVector.begin()->get().getGuard()->clone(); + } else if (currentCommandVector.size() > 1) { + std::vector>::const_iterator setIterator = currentCommandVector.begin(); + std::unique_ptr first = setIterator->get().getGuard()->clone(); + ++setIterator; + std::unique_ptr second = setIterator->get().getGuard()->clone(); + guardConjunction = std::unique_ptr(new storm::ir::expressions::BinaryBooleanFunctionExpression(std::move(first), std::move(second), storm::ir::expressions::BinaryBooleanFunctionExpression::AND)); + ++setIterator; + + while (setIterator != currentCommandVector.end()) { + guardConjunction = std::unique_ptr(new storm::ir::expressions::BinaryBooleanFunctionExpression(std::move(guardConjunction), setIterator->get().getGuard()->clone(), storm::ir::expressions::BinaryBooleanFunctionExpression::AND)); + ++setIterator; + } + } else { + throw storm::exceptions::InvalidStateException() << "Choice label set is empty."; + LOG4CPLUS_DEBUG(logger, "Choice label set is empty."); + } - // Check if the command is enabled in the initial state. - localSolver.add(expressionAdapter.translateExpression(command.getGuard())); - localSolver.add(initialStateExpression); + LOG4CPLUS_DEBUG(logger, "About to assert disjunction of negated guards."); + z3::expr guardExpression = localContext.bool_val(false); + bool firstAssignment = true; + for (auto const& command : currentCommandVector) { + if (firstAssignment) { + guardExpression = !expressionAdapter.translateExpression(command.get().getGuard()); + } else { + guardExpression = guardExpression | !expressionAdapter.translateExpression(command.get().getGuard()); + } + std::cout << command.get().getGuard()->toString() << std::endl; + } + localSolver.add(guardExpression); + LOG4CPLUS_DEBUG(logger, "Asserted disjunction of negated guards."); - z3::check_result checkResult = localSolver.check(); - localSolver.pop(); - localSolver.push(); - - if (checkResult == z3::unsat) { - localSolver.add(!expressionAdapter.translateExpression(command.getGuard())); + // Now check the possible preceding label sets for the essential ones. + for (auto const& precedingLabelSet : labelSetAndPrecedingLabelSetsPair.second) { + // Create a restore point so we can easily pop-off all weakest precondition expressions. localSolver.push(); - // We need to check all commands of the all modules, because they could enable the current - // command via a global variable. - for (uint_fast64_t otherModuleIndex = 0; otherModuleIndex < program.getNumberOfModules(); ++otherModuleIndex) { - storm::ir::Module const& otherModule = program.getModule(otherModuleIndex); + // Find out the commands for the currently considered preceding label set. + std::vector> currentPrecedingCommandVector; + for (uint_fast64_t moduleIndex = 0; moduleIndex < program.getNumberOfModules(); ++moduleIndex) { + storm::ir::Module const& module = program.getModule(moduleIndex); - for (uint_fast64_t otherCommandIndex = 0; otherCommandIndex < otherModule.getNumberOfCommands(); ++otherCommandIndex) { - storm::ir::Command const& otherCommand = otherModule.getCommand(otherCommandIndex); - - // We don't need to consider irrelevant commands and the command itself. - if (relevancyInformation.relevantLabels.find(otherCommand.getGlobalIndex()) == relevancyInformation.relevantLabels.end() - && relevancyInformation.knownLabels.find(otherCommand.getGlobalIndex()) == relevancyInformation.knownLabels.end()) { - continue; - } - if (moduleIndex == otherModuleIndex && commandIndex == otherCommandIndex) continue; + for (uint_fast64_t commandIndex = 0; commandIndex < module.getNumberOfCommands(); ++commandIndex) { + storm::ir::Command const& command = module.getCommand(commandIndex); - std::vector formulae; - formulae.reserve(otherCommand.getNumberOfUpdates()); - - localSolver.push(); - - for (uint_fast64_t updateIndex = 0; updateIndex < otherCommand.getNumberOfUpdates(); ++updateIndex) { - std::unique_ptr weakestPrecondition = storm::utility::ir::getWeakestPrecondition(command.getGuard(), {otherCommand.getUpdate(updateIndex)}); - - formulae.push_back(expressionAdapter.translateExpression(weakestPrecondition)); + // If the current command is one of the commands we need to consider, store a reference to it in the container. + if (precedingLabelSet.find(command.getGlobalIndex()) != precedingLabelSet.end()) { + currentPrecedingCommandVector.push_back(command); } - - assertDisjunction(localContext, localSolver, formulae); - - // If the assertions were satisfiable, this means the other command could successfully - // enable the current command. - if (localSolver.check() == z3::sat) { - backwardImplications[command.getGlobalIndex()].insert(otherCommand.getGlobalIndex()); + } + } + + // Assert all the guards of the preceding command set. + for (auto const& command : currentPrecedingCommandVector) { + localSolver.add(expressionAdapter.translateExpression(command.get().getGuard())); + } + + std::vector::const_iterator> iteratorVector; + for (auto const& command : currentPrecedingCommandVector) { + iteratorVector.push_back(command.get().getUpdates().begin()); + } + + // Iterate over all possible combinations of updates of the preceding command set. + std::vector formulae; + bool done = false; + while (!done) { + std::vector> currentUpdateCombination; + for (auto const& updateIterator : iteratorVector) { + currentUpdateCombination.push_back(*updateIterator); + } + + LOG4CPLUS_DEBUG(logger, "About to assert a weakest precondition."); + std::unique_ptr wp = storm::utility::ir::getWeakestPrecondition(guardConjunction->clone(), currentUpdateCombination); + formulae.push_back(expressionAdapter.translateExpression(wp)); + LOG4CPLUS_DEBUG(logger, "Asserted weakest precondition."); + + // Now try to move iterators to the next position if possible. If we could properly move it, we can directly + // move on to the next combination of updates. If we have to reset it to the start, we + uint_fast64_t k = iteratorVector.size(); + for (; k > 0; --k) { + ++iteratorVector[k - 1]; + if (iteratorVector[k - 1] == currentPrecedingCommandVector[k - 1].get().getUpdates().end()) { + iteratorVector[k - 1] = currentPrecedingCommandVector[k - 1].get().getUpdates().begin(); + } else { + break; } - - localSolver.pop(); } + + // If we had to reset all iterator to the start, we are done. + if (k == 0) { + done = true; + } + } + + // Now assert the disjunction of all weakest preconditions of all considered update combinations. + assertDisjunction(localContext, localSolver, formulae); + + LOG4CPLUS_DEBUG(logger, "Asserted disjunction of all weakest preconditions."); + + if (localSolver.check() == z3::sat) { + backwardImplications[labelSetAndPrecedingLabelSetsPair.first].insert(precedingLabelSet); } - // Remove the negated guard from the solver assertions. localSolver.pop(); } - // Restore state of solver where only the variable bounds are asserted. + // Popping the disjunction of negated guards from the solver stack. localSolver.pop(); } } std::vector formulae; - for (auto const& labelImplicationsPair : backwardImplications) { - // We only need to make this an implication if the label is not already known. If it is known, - // we can directly assert the disjunction of the implications. - if (relevancyInformation.knownLabels.find(labelImplicationsPair.first) == relevancyInformation.knownLabels.end()) { - formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelImplicationsPair.first))); - } - - std::set actualImplications; - std::set_intersection(labelImplicationsPair.second.begin(), labelImplicationsPair.second.end(), precedingLabels.at(labelImplicationsPair.first).begin(), precedingLabels.at(labelImplicationsPair.first).end(), std::inserter(actualImplications, actualImplications.begin())); - - // We should assert the implications if they are not already known to be true anyway. - std::set knownImplications; - std::set_intersection(actualImplications.begin(), actualImplications.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(knownImplications, knownImplications.begin())); - - if (knownImplications.empty()) { - for (auto label : actualImplications) { - formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); - } - - assertDisjunction(context, solver, formulae); - formulae.clear(); - } - } + std::cout << "got " << backwardImplications.size() << " backward implications." << std::endl; +// for (auto const& labelSetImplicationSetsPair : backwardImplications) { +// // We only need to make this an implication if the label is not already known. If it is known, +// // we can directly assert the disjunction of the implications. +// if (relevancyInformation.knownLabels.find(labelImplicationsPair.first) == relevancyInformation.knownLabels.end()) { +// formulae.push_back(!variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(labelImplicationsPair.first))); +// } +// +// std::set actualImplications; +// std::set_intersection(labelImplicationsPair.second.begin(), labelImplicationsPair.second.end(), precedingLabels.at(labelImplicationsPair.first).begin(), precedingLabels.at(labelImplicationsPair.first).end(), std::inserter(actualImplications, actualImplications.begin())); +// +// // We should assert the implications if they are not already known to be true anyway. +// std::set knownImplications; +// std::set_intersection(actualImplications.begin(), actualImplications.end(), relevancyInformation.knownLabels.begin(), relevancyInformation.knownLabels.end(), std::inserter(knownImplications, knownImplications.begin())); +// +// if (knownImplications.empty()) { +// for (auto label : actualImplications) { +// formulae.push_back(variableInformation.labelVariables.at(variableInformation.labelToIndexMap.at(label))); +// } +// +// std::cout << "actually asserting a backward implication." << std::endl; +// assertDisjunction(context, solver, formulae); +// formulae.clear(); +// } +// } } /*! @@ -1005,7 +1071,7 @@ namespace storm { bool isBorderState = false; for (auto currentChoice : relevancyInformation.relevantChoicesForRelevantStates.at(state)) { if (!storm::utility::set::isSubsetOf(choiceLabeling[currentChoice], commandSet)) { - for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = originalMdp.getTransitionMatrix().constColumnIteratorBegin(currentChoice), successorIte = originalMdp.getTransitionMatrix()x^.constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { + for (typename storm::storage::SparseMatrix::ConstIndexIterator successorIt = originalMdp.getTransitionMatrix().constColumnIteratorBegin(currentChoice), successorIte = originalMdp.getTransitionMatrix().constColumnIteratorEnd(currentChoice); successorIt != successorIte; ++successorIt) { if (unreachableRelevantStates.get(*successorIt)) { isBorderState = true; } diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp index 8437e6ad3..dbb1eef64 100644 --- a/src/ir/Command.cpp +++ b/src/ir/Command.cpp @@ -69,6 +69,10 @@ namespace storm { return this->updates[index]; } + std::vector const& Command::getUpdates() const { + return this->updates; + } + uint_fast64_t Command::getGlobalIndex() const { return this->globalIndex; } diff --git a/src/ir/Command.h b/src/ir/Command.h index d6ae39ee8..04efe8b86 100644 --- a/src/ir/Command.h +++ b/src/ir/Command.h @@ -93,6 +93,13 @@ namespace storm { */ storm::ir::Update const& getUpdate(uint_fast64_t index) const; + /*! + * Retrieves a vector of all updates associated with this command. + * + * @return A vector of updates associated with this command. + */ + std::vector const& getUpdates() const; + /*! * Retrieves the global index of the command, that is, a unique index over all modules. * diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h index 46a453b47..fdcf473a9 100644 --- a/src/utility/IRUtility.h +++ b/src/utility/IRUtility.h @@ -481,15 +481,15 @@ namespace storm { * @param expression The expression for which to build the weakest precondition. * @param update The update with respect to which to compute the weakest precondition. */ - std::unique_ptr getWeakestPrecondition(std::unique_ptr const& booleanExpression, std::vector const& updates) { + std::unique_ptr getWeakestPrecondition(std::unique_ptr const& booleanExpression, std::vector> const& updates) { std::map> variableToExpressionMap; // Construct the full substitution we need to perform later. for (auto const& update : updates) { - for (auto const& variableAssignmentPair : update.getBooleanAssignments()) { + for (auto const& variableAssignmentPair : update.get().getBooleanAssignments()) { variableToExpressionMap.emplace(variableAssignmentPair.first, *variableAssignmentPair.second.getExpression()); } - for (auto const& variableAssignmentPair : update.getIntegerAssignments()) { + for (auto const& variableAssignmentPair : update.get().getIntegerAssignments()) { variableToExpressionMap.emplace(variableAssignmentPair.first, *variableAssignmentPair.second.getExpression()); } }