From 34911003e016ba55d19aca939569382a88fcea2d Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 22 Nov 2017 15:06:55 +0100 Subject: [PATCH] Better comments for SMT generation --- .../modelchecker/dft/DFTASFChecker.cpp | 65 +++++++++++++++---- 1 file changed, 51 insertions(+), 14 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index b1a37aa90..ec0bcd4f9 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -271,7 +271,8 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; - // Convert all elements + + // Initialize variables for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); varNames.push_back("t_" + element->name()); @@ -294,21 +295,28 @@ namespace storm { } } - // BE + + // Generate constraints + + // No two BEs fail at the same time (first part of constraint 12) constraints.push_back(std::make_shared(beVariables)); constraints.back()->setDescription("No two BEs fail at the same time"); + + // All BEs have to fail (second part of constraint 12) for (auto const& beV : beVariables) { constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); } - // Claim variables - for (auto const& csvV : claimVariables) { - constraints.push_back(std::make_shared(csvV.second, 0, dft.nrBasicElements() + 1)); + + // Initialize claim variables in [1, |BE|+1] + for (auto const& claimVariable : claimVariables) { + constraints.push_back(std::make_shared(claimVariable.second, 0, dft.nrBasicElements() + 1)); } + // First child of each spare is claimed in the beginning for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if(element->isSpareGate()) { + if (element->isSpareGate()) { auto spare = std::static_pointer_cast const>(element); auto const& spareChild = spare->children().front(); constraints.push_back(std::make_shared(getClaimVariableIndex(spare->id(), spareChild->id()), 0)); @@ -317,7 +325,9 @@ namespace storm { } } + // Encoding for specific gates for (size_t i = 0; i < dft.nrElements(); ++i) { + // Get indices for gate children std::vector childVarIndices; if (dft.isGate(i)) { std::shared_ptr const> gate = dft.getGate(i); @@ -328,25 +338,39 @@ namespace storm { std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { + case storm::storage::DFTElementType::BE: + // BEs were already considered before + break; case storm::storage::DFTElementType::AND: + // Constraint for AND gate (constraint 1) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); constraints.back()->setDescription("And gate"); break; case storm::storage::DFTElementType::OR: + // Constraint for OR gate (constraint 2) constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); constraints.back()->setDescription("Or gate"); break; case storm::storage::DFTElementType::PAND: - constraints.push_back(std::make_shared(std::make_shared(childVarIndices), std::make_shared(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())), std::make_shared(timePointVariables.at(i), dft.nrBasicElements()+1))); + { + + // Constraint for PAND gate (constraint 3) + std::shared_ptr ifC = std::make_shared(childVarIndices); + std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), timePointVariables.at(childVarIndices.back())); + std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), dft.nrBasicElements()+1); + constraints.push_back(std::make_shared(ifC, thenC, elseC)); constraints.back()->setDescription("Pand gate"); + } case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); auto const& children = spare->children(); - - constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()), std::make_shared(timePointVariables.at(i), childVarIndices.back()))); + // If last child is claimed before failure the spare fails when the last child fails (constraint 5) + std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), children.back()->id()), childVarIndices.back()); + constraints.push_back(std::make_shared(leftC, std::make_shared(timePointVariables.at(i), childVarIndices.back()))); constraints.back()->setDescription("Last child & claimed -> spare fails"); + // Construct constraint for claiming std::shared_ptr elseCase = nullptr; for (uint64_t j = 0; j < children.size(); ++j) { uint64_t currChild = children.size() - 2 - j; @@ -354,22 +378,35 @@ namespace storm { uint64_t xv = childVarIndices.at(currChild); // if v is the child, xv is the time x fails. uint64_t csn = getClaimVariableIndex(spare->id(), childVarIndices.at(currChild+1)); // csn is the moment the spare claims the next child uint64_t xn = childVarIndices.at(currChild+1); // xn is the moment the next child fails + + // Generate constraint for trying to claim next child if (j == 0) { - elseCase = std::make_shared(timePointVariables.at(i), xv); + // Last child: spare fails at same point as xv (otherwise case in constraint 7) + elseCase = std::make_shared(timePointVariables.at(i), xv); } + // Next child is not yet failed ifcs.push_back(std::make_shared(xv, xn)); + + // Child is not yet claimed by a different spare (first part of case distinction for constraint 7) for (auto const& otherSpare : children.at(currChild+1)->parents()) { - if (otherSpare->id() == i) { continue; }// not a OTHER spare. + if (otherSpare->id() == i) { + // not an OTHER spare. + continue; + } ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(currChild+1)->id()), dft.nrBasicElements()+1)); } - std::shared_ptr ite = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); - elseCase = ite; - constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), ite)); + // Claim next child (constraint 7) + // elseCase contains the constraints for the recursive call to phi^s_{i+1} + std::shared_ptr tryClaimC = std::make_shared(std::make_shared(ifcs), std::make_shared(csn, xv), elseCase); + elseCase = tryClaimC; + // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6) + constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), xv), tryClaimC)); constraints.back()->setDescription(std::to_string(j+1) + " but last child & claimed"); } break; } default: + STORM_LOG_WARN("DFT element of type '" << element->type() << "' is ignored for SMT encoding."); break; } }