From 7d464f580715227b4694d3ed70856a2714a6b9a2 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Mon, 27 Nov 2017 18:54:43 +0100 Subject: [PATCH] SMT encoding for voting gate via or/and construction --- .../modelchecker/dft/DFTASFChecker.cpp | 50 ++++++++++++++++--- .../modelchecker/dft/DFTASFChecker.h | 1 + 2 files changed, 44 insertions(+), 7 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 06bfd1cca..8704febe3 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,6 +1,7 @@ #include "DFTASFChecker.h" #include #include "storm/utility/file.h" +#include "storm/utility/bitoperations.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -476,17 +477,46 @@ namespace storm { 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"); + constraints.back()->setDescription("AND gate " + element->name()); 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"); + constraints.back()->setDescription("OR gate " + element->name()); break; case storm::storage::DFTElementType::VOT: - //TODO implement via and/or construction - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "SMT encoding of VOTs is not implemented yet."); + { + // VOTs are implemented via OR over ANDs with all possible combinations + auto vot = std::static_pointer_cast const>(element); + std::vector tmpVars; + size_t i = 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(i)); + tmpVars.push_back(varNames.size() - 1); + tmpTimePointVariables.push_back(varNames.size() - 1); + // AND over the selected children + constraints.push_back(std::make_shared(tmpVars.at(i), combinationChildren)); + constraints.back()->setDescription("VOT gate " + element->name() + ": AND no. " + std::to_string(i)); + // Generate next permutation + combination = nextBitPermutation(combination); + ++i; + } 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"); break; + } case storm::storage::DFTElementType::PAND: { // Constraint for PAND gate (constraint 3) @@ -494,7 +524,7 @@ namespace storm { 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"); + constraints.back()->setDescription("PAND gate " + element->name()); break; } case storm::storage::DFTElementType::POR: @@ -510,7 +540,7 @@ namespace storm { 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"); + constraints.back()->setDescription("POR gate " + element->name()); break; } case storm::storage::DFTElementType::SEQ: @@ -525,7 +555,7 @@ namespace storm { // 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 " + spare->name() + " claims first child"); + 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()); @@ -708,6 +738,12 @@ namespace storm { for (auto const& markovianVarEntry : markovianVariables) { stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl; } + if (!tmpTimePointVariables.empty()) { + stream << "; Temporary variables" << std::endl; + for (auto const& tmpVar : tmpTimePointVariables) { + stream << "(declare-fun " << varNames[tmpVar] << "() Int)" << std::endl; + } + } for (auto const& constraint : constraints) { if (!constraint->description().empty()) { stream << "; " << constraint->description() << std::endl; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index af4f257ca..33f209957 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -75,6 +75,7 @@ namespace storm { std::vector> constraints; std::map claimVariables; std::unordered_map markovianVariables; + std::vector tmpTimePointVariables; uint64_t notFailed; }; }