From 7d56572ebac68210f0f6b42cd796c2de02bf2d60 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Fri, 24 Nov 2017 10:13:49 +0100 Subject: [PATCH] Recursive method for generating constrainst for 'trying to claim' --- .../modelchecker/dft/DFTASFChecker.cpp | 68 +++++++++++-------- .../modelchecker/dft/DFTASFChecker.h | 13 ++++ 2 files changed, 52 insertions(+), 29 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index fd1db1421..f112d2436 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -311,7 +311,7 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; - uint64_t notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed + notFailed = dft.nrBasicElements()+1; // Value indicating the element is not failed // Initialize variables for (size_t i = 0; i < dft.nrElements(); ++i) { @@ -410,38 +410,14 @@ namespace storm { constraints.back()->setDescription("Last child & claimed -> SPARE fails"); // Construct constraint for trying to claim next child - // We recursively build the function phi^s_i - // Last child: spare fails at same point as second to last child (otherwise case in constraint 7) - std::shared_ptr oldPhi = std::make_shared(timePointVariables.at(i), childVarIndices.at(children.size() - 2)); STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); - for (uint64_t j = 0; j+1 < children.size(); ++j) { - uint64_t currChild = children.size() - 2 - j; - uint64_t nextChild = currChild + 1; + for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails - uint64_t timeNextChild = childVarIndices.at(nextChild); // Moment when next child fails - uint64_t claimNextChild = getClaimVariableIndex(spare->id(), childVarIndices.at(nextChild)); // Moment the spare claims the next child - - // Check if next child is availble (first part of case distinction for constraint 7) - std::vector> ifcs; - // Next child is not yet failed - ifcs.push_back(std::make_shared(timeCurrChild, timeNextChild)); - // Child is not yet claimed by a different spare - for (auto const& otherSpare : children.at(nextChild)->parents()) { - if (otherSpare->id() == i) { - // not a different spare. - continue; - } - ifcs.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), children.at(nextChild)->id()), notFailed)); - } - // Claim next child (constraint 7) - // oldPhi 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(claimNextChild, timeCurrChild), oldPhi); - // Next iteration of phi - oldPhi = tryClaimC; - // If i-th child fails after being claimed, then try to claim (i+1)-th child (constraint 6) + // If i-th child fails after being claimed, then try to claim next child (constraint 6) + std::shared_ptr tryClaimC = generateTryToClaimConstraint(spare, currChild + 1, timeCurrChild); constraints.push_back(std::make_shared(std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), timeCurrChild), tryClaimC)); - constraints.back()->setDescription("Try to claim " + std::to_string(nextChild+1) + "th child"); + constraints.back()->setDescription("Try to claim " + std::to_string(currChild+2) + "th child"); } break; } @@ -483,6 +459,40 @@ namespace storm { constraints.back()->setDescription("Toplevel element should not fail"); } + std::shared_ptr DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const { + auto child = spare->children().at(childIndex); + uint64_t timeChild = timePointVariables.at(child->id()); // Moment when the child fails + uint64_t claimChild = getClaimVariableIndex(spare->id(), child->id()); // Moment the spare claims the child + + std::vector> noClaimingPossible; + if (childIndex + 1 < spare->children().size()) { + // Consider next child for claiming (second case in constraint 7) + noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint)); + } else { + // Last child: spare fails at same point as this child (third case in constraint 7) + noClaimingPossible.push_back(std::make_shared(timePointVariables.at(spare->id()), timepoint)); + } + std::shared_ptr elseCaseC = std::make_shared(noClaimingPossible); + + // Check if next child is availble (first case in constraint 7) + std::vector> claimingPossibleC; + // Next child is not yet failed + claimingPossibleC.push_back(std::make_shared(timepoint, timeChild)); + // Child is not yet claimed by a different spare + for (auto const& otherSpare : child->parents()) { + if (otherSpare->id() == spare->id()) { + // not a different spare. + continue; + } + claimingPossibleC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + } + + // Claim child if available + std::shared_ptr firstCaseC = std::make_shared(std::make_shared(claimingPossibleC), std::make_shared(claimChild, timepoint), elseCaseC); + return firstCaseC; + } + + void DFTASFChecker::toFile(std::string const& filename) { std::ofstream stream; storm::utility::openFile(filename, stream); diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index f05bd6595..d9331511b 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -50,12 +50,25 @@ namespace storm { private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; + + /** + * Generate constraint for 'spare (s) tries to claim the child (i) at the given timepoint (t)'. + * This corresponds to the function \phi^s_i(t) in constraint 7. + * + * @param spare Spare. + * @param childIndex Index of child to consider in spare children. + * @param timepoint Timepoint to try to claim. + * + * @return Constraint encoding the claiming. + */ + std::shared_ptr generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const; storm::storage::DFT const& dft; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; std::map claimVariables; + uint64_t notFailed; }; } }