From d31fae859f5377e6becc97d620965810644814a4 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Tue, 26 Feb 2019 21:26:04 +0100 Subject: [PATCH 01/44] Added error handling of gates with restricton as child and changed order of topoSort and rank computation to ensure that rank is only computed for acyclic DFTs --- src/storm-dft/builder/DFTBuilder.cpp | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 87bd5f407..54eb06779 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -26,6 +26,9 @@ namespace storm { if (itFind != mElements.end()) { // Child found DFTElementPointer childElement = itFind->second; + STORM_LOG_THROW(!childElement->isRestriction(), storm::exceptions::WrongFormatException, + "Restictor " << childElement->name() << " is not allowed as child of gate " + << gate->name()); if(!childElement->isDependency()) { gate->pushBackChild(childElement); childElement->addParent(gate); @@ -82,14 +85,13 @@ namespace storm { } } - // Sort elements topologically + DFTElementVector elems = topoSort(); // compute rank - for (auto& elem : mElements) { + for (auto &elem : mElements) { computeRank(elem.second); } - DFTElementVector elems = topoSort(); // Set ids size_t id = 0; for(DFTElementPointer e : elems) { From 2ab7c34b4d45470e9059389242d0c66ee4787454 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Tue, 5 Mar 2019 15:50:14 +0100 Subject: [PATCH 02/44] Added tests for cycles and SEQ children --- resources/examples/testfiles/dft/cyclic.dft | 5 +++++ resources/examples/testfiles/dft/seqChild.dft | 5 +++++ src/test/storm-dft/api/DftParserTest.cpp | 10 ++++++++++ 3 files changed, 20 insertions(+) create mode 100644 resources/examples/testfiles/dft/cyclic.dft create mode 100644 resources/examples/testfiles/dft/seqChild.dft diff --git a/resources/examples/testfiles/dft/cyclic.dft b/resources/examples/testfiles/dft/cyclic.dft new file mode 100644 index 000000000..b683dcf42 --- /dev/null +++ b/resources/examples/testfiles/dft/cyclic.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" and "B"; +"B" and "C"; +"C" and "A" "D"; +"D" lambda=0.5 dorm=0.3; \ No newline at end of file diff --git a/resources/examples/testfiles/dft/seqChild.dft b/resources/examples/testfiles/dft/seqChild.dft new file mode 100644 index 000000000..ad68072c8 --- /dev/null +++ b/resources/examples/testfiles/dft/seqChild.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" and "B" "X"; +"X" seq "B" "C"; +"B" lambda=0.5 dorm=0.3; +"C" lambda=0.5 dorm=0.3; diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp index 4a19aed08..dfa7ad769 100644 --- a/src/test/storm-dft/api/DftParserTest.cpp +++ b/src/test/storm-dft/api/DftParserTest.cpp @@ -20,4 +20,14 @@ namespace { EXPECT_EQ(2ul, dft->nrBasicElements()); EXPECT_TRUE(storm::api::isWellFormed(*dft)); } + + TEST(DftParserTest, CatchCycles) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/cyclic.dft"; + EXPECT_THROW(storm::api::loadDFTGalileoFile(file), storm::exceptions::WrongFormatException); + } + + TEST(DftParserTest, CatchSeqChildren) { + std::string file = STORM_TEST_RESOURCES_DIR "/dft/seqChild.dft"; + EXPECT_THROW(storm::api::loadDFTGalileoFile(file), storm::exceptions::WrongFormatException); + } } From be86014007cfa096068db2f212dc748e23c3c9e2 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Mon, 18 Mar 2019 19:08:31 +0100 Subject: [PATCH 03/44] Added test for hecs-DFT --- resources/examples/testfiles/dft/hecs_2_2.dft | 40 +++++++++++++++++++ .../storm-dft/api/DftModelCheckerTest.cpp | 15 +++++++ 2 files changed, 55 insertions(+) create mode 100644 resources/examples/testfiles/dft/hecs_2_2.dft diff --git a/resources/examples/testfiles/dft/hecs_2_2.dft b/resources/examples/testfiles/dft/hecs_2_2.dft new file mode 100644 index 000000000..788efaf16 --- /dev/null +++ b/resources/examples/testfiles/dft/hecs_2_2.dft @@ -0,0 +1,40 @@ +toplevel "System"; +"System" or "System_1" "System_2"; +"System_1" or "PSF_1" "MSF_1" "BSF_1" "IF_1"; +"PSF_1" and "P_11" "P_12"; +"P_11" wsp "A_11" "A_1S"; +"P_12" wsp "A_12" "A_1S"; +"MSF_1" 3of5 "M_1_1" "M_1_2" "M_1_3" "M_1_4" "M_1_5"; +"BSF_1" and "BUS_11" "BUS_12"; +"IF_1" or "HW_1" "SW_1"; +"System_2" or "PSF_2" "MSF_2" "BSF_2" "IF_2"; +"PSF_2" and "P_21" "P_22"; +"P_21" wsp "A_21" "A_2S"; +"P_22" wsp "A_22" "A_2S"; +"MSF_2" 3of5 "M_2_1" "M_2_2" "M_2_3" "M_2_4" "M_2_5"; +"BSF_2" and "BUS_21" "BUS_22"; +"IF_2" or "HW_2" "SW_2"; +"A_11" lambda=1.0e-4 dorm=0; +"A_12" lambda=1.0e-4 dorm=0; +"A_1S" lambda=1.0e-4 dorm=0; +"M_1_1" lambda=6.0e-5 dorm=0; +"M_1_2" lambda=6.0e-5 dorm=0; +"M_1_3" lambda=6.0e-5 dorm=0; +"M_1_4" lambda=6.0e-5 dorm=0; +"M_1_5" lambda=6.0e-5 dorm=0; +"BUS_11" lambda=1.0e-6 dorm=0; +"BUS_12" lambda=1.0e-6 dorm=0; +"HW_1" lambda=5.0e-5 dorm=0; +"SW_1" lambda=6.0e-5 dorm=0; +"A_21" lambda=1.0e-4 dorm=0; +"A_22" lambda=1.0e-4 dorm=0; +"A_2S" lambda=1.0e-4 dorm=0; +"M_2_1" lambda=6.0e-5 dorm=0; +"M_2_2" lambda=6.0e-5 dorm=0; +"M_2_3" lambda=6.0e-5 dorm=0; +"M_2_4" lambda=6.0e-5 dorm=0; +"M_2_5" lambda=6.0e-5 dorm=0; +"BUS_21" lambda=1.0e-6 dorm=0; +"BUS_22" lambda=1.0e-6 dorm=0; +"HW_2" lambda=5.0e-5 dorm=0; +"SW_2" lambda=6.0e-5 dorm=0; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 6da316081..65e1e05d2 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -71,6 +71,17 @@ namespace { return boost::get(results[0]); } + double analyzeReliability(std::string const &file, double bound) { + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; + std::vector> properties = storm::api::extractFormulasFromProperties( + storm::api::parseProperties(property)); + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT( + *dft, properties, config.useSR, config.useMod, config.useDC, false); + return boost::get(results[0]); + } + private: DftAnalysisConfig config; }; @@ -184,4 +195,8 @@ namespace { EXPECT_EQ(result, storm::utility::infinity()); } + TYPED_TEST(DftModelCheckerTest, HecsMTTF) { + double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0); + EXPECT_FLOAT_EQ(result, 0.00021997582); + } } From 33b6ba6d8fbf7d474b7b0d00ae15dc55c4026f2a Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 10 Apr 2019 15:20:43 +0200 Subject: [PATCH 04/44] Refactoring of constraint generation --- .../modelchecker/dft/DFTASFChecker.cpp | 719 +++++------------- .../modelchecker/dft/DFTASFChecker.h | 87 ++- .../modelchecker/dft/SmtConstraint.cpp | 407 ++++++++++ .../modelchecker/dft/SmtConstraint.h | 24 + 4 files changed, 689 insertions(+), 548 deletions(-) create mode 100644 src/storm-dft/modelchecker/dft/SmtConstraint.cpp create mode 100644 src/storm-dft/modelchecker/dft/SmtConstraint.h 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 From 7cab3985c04c4b855061ee352cfcd9109a896120 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 10 Apr 2019 18:10:04 +0200 Subject: [PATCH 05/44] Added basis for SMT solver integration --- .../modelchecker/dft/DFTASFChecker.cpp | 29 +++++++ .../modelchecker/dft/DFTASFChecker.h | 4 +- .../modelchecker/dft/SmtConstraint.cpp | 85 +++++++++++++++++++ .../modelchecker/dft/SmtConstraint.h | 4 + 4 files changed, 119 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index f807f1db3..77fd60108 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -1,8 +1,12 @@ #include "DFTASFChecker.h" #include "SmtConstraint.cpp" #include + #include "storm/utility/file.h" #include "storm/utility/bitoperations.h" +#include "storm/solver/SmtSolver.h" +#include "storm/storage/expressions/ExpressionManager.h" +#include "storm/storage/expressions/Type.h" #include "storm/exceptions/NotImplementedException.h" #include "storm/exceptions/NotSupportedException.h" @@ -429,5 +433,30 @@ namespace storm { stream << "(check-sat)" << std::endl; storm::utility::closeFile(stream); } + + void DFTASFChecker::toSolver() { + std::shared_ptr manager(new storm::expressions::ExpressionManager()); + std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create( + *manager); + for (auto const &timeVarEntry : timePointVariables) { + manager->declareIntegerVariable(varNames[timeVarEntry.second]); + } + for (auto const &claimVarEntry : claimVariables) { + manager->declareIntegerVariable(varNames[claimVarEntry.second]); + } + for (auto const &markovianVarEntry : markovianVariables) { + manager->declareBooleanVariable(varNames[markovianVarEntry.second]); + } + if (!tmpTimePointVariables.empty()) { + for (auto const &tmpVar : tmpTimePointVariables) { + manager->declareIntegerVariable(varNames[tmpVar]); + } + } + for (auto const &constraint : constraints) { + solver->add(constraint->toExpression(varNames, manager)); + } + + //TODO Add porperties to check + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 3df55519e..f202b40e7 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -6,7 +6,7 @@ #include "SmtConstraint.h" #include "storm-dft/storage/dft/DFT.h" - +#include "storm/utility/solver.h" namespace storm { namespace modelchecker { @@ -29,14 +29,12 @@ 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: diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 232431c21..bfec8b438 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -34,6 +34,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; std::vector varIndices; @@ -69,6 +74,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; std::vector varIndices; @@ -93,6 +103,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; uint64_t upperBound; @@ -122,6 +137,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::vector> constraints; @@ -150,6 +170,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::vector> constraints; @@ -167,6 +192,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::shared_ptr lhs; std::shared_ptr rhs; @@ -184,6 +214,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::shared_ptr lhs; std::shared_ptr rhs; @@ -204,6 +239,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: bool value; }; @@ -228,6 +268,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; bool value; @@ -249,6 +294,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; uint64_t value; @@ -270,6 +320,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; uint64_t value; @@ -290,6 +345,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t varIndex; uint64_t value; @@ -308,6 +368,11 @@ namespace storm { return "(= " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t var1Index; uint64_t var2Index; @@ -326,6 +391,11 @@ namespace storm { return "(< " + varNames.at(var1Index) + " " + varNames.at(var2Index) + ")"; } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: uint64_t var1Index; uint64_t var2Index; @@ -355,6 +425,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::vector varIndices; }; @@ -378,6 +453,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::vector varIndices; }; @@ -397,6 +477,11 @@ namespace storm { return sstr.str(); } + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + //TODO + } + private: std::shared_ptr ifConstraint; std::shared_ptr thenConstraint; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.h b/src/storm-dft/modelchecker/dft/SmtConstraint.h index ef5f6e073..2487f9dfd 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.h +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.h @@ -1,4 +1,5 @@ #include +#include namespace storm { namespace modelchecker { @@ -9,6 +10,9 @@ namespace storm { virtual std::string toSmtlib2(std::vector const &varNames) const = 0; + virtual storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const = 0; + virtual std::string description() const { return descript; } From fc9befbe9e23ce437688b1c705edb3e3cd9a14d6 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 11 Apr 2019 14:22:13 +0200 Subject: [PATCH 06/44] Added toExpression functions for SMT constraints --- .../modelchecker/dft/DFTASFChecker.cpp | 23 +++-- .../modelchecker/dft/DFTASFChecker.h | 4 +- .../modelchecker/dft/SmtConstraint.cpp | 94 +++++++++++++++---- 3 files changed, 95 insertions(+), 26 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 77fd60108..7852426e8 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -4,6 +4,7 @@ #include "storm/utility/file.h" #include "storm/utility/bitoperations.h" +#include "storm-parsers/parser/ExpressionCreator.h" #include "storm/solver/SmtSolver.h" #include "storm/storage/expressions/ExpressionManager.h" #include "storm/storage/expressions/Type.h" @@ -123,12 +124,6 @@ namespace storm { // 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"); } // Constraint Generator Functions @@ -434,10 +429,12 @@ namespace storm { storm::utility::closeFile(stream); } - void DFTASFChecker::toSolver() { + std::vector DFTASFChecker::toSolver() { + std::vector resultVector; std::shared_ptr manager(new storm::expressions::ExpressionManager()); std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create( *manager); + //Add variables to manager for (auto const &timeVarEntry : timePointVariables) { manager->declareIntegerVariable(varNames[timeVarEntry.second]); } @@ -452,11 +449,21 @@ namespace storm { manager->declareIntegerVariable(varNames[tmpVar]); } } + // Add constraints to solver for (auto const &constraint : constraints) { solver->add(constraint->toExpression(varNames, manager)); } + // Set backtracking marker to check several properties without reconstructing DFT encoding + solver->push(); + + // Constraint that toplevel element will not fail (part of constraint 13) + std::shared_ptr tleNeverFailedConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), notFailed); + solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); + resultVector.push_back(solver->check()); + solver->pop(); - //TODO Add porperties to check + return resultVector; } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index f202b40e7..0f152e6fa 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -4,6 +4,7 @@ #include #include +#include "storm/solver/SmtSolver.h" #include "SmtConstraint.h" #include "storm-dft/storage/dft/DFT.h" #include "storm/utility/solver.h" @@ -35,7 +36,8 @@ namespace storm { */ void convert(); void toFile(std::string const&); - void toSolver(); + + std::vector toSolver(); private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index bfec8b438..34450d98f 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -1,4 +1,5 @@ #include "DFTASFChecker.h" +#include #include namespace storm { @@ -36,7 +37,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector outerAnd; + std::vector innerOr; + for (auto const &ovi : varIndices) { + outerAnd.push_back((manager->getVariableExpression(varNames.at(varIndex)) >= + manager->getVariableExpression(varNames.at(ovi)))); + innerOr.push_back((manager->getVariableExpression(varNames.at(varIndex)) == + manager->getVariableExpression(varNames.at(ovi)))); + } + outerAnd.push_back(disjunction(innerOr)); + return conjunction(outerAnd); } private: @@ -76,7 +86,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector outerAnd; + std::vector innerOr; + for (auto const &ovi : varIndices) { + outerAnd.push_back((manager->getVariableExpression(varNames.at(varIndex)) <= + manager->getVariableExpression(varNames.at(ovi)))); + innerOr.push_back((manager->getVariableExpression(varNames.at(varIndex)) == + manager->getVariableExpression(varNames.at(ovi)))); + } + outerAnd.push_back(disjunction(innerOr)); + return conjunction(outerAnd); } private: @@ -105,7 +124,8 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return (manager->getVariableExpression(varNames.at(varIndex)) >= lowerBound) && + (manager->getVariableExpression(varNames.at(varIndex)) <= upperBound); } private: @@ -139,7 +159,15 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + if (constraints.empty()) { + return manager->boolean(true); + } else { + std::vector conjuncts; + for (auto const &c : constraints) { + conjuncts.push_back(c->toExpression(varNames, manager)); + } + return conjunction(conjuncts); + } } private: @@ -172,7 +200,15 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + if (constraints.empty()) { + return manager->boolean(false); + } else { + std::vector disjuncts; + for (auto const &c : constraints) { + disjuncts.push_back(c->toExpression(varNames, manager)); + } + return disjunction(disjuncts); + } } private: @@ -194,7 +230,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return implies(lhs->toExpression(varNames, manager), rhs->toExpression(varNames, manager)); } private: @@ -216,7 +252,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return iff(lhs->toExpression(varNames, manager), rhs->toExpression(varNames, manager)); } private: @@ -241,7 +277,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->boolean(value); } private: @@ -270,7 +306,11 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + if (value) { + return manager->getVariableExpression(varNames.at(varIndex)); + } else { + return !(manager->getVariableExpression(varNames.at(varIndex))); + } } private: @@ -296,7 +336,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(varIndex)) == manager->integer(value); } private: @@ -322,7 +362,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(varIndex)) < value; } private: @@ -347,7 +387,7 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(varIndex)) <= value; } private: @@ -370,7 +410,8 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(var1Index)) == + manager->getVariableExpression(varNames.at(var2Index)); } private: @@ -393,7 +434,8 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return manager->getVariableExpression(varNames.at(var1Index)) < + manager->getVariableExpression(varNames.at(var2Index)); } private: @@ -427,7 +469,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector conjuncts; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + for (uint64_t j = i + 1; j < varIndices.size(); ++j) { + // check all elements pairwise for inequality + conjuncts.push_back(manager->getVariableExpression(varNames.at(varIndices.at(i))) != + manager->getVariableExpression(varNames.at(varIndices.at(j)))); + } + } + // take the conjunction of all pairwise inequalities + return conjunction(conjuncts); } private: @@ -455,9 +506,16 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + std::vector conjuncts; + for (uint64_t i = 1; i < varIndices.size(); ++i) { + conjuncts.push_back(manager->getVariableExpression(varNames.at(varIndices.at(i - 1))) <= + manager->getVariableExpression(varNames.at(varIndices.at(i)))); + } + // take the conjunction of all pairwise inequalities + return conjunction(conjuncts); } + private: std::vector varIndices; }; @@ -479,7 +537,9 @@ namespace storm { storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const override { - //TODO + return ite(ifConstraint->toExpression(varNames, manager), + thenConstraint->toExpression(varNames, manager), + elseConstraint->toExpression(varNames, manager)); } private: From 29b0c4a78f73797b9b563ee086a5ddd79a1a3fe1 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 11 Apr 2019 16:04:42 +0200 Subject: [PATCH 07/44] First version of SMT solver integration for DFT analysis --- src/storm-dft-cli/storm-dft.cpp | 3 +- src/storm-dft/api/storm-dft.cpp | 28 +++++++++++++++++++ src/storm-dft/api/storm-dft.h | 11 ++++++++ .../modelchecker/dft/DFTASFChecker.cpp | 2 +- .../modelchecker/dft/DFTASFChecker.h | 4 +-- 5 files changed, 43 insertions(+), 5 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index f6a7d3863..c59da090a 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -76,8 +76,7 @@ void processOptions() { if (faultTreeSettings.solveWithSMT()) { // Solve with SMT STORM_LOG_DEBUG("Running DFT analysis with use of SMT"); - storm::api::exportDFTToSMT(*dft, "test.smt2"); - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Only exported to SMT file 'test.smt2' but analysis is not supported."); + storm::api::analyzeDFTSMT(*dft, true); return; } #endif diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index bae04d1e0..2da0b5b2c 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -42,6 +42,34 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Export to SMT does not support this data type."); } + template<> + std::vector + analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { + storm::modelchecker::DFTASFChecker smtChecker(dft); + smtChecker.convert(); + std::vector results = smtChecker.toSolver(); + + if (printOutput) { + for (size_t i = 0; i < results.size(); ++i) { + std::string tmp = "unknonwn"; + if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) { + tmp = "SAT"; + } else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) { + tmp = "UNSAT"; + } + std::cout << "Query " << std::to_string(i) << " : " << tmp << std::endl; + } + } + return results; + } + + template<> + std::vector + analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "Analysis by SMT not supported for this data type."); + } + template<> std::pair, uint64_t> transformToGSPN(storm::storage::DFT const& dft) { storm::settings::modules::FaultTreeSettings const& ftSettings = storm::settings::getModule(); diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h index 8b4f0ae9c..2c060cd64 100644 --- a/src/storm-dft/api/storm-dft.h +++ b/src/storm-dft/api/storm-dft.h @@ -112,6 +112,17 @@ namespace storm { return results; } + /*! + * Analyze the DFT using the SMT encoding + * + * @param dft DFT. + * + * @return Result result vector + */ + template + std::vector + analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput); + /*! * Export DFT to JSON file. * diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 7852426e8..8436fd215 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -14,7 +14,7 @@ namespace storm { namespace modelchecker { - DFTASFChecker::DFTASFChecker(storm::storage::DFT const& dft) : dft(dft) { + DFTASFChecker::DFTASFChecker(storm::storage::DFT const &dft) : dft(dft) { // Intentionally left empty. } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 0f152e6fa..097ca0732 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -24,8 +24,8 @@ namespace storm { uint64_t spareIndex; uint64_t childIndex; }; - - + + class DFTASFChecker { using ValueType = double; public: From 4507b484d5a36b15e09f7fc70007bf9a45791096 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 17 Apr 2019 11:34:45 +0200 Subject: [PATCH 08/44] Re-added option to export DFTs to smtlib2 SMT files --- src/storm-dft-cli/storm-dft.cpp | 6 ++++++ src/storm-dft/api/storm-dft.cpp | 1 + src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 2 ++ src/storm-dft/modelchecker/dft/SmtConstraint.h | 11 +++++++++++ src/storm-dft/settings/modules/DftIOSettings.cpp | 14 ++++++++++++++ src/storm-dft/settings/modules/DftIOSettings.h | 15 +++++++++++++++ src/storm/solver/SmtSolver.h | 2 +- 7 files changed, 50 insertions(+), 1 deletion(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index c59da090a..7eaa1ffac 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -51,6 +51,12 @@ void processOptions() { return; } + if (dftIOSettings.isExportToSmt()) { + // Export to json + storm::api::exportDFTToSMT(*dft, dftIOSettings.getExportSmtFilename()); + return; + } + // Check well-formedness of DFT std::stringstream stream; if (!dft->checkWellFormedness(stream)) { diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 2da0b5b2c..32796b7e8 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -50,6 +50,7 @@ namespace storm { std::vector results = smtChecker.toSolver(); if (printOutput) { + // TODO add suitable output function, maybe add query descriptions for better readability for (size_t i = 0; i < results.size(); ++i) { std::string tmp = "unknonwn"; if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 8436fd215..da5daa574 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -456,6 +456,8 @@ namespace storm { // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); + //TODO put different queries in separate functions for further modularization + // Constraint that toplevel element will not fail (part of constraint 13) std::shared_ptr tleNeverFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), notFailed); diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.h b/src/storm-dft/modelchecker/dft/SmtConstraint.h index 2487f9dfd..56c66ca73 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.h +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.h @@ -8,8 +8,19 @@ namespace storm { virtual ~SmtConstraint() { } + /** Generate a string describing the constraint in Smtlib2 format + * + * @param varNames vector of variable names + * @return Smtlib2 format string + */ virtual std::string toSmtlib2(std::vector const &varNames) const = 0; + /** Generate an expression describing the constraint in Storm format + * + * @param varNames vector of variable names + * @param manager the expression manager used to handle the expressions + * @return the expression + */ virtual storm::expressions::Expression toExpression(std::vector const &varNames, std::shared_ptr manager) const = 0; diff --git a/src/storm-dft/settings/modules/DftIOSettings.cpp b/src/storm-dft/settings/modules/DftIOSettings.cpp index 2c4caeb8e..6a039341a 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.cpp +++ b/src/storm-dft/settings/modules/DftIOSettings.cpp @@ -25,6 +25,7 @@ namespace storm { const std::string DftIOSettings::minValueOptionName = "min"; const std::string DftIOSettings::maxValueOptionName = "max"; const std::string DftIOSettings::exportToJsonOptionName = "export-json"; + const std::string DftIOSettings::exportToSmtOptionName = "export-smt"; const std::string DftIOSettings::displayStatsOptionName = "show-dft-stats"; @@ -56,6 +57,11 @@ namespace storm { this->addOption(storm::settings::OptionBuilder(moduleName, exportToJsonOptionName, false, "Export the model to the Cytoscape JSON format.") .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "The name of the JSON file to export to.").build()) .build()); + this->addOption(storm::settings::OptionBuilder(moduleName, exportToSmtOptionName, false, + "Export the model as SMT encoding to the smtlib2 format.") + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", + "The name of the smtlib2 file to export to.").build()) + .build()); this->addOption(storm::settings::OptionBuilder(moduleName, displayStatsOptionName, false, "Print stats to stdout").build()); } @@ -122,6 +128,14 @@ namespace storm { return this->getOption(exportToJsonOptionName).getArgumentByName("filename").getValueAsString(); } + bool DftIOSettings::isExportToSmt() const { + return this->getOption(exportToSmtOptionName).getHasOptionBeenSet(); + } + + std::string DftIOSettings::getExportSmtFilename() const { + return this->getOption(exportToSmtOptionName).getArgumentByName("filename").getValueAsString(); + } + bool DftIOSettings::isDisplayStatsSet() const { return this->getOption(displayStatsOptionName).getHasOptionBeenSet(); } diff --git a/src/storm-dft/settings/modules/DftIOSettings.h b/src/storm-dft/settings/modules/DftIOSettings.h index d99e6d970..60369b36e 100644 --- a/src/storm-dft/settings/modules/DftIOSettings.h +++ b/src/storm-dft/settings/modules/DftIOSettings.h @@ -108,6 +108,13 @@ namespace storm { */ bool isExportToJson() const; + /*! + * Retrieves whether the export to smtlib2 file option was set. + * + * @return True if the export to smtlib2 file option was set. + */ + bool isExportToSmt() const; + /*! * Retrieves the name of the json file to export to. * @@ -115,6 +122,13 @@ namespace storm { */ std::string getExportJsonFilename() const; + /*! + * Retrieves the name of the smtlib2 file to export to. + * + * @return The name of the smtlib2 file to export to. + */ + std::string getExportSmtFilename() const; + /*! * Retrieves whether statistics for the DFT should be displayed. * @@ -142,6 +156,7 @@ namespace storm { static const std::string minValueOptionName; static const std::string maxValueOptionName; static const std::string exportToJsonOptionName; + static const std::string exportToSmtOptionName; static const std::string displayStatsOptionName; }; diff --git a/src/storm/solver/SmtSolver.h b/src/storm/solver/SmtSolver.h index 6d842500c..27a506ff0 100644 --- a/src/storm/solver/SmtSolver.h +++ b/src/storm/solver/SmtSolver.h @@ -50,7 +50,7 @@ namespace storm { storm::expressions::ExpressionManager const& getManager() const; private: - // The expression manager responsible for the variableswhose value can be requested via this model + // The expression manager responsible for the variables whose value can be requested via this model // reference. storm::expressions::ExpressionManager const& manager; }; From 1976a412986ffcb2392619ed8600e4302cc8d5c4 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 17 Apr 2019 14:07:15 +0200 Subject: [PATCH 09/44] Reworked solver integration --- src/storm-dft/api/storm-dft.cpp | 5 +++- .../modelchecker/dft/DFTASFChecker.cpp | 26 ++++++++++++------- .../modelchecker/dft/DFTASFChecker.h | 10 ++++++- 3 files changed, 29 insertions(+), 12 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 32796b7e8..961b5fd5d 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -47,7 +47,10 @@ namespace storm { analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { storm::modelchecker::DFTASFChecker smtChecker(dft); smtChecker.convert(); - std::vector results = smtChecker.toSolver(); + smtChecker.toSolver(); + std::vector results; + + results.push_back(smtChecker.checkTleNeverFailedQuery()); if (printOutput) { // TODO add suitable output function, maybe add query descriptions for better readability diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index da5daa574..5c26ca08f 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -429,10 +429,12 @@ namespace storm { storm::utility::closeFile(stream); } - std::vector DFTASFChecker::toSolver() { - std::vector resultVector; + void DFTASFChecker::toSolver() { + // First convert the DFT + convert(); + std::shared_ptr manager(new storm::expressions::ExpressionManager()); - std::unique_ptr solver = storm::utility::solver::SmtSolverFactory().create( + solver = storm::utility::solver::SmtSolverFactory().create( *manager); //Add variables to manager for (auto const &timeVarEntry : timePointVariables) { @@ -453,19 +455,23 @@ namespace storm { for (auto const &constraint : constraints) { solver->add(constraint->toExpression(varNames, manager)); } - // Set backtracking marker to check several properties without reconstructing DFT encoding - solver->push(); - //TODO put different queries in separate functions for further modularization + } + + storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() { + STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + // Set backtracking marker to check several properties without reconstructing DFT encoding + solver->push(); // Constraint that toplevel element will not fail (part of constraint 13) std::shared_ptr tleNeverFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), notFailed); - solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); - resultVector.push_back(solver->check()); + solver->add(tleNeverFailedConstr->toExpression(varNames, + std::make_shared( + solver->getManager()))); + storm::solver::SmtSolver::CheckResult res = solver->check(); solver->pop(); - - return resultVector; + return res; } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 097ca0732..bf448b0ba 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -37,7 +37,7 @@ namespace storm { void convert(); void toFile(std::string const&); - std::vector toSolver(); + void toSolver(); private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; @@ -115,8 +115,16 @@ namespace storm { * This corresponds to constraints (9), (10) and (11) */ void addMarkovianConstraints(); + + /** + * Check if the TLE of the DFT never fails + * + * @return "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown" + */ + storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery(); storm::storage::DFT const& dft; + std::shared_ptr solver = 0; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; From d06cf59ebaa07a66796ab4cd328e9353e62528b4 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 17 Apr 2019 18:49:08 +0200 Subject: [PATCH 10/44] Added SMT function to calculate lower bound for number of DFT failures needed for failure of TLE --- src/storm-dft/api/storm-dft.cpp | 7 ++- .../modelchecker/dft/DFTASFChecker.cpp | 55 +++++++++++++++++-- .../modelchecker/dft/DFTASFChecker.h | 49 +++++++++++++---- .../storm-dft/api/DftModelCheckerTest.cpp | 19 +++++++ 4 files changed, 113 insertions(+), 17 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 961b5fd5d..96c7604a4 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -51,11 +51,11 @@ namespace storm { std::vector results; results.push_back(smtChecker.checkTleNeverFailedQuery()); - + uint64_t lower_bound = smtChecker.getLeastFailureBound(); if (printOutput) { - // TODO add suitable output function, maybe add query descriptions for better readability + //TODO add suitable output function, maybe add query descriptions for better readability for (size_t i = 0; i < results.size(); ++i) { - std::string tmp = "unknonwn"; + std::string tmp = "unknown"; if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) { tmp = "SAT"; } else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) { @@ -63,6 +63,7 @@ namespace storm { } std::cout << "Query " << std::to_string(i) << " : " << tmp << std::endl; } + std::cout << "Lower bound: " << std::to_string(lower_bound) << std::endl; } return results; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 5c26ca08f..a8d31232d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -459,19 +459,66 @@ namespace storm { } storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() { - STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + // STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); // Constraint that toplevel element will not fail (part of constraint 13) std::shared_ptr tleNeverFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), notFailed); - solver->add(tleNeverFailedConstr->toExpression(varNames, - std::make_shared( - solver->getManager()))); + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); storm::solver::SmtSolver::CheckResult res = solver->check(); solver->pop(); return res; } + + storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithLeq(uint64_t bound) { + //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + + // Set backtracking marker to check several properties without reconstructing DFT encoding + solver->push(); + // Constraint that toplevel element can fail with less or equal 'bound' failures + std::shared_ptr tleNeverFailedConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), bound); + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); + storm::solver::SmtSolver::CheckResult res = solver->check(); + solver->pop(); + return res; + } + + void DFTASFChecker::setSolverTimeout(uint_fast64_t milliseconds) { + if (!solver) { + STORM_LOG_WARN("SMT Solver was not initialized, timeout setting ignored"); + } else { + solver->setTimeout(milliseconds); + } + } + + void DFTASFChecker::unsetSolverTimeout() { + if (!solver) { + STORM_LOG_WARN("SMT Solver was not initialized, timeout unsetting ignored"); + } else { + solver->unsetTimeout(); + } + } + + uint64_t DFTASFChecker::getLeastFailureBound() { + //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + + uint64_t bound = 0; + while (bound < notFailed) { + setSolverTimeout(10000); + storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithLeq(bound); + unsetSolverTimeout(); + if (tmp_res == storm::solver::SmtSolver::CheckResult::Sat || + tmp_res == storm::solver::SmtSolver::CheckResult::Unknown) { + return bound; + } + ++bound; + } + return bound; + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index bf448b0ba..5f4b97498 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -37,7 +37,44 @@ namespace storm { void convert(); void toFile(std::string const&); + /** + * Generates a new solver instance and prepares it for SMT checking of the DFT. Needs to be called before all queries to the solver + */ void toSolver(); + + /** + * Check if the TLE of the DFT never fails + * + * @return "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown" + */ + storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery(); + + /** + * Check if there exists a sequence of BE failures of given length such that the TLE of the DFT fails + * + * @param bound the length of the sequene + * @return "Sat" if such a sequence exists, "Unsat" if it does not, otherwise "Unknown" + */ + storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound); + + /** + * Get the minimal number of BEs necessary for the TLE to fail + * + * @return the minimal number + */ + uint64_t getLeastFailureBound(); + + /** + * Set the timeout of the solver + * + * @param milliseconds the timeout in milliseconds + */ + void setSolverTimeout(uint_fast64_t milliseconds); + + /** + * Unset the timeout for the solver + */ + void unsetSolverTimeout(); private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; @@ -72,7 +109,6 @@ namespace storm { /** * Add constraints encoding VOT gates. - */ void generateVotConstraint(size_t i, std::vector childVarIndices, std::shared_ptr const> element); @@ -107,7 +143,7 @@ namespace storm { /** * Add constraints encoding claiming rules. * This corresponds to constraint (8) and addition - */ + */ void addClaimingConstraints(); /** @@ -115,16 +151,9 @@ namespace storm { * This corresponds to constraints (9), (10) and (11) */ void addMarkovianConstraints(); - - /** - * Check if the TLE of the DFT never fails - * - * @return "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown" - */ - storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery(); storm::storage::DFT const& dft; - std::shared_ptr solver = 0; + std::shared_ptr solver = NULL; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 65e1e05d2..274d5c6e5 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -2,6 +2,7 @@ #include "storm-config.h" #include "storm-dft/api/storm-dft.h" +#include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-parsers/api/storm-parsers.h" namespace { @@ -71,6 +72,17 @@ namespace { return boost::get(results[0]); } + storm::solver::SmtSolver::CheckResult analyzeSMT(std::string const &file) { + std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + std::vector results; + + return smtChecker.checkTleNeverFailedQuery(); + } + double analyzeReliability(std::string const &file, double bound) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); EXPECT_TRUE(storm::api::isWellFormed(*dft)); @@ -199,4 +211,11 @@ namespace { double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0); EXPECT_FLOAT_EQ(result, 0.00021997582); } + + TYPED_TEST(DftModelCheckerTest, SmtTest) { + storm::solver::SmtSolver::CheckResult result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); + EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Unsat); + result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/pand.dft"); + EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Sat); + } } From 5d5487140fdf260f2aa32cb356d9bbe0d3a42603 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 24 Apr 2019 12:25:04 +0200 Subject: [PATCH 11/44] Fixed bound calculation for SMT encoding --- src/storm-dft/api/storm-dft.cpp | 6 +- .../modelchecker/dft/DFTASFChecker.cpp | 83 +++++++++++++++---- .../modelchecker/dft/DFTASFChecker.h | 36 +++++++- .../modelchecker/dft/SmtConstraint.cpp | 25 ++++++ .../storm-dft/api/DftModelCheckerTest.cpp | 2 +- 5 files changed, 127 insertions(+), 25 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 96c7604a4..5c9db7040 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -46,12 +46,12 @@ namespace storm { std::vector analyzeDFTSMT(storm::storage::DFT const &dft, bool printOutput) { storm::modelchecker::DFTASFChecker smtChecker(dft); - smtChecker.convert(); smtChecker.toSolver(); std::vector results; - results.push_back(smtChecker.checkTleNeverFailedQuery()); + results.push_back(smtChecker.checkTleNeverFailed()); uint64_t lower_bound = smtChecker.getLeastFailureBound(); + uint64_t upper_bound = smtChecker.getAlwaysFailedBound(); if (printOutput) { //TODO add suitable output function, maybe add query descriptions for better readability for (size_t i = 0; i < results.size(); ++i) { @@ -61,9 +61,9 @@ namespace storm { } else if (results.at(i) == storm::solver::SmtSolver::CheckResult::Unsat) { tmp = "UNSAT"; } - std::cout << "Query " << std::to_string(i) << " : " << tmp << std::endl; } std::cout << "Lower bound: " << std::to_string(lower_bound) << std::endl; + std::cout << "Upper bound: " << std::to_string(upper_bound) << std::endl; } return results; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index a8d31232d..7b61ea655 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -242,6 +242,13 @@ namespace storm { for (uint64_t currChild = 0; currChild < children.size() - 1; ++currChild) { uint64_t timeCurrChild = childVarIndices.at(currChild); // Moment when current child fails + // If trying to claim (i+1)-th child, either child claimed before or never claimed by other spare + // (additional constraint) + std::shared_ptr claimEarlyC = generateClaimEarlyConstraint(spare, currChild); + constraints.push_back(std::make_shared( + std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), + timeCurrChild), claimEarlyC)); + constraints.back()->setDescription("Ensure earliest possible claiming"); // 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); @@ -252,6 +259,28 @@ namespace storm { } } + std::shared_ptr + DFTASFChecker::generateClaimEarlyConstraint(std::shared_ptr const> spare, + uint64_t childIndex) const { + auto child = spare->children().at(childIndex + 1); + std::vector> constraintAggregator; + for (auto const &otherSpare : child->parents()) { + if (otherSpare->id() == spare->id()) { + // not a different spare. + continue; + } + std::vector> OrAggregator; + // Other spare has claimed before + OrAggregator.push_back(std::make_shared( + getClaimVariableIndex(otherSpare->id(), child->id()), timePointVariables.at(childIndex))); + // Other spare will never claim + OrAggregator.push_back(std::make_shared( + getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + constraintAggregator.push_back(std::make_shared(OrAggregator)); + } + return std::make_shared(constraintAggregator); + } + std::shared_ptr DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const { @@ -458,14 +487,14 @@ namespace storm { } - storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailedQuery() { - // STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithEq(uint64_t bound) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); - // Constraint that toplevel element will not fail (part of constraint 13) + // Constraint that toplevel element can fail with less or equal 'bound' failures std::shared_ptr tleNeverFailedConstr = std::make_shared( - timePointVariables.at(dft.getTopLevelIndex()), notFailed); + timePointVariables.at(dft.getTopLevelIndex()), bound); std::shared_ptr manager = solver->getManager().getSharedPointer(); solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); storm::solver::SmtSolver::CheckResult res = solver->check(); @@ -474,7 +503,7 @@ namespace storm { } storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleFailsWithLeq(uint64_t bound) { - //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); @@ -489,24 +518,25 @@ namespace storm { } void DFTASFChecker::setSolverTimeout(uint_fast64_t milliseconds) { - if (!solver) { - STORM_LOG_WARN("SMT Solver was not initialized, timeout setting ignored"); - } else { - solver->setTimeout(milliseconds); - } + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, timeout cannot be set"); + solver->setTimeout(milliseconds); } void DFTASFChecker::unsetSolverTimeout() { - if (!solver) { - STORM_LOG_WARN("SMT Solver was not initialized, timeout unsetting ignored"); - } else { - solver->unsetTimeout(); - } + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, timeout cannot be unset"); + solver->unsetTimeout(); } - uint64_t DFTASFChecker::getLeastFailureBound() { - //STORM_LOG_ERROR_COND(!solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + storm::solver::SmtSolver::CheckResult DFTASFChecker::checkTleNeverFailed() { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + return checkTleFailsWithEq(notFailed); + } + uint64_t DFTASFChecker::getLeastFailureBound() { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { + return notFailed; + } uint64_t bound = 0; while (bound < notFailed) { setSolverTimeout(10000); @@ -520,5 +550,24 @@ namespace storm { } return bound; } + + uint64_t DFTASFChecker::getAlwaysFailedBound() { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { + return notFailed; + } + uint64_t bound = notFailed - 1; + while (bound >= 0) { + setSolverTimeout(10000); + storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithEq(bound); + unsetSolverTimeout(); + if (tmp_res == storm::solver::SmtSolver::CheckResult::Sat || + tmp_res == storm::solver::SmtSolver::CheckResult::Unknown) { + return bound; + } + --bound; + } + return bound; + } } } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 5f4b97498..2141694f5 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -47,23 +47,38 @@ namespace storm { * * @return "Sat" if TLE never fails, "Unsat" if it does, otherwise "Unknown" */ - storm::solver::SmtSolver::CheckResult checkTleNeverFailedQuery(); + storm::solver::SmtSolver::CheckResult checkTleNeverFailed(); /** - * Check if there exists a sequence of BE failures of given length such that the TLE of the DFT fails + * Check if there exists a sequence of BE failures of exactly given length such that the TLE of the DFT fails * * @param bound the length of the sequene * @return "Sat" if such a sequence exists, "Unsat" if it does not, otherwise "Unknown" */ + storm::solver::SmtSolver::CheckResult checkTleFailsWithEq(uint64_t bound); + + /** + * Check if there exists a sequence of BE failures of at least given length such that the TLE of the DFT fails + * + * @param bound the length of the sequence + * @return "Sat" if such a sequence exists, "Unsat" if it does not, otherwise "Unknown" + */ storm::solver::SmtSolver::CheckResult checkTleFailsWithLeq(uint64_t bound); /** - * Get the minimal number of BEs necessary for the TLE to fail + * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) * * @return the minimal number */ uint64_t getLeastFailureBound(); + /** + * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check) + * + * @return the number + */ + uint64_t getAlwaysFailedBound(); + /** * Set the timeout of the solver * @@ -79,6 +94,19 @@ namespace storm { private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; + /** + * Generate constraint for spares such that when trying to claim child (i+1), other spares either claimed it + * before or will never claim it + * + * @param spare Spare. + * @param childIndex Index of child to consider in spare children + * @param timepoint Timepoint to try to claim + * @return + */ + std::shared_ptr + generateClaimEarlyConstraint(std::shared_ptr const> spare, + 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. @@ -153,7 +181,7 @@ namespace storm { void addMarkovianConstraints(); storm::storage::DFT const& dft; - std::shared_ptr solver = NULL; + std::shared_ptr solver = nullptr; std::vector varNames; std::unordered_map timePointVariables; std::vector> constraints; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 34450d98f..e9bc2b220 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -395,6 +395,31 @@ namespace storm { uint64_t value; }; + class IsGreaterEqualConstant : public SmtConstraint { + public: + IsGreaterEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsGreaterEqualConstant() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(<= " << value << " " << varNames.at(varIndex) << ")"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(varIndex)) >= value; + } + + private: + uint64_t varIndex; + uint64_t value; + }; + class IsEqual : public SmtConstraint { public: diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 274d5c6e5..454c94f36 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -80,7 +80,7 @@ namespace { smtChecker.toSolver(); std::vector results; - return smtChecker.checkTleNeverFailedQuery(); + return smtChecker.checkTleNeverFailed(); } double analyzeReliability(std::string const &file, double bound) { From b89f8f8de433ef1fb5bf09a41b36e422db022235 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Wed, 24 Apr 2019 12:55:18 +0200 Subject: [PATCH 12/44] Refactoring of SMT tests --- .../storm-dft/api/DftModelCheckerTest.cpp | 19 -------------- src/test/storm-dft/api/DftSmtTest.cpp | 26 +++++++++++++++++++ 2 files changed, 26 insertions(+), 19 deletions(-) create mode 100644 src/test/storm-dft/api/DftSmtTest.cpp diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index 454c94f36..65e1e05d2 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -2,7 +2,6 @@ #include "storm-config.h" #include "storm-dft/api/storm-dft.h" -#include "storm-dft/modelchecker/dft/DFTASFChecker.h" #include "storm-parsers/api/storm-parsers.h" namespace { @@ -72,17 +71,6 @@ namespace { return boost::get(results[0]); } - storm::solver::SmtSolver::CheckResult analyzeSMT(std::string const &file) { - std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); - EXPECT_TRUE(storm::api::isWellFormed(*dft)); - storm::modelchecker::DFTASFChecker smtChecker(*dft); - smtChecker.convert(); - smtChecker.toSolver(); - std::vector results; - - return smtChecker.checkTleNeverFailed(); - } - double analyzeReliability(std::string const &file, double bound) { std::shared_ptr> dft = storm::api::loadDFTGalileoFile(file); EXPECT_TRUE(storm::api::isWellFormed(*dft)); @@ -211,11 +199,4 @@ namespace { double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0); EXPECT_FLOAT_EQ(result, 0.00021997582); } - - TYPED_TEST(DftModelCheckerTest, SmtTest) { - storm::solver::SmtSolver::CheckResult result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); - EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Unsat); - result = this->analyzeSMT(STORM_TEST_RESOURCES_DIR "/dft/pand.dft"); - EXPECT_EQ(result, storm::solver::SmtSolver::CheckResult::Sat); - } } diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp new file mode 100644 index 000000000..ac350b3d5 --- /dev/null +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -0,0 +1,26 @@ +#include "gtest/gtest.h" +#include "storm-config.h" + +#include "storm-dft/api/storm-dft.h" + +namespace { + TEST(DftSmtTest, AndTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/and.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Unsat); + } + + TEST(DftSmtTest, PandTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/pand.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Sat); + } +} \ No newline at end of file From aff9d2181198102a4655cefc27b20954f57febfe Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 25 Apr 2019 11:11:21 +0200 Subject: [PATCH 13/44] Easier fix for bound computation using SMT encoding --- .../modelchecker/dft/DFTASFChecker.cpp | 69 +++++++------------ .../modelchecker/dft/DFTASFChecker.h | 19 ++--- .../modelchecker/dft/SmtConstraint.cpp | 25 +++++++ 3 files changed, 55 insertions(+), 58 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 7b61ea655..e993ac7dc 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -241,14 +241,6 @@ namespace storm { 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 trying to claim (i+1)-th child, either child claimed before or never claimed by other spare - // (additional constraint) - std::shared_ptr claimEarlyC = generateClaimEarlyConstraint(spare, currChild); - constraints.push_back(std::make_shared( - std::make_shared(getClaimVariableIndex(spare->id(), children.at(currChild)->id()), - timeCurrChild), claimEarlyC)); - constraints.back()->setDescription("Ensure earliest possible claiming"); // 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); @@ -259,28 +251,6 @@ namespace storm { } } - std::shared_ptr - DFTASFChecker::generateClaimEarlyConstraint(std::shared_ptr const> spare, - uint64_t childIndex) const { - auto child = spare->children().at(childIndex + 1); - std::vector> constraintAggregator; - for (auto const &otherSpare : child->parents()) { - if (otherSpare->id() == spare->id()) { - // not a different spare. - continue; - } - std::vector> OrAggregator; - // Other spare has claimed before - OrAggregator.push_back(std::make_shared( - getClaimVariableIndex(otherSpare->id(), child->id()), timePointVariables.at(childIndex))); - // Other spare will never claim - OrAggregator.push_back(std::make_shared( - getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); - constraintAggregator.push_back(std::make_shared(OrAggregator)); - } - return std::make_shared(constraintAggregator); - } - std::shared_ptr DFTASFChecker::generateTryToClaimConstraint(std::shared_ptr const> spare, uint64_t childIndex, uint64_t timepoint) const { @@ -309,7 +279,9 @@ namespace storm { // not a different spare. continue; } - claimingPossibleC.push_back(std::make_shared(getClaimVariableIndex(otherSpare->id(), child->id()), notFailed)); + claimingPossibleC.push_back(std::make_shared(timepoint, + getClaimVariableIndex(otherSpare->id(), + child->id()))); } // Claim child if available @@ -532,40 +504,51 @@ namespace storm { return checkTleFailsWithEq(notFailed); } - uint64_t DFTASFChecker::getLeastFailureBound() { + uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { return notFailed; } uint64_t bound = 0; while (bound < notFailed) { - setSolverTimeout(10000); + setSolverTimeout(timeout * 1000); storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithLeq(bound); unsetSolverTimeout(); - if (tmp_res == storm::solver::SmtSolver::CheckResult::Sat || - tmp_res == storm::solver::SmtSolver::CheckResult::Unknown) { - return bound; + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + return bound; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Solver returned 'Unknown'"); + return bound; + default: + ++bound; + break; } - ++bound; + } return bound; } - uint64_t DFTASFChecker::getAlwaysFailedBound() { + uint64_t DFTASFChecker::getAlwaysFailedBound(uint_fast64_t timeout) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { return notFailed; } uint64_t bound = notFailed - 1; while (bound >= 0) { - setSolverTimeout(10000); + setSolverTimeout(timeout * 1000); storm::solver::SmtSolver::CheckResult tmp_res = checkTleFailsWithEq(bound); unsetSolverTimeout(); - if (tmp_res == storm::solver::SmtSolver::CheckResult::Sat || - tmp_res == storm::solver::SmtSolver::CheckResult::Unknown) { - return bound; + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + return bound; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Solver returned 'Unknown'"); + return bound; + default: + --bound; + break; } - --bound; } return bound; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 2141694f5..d8da63dce 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -68,16 +68,18 @@ namespace storm { /** * Get the minimal number of BEs necessary for the TLE to fail (lower bound for number of failures to check) * + * @param timeout timeout for each query in seconds, defaults to 10 seconds * @return the minimal number */ - uint64_t getLeastFailureBound(); + uint64_t getLeastFailureBound(uint_fast64_t timeout = 10); /** * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check) * + * @param timeout timeout for each query in seconds, defaults to 10 seconds * @return the number */ - uint64_t getAlwaysFailedBound(); + uint64_t getAlwaysFailedBound(uint_fast64_t timeout = 10); /** * Set the timeout of the solver @@ -94,19 +96,6 @@ namespace storm { private: uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; - /** - * Generate constraint for spares such that when trying to claim child (i+1), other spares either claimed it - * before or will never claim it - * - * @param spare Spare. - * @param childIndex Index of child to consider in spare children - * @param timepoint Timepoint to try to claim - * @return - */ - std::shared_ptr - generateClaimEarlyConstraint(std::shared_ptr const> spare, - 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. diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index e9bc2b220..83433989b 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -370,6 +370,31 @@ namespace storm { uint64_t value; }; + class IsGreaterConstant : public SmtConstraint { + public: + IsGreaterConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { + } + + virtual ~IsGreaterConstant() { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + assert(varIndex < varNames.size()); + sstr << "(< " << value << " " << varNames.at(varIndex) << ")"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + return manager->getVariableExpression(varNames.at(varIndex)) > value; + } + + private: + uint64_t varIndex; + uint64_t value; + }; + class IsLessEqualConstant : public SmtConstraint { public: IsLessEqualConstant(uint64_t varIndex, uint64_t val) : varIndex(varIndex), value(val) { From a669c69fc9917758ce8a2cf5eef67c503cfd4b1c Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 25 Apr 2019 13:01:08 +0200 Subject: [PATCH 14/44] Added tests for SMT encoding --- .../testfiles/dft/spareTwoModules.dft | 8 +++++++ src/storm-dft/api/storm-dft.cpp | 2 +- .../modelchecker/dft/DFTASFChecker.cpp | 13 +++++------ src/test/storm-dft/api/DftSmtTest.cpp | 22 +++++++++++++++++++ 4 files changed, 37 insertions(+), 8 deletions(-) create mode 100755 resources/examples/testfiles/dft/spareTwoModules.dft diff --git a/resources/examples/testfiles/dft/spareTwoModules.dft b/resources/examples/testfiles/dft/spareTwoModules.dft new file mode 100755 index 000000000..a2cbcbe8b --- /dev/null +++ b/resources/examples/testfiles/dft/spareTwoModules.dft @@ -0,0 +1,8 @@ +toplevel "A"; +"A" or "B" "C"; +"B" wsp "K" "J" "I"; +"C" wsp "L" "J" "I"; +"I" lambda=0.5 dorm=0.5; +"J" lambda=1 dorm=0.5; +"K" lambda=0.5 dorm=0.5; +"L" lambda=0.5 dorm=0.5; diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 5c9db7040..623d75a16 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -53,7 +53,7 @@ namespace storm { uint64_t lower_bound = smtChecker.getLeastFailureBound(); uint64_t upper_bound = smtChecker.getAlwaysFailedBound(); if (printOutput) { - //TODO add suitable output function, maybe add query descriptions for better readability + // TODO add suitable output function, maybe add query descriptions for better readability for (size_t i = 0; i < results.size(); ++i) { std::string tmp = "unknown"; if (results.at(i) == storm::solver::SmtSolver::CheckResult::Sat) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index e993ac7dc..59b736c68 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -119,8 +119,8 @@ namespace storm { } } - // Constraint (8) - addClaimingConstraints(); + // Constraint (8) intentionally commented out for testing purposes + //addClaimingConstraints(); // Handle dependencies addMarkovianConstraints(); @@ -505,10 +505,8 @@ namespace storm { } uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { + STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { - return notFailed; - } uint64_t bound = 0; while (bound < notFailed) { setSolverTimeout(timeout * 1000); @@ -518,7 +516,7 @@ namespace storm { case storm::solver::SmtSolver::CheckResult::Sat: return bound; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Solver returned 'Unknown'"); + STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); return bound; default: ++bound; @@ -530,6 +528,7 @@ namespace storm { } uint64_t DFTASFChecker::getAlwaysFailedBound(uint_fast64_t timeout) { + STORM_LOG_TRACE("Compute bound for number of BE failures such that the DFT always fails"); STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); if (checkTleNeverFailed() == storm::solver::SmtSolver::CheckResult::Sat) { return notFailed; @@ -543,7 +542,7 @@ namespace storm { case storm::solver::SmtSolver::CheckResult::Sat: return bound; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Solver returned 'Unknown'"); + STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); return bound; default: --bound; diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index ac350b3d5..bc83caa3b 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -23,4 +23,26 @@ namespace { smtChecker.toSolver(); EXPECT_EQ(smtChecker.checkTleNeverFailed(), storm::solver::SmtSolver::CheckResult::Sat); } + + TEST(DftSmtTest, SpareTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spareTwoModules.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + EXPECT_EQ(smtChecker.checkTleFailsWithLeq(2), storm::solver::SmtSolver::CheckResult::Unsat); + EXPECT_EQ(smtChecker.checkTleFailsWithEq(3), storm::solver::SmtSolver::CheckResult::Sat); + } + + TEST(DftSmtTest, BoundTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(2)); + EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(4)); + } } \ No newline at end of file From f16b4885900e0b66890618ab9399f0223ed5fd63 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 25 Apr 2019 17:06:47 +0200 Subject: [PATCH 15/44] Added conservative lower bound correction --- ...{spareTwoModules.dft => spare_two_modules.dft} | 0 src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 15 ++++++++++++++- src/storm-dft/modelchecker/dft/DFTASFChecker.h | 12 +++++++++++- src/test/storm-dft/api/DftSmtTest.cpp | 2 +- 4 files changed, 26 insertions(+), 3 deletions(-) rename resources/examples/testfiles/dft/{spareTwoModules.dft => spare_two_modules.dft} (100%) diff --git a/resources/examples/testfiles/dft/spareTwoModules.dft b/resources/examples/testfiles/dft/spare_two_modules.dft similarity index 100% rename from resources/examples/testfiles/dft/spareTwoModules.dft rename to resources/examples/testfiles/dft/spare_two_modules.dft diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 59b736c68..051b2a555 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -504,6 +504,15 @@ namespace storm { return checkTleFailsWithEq(notFailed); } + uint64_t DFTASFChecker::correctLowerBound(uint64_t bound) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); + // placeholder, set lower bound to 1 to prevent loss of precision + return 1; + // TODO correction mechanism + // easy method ("climb down" all direct predecessor states of bound) does not work + } + uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); @@ -514,7 +523,11 @@ namespace storm { unsetSolverTimeout(); switch (tmp_res) { case storm::solver::SmtSolver::CheckResult::Sat: - return bound; + if (dft.getDependencies().size() > 0) { + return correctLowerBound(bound); + } else { + return bound; + } case storm::solver::SmtSolver::CheckResult::Unknown: STORM_LOG_DEBUG("Lower bound: Solver returned 'Unknown'"); return bound; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index d8da63dce..4ebe91f0b 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -74,7 +74,8 @@ namespace storm { uint64_t getLeastFailureBound(uint_fast64_t timeout = 10); /** - * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check) + * Get the number of BE failures for which the TLE always fails (upper bound for number of failures to check). + * Note that the returned value may be higher than the real one when dependencies are present. * * @param timeout timeout for each query in seconds, defaults to 10 seconds * @return the number @@ -94,6 +95,15 @@ namespace storm { void unsetSolverTimeout(); private: + /** + * Helper function for correction of least failure bound when dependencies are present + * + * @param state number of the state in the sequence to check + * @param bound known lower bound to be corrected + * @return the corrected bound, 1 if correction cannot be completed + */ + uint64_t correctLowerBound(uint64_t bound); + uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; /** diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index bc83caa3b..9404c5f5e 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -26,7 +26,7 @@ namespace { TEST(DftSmtTest, SpareTest) { std::shared_ptr> dft = - storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spareTwoModules.dft"); + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft"); EXPECT_TRUE(storm::api::isWellFormed(*dft)); storm::modelchecker::DFTASFChecker smtChecker(*dft); smtChecker.convert(); From b34351ec85dd52c1f40cee832c154808fbd8c4fc Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 1 May 2019 20:06:58 +0200 Subject: [PATCH 16/44] Maximal exploration depth can be specified for state space generation --- src/storm-dft-cli/storm-dft.cpp | 4 +- .../builder/ExplicitDFTModelBuilder.cpp | 18 ++++++++- .../settings/modules/FaultTreeSettings.cpp | 40 +++++++++++++++---- .../settings/modules/FaultTreeSettings.h | 15 +++++++ 4 files changed, 66 insertions(+), 11 deletions(-) diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp index 533da8bf3..1f7359b7f 100644 --- a/src/storm-dft-cli/storm-dft.cpp +++ b/src/storm-dft-cli/storm-dft.cpp @@ -148,8 +148,8 @@ void processOptions() { // Add relevant event names from properties for (auto atomic : atomicLabels) { std::string label = atomic->getLabel(); - if (label == "failed") { - // Ignore as this label will always be added + if (label == "failed" or label == "skipped") { + // Ignore as these label will always be added if necessary } else { // Get name of event if (boost::ends_with(label, "_failed")) { diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index ca9415e48..efc51d89f 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -202,6 +202,13 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentException, "Heuristic not known."); } } + + auto ftSettings = storm::settings::getModule(); + if (ftSettings.isMaxDepthSet()) { + STORM_LOG_ASSERT(usedHeuristic == storm::builder::ApproximationHeuristic::DEPTH, "MaxDepth requires 'depth' exploration heuristic."); + approximationThreshold = ftSettings.getMaxDepth(); + } + exploreStateSpace(approximationThreshold); size_t stateSize = stateStorage.getNumberOfStates() + (this->uniqueFailedState ? 1 : 0); @@ -519,7 +526,16 @@ namespace storm { template std::shared_ptr> ExplicitDFTModelBuilder::getModel() { - STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); + if (storm::settings::getModule().isMaxDepthSet() && skippedStates.size() > 0) { + // Give skipped states separate label "skipped" + modelComponents.stateLabeling.addLabel("skipped"); + for (auto it = skippedStates.begin(); it != skippedStates.end(); ++it) { + modelComponents.stateLabeling.addLabelToState("skipped", it->first); + } + } else{ + STORM_LOG_ASSERT(skippedStates.size() == 0, "Concrete model has skipped states"); + } + return createModel(false); } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.cpp b/src/storm-dft/settings/modules/FaultTreeSettings.cpp index 140b0f175..b45c37498 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.cpp +++ b/src/storm-dft/settings/modules/FaultTreeSettings.cpp @@ -24,24 +24,35 @@ namespace storm { const std::string FaultTreeSettings::approximationErrorOptionName = "approximation"; const std::string FaultTreeSettings::approximationErrorOptionShortName = "approx"; const std::string FaultTreeSettings::approximationHeuristicOptionName = "approximationheuristic"; + const std::string FaultTreeSettings::maxDepthOptionName = "maxdepth"; const std::string FaultTreeSettings::firstDependencyOptionName = "firstdep"; #ifdef STORM_HAVE_Z3 const std::string FaultTreeSettings::solveWithSmtOptionName = "smt"; #endif FaultTreeSettings::FaultTreeSettings() : ModuleSettings(moduleName) { - this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName(symmetryReductionOptionShortName).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, symmetryReductionOptionName, false, "Exploit symmetric structure of model.").setShortName( + symmetryReductionOptionShortName).build()); this->addOption(storm::settings::OptionBuilder(moduleName, modularisationOptionName, false, "Use modularisation (not applicable for expected time).").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableDCOptionName, false, "Disable Don't Care propagation.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, "Avoid non-determinism by always taking the first possible dependency.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, firstDependencyOptionName, false, + "Avoid non-determinism by always taking the first possible dependency.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, relevantEventsOptionName, false, "Specifies the relevant events from the DFT.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString("").build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("values", + "A comma separated list of names of relevant events. 'all' marks all events as relevant, The default '' or 'none' marks only the top level event as relevant.").setDefaultValueString( + "").build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, allowDCRelevantOptionName, false, "Allow Don't Care propagation for relevant events.").build()); - this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName(approximationErrorOptionShortName).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, approximationErrorOptionName, false, "Approximation error allowed.").setShortName( + approximationErrorOptionShortName).addArgument( + storm::settings::ArgumentBuilder::createDoubleArgument("error", "The relative approximation error to use.").addValidatorDouble( + ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build()); this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.") - .addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "The name of the heuristic used for approximation.") - .setDefaultValueString("depth") - .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "probability", "bounddifference"})).build()).build()); + .addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "The name of the heuristic used for approximation.") + .setDefaultValueString("depth") + .addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator( + {"depth", "probability", "bounddifference"})).build()).build()); + this->addOption(storm::settings::OptionBuilder(moduleName, maxDepthOptionName, false, "Maximal depth for state space exploration.").addArgument( + storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("depth", "The maximal depth.").build()).build()); #ifdef STORM_HAVE_Z3 this->addOption(storm::settings::OptionBuilder(moduleName, solveWithSmtOptionName, true, "Solve the DFT with SMT.").build()); #endif @@ -64,7 +75,8 @@ namespace storm { } bool FaultTreeSettings::areRelevantEventsSet() const { - return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != ""); + return this->getOption(relevantEventsOptionName).getHasOptionBeenSet() && + (this->getOption(relevantEventsOptionName).getArgumentByName("values").getValueAsString() != ""); } std::vector FaultTreeSettings::getRelevantEvents() const { @@ -91,14 +103,24 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal value '" << heuristicAsString << "' set as heuristic for approximation."); } + bool FaultTreeSettings::isMaxDepthSet() const { + return this->getOption(maxDepthOptionName).getHasOptionBeenSet(); + } + + uint_fast64_t FaultTreeSettings::getMaxDepth() const { + return this->getOption(maxDepthOptionName).getArgumentByName("depth").getValueAsUnsignedInteger(); + } + bool FaultTreeSettings::isTakeFirstDependency() const { return this->getOption(firstDependencyOptionName).getHasOptionBeenSet(); } #ifdef STORM_HAVE_Z3 + bool FaultTreeSettings::solveWithSMT() const { return this->getOption(solveWithSmtOptionName).getHasOptionBeenSet(); } + #endif void FaultTreeSettings::finalize() { @@ -107,6 +129,8 @@ namespace storm { bool FaultTreeSettings::check() const { // Ensure that disableDC and relevantEvents are not set at the same time STORM_LOG_THROW(!isDisableDC() || !areRelevantEventsSet(), storm::exceptions::InvalidSettingsException, "DisableDC and relevantSets can not both be set."); + STORM_LOG_THROW(!isMaxDepthSet() || getApproximationHeuristic() == storm::builder::ApproximationHeuristic::DEPTH, storm::exceptions::InvalidSettingsException, + "Maximal depth requires approximation heuristic depth."); return true; } diff --git a/src/storm-dft/settings/modules/FaultTreeSettings.h b/src/storm-dft/settings/modules/FaultTreeSettings.h index 16a726e04..5ed230bfb 100644 --- a/src/storm-dft/settings/modules/FaultTreeSettings.h +++ b/src/storm-dft/settings/modules/FaultTreeSettings.h @@ -82,6 +82,20 @@ namespace storm { */ storm::builder::ApproximationHeuristic getApproximationHeuristic() const; + /*! + * Retrieves whether the option to set a maximal exploration depth is set. + * + * @return True iff the option was set. + */ + bool isMaxDepthSet() const; + + /*! + * Retrieves the maximal exploration depth. + * + * @return The maximal exploration depth. + */ + uint_fast64_t getMaxDepth() const; + /*! * Retrieves whether the non-determinism should be avoided by always taking the first possible dependency. * @@ -118,6 +132,7 @@ namespace storm { static const std::string approximationErrorOptionName; static const std::string approximationErrorOptionShortName; static const std::string approximationHeuristicOptionName; + static const std::string maxDepthOptionName; static const std::string firstDependencyOptionName; #ifdef STORM_HAVE_Z3 static const std::string solveWithSmtOptionName; From 4f376caccb6c034e36c40324dc9b7199d8c33393 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 2 May 2019 11:21:14 +0200 Subject: [PATCH 17/44] Fixed expand flag to avoid expanding too much --- src/storm-dft/builder/DftExplorationHeuristic.h | 2 +- src/storm-dft/builder/ExplicitDFTModelBuilder.cpp | 7 ++++--- src/storm-dft/generator/DftNextStateGenerator.cpp | 1 + 3 files changed, 6 insertions(+), 4 deletions(-) diff --git a/src/storm-dft/builder/DftExplorationHeuristic.h b/src/storm-dft/builder/DftExplorationHeuristic.h index b0fd73a66..f71f60dcc 100644 --- a/src/storm-dft/builder/DftExplorationHeuristic.h +++ b/src/storm-dft/builder/DftExplorationHeuristic.h @@ -22,7 +22,7 @@ namespace storm { class DFTExplorationHeuristic { public: - explicit DFTExplorationHeuristic(size_t id) : id(id), expand(true), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { + explicit DFTExplorationHeuristic(size_t id) : id(id), expand(false), lowerBound(storm::utility::zero()), upperBound(storm::utility::infinity()), depth(0), probability(storm::utility::one()) { // Intentionally left empty } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index efc51d89f..e71f8e4b9 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -383,7 +383,7 @@ namespace storm { setMarkovian(true); // Add transition to target state with temporary value 0 // TODO: what to do when there is no unique target state? - STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state"); + //STORM_LOG_ASSERT(this->uniqueFailedState, "Approximation only works with unique failed state"); matrixBuilder.addTransition(0, storm::utility::zero()); // Remember skipped state skippedStates[matrixBuilder.getCurrentRowGroup() - 1] = std::make_pair(currentState, currentExplorationHeuristic); @@ -425,8 +425,9 @@ namespace storm { } iter->second.second = heuristic; - if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) { - // Do not skip absorbing state or if reached by dependencies + //if (state->hasFailed(dft.getTopLevelIndex()) || state->isFailsafe(dft.getTopLevelIndex()) || state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) { + if (state->getFailableElements().hasDependencies() || (!state->getFailableElements().hasDependencies() && !state->getFailableElements().hasBEs())) { + // Do not skip absorbing state or if reached by dependencies iter->second.second->markExpand(); } if (usedHeuristic == storm::builder::ApproximationHeuristic::BOUNDDIFFERENCE) { diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 4edd26b4b..f4af34ed1 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -78,6 +78,7 @@ namespace storm { // Let BE fail bool isFirst = true; while (!state->getFailableElements().isEnd()) { + //TODO outside if (storm::settings::getModule().isTakeFirstDependency() && exploreDependencies && !isFirst) { // We discard further exploration as we already chose one dependent event break; From 0baccee440e7c5e018eb6cccdadd294b008d161d Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Thu, 2 May 2019 16:20:53 +0200 Subject: [PATCH 18/44] Added correction of constraint for non-Markovian states and better lower bound computation --- .../modelchecker/dft/DFTASFChecker.cpp | 58 ++++++++++++++++--- .../modelchecker/dft/DFTASFChecker.h | 13 ++++- .../modelchecker/dft/SmtConstraint.cpp | 33 +++++++++++ 3 files changed, 95 insertions(+), 9 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 051b2a555..19ae50a42 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -325,6 +325,7 @@ namespace storm { void DFTASFChecker::addMarkovianConstraints() { uint64_t nrMarkovian = dft.nrBasicElements(); + std::set depElements; // Vector containing (non-)Markovian constraints for each timepoint std::vector>> markovianC(nrMarkovian); std::vector>> nonMarkovianC(nrMarkovian); @@ -352,13 +353,14 @@ namespace storm { constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed."); } - // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + additions to specification in paper for (size_t j = 0; j < dft.nrElements(); ++j) { std::shared_ptr const> element = dft.getElement(j); if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { + depElements.emplace(j); for (uint64_t i = 0; i < nrMarkovian -1; ++i) { std::shared_ptr nextFailure = std::make_shared( timePointVariables.at(j), i + 1); @@ -372,6 +374,14 @@ namespace storm { } } for (uint64_t i = 0; i < nrMarkovian; ++i) { + std::vector> dependentConstr; + for (auto dependentEvent: depElements) { + std::shared_ptr nextFailure = std::make_shared( + timePointVariables.at(dependentEvent), i + 1); + dependentConstr.push_back(nextFailure); + } + // Add Constraint that any DEPENDENT event has to fail next + nonMarkovianC[i].push_back(std::make_shared(dependentConstr)); constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), false), std::make_shared(nonMarkovianC[i]))); constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE."); } @@ -504,13 +514,47 @@ namespace storm { return checkTleFailsWithEq(notFailed); } - uint64_t DFTASFChecker::correctLowerBound(uint64_t bound) { + storm::solver::SmtSolver::CheckResult + DFTASFChecker::checkFailsWithLessThanMarkovianState(uint64_t checkNumber) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + uint64_t nrMarkovian = dft.nrBasicElements(); + std::vector markovianIndices; + // Get Markovian variable indices + for (uint64_t i = 0; i < nrMarkovian; ++i) { + markovianIndices.push_back(markovianVariables.at(i)); + } + // Set backtracking marker to check several properties without reconstructing DFT encoding + solver->push(); + // Constraint that toplevel element can fail with less or equal 'bound' failures + std::shared_ptr countConstr = std::make_shared( + markovianIndices, checkNumber); + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->add(countConstr->toExpression(varNames, manager)); + storm::solver::SmtSolver::CheckResult res = solver->check(); + solver->pop(); + return res; + } + + uint64_t DFTASFChecker::correctLowerBound(uint64_t bound, uint_fast64_t timeout) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); - // placeholder, set lower bound to 1 to prevent loss of precision - return 1; - // TODO correction mechanism - // easy method ("climb down" all direct predecessor states of bound) does not work + while (bound >= 0) { + setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = checkFailsWithLessThanMarkovianState(bound); + unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Unsat: + STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(bound)); + return bound; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to "); + return bound; + default: + --bound; + break; + } + } + return bound; } uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { @@ -524,7 +568,7 @@ namespace storm { switch (tmp_res) { case storm::solver::SmtSolver::CheckResult::Sat: if (dft.getDependencies().size() > 0) { - return correctLowerBound(bound); + return correctLowerBound(bound, timeout); } else { return bound; } diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 4ebe91f0b..5c102fb6e 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -95,14 +95,23 @@ namespace storm { void unsetSolverTimeout(); private: + /** + * Helper function that checks if the DFT can fail while visiting less than a given number of Markovian states + * + * @param checkNumber the number to check against + * @return "Sat" if a sequence of BE failures exists such that less than checkNumber Markovian states are visited, + * "Unsat" if it does not, otherwise "Unknown" + */ + storm::solver::SmtSolver::CheckResult checkFailsWithLessThanMarkovianState(uint64_t checkNumber); + /** * Helper function for correction of least failure bound when dependencies are present * - * @param state number of the state in the sequence to check * @param bound known lower bound to be corrected + * @param timeout timeout timeout for each query in seconds * @return the corrected bound, 1 if correction cannot be completed */ - uint64_t correctLowerBound(uint64_t bound); + uint64_t correctLowerBound(uint64_t bound, uint_fast64_t timeout); uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 83433989b..0a56fe8f6 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -597,6 +597,39 @@ namespace storm { std::shared_ptr thenConstraint; std::shared_ptr elseConstraint; }; + + class BoolCountIsLessConstant : public SmtConstraint { + public: + BoolCountIsLessConstant(std::vector varIndices, uint64_t val) : varIndices(varIndices), + value(val) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(< (+ "; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + sstr << "(ite " << varNames.at(varIndices.at(i)) << " 1 0 )"; + } + sstr << ") " << value << " )"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + std::vector boolToInt; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + boolToInt.push_back( + ite(manager->getVariableExpression(varNames.at(varIndices.at(i))), // If variable is true + manager->integer(1), // set 1 + manager->integer(0))); // else 0 + } + return sum(boolToInt) < manager->integer(value); + } + + private: + std::vector varIndices; + uint64_t value; + }; } } From c4ba7554fd7a00dd4909758f54475636a65ce9cb Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 3 May 2019 17:07:52 +0200 Subject: [PATCH 19/44] Added upper bound correction --- .../modelchecker/dft/DFTASFChecker.cpp | 166 ++++++++++++++---- .../modelchecker/dft/DFTASFChecker.h | 42 ++++- .../modelchecker/dft/SmtConstraint.cpp | 33 ++++ 3 files changed, 204 insertions(+), 37 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 19ae50a42..ae00a86c9 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -24,7 +24,7 @@ namespace storm { void DFTASFChecker::convert() { std::vector beVariables; - 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) { @@ -35,12 +35,21 @@ namespace storm { case storm::storage::DFTElementType::BE: beVariables.push_back(varNames.size() - 1); break; - case storm::storage::DFTElementType::SPARE: - { + case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); - for( auto const& spareChild : spare->children()) { + for (auto const &spareChild : spare->children()) { varNames.push_back("c_" + element->name() + "_" + spareChild->name()); - claimVariables.emplace(SpareAndChildPair(element->id(), spareChild->id()), varNames.size() - 1); + claimVariables.emplace(SpareAndChildPair(element->id(), spareChild->id()), + varNames.size() - 1); + } + break; + } + case storm::storage::DFTElementType::PDEP: { + auto dep = std::static_pointer_cast const>(element); + for (auto const &depEvent : dep->dependentEvents()) { + varNames.push_back("d_" + element->name() + "_" + depEvent->name()); + dependencyVariables.emplace(DependencyPair(element->id(), depEvent->id()), + varNames.size() - 1); } break; } @@ -58,7 +67,7 @@ namespace storm { // Generate constraints // All BEs have to fail (first part of constraint 12) - for (auto const& beV : beVariables) { + for (auto const &beV : beVariables) { constraints.push_back(std::make_shared(beV, 1, dft.nrBasicElements())); } @@ -67,7 +76,7 @@ namespace storm { constraints.back()->setDescription("No two BEs fail at the same time"); // Initialize claim variables in [1, |BE|+1] - for (auto const& claimVariable : claimVariables) { + for (auto const &claimVariable : claimVariables) { constraints.push_back(std::make_shared(claimVariable.second, 0, notFailed)); } @@ -80,7 +89,7 @@ namespace storm { std::vector childVarIndices; if (element->isGate()) { std::shared_ptr const> gate = dft.getGate(i); - for (auto const& child : gate->children()) { + for (auto const &child : gate->children()) { childVarIndices.push_back(timePointVariables.at(child->id())); } } @@ -114,7 +123,8 @@ namespace storm { // FDEPs are considered later in the Markovian constraints break; default: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "SMT encoding for type '" << element->type() << "' is not supported."); + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, + "SMT encoding for type '" << element->type() << "' is not supported."); break; } } @@ -262,7 +272,7 @@ namespace storm { // Child cannot be claimed. if (childIndex + 1 < spare->children().size()) { // Consider next child for claiming (second case in constraint 7) - noClaimingPossible.push_back(generateTryToClaimConstraint(spare, childIndex+1, timepoint)); + 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)); @@ -274,7 +284,7 @@ namespace storm { // 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()) { + for (auto const &otherSpare : child->parents()) { if (otherSpare->id() == spare->id()) { // not a different spare. continue; @@ -323,6 +333,11 @@ namespace storm { } } + void DFTASFChecker::generatePdepConstraint(size_t i, std::vector childVarIndices, + std::shared_ptr const> element) { + // TODO + } + void DFTASFChecker::addMarkovianConstraints() { uint64_t nrMarkovian = dft.nrBasicElements(); std::set depElements; @@ -339,18 +354,24 @@ namespace storm { 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)); + for (auto const &dependency : element->outgoingDependencies()) { + for (auto const &depElement : dependency->dependentEvents()) { + depFailed.push_back( + std::make_shared(timePointVariables.at(depElement->id()), + i)); } } - markovianC[i].push_back(std::make_shared(triggerFailed, std::make_shared(depFailed))); + markovianC[i].push_back( + std::make_shared(triggerFailed, std::make_shared(depFailed))); } } } for (uint64_t i = 0; i < nrMarkovian; ++i) { - constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), true), std::make_shared(markovianC[i]))); - constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") iff all dependent events which trigger failed also failed."); + constraints.push_back( + std::make_shared(std::make_shared(markovianVariables.at(i), true), + std::make_shared(markovianC[i]))); + constraints.back()->setDescription("Markovian (" + std::to_string(i) + + ") iff all dependent events which trigger failed also failed."); } // In non-Markovian steps the next failed element is a dependent BE (constraint 10) + additions to specification in paper @@ -361,14 +382,16 @@ namespace storm { if (be->hasIngoingDependencies()) { depElements.emplace(j); - for (uint64_t i = 0; i < nrMarkovian -1; ++i) { + for (uint64_t i = 0; i < nrMarkovian - 1; ++i) { 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)); + for (auto const &dependency : be->ingoingDependencies()) { + triggerFailed.push_back(std::make_shared( + timePointVariables.at(dependency->triggerEvent()->id()), i)); } - nonMarkovianC[i].push_back(std::make_shared(nextFailure, std::make_shared(triggerFailed))); + nonMarkovianC[i].push_back( + std::make_shared(nextFailure, std::make_shared(triggerFailed))); } } } @@ -382,8 +405,11 @@ namespace storm { } // Add Constraint that any DEPENDENT event has to fail next nonMarkovianC[i].push_back(std::make_shared(dependentConstr)); - constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), false), std::make_shared(nonMarkovianC[i]))); - constraints.back()->setDescription("Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE."); + constraints.push_back( + std::make_shared(std::make_shared(markovianVariables.at(i), false), + std::make_shared(nonMarkovianC[i]))); + constraints.back()->setDescription( + "Non-Markovian (" + std::to_string(i) + ") -> next failure is dependent BE."); } // In Markovian steps the failure rate is positive (constraint 11) @@ -402,35 +428,43 @@ namespace storm { } } for (uint64_t i = 0; i < nrMarkovian; ++i) { - constraints.push_back(std::make_shared(std::make_shared(markovianVariables.at(i), true), std::make_shared(notColdC[i]))); + constraints.push_back( + std::make_shared(std::make_shared(markovianVariables.at(i), true), + std::make_shared(notColdC[i]))); constraints.back()->setDescription("Markovian (" + std::to_string(i) + ") -> positive failure rate."); } } - void DFTASFChecker::toFile(std::string const& filename) { + void DFTASFChecker::toFile(std::string const &filename) { std::ofstream stream; storm::utility::openFile(filename, stream); stream << "; time point variables" << std::endl; - for (auto const& timeVarEntry : timePointVariables) { + for (auto const &timeVarEntry : timePointVariables) { stream << "(declare-fun " << varNames[timeVarEntry.second] << "() Int)" << std::endl; } stream << "; claim variables" << std::endl; - for (auto const& claimVarEntry : claimVariables) { + for (auto const &claimVarEntry : claimVariables) { stream << "(declare-fun " << varNames[claimVarEntry.second] << "() Int)" << std::endl; } stream << "; Markovian variables" << std::endl; - for (auto const& markovianVarEntry : markovianVariables) { + for (auto const &markovianVarEntry : markovianVariables) { stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl; } + if (!dependencyVariables.empty()) { + stream << "; Dependency variables" << std::endl; + for (auto const &depVar : dependencyVariables) { + stream << "(declare-fun " << varNames[depVar.second] << "() Int)" << std::endl; + } + } if (!tmpTimePointVariables.empty()) { stream << "; Temporary variables" << std::endl; - for (auto const& tmpVar : tmpTimePointVariables) { + for (auto const &tmpVar : tmpTimePointVariables) { stream << "(declare-fun " << varNames[tmpVar] << "() Int)" << std::endl; } } - for (auto const& constraint : constraints) { + for (auto const &constraint : constraints) { if (!constraint->description().empty()) { stream << "; " << constraint->description() << std::endl; } @@ -462,6 +496,11 @@ namespace storm { manager->declareIntegerVariable(varNames[tmpVar]); } } + if (!dependencyVariables.empty()) { + for (auto const &depVar : dependencyVariables) { + manager->declareIntegerVariable(varNames[depVar]); + } + } // Add constraints to solver for (auto const &constraint : constraints) { solver->add(constraint->toExpression(varNames, manager)); @@ -475,10 +514,10 @@ namespace storm { // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); // Constraint that toplevel element can fail with less or equal 'bound' failures - std::shared_ptr tleNeverFailedConstr = std::make_shared( + std::shared_ptr tleFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), bound); std::shared_ptr manager = solver->getManager().getSharedPointer(); - solver->add(tleNeverFailedConstr->toExpression(varNames, manager)); + solver->add(tleFailedConstr->toExpression(varNames, manager)); storm::solver::SmtSolver::CheckResult res = solver->check(); solver->pop(); return res; @@ -525,7 +564,7 @@ namespace storm { } // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); - // Constraint that toplevel element can fail with less or equal 'bound' failures + // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited std::shared_ptr countConstr = std::make_shared( markovianIndices, checkNumber); std::shared_ptr manager = solver->getManager().getSharedPointer(); @@ -535,6 +574,30 @@ namespace storm { return res; } + storm::solver::SmtSolver::CheckResult + DFTASFChecker::checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + std::vector markovianIndices; + // Get Markovian variable indices + for (uint64_t i = 0; i < timepoint; ++i) { + markovianIndices.push_back(markovianVariables.at(i)); + } + // Set backtracking marker to check several properties without reconstructing DFT encoding + solver->push(); + // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited + std::shared_ptr countConstr = std::make_shared( + markovianIndices, timepoint); + // Constraint that TLE fails at timepoint + std::shared_ptr timepointConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), timepoint); + std::shared_ptr manager = solver->getManager().getSharedPointer(); + solver->add(countConstr->toExpression(varNames, manager)); + solver->add(timepointConstr->toExpression(varNames, manager)); + storm::solver::SmtSolver::CheckResult res = solver->check(); + solver->pop(); + return res; + } + uint64_t DFTASFChecker::correctLowerBound(uint64_t bound, uint_fast64_t timeout) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); @@ -547,7 +610,8 @@ namespace storm { STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(bound)); return bound; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to "); + STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to " + << std::to_string(bound)); return bound; default: --bound; @@ -557,6 +621,32 @@ namespace storm { return bound; } + uint64_t DFTASFChecker::correctUpperBound(uint64_t bound, uint_fast64_t timeout) { + STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); + STORM_LOG_DEBUG("Upper bound correction - try to correct bound " << std::to_string(bound)); + + while (bound > 1) { + setSolverTimeout(timeout * 1000); + storm::solver::SmtSolver::CheckResult tmp_res = + checkFailsAtTimepointWithOnlyMarkovianState(bound); + unsetSolverTimeout(); + switch (tmp_res) { + case storm::solver::SmtSolver::CheckResult::Sat: + STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(bound)); + return bound; + case storm::solver::SmtSolver::CheckResult::Unknown: + STORM_LOG_DEBUG("Upper bound correction - Solver returned 'Unknown', corrected to "); + return bound; + default: + --bound; + break; + + } + } + STORM_LOG_DEBUG("Upper bound correction - corrected bound to " << std::to_string(bound)); + return bound; + } + uint64_t DFTASFChecker::getLeastFailureBound(uint_fast64_t timeout) { STORM_LOG_TRACE("Compute lower bound for number of BE failures necessary for the DFT to fail"); STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); @@ -567,7 +657,7 @@ namespace storm { unsetSolverTimeout(); switch (tmp_res) { case storm::solver::SmtSolver::CheckResult::Sat: - if (dft.getDependencies().size() > 0) { + if (!dft.getDependencies().empty()) { return correctLowerBound(bound, timeout); } else { return bound; @@ -597,7 +687,11 @@ namespace storm { unsetSolverTimeout(); switch (tmp_res) { case storm::solver::SmtSolver::CheckResult::Sat: - return bound; + if (!dft.getDependencies().empty()) { + return correctUpperBound(bound, timeout); + } else { + return bound; + } case storm::solver::SmtSolver::CheckResult::Unknown: STORM_LOG_DEBUG("Upper bound: Solver returned 'Unknown'"); return bound; diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 5c102fb6e..429b2c647 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -25,6 +25,20 @@ namespace storm { uint64_t childIndex; }; + class DependencyPair { + public: + DependencyPair(uint64_t depIndex, uint64_t childIndex) : depIndex(depIndex), childIndex(childIndex) { + } + + friend bool operator<(DependencyPair const &p1, DependencyPair const &p2) { + return p1.depIndex < p2.depIndex || (p1.depIndex == p2.depIndex && p1.childIndex < p2.childIndex); + } + + private: + uint64_t depIndex; + uint64_t childIndex; + }; + class DFTASFChecker { using ValueType = double; @@ -104,15 +118,33 @@ namespace storm { */ storm::solver::SmtSolver::CheckResult checkFailsWithLessThanMarkovianState(uint64_t checkNumber); + /** + * Helper function that checks if the DFT can fail at a timepoint while visiting less than a given number of Markovian states + * + * @param timepoint point in time to check + * @return "Sat" if a sequence of BE failures exists such that less than checkNumber Markovian states are visited, + * "Unsat" if it does not, otherwise "Unknown" + */ + storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint); + /** * Helper function for correction of least failure bound when dependencies are present * * @param bound known lower bound to be corrected * @param timeout timeout timeout for each query in seconds - * @return the corrected bound, 1 if correction cannot be completed + * @return the corrected bound */ uint64_t correctLowerBound(uint64_t bound, uint_fast64_t timeout); + /** + * Helper function for correction of bound for number of BEs such that the DFT always fails when dependencies are present + * + * @param bound known bound to be corrected + * @param timeout timeout timeout for each query in seconds + * @return the corrected bound + */ + uint64_t correctUpperBound(uint64_t bound, uint_fast64_t timeout); + uint64_t getClaimVariableIndex(uint64_t spareIndex, uint64_t childIndex) const; /** @@ -176,6 +208,13 @@ namespace storm { void generateSpareConstraint(size_t i, std::vector childVarIndices, std::shared_ptr const> element); + /** + * Add constraints encoding PDEP gates. + * This corresponds to constraint (4) + */ + void generatePdepConstraint(std::vector childVarIndices, + std::shared_ptr const> element); + /** * Add constraints encoding claiming rules. * This corresponds to constraint (8) and addition @@ -194,6 +233,7 @@ namespace storm { std::unordered_map timePointVariables; std::vector> constraints; std::map claimVariables; + std::map dependencyVariables; std::unordered_map markovianVariables; std::vector tmpTimePointVariables; uint64_t notFailed; diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 0a56fe8f6..760146f13 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -630,6 +630,39 @@ namespace storm { std::vector varIndices; uint64_t value; }; + + class BoolCountIsConstantValue : public SmtConstraint { + public: + BoolCountIsConstantValue(std::vector varIndices, uint64_t val) : varIndices(varIndices), + value(val) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(= (+ "; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + sstr << "(ite " << varNames.at(varIndices.at(i)) << " 1 0 )"; + } + sstr << ") " << value << " )"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + std::vector boolToInt; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + boolToInt.push_back( + ite(manager->getVariableExpression(varNames.at(varIndices.at(i))), // If variable is true + manager->integer(1), // set 1 + manager->integer(0))); // else 0 + } + return sum(boolToInt) == manager->integer(value); + } + + private: + std::vector varIndices; + uint64_t value; + }; } } From 9b152e4940d3554b41c2bd54ff8abf2772b6398e Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 3 May 2019 18:12:14 +0200 Subject: [PATCH 20/44] Added variables vor trigger and resolution timepoints of dependencies --- .../modelchecker/dft/DFTASFChecker.cpp | 38 ++++++++++--------- .../modelchecker/dft/DFTASFChecker.h | 6 +-- 2 files changed, 24 insertions(+), 20 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index ae00a86c9..437ae326f 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -45,12 +45,8 @@ namespace storm { break; } case storm::storage::DFTElementType::PDEP: { - auto dep = std::static_pointer_cast const>(element); - for (auto const &depEvent : dep->dependentEvents()) { - varNames.push_back("d_" + element->name() + "_" + depEvent->name()); - dependencyVariables.emplace(DependencyPair(element->id(), depEvent->id()), - varNames.size() - 1); - } + varNames.push_back("dep_" + element->name()); + dependencyVariables.emplace(element->id(), varNames.size() - 1); break; } default: @@ -120,7 +116,7 @@ namespace storm { generateSpareConstraint(i, childVarIndices, element); break; case storm::storage::DFTElementType::PDEP: - // FDEPs are considered later in the Markovian constraints + generatePdepConstraint(i, childVarIndices, element); break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, @@ -335,7 +331,19 @@ namespace storm { void DFTASFChecker::generatePdepConstraint(size_t i, std::vector childVarIndices, std::shared_ptr const> element) { - // TODO + auto dependency = std::static_pointer_cast const>(element); + auto const &dependentEvents = dependency->dependentEvents(); + auto const &trigger = dependency->triggerEvent(); + std::vector dependentIndices; + for (size_t j = 0; j < dependentEvents.size(); ++j) { + dependentIndices.push_back(dependentEvents[j]->id()); + } + + constraints.push_back(std::make_shared(dependencyVariables.at(i), dependentIndices)); + constraints.back()->setDescription("Dependency " + element->name() + ": Last element"); + constraints.push_back( + std::make_shared(timePointVariables.at(i), timePointVariables.at(trigger->id()))); + constraints.back()->setDescription("Dependency " + element->name() + ": Trigger element"); } void DFTASFChecker::addMarkovianConstraints() { @@ -452,11 +460,9 @@ namespace storm { for (auto const &markovianVarEntry : markovianVariables) { stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl; } - if (!dependencyVariables.empty()) { - stream << "; Dependency variables" << std::endl; - for (auto const &depVar : dependencyVariables) { - stream << "(declare-fun " << varNames[depVar.second] << "() Int)" << std::endl; - } + stream << "; Dependency variables" << std::endl; + for (auto const &depVarEntry : dependencyVariables) { + stream << "(declare-fun " << varNames[depVarEntry.second] << "() Int)" << std::endl; } if (!tmpTimePointVariables.empty()) { stream << "; Temporary variables" << std::endl; @@ -496,10 +502,8 @@ namespace storm { manager->declareIntegerVariable(varNames[tmpVar]); } } - if (!dependencyVariables.empty()) { - for (auto const &depVar : dependencyVariables) { - manager->declareIntegerVariable(varNames[depVar]); - } + for (auto const &depVarEntry : dependencyVariables) { + manager->declareIntegerVariable(varNames[depVarEntry.second]); } // Add constraints to solver for (auto const &constraint : constraints) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 429b2c647..36a71dff5 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -210,9 +210,9 @@ namespace storm { /** * Add constraints encoding PDEP gates. - * This corresponds to constraint (4) + * */ - void generatePdepConstraint(std::vector childVarIndices, + void generatePdepConstraint(size_t i, std::vector childVarIndices, std::shared_ptr const> element); /** @@ -233,7 +233,7 @@ namespace storm { std::unordered_map timePointVariables; std::vector> constraints; std::map claimVariables; - std::map dependencyVariables; + std::unordered_map dependencyVariables; std::unordered_map markovianVariables; std::vector tmpTimePointVariables; uint64_t notFailed; From eeccb2092a8eb294b2a6a3212fe5e6d9953d83f1 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 3 May 2019 18:12:14 +0200 Subject: [PATCH 21/44] Added variables for trigger and resolution timepoints of dependencies --- .../modelchecker/dft/DFTASFChecker.cpp | 38 ++++++++++--------- .../modelchecker/dft/DFTASFChecker.h | 6 +-- 2 files changed, 24 insertions(+), 20 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index ae00a86c9..437ae326f 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -45,12 +45,8 @@ namespace storm { break; } case storm::storage::DFTElementType::PDEP: { - auto dep = std::static_pointer_cast const>(element); - for (auto const &depEvent : dep->dependentEvents()) { - varNames.push_back("d_" + element->name() + "_" + depEvent->name()); - dependencyVariables.emplace(DependencyPair(element->id(), depEvent->id()), - varNames.size() - 1); - } + varNames.push_back("dep_" + element->name()); + dependencyVariables.emplace(element->id(), varNames.size() - 1); break; } default: @@ -120,7 +116,7 @@ namespace storm { generateSpareConstraint(i, childVarIndices, element); break; case storm::storage::DFTElementType::PDEP: - // FDEPs are considered later in the Markovian constraints + generatePdepConstraint(i, childVarIndices, element); break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, @@ -335,7 +331,19 @@ namespace storm { void DFTASFChecker::generatePdepConstraint(size_t i, std::vector childVarIndices, std::shared_ptr const> element) { - // TODO + auto dependency = std::static_pointer_cast const>(element); + auto const &dependentEvents = dependency->dependentEvents(); + auto const &trigger = dependency->triggerEvent(); + std::vector dependentIndices; + for (size_t j = 0; j < dependentEvents.size(); ++j) { + dependentIndices.push_back(dependentEvents[j]->id()); + } + + constraints.push_back(std::make_shared(dependencyVariables.at(i), dependentIndices)); + constraints.back()->setDescription("Dependency " + element->name() + ": Last element"); + constraints.push_back( + std::make_shared(timePointVariables.at(i), timePointVariables.at(trigger->id()))); + constraints.back()->setDescription("Dependency " + element->name() + ": Trigger element"); } void DFTASFChecker::addMarkovianConstraints() { @@ -452,11 +460,9 @@ namespace storm { for (auto const &markovianVarEntry : markovianVariables) { stream << "(declare-fun " << varNames[markovianVarEntry.second] << "() Bool)" << std::endl; } - if (!dependencyVariables.empty()) { - stream << "; Dependency variables" << std::endl; - for (auto const &depVar : dependencyVariables) { - stream << "(declare-fun " << varNames[depVar.second] << "() Int)" << std::endl; - } + stream << "; Dependency variables" << std::endl; + for (auto const &depVarEntry : dependencyVariables) { + stream << "(declare-fun " << varNames[depVarEntry.second] << "() Int)" << std::endl; } if (!tmpTimePointVariables.empty()) { stream << "; Temporary variables" << std::endl; @@ -496,10 +502,8 @@ namespace storm { manager->declareIntegerVariable(varNames[tmpVar]); } } - if (!dependencyVariables.empty()) { - for (auto const &depVar : dependencyVariables) { - manager->declareIntegerVariable(varNames[depVar]); - } + for (auto const &depVarEntry : dependencyVariables) { + manager->declareIntegerVariable(varNames[depVarEntry.second]); } // Add constraints to solver for (auto const &constraint : constraints) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 429b2c647..36a71dff5 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -210,9 +210,9 @@ namespace storm { /** * Add constraints encoding PDEP gates. - * This corresponds to constraint (4) + * */ - void generatePdepConstraint(std::vector childVarIndices, + void generatePdepConstraint(size_t i, std::vector childVarIndices, std::shared_ptr const> element); /** @@ -233,7 +233,7 @@ namespace storm { std::unordered_map timePointVariables; std::vector> constraints; std::map claimVariables; - std::map dependencyVariables; + std::unordered_map dependencyVariables; std::unordered_map markovianVariables; std::vector tmpTimePointVariables; uint64_t notFailed; From 948485c226d6dec4ce3736621517832a41a00287 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 10 May 2019 14:00:02 +0200 Subject: [PATCH 22/44] Reworked lower bound computation --- .../modelchecker/dft/DFTASFChecker.cpp | 65 ++++++++++++++----- .../modelchecker/dft/DFTASFChecker.h | 16 +++-- .../modelchecker/dft/SmtConstraint.cpp | 41 ++++++++++-- 3 files changed, 95 insertions(+), 27 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 437ae326f..0aaeb0a71 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -558,21 +558,24 @@ namespace storm { } storm::solver::SmtSolver::CheckResult - DFTASFChecker::checkFailsWithLessThanMarkovianState(uint64_t checkNumber) { + DFTASFChecker::checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); - uint64_t nrMarkovian = dft.nrBasicElements(); std::vector markovianIndices; // Get Markovian variable indices - for (uint64_t i = 0; i < nrMarkovian; ++i) { + for (uint64_t i = 0; i < checkbound; ++i) { markovianIndices.push_back(markovianVariables.at(i)); } // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); - // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited - std::shared_ptr countConstr = std::make_shared( - markovianIndices, checkNumber); + + std::shared_ptr tleFailedConstr = std::make_shared( + timePointVariables.at(dft.getTopLevelIndex()), checkbound); std::shared_ptr manager = solver->getManager().getSharedPointer(); - solver->add(countConstr->toExpression(varNames, manager)); + solver->add(tleFailedConstr->toExpression(varNames, manager)); + // TODO comment + std::shared_ptr nonMarkovianConstr = std::make_shared( + markovianIndices, nrNonMarkovian); + solver->add(nonMarkovianConstr->toExpression(varNames, manager)); storm::solver::SmtSolver::CheckResult res = solver->check(); solver->pop(); return res; @@ -589,7 +592,7 @@ namespace storm { // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); // Constraint that toplevel element can fail with less than 'checkNumber' Markovian states visited - std::shared_ptr countConstr = std::make_shared( + std::shared_ptr countConstr = std::make_shared( markovianIndices, timepoint); // Constraint that TLE fails at timepoint std::shared_ptr timepointConstr = std::make_shared( @@ -605,24 +608,50 @@ namespace storm { uint64_t DFTASFChecker::correctLowerBound(uint64_t bound, uint_fast64_t timeout) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); STORM_LOG_DEBUG("Lower bound correction - try to correct bound " << std::to_string(bound)); - while (bound >= 0) { + uint64_t boundCandidate = bound; + uint64_t nrDepEvents = 0; + uint64_t nrNonMarkovian = 0; + // Count dependent events + for (size_t i = 0; i < dft.nrElements(); ++i) { + std::shared_ptr const> element = dft.getElement(i); + if (element->type() == storm::storage::DFTElementType::BE) { + auto be = std::static_pointer_cast const>(element); + if (be->hasIngoingDependencies()) { + ++nrDepEvents; + } + } + } + // Only need to check as long as bound candidate + nr of non-Markovians to check is smaller than number of dependent events + while (nrNonMarkovian <= nrDepEvents && boundCandidate > 0) { + STORM_LOG_TRACE( + "Lower bound correction - check possible bound " << std::to_string(boundCandidate) << " with " + << std::to_string(nrNonMarkovian) + << " non-Markovian states"); setSolverTimeout(timeout * 1000); - storm::solver::SmtSolver::CheckResult tmp_res = checkFailsWithLessThanMarkovianState(bound); + storm::solver::SmtSolver::CheckResult tmp_res = + checkFailsLeqWithEqNonMarkovianState(boundCandidate + nrNonMarkovian, nrNonMarkovian); unsetSolverTimeout(); switch (tmp_res) { - case storm::solver::SmtSolver::CheckResult::Unsat: - STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(bound)); - return bound; + case storm::solver::SmtSolver::CheckResult::Sat: + /* If SAT, there is a sequence where only boundCandidate-many BEs fail directly and rest is nonMarkovian. + * Bound candidate is vaild, therefore check the next one */ + STORM_LOG_TRACE("Lower bound correction - SAT"); + --boundCandidate; + break; case storm::solver::SmtSolver::CheckResult::Unknown: - STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to " - << std::to_string(bound)); - return bound; + // If any query returns unknown, we cannot be sure about the bound and fall back to the naive one + STORM_LOG_DEBUG("Lower bound correction - Solver returned 'Unknown', corrected to 1"); + return 1; default: - --bound; + // if query is UNSAT, increase number of non-Markovian states and try again + STORM_LOG_TRACE("Lower bound correction - UNSAT"); + ++nrNonMarkovian; break; } } - return bound; + // if for one candidate all queries are UNSAT, it is not valid. Return last valid candidate + STORM_LOG_DEBUG("Lower bound correction - corrected bound to " << std::to_string(boundCandidate + 1)); + return boundCandidate + 1; } uint64_t DFTASFChecker::correctUpperBound(uint64_t bound, uint_fast64_t timeout) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.h b/src/storm-dft/modelchecker/dft/DFTASFChecker.h index 36a71dff5..84310b775 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.h +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.h @@ -110,13 +110,16 @@ namespace storm { private: /** - * Helper function that checks if the DFT can fail while visiting less than a given number of Markovian states + * Helper function to check if the TLE fails before or at a given timepoint while visiting exactly + * a given number of non-Markovian states * - * @param checkNumber the number to check against - * @return "Sat" if a sequence of BE failures exists such that less than checkNumber Markovian states are visited, + * @param checkbound timepoint to check against + * @param nrNonMarkovian the number of non-Markovian states to check against + * @return "Sat" if a sequence of BE failures exists such that the constraints are satisfied, * "Unsat" if it does not, otherwise "Unknown" */ - storm::solver::SmtSolver::CheckResult checkFailsWithLessThanMarkovianState(uint64_t checkNumber); + storm::solver::SmtSolver::CheckResult + checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian); /** * Helper function that checks if the DFT can fail at a timepoint while visiting less than a given number of Markovian states @@ -128,7 +131,10 @@ namespace storm { storm::solver::SmtSolver::CheckResult checkFailsAtTimepointWithOnlyMarkovianState(uint64_t timepoint); /** - * Helper function for correction of least failure bound when dependencies are present + * Helper function for correction of least failure bound when dependencies are present. + * The main idea is to check if a later point of failure for the TLE than the pre-computed bound exists, but + * up until that point the number of non-Markovian states visited is so large, that less than the pre-computed bound BEs fail by themselves. + * The corrected bound is then (newTLEFailureTimepoint)-(nrNonMarkovianStatesVisited). This term is minimized. * * @param bound known lower bound to be corrected * @param timeout timeout timeout for each query in seconds diff --git a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp index 760146f13..78e963d05 100644 --- a/src/storm-dft/modelchecker/dft/SmtConstraint.cpp +++ b/src/storm-dft/modelchecker/dft/SmtConstraint.cpp @@ -598,9 +598,9 @@ namespace storm { std::shared_ptr elseConstraint; }; - class BoolCountIsLessConstant : public SmtConstraint { + class TrueCountIsLessConstant : public SmtConstraint { public: - BoolCountIsLessConstant(std::vector varIndices, uint64_t val) : varIndices(varIndices), + TrueCountIsLessConstant(std::vector varIndices, uint64_t val) : varIndices(varIndices), value(val) { } @@ -631,9 +631,42 @@ namespace storm { uint64_t value; }; - class BoolCountIsConstantValue : public SmtConstraint { + class FalseCountIsEqualConstant : public SmtConstraint { public: - BoolCountIsConstantValue(std::vector varIndices, uint64_t val) : varIndices(varIndices), + FalseCountIsEqualConstant(std::vector varIndices, uint64_t val) : varIndices(varIndices), + value(val) { + } + + std::string toSmtlib2(std::vector const &varNames) const override { + std::stringstream sstr; + sstr << "(= (+ "; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + sstr << "(ite " << varNames.at(varIndices.at(i)) << " 0 1 )"; + } + sstr << ") " << value << " )"; + return sstr.str(); + } + + storm::expressions::Expression toExpression(std::vector const &varNames, + std::shared_ptr manager) const override { + std::vector boolToInt; + for (uint64_t i = 0; i < varIndices.size(); ++i) { + boolToInt.push_back( + ite(manager->getVariableExpression(varNames.at(varIndices.at(i))), // If variable is true + manager->integer(0), // set 0 + manager->integer(1))); // else 1 + } + return sum(boolToInt) == manager->integer(value); + } + + private: + std::vector varIndices; + uint64_t value; + }; + + class TrueCountIsConstantValue : public SmtConstraint { + public: + TrueCountIsConstantValue(std::vector varIndices, uint64_t val) : varIndices(varIndices), value(val) { } From d42dea79c302f29d987d4c13db986bb24b91d1de Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 10 May 2019 14:03:54 +0200 Subject: [PATCH 23/44] Added comments to explain the query --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 7 ++++--- 1 file changed, 4 insertions(+), 3 deletions(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 0aaeb0a71..dcdcbb14c 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -561,18 +561,19 @@ namespace storm { DFTASFChecker::checkFailsLeqWithEqNonMarkovianState(uint64_t checkbound, uint64_t nrNonMarkovian) { STORM_LOG_ASSERT(solver, "SMT Solver was not initialized, call toSolver() before checking queries"); std::vector markovianIndices; - // Get Markovian variable indices + // Get Markovian variable indices up until given timepoint for (uint64_t i = 0; i < checkbound; ++i) { markovianIndices.push_back(markovianVariables.at(i)); } // Set backtracking marker to check several properties without reconstructing DFT encoding solver->push(); - + // Constraint that TLE fails before or during given timepoint std::shared_ptr tleFailedConstr = std::make_shared( timePointVariables.at(dft.getTopLevelIndex()), checkbound); std::shared_ptr manager = solver->getManager().getSharedPointer(); solver->add(tleFailedConstr->toExpression(varNames, manager)); - // TODO comment + + // Constraint that a given number of non-Markovian states are visited std::shared_ptr nonMarkovianConstr = std::make_shared( markovianIndices, nrNonMarkovian); solver->add(nonMarkovianConstr->toExpression(varNames, manager)); From f37bcea1eaf96268a96d8bdef371a36e96b32ca1 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Fri, 10 May 2019 14:32:28 +0200 Subject: [PATCH 24/44] Added test for bound correction --- resources/examples/testfiles/dft/fdep_bound.dft | 15 +++++++++++++++ src/test/storm-dft/api/DftSmtTest.cpp | 11 +++++++++++ 2 files changed, 26 insertions(+) create mode 100644 resources/examples/testfiles/dft/fdep_bound.dft diff --git a/resources/examples/testfiles/dft/fdep_bound.dft b/resources/examples/testfiles/dft/fdep_bound.dft new file mode 100644 index 000000000..4164d52a3 --- /dev/null +++ b/resources/examples/testfiles/dft/fdep_bound.dft @@ -0,0 +1,15 @@ +toplevel "A"; +"A" or "B" "C"; +"B" and "D" "L"; +"C" and "M" "N"; +"D" and "I" "J" "K"; +"DEP1" fdep "T" "I" "J" "K"; +"DEP2" fdep "D" "L"; + +"I" lambda=0.5 dorm=0; +"J" lambda=0.5 dorm=0.5; +"K" lambda=0.5 dorm=0.5; +"L" lambda=0.5 dorm=0.5; +"M" lambda=0.5 dorm=0.5; +"N" lambda=0.5 dorm=0.5; +"T" lambda=0.5 dorm=0.5; \ No newline at end of file diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp index 9404c5f5e..95bcad150 100644 --- a/src/test/storm-dft/api/DftSmtTest.cpp +++ b/src/test/storm-dft/api/DftSmtTest.cpp @@ -45,4 +45,15 @@ namespace { EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(2)); EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(4)); } + + TEST(DftSmtTest, FDEPBoundTest) { + std::shared_ptr> dft = + storm::api::loadDFTGalileoFile(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft"); + EXPECT_TRUE(storm::api::isWellFormed(*dft)); + storm::modelchecker::DFTASFChecker smtChecker(*dft); + smtChecker.convert(); + smtChecker.toSolver(); + EXPECT_EQ(smtChecker.getLeastFailureBound(30), uint64_t(1)); + EXPECT_EQ(smtChecker.getAlwaysFailedBound(30), uint64_t(5)); + } } \ No newline at end of file From 521461737a5f618d4b311d6cf6f06064e77638cd Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 12 May 2019 19:11:08 +0200 Subject: [PATCH 25/44] Adaption to changes in BEs --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index d2f3fa4a4..3b50c9098 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -95,7 +95,8 @@ namespace storm { } switch (element->type()) { - case storm::storage::DFTElementType::BE: + case storm::storage::DFTElementType::BE_EXP: + case storm::storage::DFTElementType::BE_CONST: // BEs were already considered before break; case storm::storage::DFTElementType::AND: From 799510044108cea51aac1c1df9fe2fd7bb835f38 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 12 May 2019 19:21:32 +0200 Subject: [PATCH 26/44] Small fixes in DFT tests --- .../storm-dft/api/DftModelCheckerTest.cpp | 25 +++++++++++-------- 1 file changed, 15 insertions(+), 10 deletions(-) diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp index dc68faf0e..96f9263c6 100644 --- a/src/test/storm-dft/api/DftModelCheckerTest.cpp +++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp @@ -11,6 +11,7 @@ namespace { bool useSR; bool useMod; bool useDC; + bool allowDCForRelevantEvents; }; class NoOptimizationsConfig { @@ -18,7 +19,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{false, false, false}; + return DftAnalysisConfig{false, false, false, true}; } }; @@ -27,7 +28,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{false, false, true}; + return DftAnalysisConfig{false, false, true, true}; } }; @@ -36,7 +37,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{false, true, false}; + return DftAnalysisConfig{false, true, false, true}; } }; @@ -45,7 +46,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{true, false, false}; + return DftAnalysisConfig{true, false, false, true}; } }; @@ -54,7 +55,7 @@ namespace { typedef double ValueType; static DftAnalysisConfig createConfig() { - return DftAnalysisConfig{true, true, true}; + return DftAnalysisConfig{true, true, true, true}; } }; @@ -77,11 +78,11 @@ namespace { std::string property = "Tmin=? [F \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property)); std::set relevantEvents; - if (config.useDC) { + if (!config.useDC) { relevantEvents = dft->getAllIds(); } typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, - relevantEvents, true); + relevantEvents, config.allowDCForRelevantEvents); return boost::get(results[0]); } @@ -91,8 +92,12 @@ namespace { std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]"; std::vector> properties = storm::api::extractFormulasFromProperties( storm::api::parseProperties(property)); - typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT( - *dft, properties, config.useSR, config.useMod, config.useDC, false); + std::set relevantEvents; + if (!config.useDC) { + relevantEvents = dft->getAllIds(); + } + typename storm::modelchecker::DFTModelChecker::dft_results results = storm::api::analyzeDFT(*dft, properties, config.useSR, config.useMod, + relevantEvents, config.allowDCForRelevantEvents); return boost::get(results[0]); } @@ -216,7 +221,7 @@ namespace { EXPECT_FLOAT_EQ(result, storm::utility::infinity()); } - TYPED_TEST(DftModelCheckerTest, HecsMTTF) { + TYPED_TEST(DftModelCheckerTest, HecsReliability) { double result = this->analyzeReliability(STORM_TEST_RESOURCES_DIR "/dft/hecs_2_2.dft", 1.0); EXPECT_FLOAT_EQ(result, 0.00021997582); } From 28a878f1542b11c1577d73b0998cb33e6d947394 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Mon, 13 May 2019 15:58:16 +0200 Subject: [PATCH 27/44] Adjusted lower bound correction to new BE distinction --- src/storm-dft/modelchecker/dft/DFTASFChecker.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 3b50c9098..0ed94401d 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -619,7 +619,8 @@ namespace storm { // Count dependent events for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if (element->type() == storm::storage::DFTElementType::BE) { + if (element->type() == storm::storage::DFTElementType::BE_EXP || + element->type() == storm::storage::DFTElementType::BE_CONST) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { ++nrDepEvents; From da31ca2952b57448cd46ad918b282af85bfddc35 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 21 May 2019 14:12:24 +0200 Subject: [PATCH 28/44] Main page info of Storm for Doxygen --- src/storm/storm.cpp | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/src/storm/storm.cpp b/src/storm/storm.cpp index 3cba6dd3d..a2d4aa0db 100644 --- a/src/storm/storm.cpp +++ b/src/storm/storm.cpp @@ -1,3 +1,12 @@ +/*! \mainpage Storm - A Modern Probabilistic Model Checker + * + * This document contains the Doxygen documentation of the Storm source code. + * + * \section more_info More information + * For more information, installation guides and tutorials on how to use Storm, visit the Storm website: http://www.stormchecker.org. + */ + + #include "storm/utility/macros.h" #include "storm/exceptions/BaseException.h" From 51d4652a2595cf90661d2447c65f9f046af608fa Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Tue, 21 May 2019 14:26:39 +0200 Subject: [PATCH 29/44] Updated generation of Doxygen documentation --- CMakeLists.txt | 18 +- resources/doxygen/CMakeLists.txt | 28 + resources/doxygen/Doxyfile.in | 2895 +++++++++++++++++++----------- 3 files changed, 1834 insertions(+), 1107 deletions(-) create mode 100644 resources/doxygen/CMakeLists.txt diff --git a/CMakeLists.txt b/CMakeLists.txt index 4ff9ea3a6..b2fe1b814 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -386,22 +386,8 @@ endif() # in the the system does not have a library include(resources/3rdparty/CMakeLists.txt) -############################################################# -## -## Doxygen -## -############################################################# - -find_package(Doxygen) -# Add a target to generate API documentation with Doxygen -if(DOXYGEN_FOUND) - set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") - string(REGEX REPLACE ";" " " CMAKE_DOXYGEN_INPUT_LIST "${PROJECT_SOURCE_DIR}/src") - - configure_file("${CMAKE_CURRENT_SOURCE_DIR}/resources/doxygen/Doxyfile.in" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY) - - add_custom_target(doc ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" COMMENT "Generating API documentation with Doxygen" VERBATIM) -endif(DOXYGEN_FOUND) +# Include Doxygen +include(resources/doxygen/CMakeLists.txt) ############################################################# ## diff --git a/resources/doxygen/CMakeLists.txt b/resources/doxygen/CMakeLists.txt new file mode 100644 index 000000000..6c74bbba9 --- /dev/null +++ b/resources/doxygen/CMakeLists.txt @@ -0,0 +1,28 @@ +find_package(Doxygen) +# Add a target to generate API documentation with Doxygen +if(DOXYGEN_FOUND) + + # We use the doxygen command of CMake instead of using the separate config file + set(DOXYGEN_PROJECT_NAME "Storm") + set(DOXYGEN_PROJECT_BRIEF "A Modern Probabilistic Model Checker") + set(DOXYGEN_BRIEF_MEMBER_DESC YES) + set(DOXYGEN_REPEAT_BRIEF YES) + set(DOXYGEN_JAVADOC_AUTOBRIEF YES) + set(DOXYGEN_QT_AUTOBRIEF YES) + set(DOXYGEN_EXTRACT_ALL YES) + set(DOXYGEN_EXTRACT_STATIC YES) + set(DOXYGEN_SOURCE_BROWSER YES) + set(DOXYGEN_GENERATE_TREEVIEW YES) + set(DOXYGEN_OUTPUT_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}/doc") + doxygen_add_docs( + doc + "${PROJECT_SOURCE_DIR}/src" + COMMENT "Generating API documentation with Doxygen" + ) + + # These commands can be used if the separate config files should be used + #set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc") + #string(REGEX REPLACE ";" " " CMAKE_DOXYGEN_INPUT_LIST "${PROJECT_SOURCE_DIR}/src") + #configure_file("${CMAKE_CURRENT_SOURCE_DIR}/resources/doxygen/Doxyfile.in.new" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY) + #add_custom_target(doc ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" COMMENT "Generating API documentation with Doxygen" VERBATIM) +endif(DOXYGEN_FOUND) diff --git a/resources/doxygen/Doxyfile.in b/resources/doxygen/Doxyfile.in index a328991e3..3e02d1458 100644 --- a/resources/doxygen/Doxyfile.in +++ b/resources/doxygen/Doxyfile.in @@ -1,104 +1,132 @@ -# Doxyfile 1.8.1.1 +# Doxyfile 1.8.15 # This file describes the settings to be used by the documentation system -# doxygen (www.doxygen.org) for a project +# doxygen (www.doxygen.org) for a project. # -# All text after a hash (#) is considered a comment and will be ignored +# All text after a double hash (##) is considered a comment and is placed in +# front of the TAG it is preceding. +# +# All text after a single hash (#) is considered a comment and will be ignored. # The format is: -# TAG = value [value, ...] -# For lists items can also be appended using: -# TAG += value [value, ...] -# Values that contain spaces should be placed between quotes (" ") +# TAG = value [value, ...] +# For lists, items can also be appended using: +# TAG += value [value, ...] +# Values that contain spaces should be placed between quotes (\" \"). #--------------------------------------------------------------------------- # Project related configuration options #--------------------------------------------------------------------------- -# This tag specifies the encoding used for all characters in the config file -# that follow. The default is UTF-8 which is also the encoding used for all -# text before the first occurrence of this tag. Doxygen uses libiconv (or the -# iconv built into libc) for the transcoding. See -# http://www.gnu.org/software/libiconv for the list of possible encodings. +# This tag specifies the encoding used for all characters in the configuration +# file that follow. The default is UTF-8 which is also the encoding used for all +# text before the first occurrence of this tag. Doxygen uses libiconv (or the +# iconv built into libc) for the transcoding. See +# https://www.gnu.org/software/libiconv/ for the list of possible encodings. +# The default value is: UTF-8. DOXYFILE_ENCODING = UTF-8 -# The PROJECT_NAME tag is a single word (or sequence of words) that should -# identify the project. Note that if you do not use Doxywizard you need -# to put quotes around the project name if it contains spaces. +# The PROJECT_NAME tag is a single word (or a sequence of words surrounded by +# double-quotes, unless you are using Doxywizard) that should identify the +# project for which the documentation is generated. This name is used in the +# title of most generated pages and in a few other places. +# The default value is: My Project. -PROJECT_NAME = "STORM" +PROJECT_NAME = "Storm" -# The PROJECT_NUMBER tag can be used to enter a project or revision number. -# This could be handy for archiving the generated documentation or -# if some version control system is used. +# The PROJECT_NUMBER tag can be used to enter a project or revision number. This +# could be handy for archiving the generated documentation or if some version +# control system is used. -PROJECT_NUMBER = +# TODO: set from storm-version +PROJECT_NUMBER = "1.3.0" -# Using the PROJECT_BRIEF tag one can provide an optional one line description -# for a project that appears at the top of each page and should give viewer -# a quick idea about the purpose of the project. Keep the description short. +# Using the PROJECT_BRIEF tag one can provide an optional one line description +# for a project that appears at the top of each page and should give viewer a +# quick idea about the purpose of the project. Keep the description short. -PROJECT_BRIEF = "A complete rewrite of MRMC in C++" +PROJECT_BRIEF = "A Modern Probabilistic Model Checker" -# With the PROJECT_LOGO tag one can specify an logo or icon that is -# included in the documentation. The maximum height of the logo should not -# exceed 55 pixels and the maximum width should not exceed 200 pixels. -# Doxygen will copy the logo to the output directory. +# With the PROJECT_LOGO tag one can specify a logo or an icon that is included +# in the documentation. The maximum height of the logo should not exceed 55 +# pixels and the maximum width should not exceed 200 pixels. Doxygen will copy +# the logo to the output directory. -PROJECT_LOGO = +# TODO: set logo? +PROJECT_LOGO = -# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) -# base path where the generated documentation will be put. -# If a relative path is entered, it will be relative to the location -# where doxygen was started. If left blank the current directory will be used. +# The OUTPUT_DIRECTORY tag is used to specify the (relative or absolute) path +# into which the generated documentation will be written. If a relative path is +# entered, it will be relative to the location where doxygen was started. If +# left blank the current directory will be used. OUTPUT_DIRECTORY = "@CMAKE_DOXYGEN_OUTPUT_DIR@" -# If the CREATE_SUBDIRS tag is set to YES, then doxygen will create -# 4096 sub-directories (in 2 levels) under the output directory of each output -# format and will distribute the generated files over these directories. -# Enabling this option can be useful when feeding doxygen a huge amount of -# source files, where putting all generated files in the same directory would -# otherwise cause performance problems for the file system. +# If the CREATE_SUBDIRS tag is set to YES then doxygen will create 4096 sub- +# directories (in 2 levels) under the output directory of each output format and +# will distribute the generated files over these directories. Enabling this +# option can be useful when feeding doxygen a huge amount of source files, where +# putting all generated files in the same directory would otherwise causes +# performance problems for the file system. +# The default value is: NO. CREATE_SUBDIRS = NO -# The OUTPUT_LANGUAGE tag is used to specify the language in which all -# documentation generated by doxygen is written. Doxygen will use this -# information to generate all constant output in the proper language. -# The default language is English, other supported languages are: -# Afrikaans, Arabic, Brazilian, Catalan, Chinese, Chinese-Traditional, -# Croatian, Czech, Danish, Dutch, Esperanto, Farsi, Finnish, French, German, -# Greek, Hungarian, Italian, Japanese, Japanese-en (Japanese with English -# messages), Korean, Korean-en, Lithuanian, Norwegian, Macedonian, Persian, -# Polish, Portuguese, Romanian, Russian, Serbian, Serbian-Cyrillic, Slovak, -# Slovene, Spanish, Swedish, Ukrainian, and Vietnamese. +# If the ALLOW_UNICODE_NAMES tag is set to YES, doxygen will allow non-ASCII +# characters to appear in the names of generated files. If set to NO, non-ASCII +# characters will be escaped, for example _xE3_x81_x84 will be used for Unicode +# U+3044. +# The default value is: NO. + +ALLOW_UNICODE_NAMES = NO + +# The OUTPUT_LANGUAGE tag is used to specify the language in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all constant output in the proper language. +# Possible values are: Afrikaans, Arabic, Armenian, Brazilian, Catalan, Chinese, +# Chinese-Traditional, Croatian, Czech, Danish, Dutch, English (United States), +# Esperanto, Farsi (Persian), Finnish, French, German, Greek, Hungarian, +# Indonesian, Italian, Japanese, Japanese-en (Japanese with English messages), +# Korean, Korean-en (Korean with English messages), Latvian, Lithuanian, +# Macedonian, Norwegian, Persian (Farsi), Polish, Portuguese, Romanian, Russian, +# Serbian, Serbian-Cyrillic, Slovak, Slovene, Spanish, Swedish, Turkish, +# Ukrainian and Vietnamese. +# The default value is: English. OUTPUT_LANGUAGE = English -# If the BRIEF_MEMBER_DESC tag is set to YES (the default) Doxygen will -# include brief member descriptions after the members that are listed in -# the file and class documentation (similar to JavaDoc). -# Set to NO to disable this. +# The OUTPUT_TEXT_DIRECTION tag is used to specify the direction in which all +# documentation generated by doxygen is written. Doxygen will use this +# information to generate all generated output in the proper direction. +# Possible values are: None, LTR, RTL and Context. +# The default value is: None. + +OUTPUT_TEXT_DIRECTION = None + +# If the BRIEF_MEMBER_DESC tag is set to YES, doxygen will include brief member +# descriptions after the members that are listed in the file and class +# documentation (similar to Javadoc). Set to NO to disable this. +# The default value is: YES. BRIEF_MEMBER_DESC = YES -# If the REPEAT_BRIEF tag is set to YES (the default) Doxygen will prepend -# the brief description of a member or function before the detailed description. -# Note: if both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the +# If the REPEAT_BRIEF tag is set to YES, doxygen will prepend the brief +# description of a member or function before the detailed description +# +# Note: If both HIDE_UNDOC_MEMBERS and BRIEF_MEMBER_DESC are set to NO, the # brief descriptions will be completely suppressed. +# The default value is: YES. REPEAT_BRIEF = YES -# This tag implements a quasi-intelligent brief description abbreviator -# that is used to form the text in various listings. Each string -# in this list, if found as the leading text of the brief description, will be -# stripped from the text and the result after processing the whole list, is -# used as the annotated text. Otherwise, the brief description is used as-is. -# If left blank, the following values are used ("$name" is automatically -# replaced with the name of the entity): "The $name class" "The $name widget" -# "The $name file" "is" "provides" "specifies" "contains" -# "represents" "a" "an" "the" +# This tag implements a quasi-intelligent brief description abbreviator that is +# used to form the text in various listings. Each string in this list, if found +# as the leading text of the brief description, will be stripped from the text +# and the result, after processing the whole list, is used as the annotated +# text. Otherwise, the brief description is used as-is. If left blank, the +# following values are used ($name is automatically replaced with the name of +# the entity):The $name class, The $name widget, The $name file, is, provides, +# specifies, contains, represents, a, an and the. ABBREVIATE_BRIEF = "The $name class" \ "The $name widget" \ @@ -112,247 +140,310 @@ ABBREVIATE_BRIEF = "The $name class" \ an \ the -# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then -# Doxygen will generate a detailed section even if there is only a brief +# If the ALWAYS_DETAILED_SEC and REPEAT_BRIEF tags are both set to YES then +# doxygen will generate a detailed section even if there is only a brief # description. +# The default value is: NO. ALWAYS_DETAILED_SEC = NO -# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all -# inherited members of a class in the documentation of that class as if those -# members were ordinary class members. Constructors, destructors and assignment +# If the INLINE_INHERITED_MEMB tag is set to YES, doxygen will show all +# inherited members of a class in the documentation of that class as if those +# members were ordinary class members. Constructors, destructors and assignment # operators of the base classes will not be shown. +# The default value is: NO. INLINE_INHERITED_MEMB = NO -# If the FULL_PATH_NAMES tag is set to YES then Doxygen will prepend the full -# path before files name in the file list and in the header files. If set -# to NO the shortest path that makes the file name unique will be used. +# If the FULL_PATH_NAMES tag is set to YES, doxygen will prepend the full path +# before files name in the file list and in the header files. If set to NO the +# shortest path that makes the file name unique will be used +# The default value is: YES. FULL_PATH_NAMES = YES -# If the FULL_PATH_NAMES tag is set to YES then the STRIP_FROM_PATH tag -# can be used to strip a user-defined part of the path. Stripping is -# only done if one of the specified strings matches the left-hand part of -# the path. The tag can be used to show relative paths in the file list. -# If left blank the directory from which doxygen is run is used as the -# path to strip. +# The STRIP_FROM_PATH tag can be used to strip a user-defined part of the path. +# Stripping is only done if one of the specified strings matches the left-hand +# part of the path. The tag can be used to show relative paths in the file list. +# If left blank the directory from which doxygen is run is used as the path to +# strip. +# +# Note that you can specify absolute paths here, but also relative paths, which +# will be relative from the directory where doxygen is started. +# This tag requires that the tag FULL_PATH_NAMES is set to YES. -STRIP_FROM_PATH = +STRIP_FROM_PATH = -# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of -# the path mentioned in the documentation of a class, which tells -# the reader which header file to include in order to use a class. -# If left blank only the name of the header file containing the class -# definition is used. Otherwise one should specify the include paths that -# are normally passed to the compiler using the -I flag. +# The STRIP_FROM_INC_PATH tag can be used to strip a user-defined part of the +# path mentioned in the documentation of a class, which tells the reader which +# header file to include in order to use a class. If left blank only the name of +# the header file containing the class definition is used. Otherwise one should +# specify the list of include paths that are normally passed to the compiler +# using the -I flag. -STRIP_FROM_INC_PATH = +STRIP_FROM_INC_PATH = -# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter -# (but less readable) file names. This can be useful if your file system -# doesn't support long names like on DOS, Mac, or CD-ROM. +# If the SHORT_NAMES tag is set to YES, doxygen will generate much shorter (but +# less readable) file names. This can be useful is your file systems doesn't +# support long names like on DOS, Mac, or CD-ROM. +# The default value is: NO. SHORT_NAMES = NO -# If the JAVADOC_AUTOBRIEF tag is set to YES then Doxygen -# will interpret the first line (until the first dot) of a JavaDoc-style -# comment as the brief description. If set to NO, the JavaDoc -# comments will behave just like regular Qt-style comments -# (thus requiring an explicit @brief command for a brief description.) +# If the JAVADOC_AUTOBRIEF tag is set to YES then doxygen will interpret the +# first line (until the first dot) of a Javadoc-style comment as the brief +# description. If set to NO, the Javadoc-style will behave just like regular Qt- +# style comments (thus requiring an explicit @brief command for a brief +# description.) +# The default value is: NO. -JAVADOC_AUTOBRIEF = NO +JAVADOC_AUTOBRIEF = YES -# If the QT_AUTOBRIEF tag is set to YES then Doxygen will -# interpret the first line (until the first dot) of a Qt-style -# comment as the brief description. If set to NO, the comments -# will behave just like regular Qt-style comments (thus requiring -# an explicit \brief command for a brief description.) +# If the QT_AUTOBRIEF tag is set to YES then doxygen will interpret the first +# line (until the first dot) of a Qt-style comment as the brief description. If +# set to NO, the Qt-style will behave just like regular Qt-style comments (thus +# requiring an explicit \brief command for a brief description.) +# The default value is: NO. -QT_AUTOBRIEF = NO +QT_AUTOBRIEF = YES -# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make Doxygen -# treat a multi-line C++ special comment block (i.e. a block of //! or /// -# comments) as a brief description. This used to be the default behaviour. -# The new default is to treat a multi-line C++ comment block as a detailed -# description. Set this tag to YES if you prefer the old behaviour instead. +# The MULTILINE_CPP_IS_BRIEF tag can be set to YES to make doxygen treat a +# multi-line C++ special comment block (i.e. a block of //! or /// comments) as +# a brief description. This used to be the default behavior. The new default is +# to treat a multi-line C++ comment block as a detailed description. Set this +# tag to YES if you prefer the old behavior instead. +# +# Note that setting this tag to YES also means that rational rose comments are +# not recognized any more. +# The default value is: NO. MULTILINE_CPP_IS_BRIEF = NO -# If the INHERIT_DOCS tag is set to YES (the default) then an undocumented -# member inherits the documentation from any documented member that it -# re-implements. +# If the INHERIT_DOCS tag is set to YES then an undocumented member inherits the +# documentation from any documented member that it re-implements. +# The default value is: YES. INHERIT_DOCS = YES -# If the SEPARATE_MEMBER_PAGES tag is set to YES, then doxygen will produce -# a new page for each member. If set to NO, the documentation of a member will -# be part of the file/class/namespace that contains it. +# If the SEPARATE_MEMBER_PAGES tag is set to YES then doxygen will produce a new +# page for each member. If set to NO, the documentation of a member will be part +# of the file/class/namespace that contains it. +# The default value is: NO. SEPARATE_MEMBER_PAGES = NO -# The TAB_SIZE tag can be used to set the number of spaces in a tab. -# Doxygen uses this value to replace tabs by spaces in code fragments. +# The TAB_SIZE tag can be used to set the number of spaces in a tab. Doxygen +# uses this value to replace tabs by spaces in code fragments. +# Minimum value: 1, maximum value: 16, default value: 4. + +TAB_SIZE = 4 + +# This tag can be used to specify a number of aliases that act as commands in +# the documentation. An alias has the form: +# name=value +# For example adding +# "sideeffect=@par Side Effects:\n" +# will allow you to put the command \sideeffect (or @sideeffect) in the +# documentation, which will result in a user-defined paragraph with heading +# "Side Effects:". You can put \n's in the value part of an alias to insert +# newlines (in the resulting output). You can put ^^ in the value part of an +# alias to insert a newline as if a physical newline was in the original file. +# When you need a literal { or } or , in the value part of an alias you have to +# escape them by means of a backslash (\), this can lead to conflicts with the +# commands \{ and \} for these it is advised to use the version @{ and @} or use +# a double escape (\\{ and \\}) + +ALIASES = + +# This tag can be used to specify a number of word-keyword mappings (TCL only). +# A mapping has the form "name=value". For example adding "class=itcl::class" +# will allow you to use the command class in the itcl::class meaning. + +TCL_SUBST = + +# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C sources +# only. Doxygen will then generate output that is more tailored for C. For +# instance, some of the names that are used will be different. The list of all +# members will be omitted, etc. +# The default value is: NO. -TAB_SIZE = 8 +OPTIMIZE_OUTPUT_FOR_C = NO -# This tag can be used to specify a number of aliases that acts -# as commands in the documentation. An alias has the form "name=value". -# For example adding "sideeffect=\par Side Effects:\n" will allow you to -# put the command \sideeffect (or @sideeffect) in the documentation, which -# will result in a user-defined paragraph with heading "Side Effects:". -# You can put \n's in the value part of an alias to insert newlines. +# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java or +# Python sources only. Doxygen will then generate output that is more tailored +# for that language. For instance, namespaces will be presented as packages, +# qualified scopes will look different, etc. +# The default value is: NO. -ALIASES = +OPTIMIZE_OUTPUT_JAVA = NO -# This tag can be used to specify a number of word-keyword mappings (TCL only). -# A mapping has the form "name=value". For example adding -# "class=itcl::class" will allow you to use the command class in the -# itcl::class meaning. +# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran +# sources. Doxygen will then generate output that is tailored for Fortran. +# The default value is: NO. -TCL_SUBST = +OPTIMIZE_FOR_FORTRAN = NO -# Set the OPTIMIZE_OUTPUT_FOR_C tag to YES if your project consists of C -# sources only. Doxygen will then generate output that is more tailored for C. -# For instance, some of the names that are used will be different. The list -# of all members will be omitted, etc. +# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL +# sources. Doxygen will then generate output that is tailored for VHDL. +# The default value is: NO. -OPTIMIZE_OUTPUT_FOR_C = NO +OPTIMIZE_OUTPUT_VHDL = NO -# Set the OPTIMIZE_OUTPUT_JAVA tag to YES if your project consists of Java -# sources only. Doxygen will then generate output that is more tailored for -# Java. For instance, namespaces will be presented as packages, qualified -# scopes will look different, etc. +# Set the OPTIMIZE_OUTPUT_SLICE tag to YES if your project consists of Slice +# sources only. Doxygen will then generate output that is more tailored for that +# language. For instance, namespaces will be presented as modules, types will be +# separated into more groups, etc. +# The default value is: NO. + +OPTIMIZE_OUTPUT_SLICE = NO + +# Doxygen selects the parser to use depending on the extension of the files it +# parses. With this tag you can assign which parser to use for a given +# extension. Doxygen has a built-in mapping, but you can override or extend it +# using this tag. The format is ext=language, where ext is a file extension, and +# language is one of the parsers supported by doxygen: IDL, Java, Javascript, +# Csharp (C#), C, C++, D, PHP, md (Markdown), Objective-C, Python, Slice, +# Fortran (fixed format Fortran: FortranFixed, free formatted Fortran: +# FortranFree, unknown formatted Fortran: Fortran. In the later case the parser +# tries to guess whether the code is fixed or free formatted code, this is the +# default for Fortran type files), VHDL, tcl. For instance to make doxygen treat +# .inc files as Fortran files (default is PHP), and .f files as C (default is +# Fortran), use: inc=Fortran f=C. +# +# Note: For files without extension you can use no_extension as a placeholder. +# +# Note that for custom extensions you also need to set FILE_PATTERNS otherwise +# the files are not read by doxygen. -OPTIMIZE_OUTPUT_JAVA = NO +EXTENSION_MAPPING = -# Set the OPTIMIZE_FOR_FORTRAN tag to YES if your project consists of Fortran -# sources only. Doxygen will then generate output that is more tailored for -# Fortran. +# If the MARKDOWN_SUPPORT tag is enabled then doxygen pre-processes all comments +# according to the Markdown format, which allows for more readable +# documentation. See https://daringfireball.net/projects/markdown/ for details. +# The output of markdown processing is further processed by doxygen, so you can +# mix doxygen, HTML, and XML commands with Markdown formatting. Disable only in +# case of backward compatibilities issues. +# The default value is: YES. -OPTIMIZE_FOR_FORTRAN = NO +MARKDOWN_SUPPORT = YES -# Set the OPTIMIZE_OUTPUT_VHDL tag to YES if your project consists of VHDL -# sources. Doxygen will then generate output that is tailored for -# VHDL. +# When the TOC_INCLUDE_HEADINGS tag is set to a non-zero value, all headings up +# to that level are automatically included in the table of contents, even if +# they do not have an id attribute. +# Note: This feature currently applies only to Markdown headings. +# Minimum value: 0, maximum value: 99, default value: 0. +# This tag requires that the tag MARKDOWN_SUPPORT is set to YES. -OPTIMIZE_OUTPUT_VHDL = NO +TOC_INCLUDE_HEADINGS = 0 -# Doxygen selects the parser to use depending on the extension of the files it -# parses. With this tag you can assign which parser to use for a given extension. -# Doxygen has a built-in mapping, but you can override or extend it using this -# tag. The format is ext=language, where ext is a file extension, and language -# is one of the parsers supported by doxygen: IDL, Java, Javascript, CSharp, C, -# C++, D, PHP, Objective-C, Python, Fortran, VHDL, C, C++. For instance to make -# doxygen treat .inc files as Fortran files (default is PHP), and .f files as C -# (default is Fortran), use: inc=Fortran f=C. Note that for custom extensions -# you also need to set FILE_PATTERNS otherwise the files are not read by doxygen. - -EXTENSION_MAPPING = - -# If MARKDOWN_SUPPORT is enabled (the default) then doxygen pre-processes all -# comments according to the Markdown format, which allows for more readable -# documentation. See http://daringfireball.net/projects/markdown/ for details. -# The output of markdown processing is further processed by doxygen, so you -# can mix doxygen, HTML, and XML commands with Markdown formatting. -# Disable only in case of backward compatibilities issues. +# When enabled doxygen tries to link words that correspond to documented +# classes, or namespaces to their corresponding documentation. Such a link can +# be prevented in individual cases by putting a % sign in front of the word or +# globally by setting AUTOLINK_SUPPORT to NO. +# The default value is: YES. -MARKDOWN_SUPPORT = YES +AUTOLINK_SUPPORT = YES -# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want -# to include (a tag file for) the STL sources as input, then you should -# set this tag to YES in order to let doxygen match functions declarations and -# definitions whose arguments contain STL classes (e.g. func(std::string); v.s. -# func(std::string) {}). This also makes the inheritance and collaboration +# If you use STL classes (i.e. std::string, std::vector, etc.) but do not want +# to include (a tag file for) the STL sources as input, then you should set this +# tag to YES in order to let doxygen match functions declarations and +# definitions whose arguments contain STL classes (e.g. func(std::string); +# versus func(std::string) {}). This also make the inheritance and collaboration # diagrams that involve STL classes more complete and accurate. +# The default value is: NO. BUILTIN_STL_SUPPORT = NO -# If you use Microsoft's C++/CLI language, you should set this option to YES to +# If you use Microsoft's C++/CLI language, you should set this option to YES to # enable parsing support. +# The default value is: NO. CPP_CLI_SUPPORT = NO -# Set the SIP_SUPPORT tag to YES if your project consists of sip sources only. -# Doxygen will parse them like normal C++ but will assume all classes use public -# instead of private inheritance when no explicit protection keyword is present. +# Set the SIP_SUPPORT tag to YES if your project consists of sip (see: +# https://www.riverbankcomputing.com/software/sip/intro) sources only. Doxygen +# will parse them like normal C++ but will assume all classes use public instead +# of private inheritance when no explicit protection keyword is present. +# The default value is: NO. SIP_SUPPORT = NO -# For Microsoft's IDL there are propget and propput attributes to indicate getter -# and setter methods for a property. Setting this option to YES (the default) -# will make doxygen replace the get and set methods by a property in the -# documentation. This will only work if the methods are indeed getting or -# setting a simple type. If this is not the case, or you want to show the -# methods anyway, you should set this option to NO. +# For Microsoft's IDL there are propget and propput attributes to indicate +# getter and setter methods for a property. Setting this option to YES will make +# doxygen to replace the get and set methods by a property in the documentation. +# This will only work if the methods are indeed getting or setting a simple +# type. If this is not the case, or you want to show the methods anyway, you +# should set this option to NO. +# The default value is: YES. IDL_PROPERTY_SUPPORT = YES -# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC -# tag is set to YES, then doxygen will reuse the documentation of the first -# member in the group (if any) for the other members of the group. By default +# If member grouping is used in the documentation and the DISTRIBUTE_GROUP_DOC +# tag is set to YES then doxygen will reuse the documentation of the first +# member in the group (if any) for the other members of the group. By default # all members of a group must be documented explicitly. +# The default value is: NO. DISTRIBUTE_GROUP_DOC = NO -# Set the SUBGROUPING tag to YES (the default) to allow class member groups of -# the same type (for instance a group of public functions) to be put as a -# subgroup of that type (e.g. under the Public Functions section). Set it to -# NO to prevent subgrouping. Alternatively, this can be done per class using -# the \nosubgrouping command. +# If one adds a struct or class to a group and this option is enabled, then also +# any nested class or struct is added to the same group. By default this option +# is disabled and one has to add nested compounds explicitly via \ingroup. +# The default value is: NO. + +GROUP_NESTED_COMPOUNDS = NO + +# Set the SUBGROUPING tag to YES to allow class member groups of the same type +# (for instance a group of public functions) to be put as a subgroup of that +# type (e.g. under the Public Functions section). Set it to NO to prevent +# subgrouping. Alternatively, this can be done per class using the +# \nosubgrouping command. +# The default value is: YES. SUBGROUPING = YES -# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and -# unions are shown inside the group in which they are included (e.g. using -# @ingroup) instead of on a separate page (for HTML and Man pages) or -# section (for LaTeX and RTF). +# When the INLINE_GROUPED_CLASSES tag is set to YES, classes, structs and unions +# are shown inside the group in which they are included (e.g. using \ingroup) +# instead of on a separate page (for HTML and Man pages) or section (for LaTeX +# and RTF). +# +# Note that this feature does not work in combination with +# SEPARATE_MEMBER_PAGES. +# The default value is: NO. INLINE_GROUPED_CLASSES = NO -# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and -# unions with only public data fields will be shown inline in the documentation -# of the scope in which they are defined (i.e. file, namespace, or group -# documentation), provided this scope is documented. If set to NO (the default), -# structs, classes, and unions are shown on a separate page (for HTML and Man -# pages) or section (for LaTeX and RTF). +# When the INLINE_SIMPLE_STRUCTS tag is set to YES, structs, classes, and unions +# with only public data fields or simple typedef fields will be shown inline in +# the documentation of the scope in which they are defined (i.e. file, +# namespace, or group documentation), provided this scope is documented. If set +# to NO, structs, classes, and unions are shown on a separate page (for HTML and +# Man pages) or section (for LaTeX and RTF). +# The default value is: NO. INLINE_SIMPLE_STRUCTS = NO -# When TYPEDEF_HIDES_STRUCT is enabled, a typedef of a struct, union, or enum -# is documented as struct, union, or enum with the name of the typedef. So -# typedef struct TypeS {} TypeT, will appear in the documentation as a struct -# with name TypeT. When disabled the typedef will appear as a member of a file, -# namespace, or class. And the struct will be named TypeS. This can typically -# be useful for C code in case the coding convention dictates that all compound +# When TYPEDEF_HIDES_STRUCT tag is enabled, a typedef of a struct, union, or +# enum is documented as struct, union, or enum with the name of the typedef. So +# typedef struct TypeS {} TypeT, will appear in the documentation as a struct +# with name TypeT. When disabled the typedef will appear as a member of a file, +# namespace, or class. And the struct will be named TypeS. This can typically be +# useful for C code in case the coding convention dictates that all compound # types are typedef'ed and only the typedef is referenced, never the tag name. +# The default value is: NO. TYPEDEF_HIDES_STRUCT = NO -# The SYMBOL_CACHE_SIZE determines the size of the internal cache use to -# determine which symbols to keep in memory and which to flush to disk. -# When the cache is full, less often used symbols will be written to disk. -# For small to medium size projects (<1000 input files) the default value is -# probably good enough. For larger projects a too small cache size can cause -# doxygen to be busy swapping symbols to and from disk most of the time -# causing a significant performance penalty. -# If the system has enough physical memory increasing the cache will improve the -# performance by keeping more symbols in memory. Note that the value works on -# a logarithmic scale so increasing the size by one will roughly double the -# memory usage. The cache size is given by this formula: -# 2^(16+SYMBOL_CACHE_SIZE). The valid range is 0..9, the default is 0, -# corresponding to a cache size of 2^16 = 65536 symbols. - -SYMBOL_CACHE_SIZE = 0 - -# Similar to the SYMBOL_CACHE_SIZE the size of the symbol lookup cache can be -# set using LOOKUP_CACHE_SIZE. This cache is used to resolve symbols given -# their name and scope. Since this can be an expensive process and often the -# same symbol appear multiple times in the code, doxygen keeps a cache of -# pre-resolved symbols. If the cache is too small doxygen will become slower. -# If the cache is too large, memory is wasted. The cache size is given by this -# formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range is 0..9, the default is 0, -# corresponding to a cache size of 2^16 = 65536 symbols. +# The size of the symbol lookup cache can be set using LOOKUP_CACHE_SIZE. This +# cache is used to resolve symbols given their name and scope. Since this can be +# an expensive process and often the same symbol appears multiple times in the +# code, doxygen keeps a cache of pre-resolved symbols. If the cache is too small +# doxygen will become slower. If the cache is too large, memory is wasted. The +# cache size is given by this formula: 2^(16+LOOKUP_CACHE_SIZE). The valid range +# is 0..9, the default is 0, corresponding to a cache size of 2^16=65536 +# symbols. At the end of a run doxygen will report the cache usage and suggest +# the optimal cache size from a speed point of view. +# Minimum value: 0, maximum value: 9, default value: 0. LOOKUP_CACHE_SIZE = 0 @@ -360,351 +451,421 @@ LOOKUP_CACHE_SIZE = 0 # Build related configuration options #--------------------------------------------------------------------------- -# If the EXTRACT_ALL tag is set to YES doxygen will assume all entities in -# documentation are documented, even if no documentation was available. -# Private class members and static file members will be hidden unless -# the EXTRACT_PRIVATE and EXTRACT_STATIC tags are set to YES +# If the EXTRACT_ALL tag is set to YES, doxygen will assume all entities in +# documentation are documented, even if no documentation was available. Private +# class members and static file members will be hidden unless the +# EXTRACT_PRIVATE respectively EXTRACT_STATIC tags are set to YES. +# Note: This will also disable the warnings about undocumented members that are +# normally produced when WARNINGS is set to YES. +# The default value is: NO. EXTRACT_ALL = YES -# If the EXTRACT_PRIVATE tag is set to YES all private members of a class -# will be included in the documentation. +# If the EXTRACT_PRIVATE tag is set to YES, all private members of a class will +# be included in the documentation. +# The default value is: NO. EXTRACT_PRIVATE = NO -# If the EXTRACT_PACKAGE tag is set to YES all members with package or internal +# If the EXTRACT_PACKAGE tag is set to YES, all members with package or internal # scope will be included in the documentation. +# The default value is: NO. EXTRACT_PACKAGE = NO -# If the EXTRACT_STATIC tag is set to YES all static members of a file -# will be included in the documentation. +# If the EXTRACT_STATIC tag is set to YES, all static members of a file will be +# included in the documentation. +# The default value is: NO. EXTRACT_STATIC = YES -# If the EXTRACT_LOCAL_CLASSES tag is set to YES classes (and structs) -# defined locally in source files will be included in the documentation. -# If set to NO only classes defined in header files are included. +# If the EXTRACT_LOCAL_CLASSES tag is set to YES, classes (and structs) defined +# locally in source files will be included in the documentation. If set to NO, +# only classes defined in header files are included. Does not have any effect +# for Java sources. +# The default value is: YES. EXTRACT_LOCAL_CLASSES = YES -# This flag is only useful for Objective-C code. When set to YES local -# methods, which are defined in the implementation section but not in -# the interface are included in the documentation. -# If set to NO (the default) only methods in the interface are included. +# This flag is only useful for Objective-C code. If set to YES, local methods, +# which are defined in the implementation section but not in the interface are +# included in the documentation. If set to NO, only methods in the interface are +# included. +# The default value is: NO. EXTRACT_LOCAL_METHODS = NO -# If this flag is set to YES, the members of anonymous namespaces will be -# extracted and appear in the documentation as a namespace called -# 'anonymous_namespace{file}', where file will be replaced with the base -# name of the file that contains the anonymous namespace. By default -# anonymous namespaces are hidden. +# If this flag is set to YES, the members of anonymous namespaces will be +# extracted and appear in the documentation as a namespace called +# 'anonymous_namespace{file}', where file will be replaced with the base name of +# the file that contains the anonymous namespace. By default anonymous namespace +# are hidden. +# The default value is: NO. EXTRACT_ANON_NSPACES = NO -# If the HIDE_UNDOC_MEMBERS tag is set to YES, Doxygen will hide all -# undocumented members of documented classes, files or namespaces. -# If set to NO (the default) these members will be included in the -# various overviews, but no documentation section is generated. -# This option has no effect if EXTRACT_ALL is enabled. +# If the HIDE_UNDOC_MEMBERS tag is set to YES, doxygen will hide all +# undocumented members inside documented classes or files. If set to NO these +# members will be included in the various overviews, but no documentation +# section is generated. This option has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. HIDE_UNDOC_MEMBERS = NO -# If the HIDE_UNDOC_CLASSES tag is set to YES, Doxygen will hide all -# undocumented classes that are normally visible in the class hierarchy. -# If set to NO (the default) these classes will be included in the various -# overviews. This option has no effect if EXTRACT_ALL is enabled. +# If the HIDE_UNDOC_CLASSES tag is set to YES, doxygen will hide all +# undocumented classes that are normally visible in the class hierarchy. If set +# to NO, these classes will be included in the various overviews. This option +# has no effect if EXTRACT_ALL is enabled. +# The default value is: NO. HIDE_UNDOC_CLASSES = NO -# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, Doxygen will hide all -# friend (class|struct|union) declarations. -# If set to NO (the default) these declarations will be included in the -# documentation. +# If the HIDE_FRIEND_COMPOUNDS tag is set to YES, doxygen will hide all friend +# (class|struct|union) declarations. If set to NO, these declarations will be +# included in the documentation. +# The default value is: NO. HIDE_FRIEND_COMPOUNDS = NO -# If the HIDE_IN_BODY_DOCS tag is set to YES, Doxygen will hide any -# documentation blocks found inside the body of a function. -# If set to NO (the default) these blocks will be appended to the -# function's detailed documentation block. +# If the HIDE_IN_BODY_DOCS tag is set to YES, doxygen will hide any +# documentation blocks found inside the body of a function. If set to NO, these +# blocks will be appended to the function's detailed documentation block. +# The default value is: NO. HIDE_IN_BODY_DOCS = NO -# The INTERNAL_DOCS tag determines if documentation -# that is typed after a \internal command is included. If the tag is set -# to NO (the default) then the documentation will be excluded. -# Set it to YES to include the internal documentation. +# The INTERNAL_DOCS tag determines if documentation that is typed after a +# \internal command is included. If the tag is set to NO then the documentation +# will be excluded. Set it to YES to include the internal documentation. +# The default value is: NO. INTERNAL_DOCS = NO -# If the CASE_SENSE_NAMES tag is set to NO then Doxygen will only generate -# file names in lower-case letters. If set to YES upper-case letters are also -# allowed. This is useful if you have classes or files whose names only differ -# in case and if your file system supports case sensitive file names. Windows +# If the CASE_SENSE_NAMES tag is set to NO then doxygen will only generate file +# names in lower-case letters. If set to YES, upper-case letters are also +# allowed. This is useful if you have classes or files whose names only differ +# in case and if your file system supports case sensitive file names. Windows # and Mac users are advised to set this option to NO. +# The default value is: system dependent. CASE_SENSE_NAMES = NO -# If the HIDE_SCOPE_NAMES tag is set to NO (the default) then Doxygen -# will show members with their full class and namespace scopes in the -# documentation. If set to YES the scope will be hidden. +# If the HIDE_SCOPE_NAMES tag is set to NO then doxygen will show members with +# their full class and namespace scopes in the documentation. If set to YES, the +# scope will be hidden. +# The default value is: NO. HIDE_SCOPE_NAMES = NO -# If the SHOW_INCLUDE_FILES tag is set to YES (the default) then Doxygen -# will put a list of the files that are included by a file in the documentation -# of that file. +# If the HIDE_COMPOUND_REFERENCE tag is set to NO (default) then doxygen will +# append additional text to a page's title, such as Class Reference. If set to +# YES the compound reference will be hidden. +# The default value is: NO. + +HIDE_COMPOUND_REFERENCE= NO + +# If the SHOW_INCLUDE_FILES tag is set to YES then doxygen will put a list of +# the files that are included by a file in the documentation of that file. +# The default value is: YES. SHOW_INCLUDE_FILES = YES -# If the FORCE_LOCAL_INCLUDES tag is set to YES then Doxygen -# will list include files with double quotes in the documentation -# rather than with sharp brackets. +# If the SHOW_GROUPED_MEMB_INC tag is set to YES then Doxygen will add for each +# grouped member an include statement to the documentation, telling the reader +# which file to include in order to use the member. +# The default value is: NO. + +SHOW_GROUPED_MEMB_INC = NO + +# If the FORCE_LOCAL_INCLUDES tag is set to YES then doxygen will list include +# files with double quotes in the documentation rather than with sharp brackets. +# The default value is: NO. FORCE_LOCAL_INCLUDES = NO -# If the INLINE_INFO tag is set to YES (the default) then a tag [inline] -# is inserted in the documentation for inline members. +# If the INLINE_INFO tag is set to YES then a tag [inline] is inserted in the +# documentation for inline members. +# The default value is: YES. INLINE_INFO = YES -# If the SORT_MEMBER_DOCS tag is set to YES (the default) then doxygen -# will sort the (detailed) documentation of file and class members -# alphabetically by member name. If set to NO the members will appear in -# declaration order. +# If the SORT_MEMBER_DOCS tag is set to YES then doxygen will sort the +# (detailed) documentation of file and class members alphabetically by member +# name. If set to NO, the members will appear in declaration order. +# The default value is: YES. SORT_MEMBER_DOCS = YES -# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the -# brief documentation of file, namespace and class members alphabetically -# by member name. If set to NO (the default) the members will appear in -# declaration order. +# If the SORT_BRIEF_DOCS tag is set to YES then doxygen will sort the brief +# descriptions of file, namespace and class members alphabetically by member +# name. If set to NO, the members will appear in declaration order. Note that +# this will also influence the order of the classes in the class list. +# The default value is: NO. SORT_BRIEF_DOCS = NO -# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen -# will sort the (brief and detailed) documentation of class members so that -# constructors and destructors are listed first. If set to NO (the default) -# the constructors will appear in the respective orders defined by -# SORT_MEMBER_DOCS and SORT_BRIEF_DOCS. -# This tag will be ignored for brief docs if SORT_BRIEF_DOCS is set to NO -# and ignored for detailed docs if SORT_MEMBER_DOCS is set to NO. +# If the SORT_MEMBERS_CTORS_1ST tag is set to YES then doxygen will sort the +# (brief and detailed) documentation of class members so that constructors and +# destructors are listed first. If set to NO the constructors will appear in the +# respective orders defined by SORT_BRIEF_DOCS and SORT_MEMBER_DOCS. +# Note: If SORT_BRIEF_DOCS is set to NO this option is ignored for sorting brief +# member documentation. +# Note: If SORT_MEMBER_DOCS is set to NO this option is ignored for sorting +# detailed member documentation. +# The default value is: NO. SORT_MEMBERS_CTORS_1ST = NO -# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the -# hierarchy of group names into alphabetical order. If set to NO (the default) -# the group names will appear in their defined order. +# If the SORT_GROUP_NAMES tag is set to YES then doxygen will sort the hierarchy +# of group names into alphabetical order. If set to NO the group names will +# appear in their defined order. +# The default value is: NO. SORT_GROUP_NAMES = NO -# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be -# sorted by fully-qualified names, including namespaces. If set to -# NO (the default), the class list will be sorted only by class name, -# not including the namespace part. -# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. -# Note: This option applies only to the class list, not to the -# alphabetical list. +# If the SORT_BY_SCOPE_NAME tag is set to YES, the class list will be sorted by +# fully-qualified names, including namespaces. If set to NO, the class list will +# be sorted only by class name, not including the namespace part. +# Note: This option is not very useful if HIDE_SCOPE_NAMES is set to YES. +# Note: This option applies only to the class list, not to the alphabetical +# list. +# The default value is: NO. SORT_BY_SCOPE_NAME = NO -# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to -# do proper type resolution of all parameters of a function it will reject a -# match between the prototype and the implementation of a member function even -# if there is only one candidate or it is obvious which candidate to choose -# by doing a simple string match. By disabling STRICT_PROTO_MATCHING doxygen -# will still accept a match between prototype and implementation in such cases. +# If the STRICT_PROTO_MATCHING option is enabled and doxygen fails to do proper +# type resolution of all parameters of a function it will reject a match between +# the prototype and the implementation of a member function even if there is +# only one candidate or it is obvious which candidate to choose by doing a +# simple string match. By disabling STRICT_PROTO_MATCHING doxygen will still +# accept a match between prototype and implementation in such cases. +# The default value is: NO. STRICT_PROTO_MATCHING = NO -# The GENERATE_TODOLIST tag can be used to enable (YES) or -# disable (NO) the todo list. This list is created by putting \todo -# commands in the documentation. +# The GENERATE_TODOLIST tag can be used to enable (YES) or disable (NO) the todo +# list. This list is created by putting \todo commands in the documentation. +# The default value is: YES. GENERATE_TODOLIST = YES -# The GENERATE_TESTLIST tag can be used to enable (YES) or -# disable (NO) the test list. This list is created by putting \test -# commands in the documentation. +# The GENERATE_TESTLIST tag can be used to enable (YES) or disable (NO) the test +# list. This list is created by putting \test commands in the documentation. +# The default value is: YES. GENERATE_TESTLIST = YES -# The GENERATE_BUGLIST tag can be used to enable (YES) or -# disable (NO) the bug list. This list is created by putting \bug -# commands in the documentation. +# The GENERATE_BUGLIST tag can be used to enable (YES) or disable (NO) the bug +# list. This list is created by putting \bug commands in the documentation. +# The default value is: YES. GENERATE_BUGLIST = YES -# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or -# disable (NO) the deprecated list. This list is created by putting -# \deprecated commands in the documentation. +# The GENERATE_DEPRECATEDLIST tag can be used to enable (YES) or disable (NO) +# the deprecated list. This list is created by putting \deprecated commands in +# the documentation. +# The default value is: YES. GENERATE_DEPRECATEDLIST= YES -# The ENABLED_SECTIONS tag can be used to enable conditional -# documentation sections, marked by \if sectionname ... \endif. +# The ENABLED_SECTIONS tag can be used to enable conditional documentation +# sections, marked by \if ... \endif and \cond +# ... \endcond blocks. -ENABLED_SECTIONS = +ENABLED_SECTIONS = -# The MAX_INITIALIZER_LINES tag determines the maximum number of lines -# the initial value of a variable or macro consists of for it to appear in -# the documentation. If the initializer consists of more lines than specified -# here it will be hidden. Use a value of 0 to hide initializers completely. -# The appearance of the initializer of individual variables and macros in the -# documentation can be controlled using \showinitializer or \hideinitializer -# command in the documentation regardless of this setting. +# The MAX_INITIALIZER_LINES tag determines the maximum number of lines that the +# initial value of a variable or macro / define can have for it to appear in the +# documentation. If the initializer consists of more lines than specified here +# it will be hidden. Use a value of 0 to hide initializers completely. The +# appearance of the value of individual variables and macros / defines can be +# controlled using \showinitializer or \hideinitializer command in the +# documentation regardless of this setting. +# Minimum value: 0, maximum value: 10000, default value: 30. MAX_INITIALIZER_LINES = 30 -# Set the SHOW_USED_FILES tag to NO to disable the list of files generated -# at the bottom of the documentation of classes and structs. If set to YES the +# Set the SHOW_USED_FILES tag to NO to disable the list of files generated at +# the bottom of the documentation of classes and structs. If set to YES, the # list will mention the files that were used to generate the documentation. +# The default value is: YES. SHOW_USED_FILES = YES -# Set the SHOW_FILES tag to NO to disable the generation of the Files page. -# This will remove the Files entry from the Quick Index and from the -# Folder Tree View (if specified). The default is YES. +# Set the SHOW_FILES tag to NO to disable the generation of the Files page. This +# will remove the Files entry from the Quick Index and from the Folder Tree View +# (if specified). +# The default value is: YES. SHOW_FILES = YES -# Set the SHOW_NAMESPACES tag to NO to disable the generation of the -# Namespaces page. This will remove the Namespaces entry from the Quick Index -# and from the Folder Tree View (if specified). The default is YES. +# Set the SHOW_NAMESPACES tag to NO to disable the generation of the Namespaces +# page. This will remove the Namespaces entry from the Quick Index and from the +# Folder Tree View (if specified). +# The default value is: YES. SHOW_NAMESPACES = YES -# The FILE_VERSION_FILTER tag can be used to specify a program or script that -# doxygen should invoke to get the current version for each file (typically from -# the version control system). Doxygen will invoke the program by executing (via -# popen()) the command , where is the value of -# the FILE_VERSION_FILTER tag, and is the name of an input file -# provided by doxygen. Whatever the program writes to standard output -# is used as the file version. See the manual for examples. - -FILE_VERSION_FILTER = - -# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed -# by doxygen. The layout file controls the global structure of the generated -# output files in an output format independent way. To create the layout file -# that represents doxygen's defaults, run doxygen with the -l option. -# You can optionally specify a file name after the option, if omitted -# DoxygenLayout.xml will be used as the name of the layout file. +# The FILE_VERSION_FILTER tag can be used to specify a program or script that +# doxygen should invoke to get the current version for each file (typically from +# the version control system). Doxygen will invoke the program by executing (via +# popen()) the command command input-file, where command is the value of the +# FILE_VERSION_FILTER tag, and input-file is the name of an input file provided +# by doxygen. Whatever the program writes to standard output is used as the file +# version. For an example see the documentation. + +FILE_VERSION_FILTER = + +# The LAYOUT_FILE tag can be used to specify a layout file which will be parsed +# by doxygen. The layout file controls the global structure of the generated +# output files in an output format independent way. To create the layout file +# that represents doxygen's defaults, run doxygen with the -l option. You can +# optionally specify a file name after the option, if omitted DoxygenLayout.xml +# will be used as the name of the layout file. +# +# Note that if you run doxygen from a directory containing a file called +# DoxygenLayout.xml, doxygen will parse it automatically even if the LAYOUT_FILE +# tag is left empty. -LAYOUT_FILE = +LAYOUT_FILE = -# The CITE_BIB_FILES tag can be used to specify one or more bib files -# containing the references data. This must be a list of .bib files. The -# .bib extension is automatically appended if omitted. Using this command -# requires the bibtex tool to be installed. See also -# http://en.wikipedia.org/wiki/BibTeX for more info. For LaTeX the style -# of the bibliography can be controlled using LATEX_BIB_STYLE. To use this -# feature you need bibtex and perl available in the search path. +# The CITE_BIB_FILES tag can be used to specify one or more bib files containing +# the reference definitions. This must be a list of .bib files. The .bib +# extension is automatically appended if omitted. This requires the bibtex tool +# to be installed. See also https://en.wikipedia.org/wiki/BibTeX for more info. +# For LaTeX the style of the bibliography can be controlled using +# LATEX_BIB_STYLE. To use this feature you need bibtex and perl available in the +# search path. See also \cite for info how to create references. -CITE_BIB_FILES = +CITE_BIB_FILES = #--------------------------------------------------------------------------- -# configuration options related to warning and progress messages +# Configuration options related to warning and progress messages #--------------------------------------------------------------------------- -# The QUIET tag can be used to turn on/off the messages that are generated -# by doxygen. Possible values are YES and NO. If left blank NO is used. +# The QUIET tag can be used to turn on/off the messages that are generated to +# standard output by doxygen. If QUIET is set to YES this implies that the +# messages are off. +# The default value is: NO. QUIET = NO -# The WARNINGS tag can be used to turn on/off the warning messages that are -# generated by doxygen. Possible values are YES and NO. If left blank -# NO is used. +# The WARNINGS tag can be used to turn on/off the warning messages that are +# generated to standard error (stderr) by doxygen. If WARNINGS is set to YES +# this implies that the warnings are on. +# +# Tip: Turn warnings on while writing the documentation. +# The default value is: YES. WARNINGS = YES -# If WARN_IF_UNDOCUMENTED is set to YES, then doxygen will generate warnings -# for undocumented members. If EXTRACT_ALL is set to YES then this flag will -# automatically be disabled. +# If the WARN_IF_UNDOCUMENTED tag is set to YES then doxygen will generate +# warnings for undocumented members. If EXTRACT_ALL is set to YES then this flag +# will automatically be disabled. +# The default value is: YES. WARN_IF_UNDOCUMENTED = YES -# If WARN_IF_DOC_ERROR is set to YES, doxygen will generate warnings for -# potential errors in the documentation, such as not documenting some -# parameters in a documented function, or documenting parameters that -# don't exist or using markup commands wrongly. +# If the WARN_IF_DOC_ERROR tag is set to YES, doxygen will generate warnings for +# potential errors in the documentation, such as not documenting some parameters +# in a documented function, or documenting parameters that don't exist or using +# markup commands wrongly. +# The default value is: YES. WARN_IF_DOC_ERROR = YES -# The WARN_NO_PARAMDOC option can be enabled to get warnings for -# functions that are documented, but have no documentation for their parameters -# or return value. If set to NO (the default) doxygen will only warn about -# wrong or incomplete parameter documentation, but not about the absence of -# documentation. +# This WARN_NO_PARAMDOC option can be enabled to get warnings for functions that +# are documented, but have no documentation for their parameters or return +# value. If set to NO, doxygen will only warn about wrong or incomplete +# parameter documentation, but not about the absence of documentation. If +# EXTRACT_ALL is set to YES then this flag will automatically be disabled. +# The default value is: NO. +# TODO: enable to complete documentation WARN_NO_PARAMDOC = NO -# The WARN_FORMAT tag determines the format of the warning messages that -# doxygen can produce. The string should contain the $file, $line, and $text -# tags, which will be replaced by the file and line number from which the -# warning originated and the warning text. Optionally the format may contain -# $version, which will be replaced by the version of the file (if it could -# be obtained via FILE_VERSION_FILTER) +# If the WARN_AS_ERROR tag is set to YES then doxygen will immediately stop when +# a warning is encountered. +# The default value is: NO. + +WARN_AS_ERROR = NO + +# The WARN_FORMAT tag determines the format of the warning messages that doxygen +# can produce. The string should contain the $file, $line, and $text tags, which +# will be replaced by the file and line number from which the warning originated +# and the warning text. Optionally the format may contain $version, which will +# be replaced by the version of the file (if it could be obtained via +# FILE_VERSION_FILTER) +# The default value is: $file:$line: $text. WARN_FORMAT = "$file:$line: $text" -# The WARN_LOGFILE tag can be used to specify a file to which warning -# and error messages should be written. If left blank the output is written -# to stderr. +# The WARN_LOGFILE tag can be used to specify a file to which warning and error +# messages should be written. If left blank the output is written to standard +# error (stderr). -WARN_LOGFILE = +WARN_LOGFILE = #--------------------------------------------------------------------------- -# configuration options related to the input files +# Configuration options related to the input files #--------------------------------------------------------------------------- -# The INPUT tag can be used to specify the files and/or directories that contain -# documented source files. You may enter file names like "myfile.cpp" or -# directories like "/usr/src/myproject". Separate the files or directories -# with spaces. +# The INPUT tag is used to specify the files and/or directories that contain +# documented source files. You may enter file names like myfile.cpp or +# directories like /usr/src/myproject. Separate the files or directories with +# spaces. See also FILE_PATTERNS and EXTENSION_MAPPING +# Note: If this tag is empty the current directory is searched. INPUT = "@CMAKE_DOXYGEN_INPUT_LIST@" -# This tag can be used to specify the character encoding of the source files -# that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is -# also the default input encoding. Doxygen uses libiconv (or the iconv built -# into libc) for the transcoding. See http://www.gnu.org/software/libiconv for -# the list of possible encodings. +# This tag can be used to specify the character encoding of the source files +# that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses +# libiconv (or the iconv built into libc) for the transcoding. See the libiconv +# documentation (see: https://www.gnu.org/software/libiconv/) for the list of +# possible encodings. +# The default value is: UTF-8. INPUT_ENCODING = UTF-8 -# If the value of the INPUT tag contains directories, you can use the -# FILE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp -# and *.h) to filter out the source-files in the directories. If left -# blank the following patterns are tested: -# *.c *.cc *.cxx *.cpp *.c++ *.d *.java *.ii *.ixx *.ipp *.i++ *.inl *.h *.hh -# *.hxx *.hpp *.h++ *.idl *.odl *.cs *.php *.php3 *.inc *.m *.mm *.dox *.py -# *.f90 *.f *.for *.vhd *.vhdl +# If the value of the INPUT tag contains directories, you can use the +# FILE_PATTERNS tag to specify one or more wildcard patterns (like *.cpp and +# *.h) to filter out the source-files in the directories. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# read by doxygen. +# +# If left blank the following patterns are tested:*.c, *.cc, *.cxx, *.cpp, +# *.c++, *.java, *.ii, *.ixx, *.ipp, *.i++, *.inl, *.idl, *.ddl, *.odl, *.h, +# *.hh, *.hxx, *.hpp, *.h++, *.cs, *.d, *.php, *.php4, *.php5, *.phtml, *.inc, +# *.m, *.markdown, *.md, *.mm, *.dox, *.py, *.pyw, *.f90, *.f95, *.f03, *.f08, +# *.f, *.for, *.tcl, *.vhd, *.vhdl, *.ucf, *.qsf and *.ice. FILE_PATTERNS = *.c \ *.cc \ *.cxx \ *.cpp \ *.c++ \ - *.d \ *.java \ *.ii \ *.ixx \ *.ipp \ *.i++ \ *.inl \ + *.idl \ + *.ddl \ + *.odl \ *.h \ *.hh \ *.hxx \ *.hpp \ *.h++ \ - *.idl \ - *.odl \ *.cs \ + *.d \ *.php \ - *.php3 \ + *.php4 \ + *.php5 \ + *.phtml \ *.inc \ *.m \ *.markdown \ @@ -712,892 +873,1349 @@ FILE_PATTERNS = *.c \ *.mm \ *.dox \ *.py \ + *.pyw \ *.f90 \ + *.f95 \ + *.f03 \ + *.f08 \ *.f \ *.for \ + *.tcl \ *.vhd \ - *.vhdl + *.vhdl \ + *.ucf \ + *.qsf \ + *.ice -# The RECURSIVE tag can be used to turn specify whether or not subdirectories -# should be searched for input files as well. Possible values are YES and NO. -# If left blank NO is used. +# The RECURSIVE tag can be used to specify whether or not subdirectories should +# be searched for input files as well. +# The default value is: NO. RECURSIVE = YES -# The EXCLUDE tag can be used to specify files and/or directories that should be -# excluded from the INPUT source files. This way you can easily exclude a -# subdirectory from a directory tree whose root is specified with the INPUT tag. -# Note that relative paths are relative to the directory from which doxygen is +# The EXCLUDE tag can be used to specify files and/or directories that should be +# excluded from the INPUT source files. This way you can easily exclude a +# subdirectory from a directory tree whose root is specified with the INPUT tag. +# +# Note that relative paths are relative to the directory from which doxygen is # run. -EXCLUDE = +EXCLUDE = -# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or -# directories that are symbolic links (a Unix file system feature) are excluded +# The EXCLUDE_SYMLINKS tag can be used to select whether or not files or +# directories that are symbolic links (a Unix file system feature) are excluded # from the input. +# The default value is: NO. EXCLUDE_SYMLINKS = NO -# If the value of the INPUT tag contains directories, you can use the -# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude -# certain files from those directories. Note that the wildcards are matched -# against the file with absolute path, so to exclude all test directories -# for example use the pattern */test/* +# If the value of the INPUT tag contains directories, you can use the +# EXCLUDE_PATTERNS tag to specify one or more wildcard patterns to exclude +# certain files from those directories. +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories for example use the pattern */test/* -EXCLUDE_PATTERNS = +EXCLUDE_PATTERNS = -# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names -# (namespaces, classes, functions, etc.) that should be excluded from the -# output. The symbol name can be a fully qualified name, a word, or if the -# wildcard * is used, a substring. Examples: ANamespace, AClass, +# The EXCLUDE_SYMBOLS tag can be used to specify one or more symbol names +# (namespaces, classes, functions, etc.) that should be excluded from the +# output. The symbol name can be a fully qualified name, a word, or if the +# wildcard * is used, a substring. Examples: ANamespace, AClass, # AClass::ANamespace, ANamespace::*Test +# +# Note that the wildcards are matched against the file with absolute path, so to +# exclude all test directories use the pattern */test/* -EXCLUDE_SYMBOLS = +EXCLUDE_SYMBOLS = -# The EXAMPLE_PATH tag can be used to specify one or more files or -# directories that contain example code fragments that are included (see -# the \include command). +# The EXAMPLE_PATH tag can be used to specify one or more files or directories +# that contain example code fragments that are included (see the \include +# command). -EXAMPLE_PATH = +EXAMPLE_PATH = -# If the value of the EXAMPLE_PATH tag contains directories, you can use the -# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp -# and *.h) to filter out the source-files in the directories. If left -# blank all files are included. +# If the value of the EXAMPLE_PATH tag contains directories, you can use the +# EXAMPLE_PATTERNS tag to specify one or more wildcard pattern (like *.cpp and +# *.h) to filter out the source-files in the directories. If left blank all +# files are included. EXAMPLE_PATTERNS = * -# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be -# searched for input files to be used with the \include or \dontinclude -# commands irrespective of the value of the RECURSIVE tag. -# Possible values are YES and NO. If left blank NO is used. +# If the EXAMPLE_RECURSIVE tag is set to YES then subdirectories will be +# searched for input files to be used with the \include or \dontinclude commands +# irrespective of the value of the RECURSIVE tag. +# The default value is: NO. EXAMPLE_RECURSIVE = NO -# The IMAGE_PATH tag can be used to specify one or more files or -# directories that contain image that are included in the documentation (see -# the \image command). +# The IMAGE_PATH tag can be used to specify one or more files or directories +# that contain images that are to be included in the documentation (see the +# \image command). -IMAGE_PATH = +IMAGE_PATH = -# The INPUT_FILTER tag can be used to specify a program that doxygen should -# invoke to filter for each input file. Doxygen will invoke the filter program -# by executing (via popen()) the command , where -# is the value of the INPUT_FILTER tag, and is the name of an -# input file. Doxygen will then use the output that the filter program writes -# to standard output. If FILTER_PATTERNS is specified, this tag will be -# ignored. +# The INPUT_FILTER tag can be used to specify a program that doxygen should +# invoke to filter for each input file. Doxygen will invoke the filter program +# by executing (via popen()) the command: +# +# +# +# where is the value of the INPUT_FILTER tag, and is the +# name of an input file. Doxygen will then use the output that the filter +# program writes to standard output. If FILTER_PATTERNS is specified, this tag +# will be ignored. +# +# Note that the filter must not add or remove lines; it is applied before the +# code is scanned, but not when the output code is generated. If lines are added +# or removed, the anchors will not be placed correctly. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# properly processed by doxygen. + +INPUT_FILTER = + +# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern +# basis. Doxygen will compare the file name with each pattern and apply the +# filter if there is a match. The filters are a list of the form: pattern=filter +# (like *.cpp=my_cpp_filter). See INPUT_FILTER for further information on how +# filters are used. If the FILTER_PATTERNS tag is empty or if none of the +# patterns match the file name, INPUT_FILTER is applied. +# +# Note that for custom extensions or not directly supported extensions you also +# need to set EXTENSION_MAPPING for the extension otherwise the files are not +# properly processed by doxygen. -INPUT_FILTER = +FILTER_PATTERNS = -# The FILTER_PATTERNS tag can be used to specify filters on a per file pattern -# basis. Doxygen will compare the file name with each pattern and apply the -# filter if there is a match. The filters are a list of the form: -# pattern=filter (like *.cpp=my_cpp_filter). See INPUT_FILTER for further -# info on how filters are used. If FILTER_PATTERNS is empty or if -# non of the patterns match the file name, INPUT_FILTER is applied. +# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using +# INPUT_FILTER) will also be used to filter the input files that are used for +# producing the source files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The default value is: NO. -FILTER_PATTERNS = +FILTER_SOURCE_FILES = NO -# If the FILTER_SOURCE_FILES tag is set to YES, the input filter (if set using -# INPUT_FILTER) will be used to filter the input files when producing source -# files to browse (i.e. when SOURCE_BROWSER is set to YES). +# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file +# pattern. A pattern will override the setting for FILTER_PATTERN (if any) and +# it is also possible to disable source filtering for a specific pattern using +# *.ext= (so without naming a filter). +# This tag requires that the tag FILTER_SOURCE_FILES is set to YES. -FILTER_SOURCE_FILES = NO +FILTER_SOURCE_PATTERNS = -# The FILTER_SOURCE_PATTERNS tag can be used to specify source filters per file -# pattern. A pattern will override the setting for FILTER_PATTERN (if any) -# and it is also possible to disable source filtering for a specific pattern -# using *.ext= (so without naming a filter). This option only has effect when -# FILTER_SOURCE_FILES is enabled. +# If the USE_MDFILE_AS_MAINPAGE tag refers to the name of a markdown file that +# is part of the input, its contents will be placed on the main page +# (index.html). This can be useful if you have a project on for instance GitHub +# and want to reuse the introduction page also for the doxygen output. -FILTER_SOURCE_PATTERNS = +USE_MDFILE_AS_MAINPAGE = #--------------------------------------------------------------------------- -# configuration options related to source browsing +# Configuration options related to source browsing #--------------------------------------------------------------------------- -# If the SOURCE_BROWSER tag is set to YES then a list of source files will -# be generated. Documented entities will be cross-referenced with these sources. -# Note: To get rid of all source code in the generated output, make sure also -# VERBATIM_HEADERS is set to NO. +# If the SOURCE_BROWSER tag is set to YES then a list of source files will be +# generated. Documented entities will be cross-referenced with these sources. +# +# Note: To get rid of all source code in the generated output, make sure that +# also VERBATIM_HEADERS is set to NO. +# The default value is: NO. SOURCE_BROWSER = YES -# Setting the INLINE_SOURCES tag to YES will include the body -# of functions and classes directly in the documentation. +# Setting the INLINE_SOURCES tag to YES will include the body of functions, +# classes and enums directly into the documentation. +# The default value is: NO. INLINE_SOURCES = NO -# Setting the STRIP_CODE_COMMENTS tag to YES (the default) will instruct -# doxygen to hide any special comment blocks from generated source code -# fragments. Normal C, C++ and Fortran comments will always remain visible. +# Setting the STRIP_CODE_COMMENTS tag to YES will instruct doxygen to hide any +# special comment blocks from generated source code fragments. Normal C, C++ and +# Fortran comments will always remain visible. +# The default value is: YES. STRIP_CODE_COMMENTS = YES -# If the REFERENCED_BY_RELATION tag is set to YES -# then for each documented function all documented -# functions referencing it will be listed. +# If the REFERENCED_BY_RELATION tag is set to YES then for each documented +# entity all documented functions referencing it will be listed. +# The default value is: NO. REFERENCED_BY_RELATION = NO -# If the REFERENCES_RELATION tag is set to YES -# then for each documented function all documented entities -# called/used by that function will be listed. +# If the REFERENCES_RELATION tag is set to YES then for each documented function +# all documented entities called/used by that function will be listed. +# The default value is: NO. REFERENCES_RELATION = NO -# If the REFERENCES_LINK_SOURCE tag is set to YES (the default) -# and SOURCE_BROWSER tag is set to YES, then the hyperlinks from -# functions in REFERENCES_RELATION and REFERENCED_BY_RELATION lists will -# link to the source code. Otherwise they will link to the documentation. +# If the REFERENCES_LINK_SOURCE tag is set to YES and SOURCE_BROWSER tag is set +# to YES then the hyperlinks from functions in REFERENCES_RELATION and +# REFERENCED_BY_RELATION lists will link to the source code. Otherwise they will +# link to the documentation. +# The default value is: YES. REFERENCES_LINK_SOURCE = YES -# If the USE_HTAGS tag is set to YES then the references to source code -# will point to the HTML generated by the htags(1) tool instead of doxygen -# built-in source browser. The htags tool is part of GNU's global source -# tagging system (see http://www.gnu.org/software/global/global.html). You -# will need version 4.8.6 or higher. +# If SOURCE_TOOLTIPS is enabled (the default) then hovering a hyperlink in the +# source code will show a tooltip with additional information such as prototype, +# brief description and links to the definition and documentation. Since this +# will make the HTML file larger and loading of large files a bit slower, you +# can opt to disable this feature. +# The default value is: YES. +# This tag requires that the tag SOURCE_BROWSER is set to YES. + +SOURCE_TOOLTIPS = YES + +# If the USE_HTAGS tag is set to YES then the references to source code will +# point to the HTML generated by the htags(1) tool instead of doxygen built-in +# source browser. The htags tool is part of GNU's global source tagging system +# (see https://www.gnu.org/software/global/global.html). You will need version +# 4.8.6 or higher. +# +# To use it do the following: +# - Install the latest version of global +# - Enable SOURCE_BROWSER and USE_HTAGS in the configuration file +# - Make sure the INPUT points to the root of the source tree +# - Run doxygen as normal +# +# Doxygen will invoke htags (and that will in turn invoke gtags), so these +# tools must be available from the command line (i.e. in the search path). +# +# The result: instead of the source browser generated by doxygen, the links to +# source code will now point to the output of htags. +# The default value is: NO. +# This tag requires that the tag SOURCE_BROWSER is set to YES. USE_HTAGS = NO -# If the VERBATIM_HEADERS tag is set to YES (the default) then Doxygen -# will generate a verbatim copy of the header file for each class for -# which an include is specified. Set to NO to disable this. +# If the VERBATIM_HEADERS tag is set the YES then doxygen will generate a +# verbatim copy of the header file for each class for which an include is +# specified. Set to NO to disable this. +# See also: Section \class. +# The default value is: YES. VERBATIM_HEADERS = YES #--------------------------------------------------------------------------- -# configuration options related to the alphabetical class index +# Configuration options related to the alphabetical class index #--------------------------------------------------------------------------- -# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index -# of all compounds will be generated. Enable this if the project -# contains a lot of classes, structs, unions or interfaces. +# If the ALPHABETICAL_INDEX tag is set to YES, an alphabetical index of all +# compounds will be generated. Enable this if the project contains a lot of +# classes, structs, unions or interfaces. +# The default value is: YES. ALPHABETICAL_INDEX = YES -# If the alphabetical index is enabled (see ALPHABETICAL_INDEX) then -# the COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns -# in which this list will be split (can be a number in the range [1..20]) +# The COLS_IN_ALPHA_INDEX tag can be used to specify the number of columns in +# which the alphabetical index list will be split. +# Minimum value: 1, maximum value: 20, default value: 5. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. COLS_IN_ALPHA_INDEX = 5 -# In case all classes in a project start with a common prefix, all -# classes will be put under the same header in the alphabetical index. -# The IGNORE_PREFIX tag can be used to specify one or more prefixes that -# should be ignored while generating the index headers. +# In case all classes in a project start with a common prefix, all classes will +# be put under the same header in the alphabetical index. The IGNORE_PREFIX tag +# can be used to specify a prefix (or a list of prefixes) that should be ignored +# while generating the index headers. +# This tag requires that the tag ALPHABETICAL_INDEX is set to YES. -IGNORE_PREFIX = +IGNORE_PREFIX = #--------------------------------------------------------------------------- -# configuration options related to the HTML output +# Configuration options related to the HTML output #--------------------------------------------------------------------------- -# If the GENERATE_HTML tag is set to YES (the default) Doxygen will -# generate HTML output. +# If the GENERATE_HTML tag is set to YES, doxygen will generate HTML output +# The default value is: YES. GENERATE_HTML = YES -# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. -# If a relative path is entered the value of OUTPUT_DIRECTORY will be -# put in front of it. If left blank `html' will be used as the default path. +# The HTML_OUTPUT tag is used to specify where the HTML docs will be put. If a +# relative path is entered the value of OUTPUT_DIRECTORY will be put in front of +# it. +# The default directory is: html. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_OUTPUT = html -# The HTML_FILE_EXTENSION tag can be used to specify the file extension for -# each generated HTML page (for example: .htm,.php,.asp). If it is left blank -# doxygen will generate files with .html extension. +# The HTML_FILE_EXTENSION tag can be used to specify the file extension for each +# generated HTML page (for example: .htm, .php, .asp). +# The default value is: .html. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_FILE_EXTENSION = .html -# The HTML_HEADER tag can be used to specify a personal HTML header for -# each generated HTML page. If it is left blank doxygen will generate a -# standard header. Note that when using a custom header you are responsible -# for the proper inclusion of any scripts and style sheets that doxygen -# needs, which is dependent on the configuration options used. -# It is advised to generate a default header using "doxygen -w html -# header.html footer.html stylesheet.css YourConfigFile" and then modify -# that header. Note that the header is subject to change so you typically -# have to redo this when upgrading to a newer version of doxygen or when -# changing the value of configuration settings such as GENERATE_TREEVIEW! - -HTML_HEADER = - -# The HTML_FOOTER tag can be used to specify a personal HTML footer for -# each generated HTML page. If it is left blank doxygen will generate a -# standard footer. - -HTML_FOOTER = - -# The HTML_STYLESHEET tag can be used to specify a user-defined cascading -# style sheet that is used by each HTML page. It can be used to -# fine-tune the look of the HTML output. If the tag is left blank doxygen -# will generate a default style sheet. Note that doxygen will try to copy -# the style sheet file to the HTML output directory, so don't put your own -# style sheet in the HTML output directory as well, or it will be erased! - -HTML_STYLESHEET = - -# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or -# other source files which should be copied to the HTML output directory. Note -# that these files will be copied to the base HTML output directory. Use the -# $relpath$ marker in the HTML_HEADER and/or HTML_FOOTER files to load these -# files. In the HTML_STYLESHEET file, use the file name only. Also note that -# the files will be copied as-is; there are no commands or markers available. - -HTML_EXTRA_FILES = - -# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. -# Doxygen will adjust the colors in the style sheet and background images -# according to this color. Hue is specified as an angle on a colorwheel, -# see http://en.wikipedia.org/wiki/Hue for more information. -# For instance the value 0 represents red, 60 is yellow, 120 is green, -# 180 is cyan, 240 is blue, 300 purple, and 360 is red again. -# The allowed range is 0 to 359. - -HTML_COLORSTYLE_HUE = 220 - -# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of -# the colors in the HTML output. For a value of 0 the output will use -# grayscales only. A value of 255 will produce the most vivid colors. +# The HTML_HEADER tag can be used to specify a user-defined HTML header file for +# each generated HTML page. If the tag is left blank doxygen will generate a +# standard header. +# +# To get valid HTML the header file that includes any scripts and style sheets +# that doxygen needs, which is dependent on the configuration options used (e.g. +# the setting GENERATE_TREEVIEW). It is highly recommended to start with a +# default header using +# doxygen -w html new_header.html new_footer.html new_stylesheet.css +# YourConfigFile +# and then modify the file new_header.html. See also section "Doxygen usage" +# for information on how to generate the default header that doxygen normally +# uses. +# Note: The header is subject to change so you typically have to regenerate the +# default header when upgrading to a newer version of doxygen. For a description +# of the possible markers and block names see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_HEADER = + +# The HTML_FOOTER tag can be used to specify a user-defined HTML footer for each +# generated HTML page. If the tag is left blank doxygen will generate a standard +# footer. See HTML_HEADER for more information on how to generate a default +# footer and what special commands can be used inside the footer. See also +# section "Doxygen usage" for information on how to generate the default footer +# that doxygen normally uses. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_FOOTER = + +# The HTML_STYLESHEET tag can be used to specify a user-defined cascading style +# sheet that is used by each HTML page. It can be used to fine-tune the look of +# the HTML output. If left blank doxygen will generate a default style sheet. +# See also section "Doxygen usage" for information on how to generate the style +# sheet that doxygen normally uses. +# Note: It is recommended to use HTML_EXTRA_STYLESHEET instead of this tag, as +# it is more robust and this tag (HTML_STYLESHEET) will in the future become +# obsolete. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_STYLESHEET = + +# The HTML_EXTRA_STYLESHEET tag can be used to specify additional user-defined +# cascading style sheets that are included after the standard style sheets +# created by doxygen. Using this option one can overrule certain style aspects. +# This is preferred over using HTML_STYLESHEET since it does not replace the +# standard style sheet and is therefore more robust against future updates. +# Doxygen will copy the style sheet files to the output directory. +# Note: The order of the extra style sheet files is of importance (e.g. the last +# style sheet in the list overrules the setting of the previous ones in the +# list). For an example see the documentation. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_STYLESHEET = + +# The HTML_EXTRA_FILES tag can be used to specify one or more extra images or +# other source files which should be copied to the HTML output directory. Note +# that these files will be copied to the base HTML output directory. Use the +# $relpath^ marker in the HTML_HEADER and/or HTML_FOOTER files to load these +# files. In the HTML_STYLESHEET file, use the file name only. Also note that the +# files will be copied as-is; there are no commands or markers available. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_EXTRA_FILES = + +# The HTML_COLORSTYLE_HUE tag controls the color of the HTML output. Doxygen +# will adjust the colors in the style sheet and background images according to +# this color. Hue is specified as an angle on a colorwheel, see +# https://en.wikipedia.org/wiki/Hue for more information. For instance the value +# 0 represents red, 60 is yellow, 120 is green, 180 is cyan, 240 is blue, 300 +# purple, and 360 is red again. +# Minimum value: 0, maximum value: 359, default value: 220. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_HUE = 210 + +# The HTML_COLORSTYLE_SAT tag controls the purity (or saturation) of the colors +# in the HTML output. For a value of 0 the output will use grayscales only. A +# value of 255 will produce the most vivid colors. +# Minimum value: 0, maximum value: 255, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_COLORSTYLE_SAT = 100 -# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to -# the luminance component of the colors in the HTML output. Values below -# 100 gradually make the output lighter, whereas values above 100 make -# the output darker. The value divided by 100 is the actual gamma applied, -# so 80 represents a gamma of 0.8, The value 220 represents a gamma of 2.2, -# and 100 does not change the gamma. - -HTML_COLORSTYLE_GAMMA = 80 - -# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML -# page will contain the date and time when the page was generated. Setting -# this to NO can help when comparing the output of multiple runs. - -HTML_TIMESTAMP = YES - -# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML -# documentation will contain sections that can be hidden and shown after the +# The HTML_COLORSTYLE_GAMMA tag controls the gamma correction applied to the +# luminance component of the colors in the HTML output. Values below 100 +# gradually make the output lighter, whereas values above 100 make the output +# darker. The value divided by 100 is the actual gamma applied, so 80 represents +# a gamma of 0.8, The value 220 represents a gamma of 2.2, and 100 does not +# change the gamma. +# Minimum value: 40, maximum value: 240, default value: 80. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_COLORSTYLE_GAMMA = 100 + +# If the HTML_TIMESTAMP tag is set to YES then the footer of each generated HTML +# page will contain the date and time when the page was generated. Setting this +# to YES can help to show when doxygen was last run and thus if the +# documentation is up to date. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_TIMESTAMP = NO + +# If the HTML_DYNAMIC_MENUS tag is set to YES then the generated HTML +# documentation will contain a main index with vertical navigation menus that +# are dynamically created via Javascript. If disabled, the navigation index will +# consists of multiple levels of tabs that are statically embedded in every HTML +# page. Disable this option to support browsers that do not have Javascript, +# like the Qt help browser. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. + +HTML_DYNAMIC_MENUS = YES + +# If the HTML_DYNAMIC_SECTIONS tag is set to YES then the generated HTML +# documentation will contain sections that can be hidden and shown after the # page has loaded. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_DYNAMIC_SECTIONS = NO -# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of -# entries shown in the various tree structured indices initially; the user -# can expand and collapse entries dynamically later on. Doxygen will expand -# the tree to such a level that at most the specified number of entries are -# visible (unless a fully collapsed tree already exceeds this amount). -# So setting the number of entries 1 will produce a full collapsed tree by -# default. 0 is a special value representing an infinite number of entries -# and will result in a full expanded tree by default. +# With HTML_INDEX_NUM_ENTRIES one can control the preferred number of entries +# shown in the various tree structured indices initially; the user can expand +# and collapse entries dynamically later on. Doxygen will expand the tree to +# such a level that at most the specified number of entries are visible (unless +# a fully collapsed tree already exceeds this amount). So setting the number of +# entries 1 will produce a full collapsed tree by default. 0 is a special value +# representing an infinite number of entries and will result in a full expanded +# tree by default. +# Minimum value: 0, maximum value: 9999, default value: 100. +# This tag requires that the tag GENERATE_HTML is set to YES. HTML_INDEX_NUM_ENTRIES = 100 -# If the GENERATE_DOCSET tag is set to YES, additional index files -# will be generated that can be used as input for Apple's Xcode 3 -# integrated development environment, introduced with OSX 10.5 (Leopard). -# To create a documentation set, doxygen will generate a Makefile in the -# HTML output directory. Running make will produce the docset in that -# directory and running "make install" will install the docset in -# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find -# it at startup. -# See http://developer.apple.com/tools/creatingdocsetswithdoxygen.html -# for more information. +# If the GENERATE_DOCSET tag is set to YES, additional index files will be +# generated that can be used as input for Apple's Xcode 3 integrated development +# environment (see: https://developer.apple.com/xcode/), introduced with OSX +# 10.5 (Leopard). To create a documentation set, doxygen will generate a +# Makefile in the HTML output directory. Running make will produce the docset in +# that directory and running make install will install the docset in +# ~/Library/Developer/Shared/Documentation/DocSets so that Xcode will find it at +# startup. See https://developer.apple.com/library/archive/featuredarticles/Doxy +# genXcode/_index.html for more information. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. GENERATE_DOCSET = NO -# When GENERATE_DOCSET tag is set to YES, this tag determines the name of the -# feed. A documentation feed provides an umbrella under which multiple -# documentation sets from a single provider (such as a company or product suite) -# can be grouped. +# This tag determines the name of the docset feed. A documentation feed provides +# an umbrella under which multiple documentation sets from a single provider +# (such as a company or product suite) can be grouped. +# The default value is: Doxygen generated docs. +# This tag requires that the tag GENERATE_DOCSET is set to YES. DOCSET_FEEDNAME = "Doxygen generated docs" -# When GENERATE_DOCSET tag is set to YES, this tag specifies a string that -# should uniquely identify the documentation set bundle. This should be a -# reverse domain-name style string, e.g. com.mycompany.MyDocSet. Doxygen -# will append .docset to the name. +# This tag specifies a string that should uniquely identify the documentation +# set bundle. This should be a reverse domain-name style string, e.g. +# com.mycompany.MyDocSet. Doxygen will append .docset to the name. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_DOCSET is set to YES. DOCSET_BUNDLE_ID = org.doxygen.Project -# When GENERATE_PUBLISHER_ID tag specifies a string that should uniquely identify -# the documentation publisher. This should be a reverse domain-name style +# The DOCSET_PUBLISHER_ID tag specifies a string that should uniquely identify +# the documentation publisher. This should be a reverse domain-name style # string, e.g. com.mycompany.MyDocSet.documentation. +# The default value is: org.doxygen.Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. DOCSET_PUBLISHER_ID = org.doxygen.Publisher -# The GENERATE_PUBLISHER_NAME tag identifies the documentation publisher. +# The DOCSET_PUBLISHER_NAME tag identifies the documentation publisher. +# The default value is: Publisher. +# This tag requires that the tag GENERATE_DOCSET is set to YES. DOCSET_PUBLISHER_NAME = Publisher -# If the GENERATE_HTMLHELP tag is set to YES, additional index files -# will be generated that can be used as input for tools like the -# Microsoft HTML help workshop to generate a compiled HTML help file (.chm) -# of the generated HTML documentation. +# If the GENERATE_HTMLHELP tag is set to YES then doxygen generates three +# additional HTML index files: index.hhp, index.hhc, and index.hhk. The +# index.hhp is a project file that can be read by Microsoft's HTML Help Workshop +# (see: https://www.microsoft.com/en-us/download/details.aspx?id=21138) on +# Windows. +# +# The HTML Help Workshop contains a compiler that can convert all HTML output +# generated by doxygen into a single compiled HTML file (.chm). Compiled HTML +# files are now used as the Windows 98 help format, and will replace the old +# Windows help format (.hlp) on all Windows platforms in the future. Compressed +# HTML files also contain an index, a table of contents, and you can search for +# words in the documentation. The HTML workshop also contains a viewer for +# compressed HTML files. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. GENERATE_HTMLHELP = NO -# If the GENERATE_HTMLHELP tag is set to YES, the CHM_FILE tag can -# be used to specify the file name of the resulting .chm file. You -# can add a path in front of the file if the result should not be +# The CHM_FILE tag can be used to specify the file name of the resulting .chm +# file. You can add a path in front of the file if the result should not be # written to the html output directory. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. -CHM_FILE = +CHM_FILE = -# If the GENERATE_HTMLHELP tag is set to YES, the HHC_LOCATION tag can -# be used to specify the location (absolute path including file name) of -# the HTML help compiler (hhc.exe). If non-empty doxygen will try to run -# the HTML help compiler on the generated index.hhp. +# The HHC_LOCATION tag can be used to specify the location (absolute path +# including file name) of the HTML help compiler (hhc.exe). If non-empty, +# doxygen will try to run the HTML help compiler on the generated index.hhp. +# The file has to be specified with full path. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. -HHC_LOCATION = +HHC_LOCATION = -# If the GENERATE_HTMLHELP tag is set to YES, the GENERATE_CHI flag -# controls if a separate .chi index file is generated (YES) or that -# it should be included in the master .chm file (NO). +# The GENERATE_CHI flag controls if a separate .chi index file is generated +# (YES) or that it should be included in the master .chm file (NO). +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. GENERATE_CHI = NO -# If the GENERATE_HTMLHELP tag is set to YES, the CHM_INDEX_ENCODING -# is used to encode HtmlHelp index (hhk), content (hhc) and project file -# content. +# The CHM_INDEX_ENCODING is used to encode HtmlHelp index (hhk), content (hhc) +# and project file content. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. -CHM_INDEX_ENCODING = +CHM_INDEX_ENCODING = -# If the GENERATE_HTMLHELP tag is set to YES, the BINARY_TOC flag -# controls whether a binary table of contents is generated (YES) or a -# normal table of contents (NO) in the .chm file. +# The BINARY_TOC flag controls whether a binary table of contents is generated +# (YES) or a normal table of contents (NO) in the .chm file. Furthermore it +# enables the Previous and Next buttons. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. BINARY_TOC = NO -# The TOC_EXPAND flag can be set to YES to add extra items for group members -# to the contents of the HTML help documentation and to the tree view. +# The TOC_EXPAND flag can be set to YES to add extra items for group members to +# the table of contents of the HTML help documentation and to the tree view. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTMLHELP is set to YES. TOC_EXPAND = NO -# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and -# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated -# that can be used as input for Qt's qhelpgenerator to generate a -# Qt Compressed Help (.qch) of the generated HTML documentation. +# If the GENERATE_QHP tag is set to YES and both QHP_NAMESPACE and +# QHP_VIRTUAL_FOLDER are set, an additional index file will be generated that +# can be used as input for Qt's qhelpgenerator to generate a Qt Compressed Help +# (.qch) of the generated HTML documentation. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. GENERATE_QHP = NO -# If the QHG_LOCATION tag is specified, the QCH_FILE tag can -# be used to specify the file name of the resulting .qch file. -# The path specified is relative to the HTML output folder. +# If the QHG_LOCATION tag is specified, the QCH_FILE tag can be used to specify +# the file name of the resulting .qch file. The path specified is relative to +# the HTML output folder. +# This tag requires that the tag GENERATE_QHP is set to YES. -QCH_FILE = +QCH_FILE = -# The QHP_NAMESPACE tag specifies the namespace to use when generating -# Qt Help Project output. For more information please see -# http://doc.trolltech.com/qthelpproject.html#namespace +# The QHP_NAMESPACE tag specifies the namespace to use when generating Qt Help +# Project output. For more information please see Qt Help Project / Namespace +# (see: http://doc.qt.io/archives/qt-4.8/qthelpproject.html#namespace). +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_QHP is set to YES. QHP_NAMESPACE = org.doxygen.Project -# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating -# Qt Help Project output. For more information please see -# http://doc.trolltech.com/qthelpproject.html#virtual-folders +# The QHP_VIRTUAL_FOLDER tag specifies the namespace to use when generating Qt +# Help Project output. For more information please see Qt Help Project / Virtual +# Folders (see: http://doc.qt.io/archives/qt-4.8/qthelpproject.html#virtual- +# folders). +# The default value is: doc. +# This tag requires that the tag GENERATE_QHP is set to YES. QHP_VIRTUAL_FOLDER = doc -# If QHP_CUST_FILTER_NAME is set, it specifies the name of a custom filter to -# add. For more information please see -# http://doc.trolltech.com/qthelpproject.html#custom-filters +# If the QHP_CUST_FILTER_NAME tag is set, it specifies the name of a custom +# filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://doc.qt.io/archives/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. -QHP_CUST_FILTER_NAME = +QHP_CUST_FILTER_NAME = -# The QHP_CUST_FILT_ATTRS tag specifies the list of the attributes of the -# custom filter to add. For more information please see -# -# Qt Help Project / Custom Filters. +# The QHP_CUST_FILTER_ATTRS tag specifies the list of the attributes of the +# custom filter to add. For more information please see Qt Help Project / Custom +# Filters (see: http://doc.qt.io/archives/qt-4.8/qthelpproject.html#custom- +# filters). +# This tag requires that the tag GENERATE_QHP is set to YES. -QHP_CUST_FILTER_ATTRS = +QHP_CUST_FILTER_ATTRS = -# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this -# project's -# filter section matches. -# -# Qt Help Project / Filter Attributes. +# The QHP_SECT_FILTER_ATTRS tag specifies the list of the attributes this +# project's filter section matches. Qt Help Project / Filter Attributes (see: +# http://doc.qt.io/archives/qt-4.8/qthelpproject.html#filter-attributes). +# This tag requires that the tag GENERATE_QHP is set to YES. -QHP_SECT_FILTER_ATTRS = +QHP_SECT_FILTER_ATTRS = -# If the GENERATE_QHP tag is set to YES, the QHG_LOCATION tag can -# be used to specify the location of Qt's qhelpgenerator. -# If non-empty doxygen will try to run qhelpgenerator on the generated -# .qhp file. +# The QHG_LOCATION tag can be used to specify the location of Qt's +# qhelpgenerator. If non-empty doxygen will try to run qhelpgenerator on the +# generated .qhp file. +# This tag requires that the tag GENERATE_QHP is set to YES. -QHG_LOCATION = +QHG_LOCATION = -# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files -# will be generated, which together with the HTML files, form an Eclipse help -# plugin. To install this plugin and make it available under the help contents -# menu in Eclipse, the contents of the directory containing the HTML and XML -# files needs to be copied into the plugins directory of eclipse. The name of -# the directory within the plugins directory should be the same as -# the ECLIPSE_DOC_ID value. After copying Eclipse needs to be restarted before -# the help appears. +# If the GENERATE_ECLIPSEHELP tag is set to YES, additional index files will be +# generated, together with the HTML files, they form an Eclipse help plugin. To +# install this plugin and make it available under the help contents menu in +# Eclipse, the contents of the directory containing the HTML and XML files needs +# to be copied into the plugins directory of eclipse. The name of the directory +# within the plugins directory should be the same as the ECLIPSE_DOC_ID value. +# After copying Eclipse needs to be restarted before the help appears. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. GENERATE_ECLIPSEHELP = NO -# A unique identifier for the eclipse help plugin. When installing the plugin -# the directory name containing the HTML and XML files should also have -# this name. +# A unique identifier for the Eclipse help plugin. When installing the plugin +# the directory name containing the HTML and XML files should also have this +# name. Each documentation set should have its own identifier. +# The default value is: org.doxygen.Project. +# This tag requires that the tag GENERATE_ECLIPSEHELP is set to YES. ECLIPSE_DOC_ID = org.doxygen.Project -# The DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) -# at top of each HTML page. The value NO (the default) enables the index and -# the value YES disables it. Since the tabs have the same information as the -# navigation tree you can set this option to NO if you already set -# GENERATE_TREEVIEW to YES. +# If you want full control over the layout of the generated HTML pages it might +# be necessary to disable the index and replace it with your own. The +# DISABLE_INDEX tag can be used to turn on/off the condensed index (tabs) at top +# of each HTML page. A value of NO enables the index and the value YES disables +# it. Since the tabs in the index contain the same information as the navigation +# tree, you can set this option to YES if you also set GENERATE_TREEVIEW to YES. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. DISABLE_INDEX = NO -# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index -# structure should be generated to display hierarchical information. -# If the tag value is set to YES, a side panel will be generated -# containing a tree-like index structure (just like the one that -# is generated for HTML Help). For this to work a browser that supports -# JavaScript, DHTML, CSS and frames is required (i.e. any modern browser). -# Windows users are probably better off using the HTML help feature. -# Since the tree basically has the same information as the tab index you -# could consider to set DISABLE_INDEX to NO when enabling this option. +# The GENERATE_TREEVIEW tag is used to specify whether a tree-like index +# structure should be generated to display hierarchical information. If the tag +# value is set to YES, a side panel will be generated containing a tree-like +# index structure (just like the one that is generated for HTML Help). For this +# to work a browser that supports JavaScript, DHTML, CSS and frames is required +# (i.e. any modern browser). Windows users are probably better off using the +# HTML help feature. Via custom style sheets (see HTML_EXTRA_STYLESHEET) one can +# further fine-tune the look of the index. As an example, the default style +# sheet generated by doxygen has an example that shows how to put an image at +# the root of the tree instead of the PROJECT_NAME. Since the tree basically has +# the same information as the tab index, you could consider setting +# DISABLE_INDEX to YES when enabling this option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. GENERATE_TREEVIEW = YES -# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values -# (range [0,1..20]) that doxygen will group on one line in the generated HTML -# documentation. Note that a value of 0 will completely suppress the enum -# values from appearing in the overview section. +# The ENUM_VALUES_PER_LINE tag can be used to set the number of enum values that +# doxygen will group on one line in the generated HTML documentation. +# +# Note that a value of 0 will completely suppress the enum values from appearing +# in the overview section. +# Minimum value: 0, maximum value: 20, default value: 4. +# This tag requires that the tag GENERATE_HTML is set to YES. ENUM_VALUES_PER_LINE = 4 -# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be -# used to set the initial width (in pixels) of the frame in which the tree -# is shown. +# If the treeview is enabled (see GENERATE_TREEVIEW) then this tag can be used +# to set the initial width (in pixels) of the frame in which the tree is shown. +# Minimum value: 0, maximum value: 1500, default value: 250. +# This tag requires that the tag GENERATE_HTML is set to YES. TREEVIEW_WIDTH = 250 -# When the EXT_LINKS_IN_WINDOW option is set to YES doxygen will open -# links to external symbols imported via tag files in a separate window. +# If the EXT_LINKS_IN_WINDOW option is set to YES, doxygen will open links to +# external symbols imported via tag files in a separate window. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. EXT_LINKS_IN_WINDOW = NO -# Use this tag to change the font size of Latex formulas included -# as images in the HTML documentation. The default is 10. Note that -# when you change the font size after a successful doxygen run you need -# to manually remove any form_*.png images from the HTML output directory -# to force them to be regenerated. +# Use this tag to change the font size of LaTeX formulas included as images in +# the HTML documentation. When you change the font size after a successful +# doxygen run you need to manually remove any form_*.png images from the HTML +# output directory to force them to be regenerated. +# Minimum value: 8, maximum value: 50, default value: 10. +# This tag requires that the tag GENERATE_HTML is set to YES. FORMULA_FONTSIZE = 10 -# Use the FORMULA_TRANPARENT tag to determine whether or not the images -# generated for formulas are transparent PNGs. Transparent PNGs are -# not supported properly for IE 6.0, but are supported on all modern browsers. -# Note that when changing this option you need to delete any form_*.png files -# in the HTML output before the changes have effect. +# Use the FORMULA_TRANSPARENT tag to determine whether or not the images +# generated for formulas are transparent PNGs. Transparent PNGs are not +# supported properly for IE 6.0, but are supported on all modern browsers. +# +# Note that when changing this option you need to delete any form_*.png files in +# the HTML output directory before the changes have effect. +# The default value is: YES. +# This tag requires that the tag GENERATE_HTML is set to YES. FORMULA_TRANSPARENT = YES -# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax -# (see http://www.mathjax.org) which uses client side Javascript for the -# rendering instead of using prerendered bitmaps. Use this if you do not -# have LaTeX installed or if you want to formulas look prettier in the HTML -# output. When enabled you may also need to install MathJax separately and -# configure the path to it using the MATHJAX_RELPATH option. +# Enable the USE_MATHJAX option to render LaTeX formulas using MathJax (see +# https://www.mathjax.org) which uses client side Javascript for the rendering +# instead of using pre-rendered bitmaps. Use this if you do not have LaTeX +# installed or if you want to formulas look prettier in the HTML output. When +# enabled you may also need to install MathJax separately and configure the path +# to it using the MATHJAX_RELPATH option. +# The default value is: NO. +# This tag requires that the tag GENERATE_HTML is set to YES. USE_MATHJAX = NO -# When MathJax is enabled you need to specify the location relative to the -# HTML output directory using the MATHJAX_RELPATH option. The destination -# directory should contain the MathJax.js script. For instance, if the mathjax -# directory is located at the same level as the HTML output directory, then -# MATHJAX_RELPATH should be ../mathjax. The default value points to -# the MathJax Content Delivery Network so you can quickly see the result without -# installing MathJax. However, it is strongly recommended to install a local -# copy of MathJax from http://www.mathjax.org before deployment. +# When MathJax is enabled you can set the default output format to be used for +# the MathJax output. See the MathJax site (see: +# http://docs.mathjax.org/en/latest/output.html) for more details. +# Possible values are: HTML-CSS (which is slower, but has the best +# compatibility), NativeMML (i.e. MathML) and SVG. +# The default value is: HTML-CSS. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_FORMAT = HTML-CSS + +# When MathJax is enabled you need to specify the location relative to the HTML +# output directory using the MATHJAX_RELPATH option. The destination directory +# should contain the MathJax.js script. For instance, if the mathjax directory +# is located at the same level as the HTML output directory, then +# MATHJAX_RELPATH should be ../mathjax. The default value points to the MathJax +# Content Delivery Network so you can quickly see the result without installing +# MathJax. However, it is strongly recommended to install a local copy of +# MathJax from https://www.mathjax.org before deployment. +# The default value is: https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_RELPATH = https://cdnjs.cloudflare.com/ajax/libs/mathjax/2.7.5/ + +# The MATHJAX_EXTENSIONS tag can be used to specify one or more MathJax +# extension names that should be enabled during MathJax rendering. For example +# MATHJAX_EXTENSIONS = TeX/AMSmath TeX/AMSsymbols +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_EXTENSIONS = + +# The MATHJAX_CODEFILE tag can be used to specify a file with javascript pieces +# of code that will be used on startup of the MathJax code. See the MathJax site +# (see: http://docs.mathjax.org/en/latest/output.html) for more details. For an +# example see the documentation. +# This tag requires that the tag USE_MATHJAX is set to YES. + +MATHJAX_CODEFILE = + +# When the SEARCHENGINE tag is enabled doxygen will generate a search box for +# the HTML output. The underlying search engine uses javascript and DHTML and +# should work on any modern browser. Note that when using HTML help +# (GENERATE_HTMLHELP), Qt help (GENERATE_QHP), or docsets (GENERATE_DOCSET) +# there is already a search function so this one should typically be disabled. +# For large projects the javascript based search engine can be slow, then +# enabling SERVER_BASED_SEARCH may provide a better solution. It is possible to +# search using the keyboard; to jump to the search box use + S +# (what the is depends on the OS and browser, but it is typically +# , /