From 641c9992a138a5e3b6330176340bf2985acefb2f Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Sun, 10 May 2020 20:49:52 +0200 Subject: [PATCH] Distinguish between different BEType and use single BE type in DFTElementTypes --- src/storm-dft/builder/DFTBuilder.cpp | 39 +++++++---- src/storm-dft/builder/DFTBuilder.h | 8 +++ .../builder/ExplicitDFTModelBuilder.cpp | 10 +-- .../generator/DftNextStateGenerator.cpp | 7 +- .../modelchecker/dft/DFTASFChecker.cpp | 64 +++++++++--------- src/storm-dft/storage/dft/DFT.cpp | 14 ++-- src/storm-dft/storage/dft/DFT.h | 10 +-- src/storm-dft/storage/dft/DFTElementType.h | 41 +++++++++--- src/storm-dft/storage/dft/DFTIsomorphism.h | 52 +++++++-------- src/storm-dft/storage/dft/DFTState.cpp | 24 +++---- src/storm-dft/storage/dft/DftJsonExporter.cpp | 22 +++---- src/storm-dft/storage/dft/elements/BEConst.h | 4 +- .../storage/dft/elements/BEExponential.h | 4 +- src/storm-dft/storage/dft/elements/DFTBE.h | 10 +++ .../DftToGspnTransformator.cpp | 22 +++++-- .../transformations/DftToGspnTransformator.h | 7 ++ .../transformations/DftTransformator.cpp | 65 +++++++++++-------- src/storm-dft/utility/FailureBoundFinder.cpp | 8 +-- .../storm-dft/api/DftTransformatorTest.cpp | 4 +- 19 files changed, 247 insertions(+), 168 deletions(-) diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index c02fb3364..acb808657 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -187,8 +187,7 @@ namespace storm { case storm::storage::DFTElementType::SPARE: element = std::make_shared>(mNextId++, name); break; - case storm::storage::DFTElementType::BE_EXP: - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::DFTElementType::BE: case storm::storage::DFTElementType::VOT: case storm::storage::DFTElementType::PDEP: // Handled separately @@ -254,6 +253,9 @@ namespace storm { void DFTBuilder::copyElement(DFTElementPointer element) { std::vector children; switch (element->type()) { + case storm::storage::DFTElementType::BE: + copyBE(std::static_pointer_cast>(element)); + break; case storm::storage::DFTElementType::AND: case storm::storage::DFTElementType::OR: case storm::storage::DFTElementType::PAND: @@ -267,18 +269,6 @@ namespace storm { copyGate(std::static_pointer_cast>(element), children); break; } - case storm::storage::DFTElementType::BE_EXP: - { - auto beExp = std::static_pointer_cast>(element); - addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); - break; - } - case storm::storage::DFTElementType::BE_CONST: - { - auto beConst = std::static_pointer_cast>(element); - addBasicElementConst(beConst->name(), beConst->failed()); - break; - } case storm::storage::DFTElementType::PDEP: { DFTDependencyPointer dependency = std::static_pointer_cast>(element); @@ -304,6 +294,27 @@ namespace storm { } } + template + void DFTBuilder::copyBE(DFTBEPointer be) { + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + { + auto beConst = std::static_pointer_cast>(be); + addBasicElementConst(beConst->name(), beConst->failed()); + break; + } + case storm::storage::BEType::EXPONENTIAL: + { + auto beExp = std::static_pointer_cast>(be); + addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); + break; + } + default: + STORM_LOG_ASSERT(false, "BE type not known."); + break; + } + } + template void DFTBuilder::copyGate(DFTGatePointer gate, std::vector const& children) { switch (gate->type()) { diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 2529ff5c1..0492d079e 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -25,6 +25,7 @@ namespace storm { using DFTElementPointer = std::shared_ptr>; using DFTElementVector = std::vector; + using DFTBEPointer = std::shared_ptr>; using DFTGatePointer = std::shared_ptr>; using DFTGateVector = std::vector; using DFTDependencyPointer = std::shared_ptr>; @@ -214,6 +215,13 @@ namespace storm { */ void copyElement(DFTElementPointer element); + /** + * Copy BE and insert it again in the builder.i + * + * @param be BE to copy. + */ + void copyBE(DFTBEPointer be); + /** * Copy gate with given children and insert it again in the builder. The current children of the element * are discarded. diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index 1f5f3c18f..7b601032e 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -748,8 +748,11 @@ namespace storm { // Consider only still operational BEs if (state->isOperational(id)) { auto be = dft.getBasicElement(id); - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + // Ignore BE which cannot fail + continue; + case storm::storage::BEType::EXPONENTIAL: { // Get BE rate ValueType rate = state->getBERate(id); @@ -765,9 +768,6 @@ namespace storm { rateSum += rate; break; } - case storm::storage::DFTElementType::BE_CONST: - // Ignore BE which cannot fail - continue; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); break; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 0844f08f9..ab49cad13 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -26,7 +26,7 @@ namespace storm { size_t constFailedBeCounter = 0; std::shared_ptr const> constFailedBE = nullptr; for (auto &be : mDft.getBasicElements()) { - if (be->type() == storm::storage::DFTElementType::BE_CONST) { + if (be->beType() == storm::storage::BEType::CONSTANT) { auto constBe = std::static_pointer_cast const>(be); if (constBe->failed()) { constFailedBeCounter++; @@ -143,7 +143,8 @@ namespace storm { propagateFailure(newState, nextBE, queues); bool transient = false; - if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) { + // TODO handle for all types of BEs. + if (nextBE->beType() == storm::storage::BEType::EXPONENTIAL) { auto beExp = std::static_pointer_cast const>(nextBE); transient = beExp->isTransient(); } @@ -194,7 +195,7 @@ namespace storm { } else { // Failure is due to "normal" BE failure // Set failure rate according to activation - STORM_LOG_THROW(nextBE->type() == storm::storage::DFTElementType::BE_EXP, storm::exceptions::NotSupportedException, "BE of type '" << nextBE->type() << "' is not supported."); + STORM_LOG_THROW(nextBE->beType() == storm::storage::BEType::EXPONENTIAL, storm::exceptions::NotSupportedException, "BE of type '" << nextBE->type() << "' is not supported."); auto beExp = std::static_pointer_cast const>(nextBE); bool isActive = true; if (mDft.hasRepresentant(beExp->id())) { diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 30d9bcb63..dd7a847ab 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -35,21 +35,30 @@ namespace storm { varNames.push_back("t_" + element->name()); timePointVariables.emplace(i, varNames.size() - 1); switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: - beVariables.push_back(varNames.size() - 1); - break; - case storm::storage::DFTElementType::BE_CONST: { - STORM_LOG_WARN("Constant BEs are only experimentally supported in the SMT encoding"); - // Constant BEs are initially either failed or failsafe, treat them differently - auto be = std::static_pointer_cast const>(element); - if (be->failed()) { - STORM_LOG_THROW(!failedBeIsSet, storm::exceptions::NotSupportedException, - "DFTs containing more than one constantly failed BE are not supported"); - notFailed = dft.nrBasicElements(); - failedBeVariables = varNames.size() - 1; - failedBeIsSet = true; - } else { - failsafeBeVariables.push_back(varNames.size() - 1); + case storm::storage::DFTElementType::BE: { + auto be = std::static_pointer_cast const>(element); + switch (be->beType()) { + case storm::storage::BEType::EXPONENTIAL: + beVariables.push_back(varNames.size() - 1); + break; + case storm::storage::BEType::CONSTANT: { + STORM_LOG_WARN("Constant BEs are only experimentally supported in the SMT encoding"); + // Constant BEs are initially either failed or failsafe, treat them differently + auto be = std::static_pointer_cast const>(element); + if (be->failed()) { + STORM_LOG_THROW(!failedBeIsSet, storm::exceptions::NotSupportedException, + "DFTs containing more than one constantly failed BE are not supported"); + notFailed = dft.nrBasicElements(); + failedBeVariables = varNames.size() - 1; + failedBeIsSet = true; + } else { + failsafeBeVariables.push_back(varNames.size() - 1); + } + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "BE type '" << be->beType() << "' not known."); + break; } break; } @@ -146,8 +155,7 @@ namespace storm { } switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::DFTElementType::BE: // BEs were already considered before break; case storm::storage::DFTElementType::AND: @@ -208,19 +216,17 @@ namespace storm { std::vector> triggerConstraints; for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); - if (element->type() == storm::storage::DFTElementType::BE_CONST) { + if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); - triggerConstraints.clear(); - for (auto const &dependency : be->ingoingDependencies()) { - triggerConstraints.push_back(std::make_shared( - timePointVariables.at(dependency->triggerEvent()->id()), notFailed)); - } - if (!triggerConstraints.empty()) { - constraints.push_back(std::make_shared( - std::make_shared(timePointVariables.at(be->id()), notFailed), - std::make_shared(triggerConstraints))); - constraints.back()->setDescription( - "Failsafe BE " + be->name() + " stays failsafe if no trigger fails"); + if (be->beType() == storm::storage::BEType::CONSTANT) { + triggerConstraints.clear(); + for (auto const &dependency : be->ingoingDependencies()) { + triggerConstraints.push_back(std::make_shared(timePointVariables.at(dependency->triggerEvent()->id()), notFailed)); + } + if (!triggerConstraints.empty()) { + constraints.push_back(std::make_shared(std::make_shared(timePointVariables.at(be->id()), notFailed), std::make_shared(triggerConstraints))); + constraints.back()->setDescription("Failsafe BE " + be->name() + " stays failsafe if no trigger fails"); + } } } } diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 6b79e1c1e..94e33cbaa 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -206,8 +206,6 @@ namespace storm { break; } //BEs - case storage::DFTElementType::BE_EXP: - case storage::DFTElementType::BE_CONST: case storage::DFTElementType::BE: { auto be = std::static_pointer_cast>(currentElement); dynamicBehaviorVector[be->id()] = true; @@ -506,8 +504,7 @@ namespace storm { case DFTElementType::OR: builder.addOrElement(newParentName, childrenNames); break; - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: case DFTElementType::VOT: case DFTElementType::PAND: case DFTElementType::SPARE: @@ -548,8 +545,7 @@ namespace storm { case DFTElementType::AND: case DFTElementType::OR: case DFTElementType::VOT: - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: break; case DFTElementType::PAND: case DFTElementType::SPARE: @@ -577,8 +573,7 @@ namespace storm { case DFTElementType::VOT: ++noStatic; break; - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: case DFTElementType::PAND: case DFTElementType::SPARE: case DFTElementType::POR: @@ -1089,8 +1084,7 @@ namespace storm { size_t noRestriction = 0; for (auto const& elem : mElements) { switch (elem->type()) { - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: ++noBE; break; case DFTElementType::AND: diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index c7c790350..a95b06937 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -160,17 +160,17 @@ namespace storm { if (elem->isBasicElement()) { std::shared_ptr> be = std::static_pointer_cast>(elem); if (be->canFail()) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: { + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + result.push_back(be->id()); + break; + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast>(be); if (!beExp->isColdBasicElement()) { result.push_back(be->id()); } break; } - case storm::storage::DFTElementType::BE_CONST: - result.push_back(be->id()); - break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); } diff --git a/src/storm-dft/storage/dft/DFTElementType.h b/src/storm-dft/storage/dft/DFTElementType.h index c76b071fe..3496f3c8d 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -9,9 +9,8 @@ namespace storm { * Element types in a DFT. */ enum class DFTElementType { - BE_EXP, BE_CONST, - AND, OR, VOT, BE, + AND, OR, VOT, PAND, POR, SPARE, @@ -20,6 +19,15 @@ namespace storm { MUTEX }; + /*! + * BE types in a DFT. + */ + enum class BEType { + CONSTANT, + EXPONENTIAL + }; + + inline bool isGateType(DFTElementType const& type) { switch (type) { case DFTElementType::AND: @@ -29,8 +37,7 @@ namespace storm { case DFTElementType::POR: case DFTElementType::SPARE: return true; - case DFTElementType::BE_EXP: - case DFTElementType::BE_CONST: + case DFTElementType::BE: case DFTElementType::PDEP: case DFTElementType::SEQ: case DFTElementType::MUTEX: @@ -60,12 +67,10 @@ namespace storm { } } - inline std::string toString(DFTElementType const& tp) { - switch (tp) { - case DFTElementType::BE_EXP: - return "BE_EXP"; - case DFTElementType::BE_CONST: - return "BE_CONST"; + inline std::string toString(DFTElementType const& type) { + switch (type) { + case DFTElementType::BE: + return "BE"; case DFTElementType::AND: return "AND"; case DFTElementType::OR: @@ -90,9 +95,25 @@ namespace storm { } } + inline std::string toString(BEType const& type) { + switch (type) { + case BEType::CONSTANT: + return "CONST"; + case BEType::EXPONENTIAL: + return "EXPONENTIAL"; + default: + STORM_LOG_ASSERT(false, "BE type not known."); + return ""; + } + } + inline std::ostream& operator<<(std::ostream& os, DFTElementType const& type) { return os << toString(type); } + inline std::ostream& operator<<(std::ostream& os, BEType const& type) { + return os << toString(type); + } + } } diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index 34287b540..701082443 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -57,15 +57,15 @@ namespace storage { BEColourClass() = default; - BEColourClass(storm::storage::DFTElementType t, ValueType a, ValueType p, size_t h) : type(t), hash(h), aRate(a), pRate(p) { - STORM_LOG_ASSERT(t == storm::storage::DFTElementType::BE_EXP, "Expected type BE_EXP but got type " << t); + BEColourClass(storm::storage::BEType t, ValueType a, ValueType p, size_t h) : type(t), hash(h), aRate(a), pRate(p) { + STORM_LOG_ASSERT(t == storm::storage::BEType::EXPONENTIAL, "Expected type EXPONENTIAL but got type " << t); } - BEColourClass(storm::storage::DFTElementType t, bool fail, size_t h) : type(t), hash(h), failed(fail) { - STORM_LOG_ASSERT(t == storm::storage::DFTElementType::BE_CONST, "Expected type BE_CONST but got type " << t); + BEColourClass(storm::storage::BEType t, bool fail, size_t h) : type(t), hash(h), failed(fail) { + STORM_LOG_ASSERT(t == storm::storage::BEType::CONSTANT, "Expected type CONSTANT but got type " << t); } - storm::storage::DFTElementType type; + storm::storage::BEType type; size_t hash; ValueType aRate; ValueType pRate; @@ -79,9 +79,9 @@ namespace storage { return false; } switch (lhs.type) { - case storm::storage::DFTElementType::BE_EXP: + case storm::storage::BEType::EXPONENTIAL: return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::CONSTANT: return lhs.hash == rhs.hash && lhs.failed == rhs.failed; default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << lhs.type << "' is not known."); @@ -271,21 +271,21 @@ namespace storage { protected: void colourize(std::shared_ptr> const& be) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { - auto beExp = std::static_pointer_cast const>(be); - beColour[beExp->id()] = BEColourClass(beExp->type(), beExp->activeFailureRate(), beExp->passiveFailureRate(), beExp->nrParents()); + auto beConst = std::static_pointer_cast const>(be); + beColour[beConst->id()] = BEColourClass(beConst->beType(), beConst->failed(), beConst->nrParents()); break; } - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::EXPONENTIAL: { - auto beConst = std::static_pointer_cast const>(be); - beColour[beConst->id()] = BEColourClass(beConst->type(), beConst->failed(), beConst->nrParents()); + auto beExp = std::static_pointer_cast const>(be); + beColour[beExp->id()] = BEColourClass(beExp->beType(), beExp->activeFailureRate(), beExp->passiveFailureRate(), beExp->nrParents()); break; } default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->beType() << "' is not known."); break; } } @@ -299,21 +299,21 @@ namespace storage { void colourize(std::shared_ptr> const& dep) { // TODO this can be improved for n-ary dependencies. std::shared_ptr const> be = dep->dependentEvents()[0]; - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { - auto beExp = std::static_pointer_cast const>(be); - depColour[dep->id()] = std::pair(dep->probability(), beExp->activeFailureRate()); + auto beConst = std::static_pointer_cast const>(be); + depColour[dep->id()] = std::pair(dep->probability(), beConst->failed() ? storm::utility::one() : storm::utility::zero()); break; } - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::EXPONENTIAL: { - auto beConst = std::static_pointer_cast const>(be); - depColour[dep->id()] = std::pair(dep->probability(), beConst->failed() ? storm::utility::one() : storm::utility::zero()); + auto beExp = std::static_pointer_cast const>(be); + depColour[dep->id()] = std::pair(dep->probability(), beExp->activeFailureRate()); break; } default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->beType() << "' is not known."); break; } } @@ -706,10 +706,10 @@ namespace std { groupHash |= (static_cast(bcc.type) & fivebitmask) << (62 - 5); switch (bcc.type) { - case storm::storage::DFTElementType::BE_EXP: - return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8); - case storm::storage::DFTElementType::BE_CONST: + case storm::storage::BEType::CONSTANT: return (bcc.failed << 8); + case storm::storage::BEType::EXPONENTIAL: + return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8); default: STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << bcc.type << "' is not known."); break; diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 082b4e8a6..65e0b3fb8 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -49,8 +49,12 @@ namespace storm { if (mDft.isBasicElement(index) && isOperational(index) && !isEventDisabledViaRestriction(index)) { std::shared_ptr> be = mDft.getBasicElement(index); if (be->canFail()) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + failableElements.addBE(index); + STORM_LOG_TRACE("Currently failable: " << *be); + break; + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); if (!beExp->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { @@ -59,10 +63,6 @@ namespace storm { } break; } - case storm::storage::DFTElementType::BE_CONST: - failableElements.addBE(index); - STORM_LOG_TRACE("Currently failable: " << *be); - break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); break; @@ -315,7 +315,7 @@ namespace storm { template ValueType DFTState::getBERate(size_t id) const { STORM_LOG_ASSERT(mDft.isBasicElement(id), "Element is no BE."); - STORM_LOG_THROW(mDft.getBasicElement(id)->type() == storm::storage::DFTElementType::BE_EXP, storm::exceptions::NotSupportedException, "BE of type '" << mDft.getBasicElement(id)->type() << "' is not supported."); + STORM_LOG_THROW(mDft.getBasicElement(id)->beType() == storm::storage::BEType::EXPONENTIAL, storm::exceptions::NotSupportedException, "BE of type '" << mDft.getBasicElement(id)->type() << "' is not supported."); auto beExp = std::static_pointer_cast const>(mDft.getBasicElement(id)); if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { // Return passive failure rate @@ -380,8 +380,11 @@ namespace storm { if(mDft.isBasicElement(elem) && isOperational(elem) && !isEventDisabledViaRestriction(elem)) { std::shared_ptr> be = mDft.getBasicElement(elem); if (be->canFail()) { - switch (be->type()) { - case storm::storage::DFTElementType::BE_EXP: { + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + // Nothing to do + break; + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); if (beExp->isColdBasicElement()) { // Add to failable BEs @@ -389,9 +392,6 @@ namespace storm { } break; } - case storm::storage::DFTElementType::BE_CONST: - // Nothing to do - break; default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "BE type '" << be->type() << "' is not supported."); } diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 63b2e8602..c0a5bf2cb 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -88,8 +88,16 @@ namespace storm { } else if (element->isBasicElement()) { std::shared_ptr const> be = std::static_pointer_cast const>(element); // Set BE specific data - switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: + { + auto beConst = std::static_pointer_cast const>(be); + std::stringstream stream; + nodeData["distribution"] = "const"; + nodeData["failed"] = beConst->failed(); + break; + } + case storm::storage::BEType::EXPONENTIAL: { auto beExp = std::static_pointer_cast const>(be); std::stringstream stream; @@ -101,16 +109,8 @@ namespace storm { nodeData["dorm"] = stream.str(); break; } - case storm::storage::DFTElementType::BE_CONST: - { - auto beConst = std::static_pointer_cast const>(be); - std::stringstream stream; - nodeData["distribution"] = "const"; - nodeData["failed"] = beConst->failed(); - break; - } default: - STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->beType() << "' is not known."); break; } } else { diff --git a/src/storm-dft/storage/dft/elements/BEConst.h b/src/storm-dft/storage/dft/elements/BEConst.h index 2cbf9fd38..050cdf51e 100644 --- a/src/storm-dft/storage/dft/elements/BEConst.h +++ b/src/storm-dft/storage/dft/elements/BEConst.h @@ -23,8 +23,8 @@ namespace storm { // Intentionally empty } - DFTElementType type() const override { - return DFTElementType::BE_CONST; + BEType beType() const override { + return BEType::CONSTANT; } /*! diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h index 1ed6221d6..71786fda8 100644 --- a/src/storm-dft/storage/dft/elements/BEExponential.h +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -25,8 +25,8 @@ namespace storm { STORM_LOG_ASSERT(!storm::utility::isZero(failureRate), "Exponential failure rate should not be zero."); } - DFTElementType type() const override { - return DFTElementType::BE_EXP; + BEType beType() const override { + return BEType::EXPONENTIAL; } /*! diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 38eeb4de1..899ece201 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -22,6 +22,16 @@ namespace storm { // Intentionally empty } + DFTElementType type() const override { + return DFTElementType::BE; + } + + /*! + * Get type of BE (constant, exponential, etc.). + * @return BE type. + */ + virtual BEType beType() const = 0; + size_t nrChildren() const override { return 0; } diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 60a4d04e5..7a57fe8fa 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -122,11 +122,8 @@ namespace storm { // Check which type the element is and call the corresponding translate-function. switch (dftElement->type()) { - case storm::storage::DFTElementType::BE_EXP: - translateBEExponential(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::BE_CONST: - translateBEConst(std::static_pointer_cast const>(dftElement)); + case storm::storage::DFTElementType::BE: + translateBE(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::AND: translateAND(std::static_pointer_cast const>(dftElement)); @@ -167,6 +164,21 @@ namespace storm { } + template + void DftToGspnTransformator::translateBE(std::shared_ptr const> dftBE) { + switch (dftBE->beType()) { + case storm::storage::BEType::CONSTANT: + translateBEConst(std::static_pointer_cast const>(dftBE)); + break; + case storm::storage::BEType::EXPONENTIAL: + translateBEExponential(std::static_pointer_cast const>(dftBE)); + break; + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE type '" << dftBE->beType() << "' not known."); + break; + } + } + template void DftToGspnTransformator::translateBEExponential(std::shared_ptr const> dftBE) { double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 72b6d1831..d54687bea 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -61,6 +61,13 @@ namespace storm { */ void translateGSPNElements(); + /*! + * Translate a BE. + * + * @param dftBE The basic event. + */ + void translateBE(std::shared_ptr const> dftBE); + /*! * Translate an exponential BE. * diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index 6dcbdf17c..ea62a686c 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -20,22 +20,28 @@ namespace storm { for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: { - auto be_exp = std::static_pointer_cast const>( - element); - builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), - be_exp->dormancyFactor()); - break; - } - case storm::storage::DFTElementType::BE_CONST: { - auto be_const = std::static_pointer_cast const>( - element); - if (be_const->canFail()) { - STORM_LOG_TRACE("Transform " + element->name() + " [BE (const failed)]"); - failedBEs.push_back(be_const->name()); + case storm::storage::DFTElementType::BE: { + auto be = std::static_pointer_cast const>(element); + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { + auto beConst = std::static_pointer_cast const>(element); + if (beConst->canFail()) { + STORM_LOG_TRACE("Transform " + beConst->name() + " [BE (const failed)]"); + failedBEs.push_back(beConst->name()); + } + // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element + builder.addBasicElementConst(beConst->name(), false); + break; + } + case storm::storage::BEType::EXPONENTIAL: { + auto beExp = std::static_pointer_cast const>(element); + builder.addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "BE type '" << be->beType() << "' not known."); + break; } - // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element - builder.addBasicElementConst(be_const->name(), false); break; } case storm::storage::DFTElementType::AND: @@ -107,18 +113,23 @@ namespace storm { for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr const> element = dft.getElement(i); switch (element->type()) { - case storm::storage::DFTElementType::BE_EXP: { - auto be_exp = std::static_pointer_cast const>( - element); - builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), - be_exp->dormancyFactor()); - break; - } - case storm::storage::DFTElementType::BE_CONST: { - auto be_const = std::static_pointer_cast const>( - element); - // All original constant BEs are set to failsafe, failed BEs are later triggered by a new element - builder.addBasicElementConst(be_const->name(), be_const->canFail()); + case storm::storage::DFTElementType::BE: { + auto be = std::static_pointer_cast const>(element); + switch (be->beType()) { + case storm::storage::BEType::CONSTANT: { + auto beConst = std::static_pointer_cast const>(element); + builder.addBasicElementConst(beConst->name(), beConst->canFail()); + break; + } + case storm::storage::BEType::EXPONENTIAL: { + auto beExp = std::static_pointer_cast const>(element); + builder.addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "BE type '" << be->beType() << "' not known."); + break; + } break; } case storm::storage::DFTElementType::AND: diff --git a/src/storm-dft/utility/FailureBoundFinder.cpp b/src/storm-dft/utility/FailureBoundFinder.cpp index d09caae83..fced153c2 100644 --- a/src/storm-dft/utility/FailureBoundFinder.cpp +++ b/src/storm-dft/utility/FailureBoundFinder.cpp @@ -15,8 +15,7 @@ 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_EXP || - element->type() == storm::storage::DFTElementType::BE_CONST) { + if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { ++nrDepEvents; @@ -81,8 +80,7 @@ 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_EXP || - element->type() == storm::storage::DFTElementType::BE_CONST) { + if (element->isBasicElement()) { auto be = std::static_pointer_cast const>(element); if (be->hasIngoingDependencies()) { ++nrDepEvents; @@ -236,4 +234,4 @@ namespace storm { class FailureBoundFinder; } } -} \ No newline at end of file +} diff --git a/src/test/storm-dft/api/DftTransformatorTest.cpp b/src/test/storm-dft/api/DftTransformatorTest.cpp index c249cd2df..bca6e4ae5 100644 --- a/src/test/storm-dft/api/DftTransformatorTest.cpp +++ b/src/test/storm-dft/api/DftTransformatorTest.cpp @@ -17,7 +17,7 @@ namespace { uint64_t constBeFailedCount = 0; uint64_t constBeFailsafeCount = 0; for (auto &be : bes) { - if (be->type() == storm::storage::DFTElementType::BE_CONST) { + if (be->beType() == storm::storage::BEType::CONSTANT) { if (be->canFail()) { ++constBeFailedCount; } else { @@ -66,4 +66,4 @@ namespace { EXPECT_EQ(4ul, transformedDft->nrBasicElements()); } -} \ No newline at end of file +}