diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 41f688da0..f807f1db3 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,4 +1,5 @@ #include "DFTASFChecker.h" +#include "SmtConstraint.cpp" #include #include "storm/utility/file.h" #include "storm/utility/bitoperations.h" @@ -6,399 +7,8 @@ #include "storm/exceptions/NotSupportedException.h" namespace storm { - - namespace modelchecker { - - /* - * Variable[VarIndex] is the maximum of the others - */ - class IsMaximum : public DFTConstraint { - public: - IsMaximum(uint64_t varIndex, std::vector const& varIndices) : varIndex(varIndex), varIndices(varIndices) { - } - - virtual ~IsMaximum() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(and "; - // assert it is largereq than all values. - for (auto const& ovi : varIndices) { - sstr << "(>= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; - } - // assert it is one of the values. - sstr << "(or "; - for (auto const& ovi : varIndices) { - sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; - } - sstr << ")"; // end of the or - sstr << ")"; // end outer and. - return sstr.str(); - } - - private: - uint64_t varIndex; - std::vector varIndices; - }; - - - /* - * First is the minimum of the others - */ - class IsMinimum : public DFTConstraint { - public: - IsMinimum(uint64_t varIndex, std::vector const& varIndices) : varIndex(varIndex), varIndices(varIndices) { - } - - virtual ~IsMinimum() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(and "; - // assert it is smallereq than all values. - for (auto const& ovi : varIndices) { - sstr << "(<= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; - } - // assert it is one of the values. - sstr << "(or "; - for (auto const& ovi : varIndices) { - sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; - } - sstr << ")"; // end of the or - sstr << ")"; // end outer and. - return sstr.str(); - } - - private: - uint64_t varIndex; - std::vector varIndices; - }; - - - class BetweenValues : public DFTConstraint { - public: - BetweenValues(uint64_t varIndex, uint64_t lower, uint64_t upper) : varIndex(varIndex), upperBound(upper) , lowerBound(lower) { - } - virtual ~BetweenValues() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(and "; - sstr << "(>= " << varNames.at(varIndex) << " " << lowerBound << ")"; - sstr << "(<= " << varNames.at(varIndex) << " " << upperBound << ")"; - sstr << ")"; - return sstr.str(); - } - - private: - uint64_t varIndex; - uint64_t upperBound; - uint64_t lowerBound; - }; - - - class And : public DFTConstraint { - public: - And(std::vector> const& constraints) : constraints(constraints) { - } - virtual ~And() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - if (constraints.empty()) { - sstr << "true"; - } else { - sstr << "(and"; - for(auto const& c : constraints) { - sstr << " " << c->toSmtlib2(varNames); - } - sstr << ")"; - } - return sstr.str(); - } - - private: - std::vector> constraints; - - }; - - - class Or : public DFTConstraint { - public: - Or(std::vector> const& constraints) : constraints(constraints) { - } - - virtual ~Or() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - if (constraints.empty()) { - sstr << "false"; - } else { - sstr << "(or"; - for(auto const& c : constraints) { - sstr << " " << c->toSmtlib2(varNames); - } - sstr << ")"; - } - return sstr.str(); - } - - private: - std::vector> constraints; - - }; - - - class Implies : public DFTConstraint { - public: - Implies(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(=> " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")"; - return sstr.str(); - } - - private: - std::shared_ptr lhs; - std::shared_ptr rhs; - }; - - - class Iff : public DFTConstraint { - public: - Iff(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(= " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")"; - return sstr.str(); - } - - private: - std::shared_ptr lhs; - std::shared_ptr rhs; - }; - - - class IsTrue : public DFTConstraint { - public: - IsTrue(bool val) :value(val) { - } - - virtual ~IsTrue() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << (value ? "true" : "false"); - return sstr.str(); - } - - private: - bool value; - }; - - - class IsBoolValue : public DFTConstraint { - public: - IsBoolValue(uint64_t varIndex, bool val) : varIndex(varIndex), value(val) { - } - - virtual ~IsBoolValue() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - assert(varIndex < varNames.size()); - if (value) { - sstr << varNames.at(varIndex); - } else { - sstr << "(not " << varNames.at(varIndex) << ")"; - } - return sstr.str(); - } - - private: - uint64_t varIndex; - bool value; - }; - - - class IsConstantValue : public DFTConstraint { - public: - IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { - } - - virtual ~IsConstantValue() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - assert(varIndex < varNames.size()); - sstr << "(= " << varNames.at(varIndex) << " " << value << ")"; - return sstr.str(); - } - - private: - uint64_t varIndex; - uint64_t value; - }; - - - class IsLessConstant : public DFTConstraint { - public: - IsLessConstant(uint64_t varIndex, uint64_t val) :varIndex(varIndex), value(val) { - } - - virtual ~IsLessConstant() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - assert(varIndex < varNames.size()); - sstr << "(< " << varNames.at(varIndex) << " " << value << ")"; - return sstr.str(); - } - - private: - uint64_t varIndex; - uint64_t value; - }; - - class IsLessEqualConstant : public DFTConstraint { - public: - IsLessEqualConstant(uint64_t varIndex, uint64_t val) :varIndex(varIndex), value(val) { - } - - virtual ~IsLessEqualConstant() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - assert(varIndex < varNames.size()); - sstr << "(<= " << varNames.at(varIndex) << " " << value << ")"; - return sstr.str(); - } - - private: - uint64_t varIndex; - uint64_t value; - }; - - - class IsEqual : public DFTConstraint { - public: - IsEqual(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { - } - - virtual ~IsEqual() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; - } - - private: - uint64_t var1Index; - uint64_t var2Index; - }; - - class IsLess : public DFTConstraint { - public: - IsLess(uint64_t varIndex1, uint64_t varIndex2) :var1Index(varIndex1), var2Index(varIndex2) { - } - - virtual ~IsLess() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - return "(< " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; - } - - private: - uint64_t var1Index; - uint64_t var2Index; - }; - - - class PairwiseDifferent : public DFTConstraint { - public: - PairwiseDifferent(std::vector const& indices) : varIndices(indices) { - } - virtual ~PairwiseDifferent() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(distinct"; - // for(uint64_t i = 0; i < varIndices.size(); ++i) { - // for(uint64_t j = i + 1; j < varIndices.size(); ++j) { - // sstr << "()"; - // } - // } - for (auto const& varIndex : varIndices) { - sstr << " " << varNames.at(varIndex); - } - sstr << ")"; - return sstr.str(); - } - - private: - std::vector varIndices; - }; - - - class Sorted : public DFTConstraint { - public: - Sorted(std::vector varIndices) : varIndices(varIndices) { - } - - virtual ~Sorted() { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(and "; - for(uint64_t i = 1; i < varIndices.size(); ++i) { - sstr << "(<= " << varNames.at(varIndices.at(i-1)) << " " << varNames.at(varIndices.at(i)) << ")"; - } - sstr << ") "; - return sstr.str(); - } - - private: - std::vector varIndices; - }; - - - class IfThenElse : public DFTConstraint { - public: - IfThenElse(std::shared_ptr ifC, std::shared_ptr thenC, std::shared_ptr elseC) : ifConstraint(ifC), thenConstraint(thenC), elseConstraint(elseC) { - } - - std::string toSmtlib2(std::vector const& varNames) const override { - std::stringstream sstr; - sstr << "(ite " << ifConstraint->toSmtlib2(varNames) << " " << thenConstraint->toSmtlib2(varNames) << " " << elseConstraint->toSmtlib2(varNames) << ")"; - return sstr.str(); - } - - private: - std::shared_ptr ifConstraint; - std::shared_ptr thenConstraint; - std::shared_ptr elseConstraint; - }; - - + namespace modelchecker { DFTASFChecker::DFTASFChecker(storm::storage::DFT const& dft) : dft(dft) { // Intentionally left empty. } @@ -475,116 +85,26 @@ namespace storm { // 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 " + element->name()); + generateAndConstraint(i, childVarIndices, element); 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 " + element->name()); + generateOrConstraint(i, childVarIndices, element); break; case storm::storage::DFTElementType::VOT: - { - // VOTs are implemented via OR over ANDs with all possible combinations - auto vot = std::static_pointer_cast const>(element); - std::vector tmpVars; - size_t k = 0; - // Generate all permutations of k out of n - size_t combination = smallestIntWithNBitsSet(static_cast(vot->threshold())); - do { - // Construct selected children from combination - std::vector combinationChildren; - for (size_t j = 0; j < vot->nrChildren(); ++j) { - if (combination & (1 << j)) { - combinationChildren.push_back(childVarIndices.at(j)); - } - } - // Introduce temporary variable for this AND - varNames.push_back("v_" + vot->name() + "_" + std::to_string(k)); - size_t index = varNames.size() - 1; - tmpVars.push_back(index); - tmpTimePointVariables.push_back(index); - // AND over the selected children - constraints.push_back(std::make_shared(index, combinationChildren)); - constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(k)); - // Generate next permutation - combination = nextBitPermutation(combination); - ++k; - } while(combination < (1 << vot->nrChildren()) && combination != 0); - - // Constraint is OR over all possible combinations - constraints.push_back(std::make_shared(timePointVariables.at(i), tmpVars)); - constraints.back()->setDescription("VOT gate " + element->name() + ": OR"); + generateVotConstraint(i, childVarIndices, element); break; - } case storm::storage::DFTElementType::PAND: - { - // Constraint for PAND gate (constraint 3) - std::shared_ptr ifC = std::make_shared(childVarIndices); - std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), childVarIndices.back()); - std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); - constraints.push_back(std::make_shared(ifC, thenC, elseC)); - constraints.back()->setDescription("PAND gate " + element->name()); + generatePandConstraint(i, childVarIndices, element); break; - } case storm::storage::DFTElementType::POR: - { - // Constraint for POR gate - // First child fails before all others - std::vector> firstSmallestC; - uint64_t timeFirstChild = childVarIndices.front(); - for (uint64_t i = 1; i < childVarIndices.size(); ++i) { - firstSmallestC.push_back(std::make_shared(timeFirstChild, childVarIndices.at(i))); - } - std::shared_ptr ifC = std::make_shared(firstSmallestC); - std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), childVarIndices.front()); - std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), notFailed); - constraints.push_back(std::make_shared(ifC, thenC, elseC)); - constraints.back()->setDescription("POR gate " + element->name()); + generatePorConstraint(i, childVarIndices, element); break; - } case storm::storage::DFTElementType::SEQ: - { - // Constraint for SEQ gate (constraint 4) - // As the restriction is not a gate we have to enumerate its children here - auto seq = std::static_pointer_cast const>(element); - for (auto const& child : seq->children()) { - childVarIndices.push_back(timePointVariables.at(child->id())); - } - - constraints.push_back(std::make_shared(childVarIndices)); - constraints.back()->setDescription("SEQ gate " + element->name()); + generateSeqConstraint(childVarIndices, element); break; - } case storm::storage::DFTElementType::SPARE: - { - auto spare = std::static_pointer_cast const>(element); - auto const& children = spare->children(); - uint64_t firstChild = children.front()->id(); - uint64_t lastChild = children.back()->id(); - - // First child of each spare is claimed in the beginning - constraints.push_back(std::make_shared(getClaimVariableIndex(spare->id(), firstChild), 0)); - constraints.back()->setDescription("SPARE gate " + spare->name() + " claims first child"); - - // If last child is claimed before failure, then the spare fails when the last child fails (constraint 5) - std::shared_ptr leftC = std::make_shared(getClaimVariableIndex(spare->id(), lastChild), 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 trying to claim next child - STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); - for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { - uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails - - // 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(currChild+2) + "th child"); - } + generateSpareConstraint(i, childVarIndices, element); break; - } case storm::storage::DFTElementType::PDEP: // FDEPs are considered later in the Markovian constraints break; @@ -594,45 +114,153 @@ namespace storm { } } - // Only one spare can claim a child (constraint 8) - // and only not failed childs can be claimed (addition to constrain 8) - for (size_t i = 0; i < dft.nrElements(); ++i) { - std::shared_ptr const> element = dft.getElement(i); - if (element->isSpareGate()) { - auto spare = std::static_pointer_cast const>(element); - for (auto const& child : spare->children()) { - std::vector> additionalC; - uint64_t timeClaiming = getClaimVariableIndex(spare->id(), child->id()); - std::shared_ptr leftC = std::make_shared(timeClaiming, notFailed); - // Child must be operational at time of claiming - additionalC.push_back(std::make_shared(timeClaiming, timePointVariables.at(child->id()))); - // No other spare claims this child - for (auto const& parent : child->parents()) { - if (parent->isSpareGate() && parent->id() != spare->id()) { - // Different spare - additionalC.push_back(std::make_shared(getClaimVariableIndex(parent->id(), child->id()), notFailed)); - } - } - constraints.push_back(std::make_shared(leftC, std::make_shared(additionalC))); - constraints.back()->setDescription("Child " + child->name() + " must be operational at time of claiming by spare " + spare->name() + " and can only be claimed by one spare."); - } - } - } + // Constraint (8) + addClaimingConstraints(); // Handle dependencies addMarkovianConstraints(); + //TODO Move this out of convert method + // Toplevel element will not fail (part of constraint 13) constraints.push_back(std::make_shared(timePointVariables.at(dft.getTopLevelIndex()), notFailed)); 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 { + // Constraint Generator Functions + + void DFTASFChecker::generateAndConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + // Constraint for AND gate (constraint 1) + constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); + constraints.back()->setDescription("AND gate " + element->name()); + } + + void DFTASFChecker::generateOrConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + // Constraint for OR gate (constraint 2) + constraints.push_back(std::make_shared(timePointVariables.at(i), childVarIndices)); + constraints.back()->setDescription("OR gate " + element->name()); + } + + void DFTASFChecker::generateVotConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + auto vot = std::static_pointer_cast const>(element); + // VOTs are implemented via OR over ANDs with all possible combinations + std::vector tmpVars; + size_t k = 0; + // Generate all permutations of k out of n + size_t combination = smallestIntWithNBitsSet(static_cast(vot->threshold())); + do { + // Construct selected children from combination + std::vector combinationChildren; + for (size_t j = 0; j < vot->nrChildren(); ++j) { + if (combination & (1 << j)) { + combinationChildren.push_back(childVarIndices.at(j)); + } + } + // Introduce temporary variable for this AND + varNames.push_back("v_" + vot->name() + "_" + std::to_string(k)); + size_t index = varNames.size() - 1; + tmpVars.push_back(index); + tmpTimePointVariables.push_back(index); + // AND over the selected children + constraints.push_back(std::make_shared(index, combinationChildren)); + constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(k)); + // Generate next permutation + combination = nextBitPermutation(combination); + ++k; + } while (combination < (1 << vot->nrChildren()) && combination != 0); + + // Constraint is OR over all possible combinations + constraints.push_back(std::make_shared(timePointVariables.at(i), tmpVars)); + constraints.back()->setDescription("VOT gate " + element->name() + ": OR"); + } + + void DFTASFChecker::generatePandConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + // Constraint for PAND gate (constraint 3) + std::shared_ptr ifC = std::make_shared(childVarIndices); + std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), + childVarIndices.back()); + std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), + notFailed); + constraints.push_back(std::make_shared(ifC, thenC, elseC)); + constraints.back()->setDescription("PAND gate " + element->name()); + } + + void DFTASFChecker::generatePorConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + // Constraint for POR gate + // First child fails before all others + std::vector> firstSmallestC; + uint64_t timeFirstChild = childVarIndices.front(); + for (uint64_t i = 1; i < childVarIndices.size(); ++i) { + firstSmallestC.push_back(std::make_shared(timeFirstChild, childVarIndices.at(i))); + } + std::shared_ptr ifC = std::make_shared(firstSmallestC); + std::shared_ptr thenC = std::make_shared(timePointVariables.at(i), + childVarIndices.front()); + std::shared_ptr elseC = std::make_shared(timePointVariables.at(i), + notFailed); + constraints.push_back(std::make_shared(ifC, thenC, elseC)); + constraints.back()->setDescription("POR gate " + element->name()); + } + + void DFTASFChecker::generateSeqConstraint(std::vector childVarIndices, + std::shared_ptr const> element) { + // Constraint for SEQ gate (constraint 4) + // As the restriction is not a gate we have to enumerate its children here + auto seq = std::static_pointer_cast const>(element); + for (auto const &child : seq->children()) { + childVarIndices.push_back(timePointVariables.at(child->id())); + } + + constraints.push_back(std::make_shared(childVarIndices)); + constraints.back()->setDescription("SEQ gate " + element->name()); + } + + void DFTASFChecker::generateSpareConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + auto spare = std::static_pointer_cast const>(element); + auto const &children = spare->children(); + uint64_t firstChild = children.front()->id(); + uint64_t lastChild = children.back()->id(); + + // First child of each spare is claimed in the beginning + constraints.push_back(std::make_shared(getClaimVariableIndex(spare->id(), firstChild), 0)); + constraints.back()->setDescription("SPARE gate " + spare->name() + " claims first child"); + + // If last child is claimed before failure, then the spare fails when the last child fails (constraint 5) + std::shared_ptr leftC = std::make_shared( + getClaimVariableIndex(spare->id(), lastChild), 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 trying to claim next child + STORM_LOG_ASSERT(children.size() >= 2, "Spare has only one child"); + for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { + uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails + + // 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(currChild + 2) + "th child"); + } + } + + 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; + std::vector> noClaimingPossible; // Child cannot be claimed. if (childIndex + 1 < spare->children().size()) { // Consider next child for claiming (second case in constraint 7) @@ -641,10 +269,10 @@ namespace storm { // 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); + std::shared_ptr elseCaseC = std::make_shared(noClaimingPossible); - // Check if next child is availble (first case in constraint 7) - std::vector> claimingPossibleC; + // Check if next child is available (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 @@ -657,24 +285,59 @@ namespace storm { } // Claim child if available - std::shared_ptr firstCaseC = std::make_shared(std::make_shared(claimingPossibleC), std::make_shared(claimChild, timepoint), elseCaseC); + std::shared_ptr firstCaseC = std::make_shared( + std::make_shared(claimingPossibleC), std::make_shared(claimChild, timepoint), + elseCaseC); return firstCaseC; } + void DFTASFChecker::addClaimingConstraints() { + // Only one spare can claim a child (constraint 8) + // and only not failed children can be claimed (addition to constrain 8) + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + if (element->isSpareGate()) { + auto spare = std::static_pointer_cast const>(element); + for (auto const &child : spare->children()) { + std::vector> additionalC; + uint64_t timeClaiming = getClaimVariableIndex(spare->id(), child->id()); + std::shared_ptr leftC = std::make_shared(timeClaiming, + notFailed); + // Child must be operational at time of claiming + additionalC.push_back( + std::make_shared(timeClaiming, timePointVariables.at(child->id()))); + // No other spare claims this child + for (auto const &parent : child->parents()) { + if (parent->isSpareGate() && parent->id() != spare->id()) { + // Different spare + additionalC.push_back(std::make_shared( + getClaimVariableIndex(parent->id(), child->id()), notFailed)); + } + } + constraints.push_back(std::make_shared(leftC, std::make_shared(additionalC))); + constraints.back()->setDescription( + "Child " + child->name() + " must be operational at time of claiming by spare " + + spare->name() + " and can only be claimed by one spare."); + } + } + } + } + void DFTASFChecker::addMarkovianConstraints() { uint64_t nrMarkovian = dft.nrBasicElements(); // Vector containing (non-)Markovian constraints for each timepoint - std::vector>> markovianC(nrMarkovian); - std::vector>> nonMarkovianC(nrMarkovian); - std::vector>> notColdC(nrMarkovian); + std::vector>> markovianC(nrMarkovian); + std::vector>> nonMarkovianC(nrMarkovian); + std::vector>> notColdC(nrMarkovian); // All dependent events of a failed trigger have failed as well (constraint 9) for (size_t j = 0; j < dft.nrElements(); ++j) { std::shared_ptr const> element = dft.getElement(j); if (element->hasOutgoingDependencies()) { for (uint64_t i = 0; i < nrMarkovian; ++i) { - std::shared_ptr triggerFailed = std::make_shared(timePointVariables.at(j), i); - std::vector> depFailed; + std::shared_ptr triggerFailed = std::make_shared( + timePointVariables.at(j), i); + std::vector> depFailed; for (auto const& dependency : element->outgoingDependencies()) { for (auto const& depElement : dependency->dependentEvents()) { depFailed.push_back(std::make_shared(timePointVariables.at(depElement->id()), i)); @@ -697,8 +360,9 @@ namespace storm { if (be->hasIngoingDependencies()) { for (uint64_t i = 0; i < nrMarkovian -1; ++i) { - std::shared_ptr nextFailure = std::make_shared(timePointVariables.at(j), i+1); - std::vector> triggerFailed; + std::shared_ptr nextFailure = std::make_shared( + timePointVariables.at(j), i + 1); + std::vector> triggerFailed; for (auto const& dependency : be->ingoingDependencies()) { triggerFailed.push_back(std::make_shared(timePointVariables.at(dependency->triggerEvent()->id()), i)); } @@ -718,7 +382,8 @@ namespace storm { if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); for (uint64_t i = 0; i < nrMarkovian; ++i) { - std::shared_ptr nextFailure = std::make_shared(timePointVariables.at(j), i+1); + std::shared_ptr nextFailure = std::make_shared( + timePointVariables.at(j), i + 1); // BE is not cold // TODO: implement use of activation variables here bool cold = storm::utility::isZero(be->activeFailureRate()); diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index ee53b152d..3df55519e 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -4,30 +4,12 @@ #include #include +#include "SmtConstraint.h" #include "storm-dft/storage/dft/DFT.h" namespace storm { namespace modelchecker { - class DFTConstraint { - public: - virtual ~DFTConstraint() { - } - - virtual std::string toSmtlib2(std::vector const& varNames) const = 0; - - virtual std::string description() const { - return descript; - } - - void setDescription(std::string const& descr) { - descript = descr; - } - - private: - std::string descript; - }; - class SpareAndChildPair { public: SpareAndChildPair(uint64_t spareIndex, uint64_t childIndex) : spareIndex(spareIndex), childIndex(childIndex) { @@ -47,8 +29,15 @@ namespace storm { using ValueType = double; public: DFTASFChecker(storm::storage::DFT const&); + + /** + * Generate general variables and constraints for the DFT and store them in the corresponding maps and vectors + * + */ void convert(); void toFile(std::string const&); + + void toSolver(); private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; @@ -63,7 +52,63 @@ namespace storm { * * @return Constraint encoding the claiming. */ - std::shared_ptr generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const; + std::shared_ptr + generateTryToClaimConstraint(std::shared_ptr const> spare, + uint64_t childIndex, uint64_t timepoint) const; + + /** + * Add constraints encoding AND gates. + * This corresponds to constraint (1) + */ + void generateAndConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding OR gates. + * This corresponds to constraint (2) + */ + void generateOrConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding VOT gates. + + */ + void generateVotConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding PAND gates. + * This corresponds to constraint (3) + */ + void generatePandConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding POR gates. + */ + void generatePorConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding SEQ gates. + * This corresponds to constraint (4) + */ + void generateSeqConstraint(std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding SPARE gates. + * This corresponds to constraints (5),(6),(7) + */ + void generateSpareConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element); + + /** + * Add constraints encoding claiming rules. + * This corresponds to constraint (8) and addition + */ + void addClaimingConstraints(); /** * Add constraints encoding Markovian states. @@ -74,7 +119,7 @@ namespace storm { storm::storage::DFT const& dft; std::vector varNames; std::unordered_map timePointVariables; - std::vector> constraints; + std::vector> constraints; std::map claimVariables; std::unordered_map markovianVariables; std::vector tmpTimePointVariables; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp new file mode 100644 index 000000000..232431c21 --- /dev/null +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -0,0 +1,407 @@ +#include "DFTASFChecker.h" +#include + +namespace storm { + + namespace modelchecker { + + /* + * Variable[VarIndex] is the maximum of the others + */ + class IsMaximum : public SmtConstraint { + public: + IsMaximum(uint64_t varIndex, std::vector const &varIndices) : varIndex(varIndex), + varIndices(varIndices) { + } + + virtual ~IsMaximum() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(and "; + // assert it is largereq than all values. + for (auto const &ovi : varIndices) { + sstr << "(>= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + // assert it is one of the values. + sstr << "(or "; + for (auto const &ovi : varIndices) { + sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + sstr << ")"; // end of the or + sstr << ")"; // end outer and. + return sstr.str(); + } + + private: + uint64_t varIndex; + std::vector varIndices; + }; + + + /* + * First is the minimum of the others + */ + class IsMinimum : public SmtConstraint { + public: + IsMinimum(uint64_t varIndex, std::vector const &varIndices) : varIndex(varIndex), + varIndices(varIndices) { + } + + virtual ~IsMinimum() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(and "; + // assert it is smallereq than all values. + for (auto const &ovi : varIndices) { + sstr << "(<= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + // assert it is one of the values. + sstr << "(or "; + for (auto const &ovi : varIndices) { + sstr << "(= " << varNames.at(varIndex) << " " << varNames.at(ovi) << ") "; + } + sstr << ")"; // end of the or + sstr << ")"; // end outer and. + return sstr.str(); + } + + private: + uint64_t varIndex; + std::vector varIndices; + }; + + + class BetweenValues : public SmtConstraint { + public: + BetweenValues(uint64_t varIndex, uint64_t lower, uint64_t upper) : varIndex(varIndex), upperBound(upper), + lowerBound(lower) { + } + + virtual ~BetweenValues() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(and "; + sstr << "(>= " << varNames.at(varIndex) << " " << lowerBound << ")"; + sstr << "(<= " << varNames.at(varIndex) << " " << upperBound << ")"; + sstr << ")"; + return sstr.str(); + } + + private: + uint64_t varIndex; + uint64_t upperBound; + uint64_t lowerBound; + }; + + + class And : public SmtConstraint { + public: + And(std::vector> const &constraints) : constraints(constraints) { + } + + virtual ~And() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + if (constraints.empty()) { + sstr << "true"; + } else { + sstr << "(and"; + for (auto const &c : constraints) { + sstr << " " << c->toSmtlib2(varNames); + } + sstr << ")"; + } + return sstr.str(); + } + + private: + std::vector> constraints; + + }; + + + class Or : public SmtConstraint { + public: + Or(std::vector> const &constraints) : constraints(constraints) { + } + + virtual ~Or() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + if (constraints.empty()) { + sstr << "false"; + } else { + sstr << "(or"; + for (auto const &c : constraints) { + sstr << " " << c->toSmtlib2(varNames); + } + sstr << ")"; + } + return sstr.str(); + } + + private: + std::vector> constraints; + + }; + + + class Implies : public SmtConstraint { + public: + Implies(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(=> " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")"; + return sstr.str(); + } + + private: + std::shared_ptr lhs; + std::shared_ptr rhs; + }; + + + class Iff : public SmtConstraint { + public: + Iff(std::shared_ptr l, std::shared_ptr r) : lhs(l), rhs(r) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(= " << lhs->toSmtlib2(varNames) << " " << rhs->toSmtlib2(varNames) << ")"; + return sstr.str(); + } + + private: + std::shared_ptr lhs; + std::shared_ptr rhs; + }; + + + class IsTrue : public SmtConstraint { + public: + IsTrue(bool val) : value(val) { + } + + virtual ~IsTrue() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << (value ? "true" : "false"); + return sstr.str(); + } + + private: + bool value; + }; + + + class IsBoolValue : public SmtConstraint { + public: + IsBoolValue(uint64_t varIndex, bool val) : varIndex(varIndex), value(val) { + } + + virtual ~IsBoolValue() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + if (value) { + sstr << varNames.at(varIndex); + } else { + sstr << "(not " << varNames.at(varIndex) << ")"; + } + return sstr.str(); + } + + private: + uint64_t varIndex; + bool value; + }; + + + class IsConstantValue : public SmtConstraint { + public: + IsConstantValue(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsConstantValue() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(= " << varNames.at(varIndex) << " " << value << ")"; + return sstr.str(); + } + + private: + uint64_t varIndex; + uint64_t value; + }; + + + class IsLessConstant : public SmtConstraint { + public: + IsLessConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsLessConstant() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(< " << varNames.at(varIndex) << " " << value << ")"; + return sstr.str(); + } + + private: + uint64_t varIndex; + uint64_t value; + }; + + class IsLessEqualConstant : public SmtConstraint { + public: + IsLessEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsLessEqualConstant() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(<= " << varNames.at(varIndex) << " " << value << ")"; + return sstr.str(); + } + + private: + uint64_t varIndex; + uint64_t value; + }; + + + class IsEqual : public SmtConstraint { + public: + IsEqual(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsEqual() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + + + class IsLess : public SmtConstraint { + public: + IsLess(uint64_t varIndex1, uint64_t varIndex2) : var1Index(varIndex1), var2Index(varIndex2) { + } + + virtual ~IsLess() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + return "(< " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; + } + + private: + uint64_t var1Index; + uint64_t var2Index; + }; + + + class PairwiseDifferent : public SmtConstraint { + public: + PairwiseDifferent(std::vector const &indices) : varIndices(indices) { + } + + virtual ~PairwiseDifferent() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(distinct"; + // for(uint64_t i = 0; i < varIndices.size(); ++i) { + // for(uint64_t j = i + 1; j < varIndices.size(); ++j) { + // sstr << "()"; + // } + // } + for (auto const &varIndex : varIndices) { + sstr << " " << varNames.at(varIndex); + } + sstr << ")"; + return sstr.str(); + } + + private: + std::vector varIndices; + }; + + + class Sorted : public SmtConstraint { + public: + Sorted(std::vector varIndices) : varIndices(varIndices) { + } + + virtual ~Sorted() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(and "; + for (uint64_t i = 1; i < varIndices.size(); ++i) { + sstr << "(<= " << varNames.at(varIndices.at(i - 1)) << " " << varNames.at(varIndices.at(i)) << ")"; + } + sstr << ") "; + return sstr.str(); + } + + private: + std::vector varIndices; + }; + + + class IfThenElse : public SmtConstraint { + public: + IfThenElse(std::shared_ptr ifC, std::shared_ptr thenC, + std::shared_ptr elseC) : ifConstraint(ifC), thenConstraint(thenC), + elseConstraint(elseC) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(ite " << ifConstraint->toSmtlib2(varNames) << " " << thenConstraint->toSmtlib2(varNames) + << " " << elseConstraint->toSmtlib2(varNames) << ")"; + return sstr.str(); + } + + private: + std::shared_ptr ifConstraint; + std::shared_ptr thenConstraint; + std::shared_ptr elseConstraint; + }; + } +} + diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.h b/src/storm-dft/modelchecker/dft/SmtConstraint.h new file mode 100644 index 000000000..ef5f6e073 --- /dev/null +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.h @@ -0,0 +1,24 @@ +#include + +namespace storm { + namespace modelchecker { + class SmtConstraint { + public: + virtual ~SmtConstraint() { + } + + virtual std::string toSmtlib2(std::vector const &varNames) const = 0; + + virtual std::string description() const { + return descript; + } + + void setDescription(std::string const &descr) { + descript = descr; + } + + private: + std::string descript; + }; + } +} \ No newline at end of file