From 3bf14c5198f06e67fd692721cdfde124bd172412 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Wed, 3 Apr 2019 17:15:11 +0200 Subject: [PATCH] Larger refactoring for DFT BEs. Split into BEExponential and BEConst --- src/storm-dft/builder/DFTBuilder.cpp | 22 ++- src/storm-dft/builder/DFTBuilder.h | 4 +- .../builder/ExplicitDFTModelBuilder.cpp | 26 +++- .../generator/DftNextStateGenerator.cpp | 16 +- .../modelchecker/dft/DFTASFChecker.cpp | 8 +- src/storm-dft/parser/DFTJsonParser.cpp | 25 ++- src/storm-dft/storage/dft/DFT.cpp | 25 ++- src/storm-dft/storage/dft/DFT.h | 21 ++- src/storm-dft/storage/dft/DFTElementType.h | 70 +++++---- src/storm-dft/storage/dft/DFTElements.h | 3 +- src/storm-dft/storage/dft/DFTIsomorphism.h | 83 +++++++++- src/storm-dft/storage/dft/DFTState.cpp | 58 +++++-- src/storm-dft/storage/dft/DftJsonExporter.cpp | 34 ++++- src/storm-dft/storage/dft/elements/BEConst.h | 61 ++++++++ .../storage/dft/elements/BEExponential.h | 103 +++++++++++++ src/storm-dft/storage/dft/elements/DFTAnd.h | 6 - src/storm-dft/storage/dft/elements/DFTBE.h | 143 +++++++----------- src/storm-dft/storage/dft/elements/DFTConst.h | 58 ------- .../storage/dft/elements/DFTDependency.h | 10 +- .../storage/dft/elements/DFTElement.h | 112 +++++++++----- src/storm-dft/storage/dft/elements/DFTOr.h | 4 - src/storm-dft/storage/dft/elements/DFTPand.h | 5 - src/storm-dft/storage/dft/elements/DFTPor.h | 5 - .../storage/dft/elements/DFTRestriction.h | 30 ++-- src/storm-dft/storage/dft/elements/DFTSpare.h | 1 + src/storm-dft/storage/dft/elements/DFTVot.h | 5 - .../DftToGspnTransformator.cpp | 63 ++++---- .../transformations/DftToGspnTransformator.h | 19 +-- 28 files changed, 635 insertions(+), 385 deletions(-) create mode 100644 src/storm-dft/storage/dft/elements/BEConst.h create mode 100644 src/storm-dft/storage/dft/elements/BEExponential.h delete mode 100644 src/storm-dft/storage/dft/elements/DFTConst.h diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 2c3f4a656..56fda6401 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -3,6 +3,7 @@ #include #include "storm/utility/macros.h" +#include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/WrongFormatException.h" @@ -188,14 +189,12 @@ namespace storm { case storm::storage::DFTElementType::SPARE: element = std::make_shared>(mNextId++, name); break; - case storm::storage::DFTElementType::BE: + case storm::storage::DFTElementType::BE_EXP: + case storm::storage::DFTElementType::BE_CONST: case storm::storage::DFTElementType::VOT: case storm::storage::DFTElementType::PDEP: // Handled separately STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type handled separately."); - case storm::storage::DFTElementType::CONSTF: - case storm::storage::DFTElementType::CONSTS: - STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not supported."); default: STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Gate type not known."); } @@ -270,17 +269,16 @@ namespace storm { copyGate(std::static_pointer_cast>(element), children); break; } - case storm::storage::DFTElementType::BE: + case storm::storage::DFTElementType::BE_EXP: { - std::shared_ptr> be = std::static_pointer_cast>(element); - addBasicElementExponential(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient()); + auto beExp = std::static_pointer_cast>(element); + addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient()); break; } - case storm::storage::DFTElementType::CONSTF: - case storm::storage::DFTElementType::CONSTS: + case storm::storage::DFTElementType::BE_CONST: { - std::shared_ptr> be = std::static_pointer_cast>(element); - addBasicElementConst(be->name(), be->failed()); + auto beConst = std::static_pointer_cast>(element); + addBasicElementConst(beConst->name(), beConst->failed()); break; } case storm::storage::DFTElementType::PDEP: @@ -303,7 +301,7 @@ namespace storm { break; } default: - STORM_LOG_ASSERT(false, "Dft type not known."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "DFT type '" << element->type() << "' not known."); break; } } diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 2f89b8306..b12013fc7 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -175,7 +175,7 @@ namespace storm { STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } - mElements[name] = std::make_shared>(mNextId++, name, failed); + mElements[name] = std::make_shared>(mNextId++, name, failed); return true; } @@ -205,7 +205,7 @@ namespace storm { return addBasicElementConst(name, false); } - mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } diff --git a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp index eb7d50e06..8c23c6d6a 100644 --- a/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp +++ b/src/storm-dft/builder/ExplicitDFTModelBuilder.cpp @@ -9,6 +9,7 @@ #include "storm/utility/vector.h" #include "storm/utility/bitoperations.h" #include "storm/utility/ProgressMeasurement.h" +#include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/UnexpectedException.h" #include "storm/settings/SettingsManager.h" #include "storm/logic/AtomicLabelFormula.h" @@ -704,13 +705,26 @@ namespace storm { ValueType rate = state->getBERate(id); if (storm::utility::isZero(rate)) { // Get active failure rate for cold BE - rate = dft.getBasicElement(id)->activeFailureRate(); - if (storm::utility::isZero(rate)) { - // Ignore BE which cannot fail - continue; + auto be = dft.getBasicElement(id); + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + auto beExp = std::static_pointer_cast const>(be); + rate = beExp->activeFailureRate(); + STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Failure rate should not be zero."); + // Mark BE as cold + coldBEs.set(i, true); + 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; } - // Mark BE as cold - coldBEs.set(i, true); } rates.push_back(rate); rateSum += rate; diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 69751ea62..b59e91d52 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -118,7 +118,13 @@ namespace storm { newState->updateFailableDependencies(next->id()); } - if(newState->isInvalid() || (nextBE->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex()))) { + bool transient = false; + if (nextBE->type() == storm::storage::DFTElementType::BE_EXP) { + auto beExp = std::static_pointer_cast const>(nextBE); + transient = beExp->isTransient(); + } + + if(newState->isInvalid() || (transient && !newState->hasFailed(mDft.getTopLevelIndex()))) { // Continue with next possible state state->getFailableElements().next(); STORM_LOG_TRACE("State is ignored because " << (newState->isInvalid() ? "it is invalid" : "the transient fault is ignored")); @@ -173,12 +179,14 @@ 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."); + auto beExp = std::static_pointer_cast const>(nextBE); bool isActive = true; - if (mDft.hasRepresentant(nextBE->id())) { + if (mDft.hasRepresentant(beExp->id())) { // Active must be checked for the state we are coming from as this state is responsible for the rate - isActive = state->isActive(mDft.getRepresentant(nextBE->id())); + isActive = state->isActive(mDft.getRepresentant(beExp->id())); } - ValueType rate = isActive ? nextBE->activeFailureRate() : nextBE->passiveFailureRate(); + ValueType rate = isActive ? beExp->activeFailureRate() : beExp->passiveFailureRate(); STORM_LOG_ASSERT(!storm::utility::isZero(rate), "Rate is 0."); choice.addProbability(newStateId, rate); STORM_LOG_TRACE("Added transition to " << newStateId << " with " << (isActive ? "active" : "passive") << " failure rate " << rate); diff --git a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp index 41f688da0..1b9a2ea89 100644 --- a/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp +++ b/src/storm-dft/modelchecker/dft/DFTASFChecker.cpp @@ -417,9 +417,12 @@ namespace storm { varNames.push_back("t_" + element->name()); timePointVariables.emplace(i, varNames.size() - 1); switch (element->type()) { - case storm::storage::DFTElementType::BE: + case storm::storage::DFTElementType::BE_EXP: beVariables.push_back(varNames.size() - 1); break; + case storm::storage::DFTElementType::BE_CONST: + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant BEs are not supported in SMT translation."); + break; case storm::storage::DFTElementType::SPARE: { auto spare = std::static_pointer_cast const>(element); @@ -721,8 +724,7 @@ namespace storm { 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()); - notColdC[i].push_back(std::make_shared(nextFailure, std::make_shared(!cold))); + notColdC[i].push_back(std::make_shared(nextFailure, std::make_shared(be->canFail()))); } } } diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index 23d83fed2..1272e033e 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -93,14 +93,25 @@ namespace storm { ValueType probability = parseRationalExpression(parseJsonNumber(data.at("probability"))); success = builder.addDepElement(name, childNames, probability); } else if (type == "be") { - // TODO support different distributions - ValueType failureRate = parseRationalExpression(parseJsonNumber(data.at("rate"))); - ValueType dormancyFactor = parseRationalExpression(parseJsonNumber(data.at("dorm"))); - bool transient = false; - if (data.count("transient") > 0) { - transient = data.at("transient"); + std::string distribution = "exp"; // Set default of exponential distribution + if (data.count("distribution") > 0) { + distribution = data.at("distribution"); + } + if (distribution == "exp") { + ValueType failureRate = parseRationalExpression(parseJsonNumber(data.at("rate"))); + ValueType dormancyFactor = parseRationalExpression(parseJsonNumber(data.at("dorm"))); + bool transient = false; + if (data.count("transient") > 0) { + transient = data.at("transient"); + } + success = builder.addBasicElementExponential(name, failureRate, dormancyFactor, transient); + } else if (distribution == "const") { + bool failed = data.at("failed"); + success = builder.addBasicElementConst(name, failed); + } else { + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Distribution: " << distribution << " not supported."); + success = false; } - success = builder.addBasicElementExponential(name, failureRate, dormancyFactor, transient); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized."); success = false; diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp index 5caa0d555..c66af8550 100644 --- a/src/storm-dft/storage/dft/DFT.cpp +++ b/src/storm-dft/storage/dft/DFT.cpp @@ -3,6 +3,7 @@ #include #include +#include "storm/exceptions/InvalidArgumentException.h" #include "storm/exceptions/NotSupportedException.h" #include "storm/exceptions/WrongFormatException.h" #include "storm/utility/iota_n.h" @@ -348,9 +349,8 @@ namespace storm { case DFTElementType::OR: builder.addOrElement(newParentName, childrenNames); break; - case DFTElementType::BE: - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: + case DFTElementType::BE_EXP: + case DFTElementType::BE_CONST: case DFTElementType::VOT: case DFTElementType::PAND: case DFTElementType::SPARE: @@ -391,9 +391,8 @@ namespace storm { case DFTElementType::AND: case DFTElementType::OR: case DFTElementType::VOT: - case DFTElementType::BE: - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: + case DFTElementType::BE_EXP: + case DFTElementType::BE_CONST: break; case DFTElementType::PAND: case DFTElementType::SPARE: @@ -421,9 +420,8 @@ namespace storm { case DFTElementType::VOT: ++noStatic; break; - case DFTElementType::BE: - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: + case DFTElementType::BE_EXP: + case DFTElementType::BE_CONST: case DFTElementType::PAND: case DFTElementType::SPARE: case DFTElementType::POR: @@ -443,7 +441,7 @@ namespace storm { std::string DFT::getElementsString() const { std::stringstream stream; for (auto const& elem : mElements) { - stream << "[" << elem->id() << "]" << elem->toString() << std::endl; + stream << "[" << elem->id() << "]" << *elem << std::endl; } return stream.str(); } @@ -495,7 +493,7 @@ namespace storm { std::stringstream stream; for (auto const& elem : mElements) { stream << "[" << elem->id() << "]"; - stream << elem->toString(); + stream << *elem; if (elem->isDependency()) { stream << "\t** " << storm::storage::toChar(state->getDependencyState(elem->id())) << "[dep]"; } else { @@ -860,9 +858,8 @@ namespace storm { size_t noRestriction = 0; for (auto const& elem : mElements) { switch (elem->type()) { - case DFTElementType::BE: - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: + case DFTElementType::BE_EXP: + case DFTElementType::BE_CONST: ++noBE; break; case DFTElementType::AND: diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h index aef5036d8..b902d6218 100644 --- a/src/storm-dft/storage/dft/DFT.h +++ b/src/storm-dft/storage/dft/DFT.h @@ -11,6 +11,7 @@ #include "storm/storage/BitVector.h" #include "storm/utility/math.h" #include "storm/utility/macros.h" +#include "storm/exceptions/NotSupportedException.h" #include "storm-dft/storage/dft/DFTElements.h" #include "storm-dft/storage/dft/SymmetricUnits.h" @@ -134,11 +135,23 @@ namespace storm { std::vector nonColdBEs() const { std::vector result; - for(DFTElementPointer elem : mElements) { - if(elem->isBasicElement()) { + for (DFTElementPointer elem : mElements) { + if (elem->isBasicElement()) { std::shared_ptr> be = std::static_pointer_cast>(elem); - if (be->canFail() && !be->isColdBasicElement()) { - result.push_back(be->id()); + if (be->canFail()) { + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: { + 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()); + 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 1527efe25..c76b071fe 100644 --- a/src/storm-dft/storage/dft/DFTElementType.h +++ b/src/storm-dft/storage/dft/DFTElementType.h @@ -5,80 +5,94 @@ namespace storm { namespace storage { - enum class DFTElementType : int {AND = 0, OR = 2, VOT = 3, BE = 4, CONSTF = 5, CONSTS = 6, PAND = 7, SPARE = 8, POR = 9, PDEP = 10, SEQ = 11, MUTEX=12}; + /*! + * Element types in a DFT. + */ + enum class DFTElementType { + BE_EXP, BE_CONST, + AND, OR, VOT, + BE, + PAND, + POR, + SPARE, + PDEP, + SEQ, + MUTEX + }; - inline bool isGateType(DFTElementType const& tp) { - switch(tp) { + inline bool isGateType(DFTElementType const& type) { + switch (type) { case DFTElementType::AND: case DFTElementType::OR: case DFTElementType::VOT: case DFTElementType::PAND: - case DFTElementType::SPARE: case DFTElementType::POR: + case DFTElementType::SPARE: return true; + case DFTElementType::BE_EXP: + case DFTElementType::BE_CONST: + case DFTElementType::PDEP: case DFTElementType::SEQ: case DFTElementType::MUTEX: - case DFTElementType::BE: - case DFTElementType::CONSTF: - case DFTElementType::CONSTS: - case DFTElementType::PDEP: return false; default: - STORM_LOG_ASSERT(false, "Dft type not known."); + STORM_LOG_ASSERT(false, "DFT type not known."); return false; } } - inline bool isStaticGateType(DFTElementType const& tp) { - if(!isGateType(tp)) return false; - switch(tp) { + inline bool isStaticGateType(DFTElementType const& type) { + if (!isGateType(type)) { + return false; + } + switch (type) { case DFTElementType::AND: case DFTElementType::OR: case DFTElementType::VOT: return true; + case DFTElementType::PAND: case DFTElementType::POR: case DFTElementType::SPARE: - case DFTElementType::PAND: return false; default: - STORM_LOG_ASSERT(false, "Dft gate type not known."); + STORM_LOG_ASSERT(false, "DFT gate type not known."); return false; } } inline std::string toString(DFTElementType const& tp) { - switch(tp) { - case DFTElementType::BE: - return "BE"; - case DFTElementType::OR: - return "OR"; + switch (tp) { + case DFTElementType::BE_EXP: + return "BE_EXP"; + case DFTElementType::BE_CONST: + return "BE_CONST"; case DFTElementType::AND: return "AND"; + case DFTElementType::OR: + return "OR"; case DFTElementType::VOT: return "VOT"; - case DFTElementType::POR: - return "POR"; case DFTElementType::PAND: return "PAND"; + case DFTElementType::POR: + return "POR"; case DFTElementType::SPARE: return "SPARE"; + case DFTElementType::PDEP: + return "PDEP"; case DFTElementType::SEQ: return "SEQ"; case DFTElementType::MUTEX: return "MUTEX"; - case DFTElementType::PDEP: - return "PDEP"; default: - STORM_LOG_ASSERT(false, "Dft type not known."); + STORM_LOG_ASSERT(false, "DFT type not known."); return ""; } } - inline std::ostream& operator<<(std::ostream& os, DFTElementType const& tp) { - return os << toString(tp); + inline std::ostream& operator<<(std::ostream& os, DFTElementType const& type) { + return os << toString(type); } - - } } diff --git a/src/storm-dft/storage/dft/DFTElements.h b/src/storm-dft/storage/dft/DFTElements.h index 8cbfec680..42aaa4b18 100644 --- a/src/storm-dft/storage/dft/DFTElements.h +++ b/src/storm-dft/storage/dft/DFTElements.h @@ -2,8 +2,9 @@ #include "storm-dft/storage/dft/elements/DFTAnd.h" #include "storm-dft/storage/dft/elements/DFTBE.h" -#include "storm-dft/storage/dft/elements/DFTConst.h" +#include "storm-dft/storage/dft/elements/BEConst.h" #include "storm-dft/storage/dft/elements/DFTDependency.h" +#include "storm-dft/storage/dft/elements/BEExponential.h" #include "storm-dft/storage/dft/elements/DFTOr.h" #include "storm-dft/storage/dft/elements/DFTPand.h" #include "storm-dft/storage/dft/elements/DFTPor.h" diff --git a/src/storm-dft/storage/dft/DFTIsomorphism.h b/src/storm-dft/storage/dft/DFTIsomorphism.h index f8fd27d8f..ab823b00a 100644 --- a/src/storm-dft/storage/dft/DFTIsomorphism.h +++ b/src/storm-dft/storage/dft/DFTIsomorphism.h @@ -54,17 +54,39 @@ namespace storage { template struct BEColourClass { + BEColourClass() = default; - BEColourClass(ValueType a, ValueType p, size_t h) : aRate(a), pRate(p), hash(h) {} + 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::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); + } + + storm::storage::DFTElementType type; + size_t hash; ValueType aRate; ValueType pRate; - size_t hash; + bool failed; }; + template bool operator==(BEColourClass const& lhs, BEColourClass const& rhs) { - return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; + if (lhs.type != rhs.type) { + return false; + } + switch (lhs.type) { + case storm::storage::DFTElementType::BE_EXP: + return lhs.hash == rhs.hash && lhs.aRate == rhs.aRate && lhs.pRate == rhs.pRate; + case storm::storage::DFTElementType::BE_CONST: + 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."); + break; + } } /** @@ -249,7 +271,23 @@ namespace storage { protected: void colourize(std::shared_ptr> const& be) { - beColour[be->id()] = BEColourClass(be->activeFailureRate(), be->passiveFailureRate(), be->nrParents()); + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + auto beExp = std::static_pointer_cast const>(be); + beColour[beExp->id()] = BEColourClass(beExp->type(), beExp->activeFailureRate(), beExp->passiveFailureRate(), beExp->nrParents()); + break; + } + case storm::storage::DFTElementType::BE_CONST: + { + auto beConst = std::static_pointer_cast const>(be); + beColour[beConst->id()] = BEColourClass(beConst->type(), beConst->failed(), beConst->nrParents()); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + break; + } } void colourize(std::shared_ptr> const& gate) { @@ -260,7 +298,24 @@ namespace storage { void colourize(std::shared_ptr> const& dep) { // TODO this can be improved for n-ary dependencies. - depColour[dep->id()] = std::pair(dep->probability(), dep->dependentEvents()[0]->activeFailureRate()); + std::shared_ptr const> be = dep->dependentEvents()[0]; + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + auto beExp = std::static_pointer_cast const>(be); + depColour[dep->id()] = std::pair(dep->probability(), beExp->activeFailureRate()); + break; + } + case storm::storage::DFTElementType::BE_CONST: + { + auto beConst = std::static_pointer_cast const>(be); + depColour[dep->id()] = std::pair(dep->probability(), beConst->failed()); + break; + } + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << be->type() << "' is not known."); + break; + } } void colourize(std::shared_ptr> const& restr) { @@ -644,11 +699,27 @@ namespace std { template struct hash> { size_t operator()(storm::storage::BEColourClass const& bcc) const { + constexpr uint_fast64_t fivebitmask = (1 << 6) - 1; + constexpr uint_fast64_t eightbitmask = (1 << 9) - 1; std::hash hasher; - return (hasher(bcc.aRate) ^ hasher(bcc.pRate) << 8) | bcc.hash; + uint_fast64_t groupHash = static_cast(1) << 63; + 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: + return (bcc.failed << 8); + default: + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE of type '" << bcc.type << "' is not known."); + break; + } + groupHash |= static_cast(bcc.hash) & eightbitmask; + return groupHash; } }; + template struct hash> { size_t operator()(std::pair const& p) const { diff --git a/src/storm-dft/storage/dft/DFTState.cpp b/src/storm-dft/storage/dft/DFTState.cpp index 18b0559a0..13d9c5279 100644 --- a/src/storm-dft/storage/dft/DFTState.cpp +++ b/src/storm-dft/storage/dft/DFTState.cpp @@ -42,9 +42,25 @@ namespace storm { // Initialize currently failable BE if (mDft.isBasicElement(index) && isOperational(index)) { std::shared_ptr> be = mDft.getBasicElement(index); - if (be->canFail() && (!be->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)))) { - failableElements.addBE(index); - STORM_LOG_TRACE("Currently failable: " << be->toString()); + if (be->canFail()) { + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + auto beExp = std::static_pointer_cast const>(be); + if (!beExp->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index))) { + failableElements.addBE(index); + STORM_LOG_TRACE("Currently failable: " << *beExp); + } + 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; + } } } else if (mDft.getElement(index)->isSpareGate()) { // Initialize used representants @@ -61,7 +77,7 @@ namespace storm { assert(dependency->dependentEvents().size() == 1); if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) { failableElements.addDependency(dependencyId); - STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); + STORM_LOG_TRACE("New dependency failure: " << *dependency); } } mPseudoState = false; @@ -203,7 +219,7 @@ namespace storm { if (getElementState(dependency->dependentEvents()[0]->id()) == DFTElementState::Operational) { STORM_LOG_ASSERT(!isFailsafe(dependency->dependentEvents()[0]->id()), "Dependent event is failsafe."); failableElements.addDependency(dependency->id()); - STORM_LOG_TRACE("New dependency failure: " << dependency->toString()); + STORM_LOG_TRACE("New dependency failure: " << *dependency); addedFailableDependency = true; } } @@ -226,13 +242,14 @@ 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."); + auto beExp = std::static_pointer_cast const>(mDft.getBasicElement(id)); if (mDft.hasRepresentant(id) && !isActive(mDft.getRepresentant(id))) { // Return passive failure rate - return mDft.getBasicElement(id)->passiveFailureRate(); + return beExp->passiveFailureRate(); } else { // Return active failure rate - return mDft.getBasicElement(id)->activeFailureRate(); + return beExp->activeFailureRate(); } } @@ -244,7 +261,7 @@ namespace storm { std::shared_ptr const> dependency = mDft.getDependency(id); STORM_LOG_ASSERT(dependency->dependentEvents().size() == 1, "More than one dependent event"); std::pair const>,bool> res(mDft.getBasicElement(dependency->dependentEvents()[0]->id()), true); - STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << res.first->toString() << " has already failed."); + STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << *(res.first) << " has already failed."); failableElements.removeDependency(id); setFailed(res.first->id()); setDependencySuccessful(dependency->id()); @@ -253,7 +270,7 @@ namespace storm { } else { // Consider "normal" failure std::pair const>,bool> res(mDft.getBasicElement(id), false); - STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << res.first->toString() << " has already failed."); + STORM_LOG_ASSERT(!hasFailed(res.first->id()), "Element " << *(res.first) << " has already failed."); STORM_LOG_ASSERT(res.first->canFail(), "Element " << *(res.first) << " cannot fail."); failableElements.removeBE(id); setFailed(res.first->id()); @@ -277,7 +294,7 @@ namespace storm { template bool DFTState::isActive(size_t id) const { - STORM_LOG_ASSERT(mDft.isRepresentative(id), "Element " << mDft.getElement(id)->toString() << " is no representative."); + STORM_LOG_ASSERT(mDft.isRepresentative(id), "Element " << *(mDft.getElement(id)) << " is no representative."); return mStatus[mStateGenerationInfo.getSpareActivationIndex(id)]; } @@ -289,9 +306,22 @@ namespace storm { for(size_t elem : mDft.module(representativeId)) { if(mDft.isBasicElement(elem) && isOperational(elem)) { std::shared_ptr> be = mDft.getBasicElement(elem); - if (be->isColdBasicElement() && be->canFail()) { - // Add to failable BEs - failableElements.addBE(elem); + if (be->canFail()) { + switch (be->type()) { + case storm::storage::DFTElementType::BE_EXP: { + auto beExp = std::static_pointer_cast const>(be); + if (beExp->isColdBasicElement()) { + // Add to failable BEs + failableElements.addBE(elem); + } + 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."); + } } } else if (mDft.getElement(elem)->isSpareGate() && !isActive(uses(elem))) { propagateActivation(uses(elem)); diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp index 6dd3d2299..2eb811095 100644 --- a/src/storm-dft/storage/dft/DftJsonExporter.cpp +++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp @@ -5,6 +5,7 @@ #include #include +#include namespace storm { namespace storage { @@ -84,14 +85,33 @@ namespace storm { nodeData["type"] = "fdep"; } } else if (element->isBasicElement()) { - // Set BE specific data std::shared_ptr const> be = std::static_pointer_cast const>(element); - std::stringstream stream; - stream << be->activeFailureRate(); - nodeData["rate"] = stream.str(); - stream.str(std::string()); // Clear stringstream - stream << be->dormancyFactor(); - nodeData["dorm"] = stream.str(); + // Set BE specific data + switch (element->type()) { + case storm::storage::DFTElementType::BE_EXP: + { + auto beExp = std::static_pointer_cast const>(be); + std::stringstream stream; + nodeData["distribution"] = "exp"; + stream << beExp->activeFailureRate(); + nodeData["rate"] = stream.str(); + stream.str(std::string()); // Clear stringstream + stream << beExp->dormancyFactor(); + 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."); + break; + } } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Element of type '" << element->type() << "' is not supported."); } diff --git a/src/storm-dft/storage/dft/elements/BEConst.h b/src/storm-dft/storage/dft/elements/BEConst.h new file mode 100644 index 000000000..22cb13b9a --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BEConst.h @@ -0,0 +1,61 @@ +#pragma once + +#include "DFTBE.h" + +namespace storm { + namespace storage { + + /*! + * BE which is either constant failed or constant failsafe. + */ + template + class BEConst : public DFTBE { + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param failed True iff the const BE is failed, otherwise it is failsafe. + */ + BEConst(size_t id, std::string const& name, bool failed) : DFTBE(id, name), mFailed(failed) { + // Intentionally empty + } + + DFTElementType type() const override { + return DFTElementType::BE_CONST; + } + + /*! + * Return whether the BE has failed. + * @return True iff the BE is const failed. + */ + bool failed() const { + return mFailed; + } + + bool canFail() const override { + return this->failed(); + } + + bool isTypeEqualTo(DFTElement const& other) const override { + if (!DFTElement::isTypeEqualTo(other)) { + return false; + } + auto& otherBE = static_cast const&>(other); + return this->failed() == otherBE.failed(); + } + + std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} BE(const " << (this->failed() ? "failed" : "failsafe") << ")"; + return stream.str(); + } + + private: + bool mFailed; + + }; + + } +} diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h new file mode 100644 index 000000000..3275aac15 --- /dev/null +++ b/src/storm-dft/storage/dft/elements/BEExponential.h @@ -0,0 +1,103 @@ +#pragma once + +#include "DFTBE.h" + +namespace storm { + namespace storage { + + /*! + * BE with exponential failure rate. + */ + template + class BEExponential : public DFTBE { + + public: + /*! + * Constructor. + * @param id Id. + * @param name Name. + * @param failureRate Active failure rate. + * @param dormancyFactor Dormancy factor. + * @param transient True iff the BE experiences transient failures. + */ + BEExponential(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : + DFTBE(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) { + STORM_LOG_ASSERT(!storm::utility::isZero(failureRate), "Exponential failure rate should not be zero."); + } + + DFTElementType type() const override { + return DFTElementType::BE_EXP; + } + + /*! + * Return failure rate in active state. + * @return Active failure rate. + */ + ValueType const& activeFailureRate() const { + return mActiveFailureRate; + } + + /*! + * Return failure rate in passive state. + * @return Passive failure rate. + */ + ValueType const& passiveFailureRate() const { + return mPassiveFailureRate; + } + + /*! + * Return dormancy factor given by passive_failure_rate/active_failure_rate. + * @return Dormancy factor. + */ + ValueType dormancyFactor() const { + if (storm::utility::isZero(this->activeFailureRate())) { + // Return default value of 1 + return storm::utility::one(); + } else { + return this->passiveFailureRate() / this->activeFailureRate(); + } + } + + /*! + * Return whether the BE experiences transient failures. + * @return True iff BE is transient. + */ + bool isTransient() const { + return mTransient; + } + + bool canFail() const override { + return !storm::utility::isZero(this->activeFailureRate()); + } + + /*! + * Return whether the BE is a cold BE, i.e., passive failure rate = 0. + * @return True iff BE is cold BE. + */ + bool isColdBasicElement() const { + return storm::utility::isZero(this->passiveFailureRate()); + } + + bool isTypeEqualTo(DFTElement const& other) const override { + if (!DFTElement::isTypeEqualTo(other)) { + return false; + } + auto& otherBE = static_cast const&>(other); + return (this->activeFailureRate() == otherBE.activeFailureRate()) && (this->passiveFailureRate() == otherBE.passiveFailureRate()); + } + + std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} BE exp(" << this->activeFailureRate() << ", " << this->passiveFailureRate() << ")"; + return stream.str(); + } + + private: + ValueType mActiveFailureRate; + ValueType mPassiveFailureRate; + bool mTransient; + + }; + + } +} diff --git a/src/storm-dft/storage/dft/elements/DFTAnd.h b/src/storm-dft/storage/dft/elements/DFTAnd.h index 00f671837..c57e54c3b 100644 --- a/src/storm-dft/storage/dft/elements/DFTAnd.h +++ b/src/storm-dft/storage/dft/elements/DFTAnd.h @@ -39,12 +39,6 @@ namespace storm { return "AND"; } }; - - template - inline std::ostream& operator<<(std::ostream& os, DFTAnd const& gate) { - return os << gate.toString(); - } - } } diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 84f05b5b1..912c4b42b 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -1,131 +1,98 @@ #pragma once + +#include "DFTElement.h" + namespace storm { namespace storage { + + /*! + * Abstract base class for basic elements (BEs) in DFTs. + */ template class DFTBE : public DFTElement { - - using DFTDependencyPointer = std::shared_ptr>; - using DFTDependencyVector = std::vector; - - protected: - ValueType mActiveFailureRate; - ValueType mPassiveFailureRate; - DFTDependencyVector mIngoingDependencies; - bool mTransient; public: - DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : - DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) - {} - - DFTElementType type() const override { - return DFTElementType::BE; + /*! + * Constructor. + * @param id Id. + * @param name Name. + */ + DFTBE(size_t id, std::string const& name) : DFTElement(id, name) { + // Intentionally empty } - virtual size_t nrChildren() const override { + size_t nrChildren() const override { return 0; } - ValueType const& activeFailureRate() const { - return mActiveFailureRate; - } - - ValueType const& passiveFailureRate() const { - return mPassiveFailureRate; - } - - ValueType dormancyFactor() const { - if (storm::utility::isZero(this->activeFailureRate())) { - // Return default value of 0 - return storm::utility::zero(); - } else { - return this->passiveFailureRate() / this->activeFailureRate(); - } - } + /*! + * Return whether the BE can fail. + * @return True iff BE is not failsafe. + */ + virtual bool canFail() const = 0; - bool isTransient() const { - return mTransient; - } - - bool canFail() const { - return !storm::utility::isZero(mActiveFailureRate); - } - - bool addIngoingDependency(DFTDependencyPointer const& e) { - // TODO write this assertion for n-ary dependencies, probably by addign a method to the dependencies to support this. + /*! + * Add dependency which can trigger this BE. + * @param dependency Ingoing dependency. + */ + void addIngoingDependency(std::shared_ptr> const& dependency) { + // TODO write this assertion for n-ary dependencies, probably by adding a method to the dependencies to support this. //STORM_LOG_ASSERT(e->dependentEvent()->id() == this->id(), "Ids do not match."); - if(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), e) != mIngoingDependencies.end()) { - return false; - } - else - { - mIngoingDependencies.push_back(e); - return true; - } + STORM_LOG_ASSERT(std::find(mIngoingDependencies.begin(), mIngoingDependencies.end(), dependency) == mIngoingDependencies.end(), + "Ingoing Dependency " << dependency << " already present."); + mIngoingDependencies.push_back(dependency); } - + + /*! + * Return whether the BE has ingoing dependencies. + * @return True iff BE can be triggered by dependencies. + */ bool hasIngoingDependencies() const { return !mIngoingDependencies.empty(); } - - size_t nrIngoingDependencies() const { - return mIngoingDependencies.size(); - } - - DFTDependencyVector const& ingoingDependencies() const { + + /*! + * Return ingoing dependencies. + * @return List of dependencies which can trigger this BE. + */ + std::vector>> const& ingoingDependencies() const { return mIngoingDependencies; } - - std::string toString() const override { - std::stringstream stream; - stream << *this; - return stream.str(); - } - + bool isBasicElement() const override { return true; } - - bool isColdBasicElement() const { - return storm::utility::isZero(mPassiveFailureRate); - } - - virtual void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { - if(elemsInSubtree.count(this->id())) { + + void extendSubDft(std::set& elemsInSubtree, std::vector const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override { + if (elemsInSubtree.count(this->id())) { return; } DFTElement::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { + if (elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } - for(auto const& incDep : mIngoingDependencies) { + for (auto const& incDep : ingoingDependencies()) { incDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves); - if(elemsInSubtree.empty()) { + if (elemsInSubtree.empty()) { // Parent in the subdft, ie it is *not* a subdft return; } } } - - bool isTypeEqualTo(DFTElement const& other) const override { - if(!DFTElement::isTypeEqualTo(other)) return false; - DFTBE const& otherBE = static_cast const&>(other); - return (mActiveFailureRate == otherBE.mActiveFailureRate) && (mPassiveFailureRate == otherBE.mPassiveFailureRate); - } - - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { - if(DFTElement::checkDontCareAnymore(state, queues)) { - state.beNoLongerFailable(this->mId); + + bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues & queues) const override { + if (DFTElement::checkDontCareAnymore(state, queues)) { + state.beNoLongerFailable(this->id()); return true; } return false; } + + private: + std::vector>> mIngoingDependencies; + }; - template - inline std::ostream& operator<<(std::ostream& os, DFTBE const& be) { - return os << "{" << be.name() << "} BE(" << be.activeFailureRate() << ", " << be.passiveFailureRate() << ")"; - } } } diff --git a/src/storm-dft/storage/dft/elements/DFTConst.h b/src/storm-dft/storage/dft/elements/DFTConst.h deleted file mode 100644 index 6ff4cd39e..000000000 --- a/src/storm-dft/storage/dft/elements/DFTConst.h +++ /dev/null @@ -1,58 +0,0 @@ -#pragma once - - -#include "DFTElement.h" -namespace storm { - namespace storage { - template - class DFTConst : public DFTElement { - - bool mFailed; - - public: - DFTConst(size_t id, std::string const& name, bool failed) : - DFTElement(id, name), mFailed(failed) - {} - - DFTElementType type() const override { - if(mFailed) { - return DFTElementType::CONSTF; - } else { - return DFTElementType::CONSTS; - } - } - - - bool failed() const { - return mFailed; - } - - virtual bool isConstant() const override { - return true; - } - - virtual size_t nrChildren() const override { - return 0; - } - - std::string toString() const override { - std::stringstream stream; - stream << *this; - return stream.str(); - } - - bool isTypeEqualTo(DFTElement const& other) const override { - if(!DFTElement::isTypeEqualTo(other)) return false; - DFTConst const& otherCNST = static_cast const&>(other); - return (mFailed == otherCNST.mFailed); - } - - }; - - template - inline std::ostream& operator<<(std::ostream& os, DFTConst const& be) { - return os << "{" << be.name() << "} BE(const " << (be.failed() ? "failed" : "failsafe") << ")"; - } - - } -} diff --git a/src/storm-dft/storage/dft/elements/DFTDependency.h b/src/storm-dft/storage/dft/elements/DFTDependency.h index c1d877cb3..b398518ad 100644 --- a/src/storm-dft/storage/dft/elements/DFTDependency.h +++ b/src/storm-dft/storage/dft/elements/DFTDependency.h @@ -102,14 +102,14 @@ namespace storm { virtual std::string toString() const override { std::stringstream stream; - bool fdep = storm::utility::isOne(mProbability); - stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => { "; - for(auto const& depEv : mDependentEvents) { + bool isFDEP = storm::utility::isOne(this->probability()); + stream << "{" << this->name() << "} " << (isFDEP ? "FDEP" : "PDEP") << "(" << this->triggerEvent()->name() << " => { "; + for(auto const& depEv : this->dependentEvents()) { stream << depEv->name() << " "; } stream << "}"; - if (!fdep) { - stream << " with probability " << mProbability; + if (!isFDEP) { + stream << " with probability " << this->probability(); } return stream.str(); } diff --git a/src/storm-dft/storage/dft/elements/DFTElement.h b/src/storm-dft/storage/dft/elements/DFTElement.h index d5d82db5a..2c43bdab8 100644 --- a/src/storm-dft/storage/dft/elements/DFTElement.h +++ b/src/storm-dft/storage/dft/elements/DFTElement.h @@ -9,11 +9,9 @@ #include #include - - -#include "../DFTElementType.h" -#include "../DFTState.h" -#include "../DFTStateSpaceGenerationQueues.h" +#include "storm-dft/storage/dft/DFTElementType.h" +#include "storm-dft/storage/dft/DFTState.h" +#include "storm-dft/storage/dft/DFTStateSpaceGenerationQueues.h" #include "storm/utility/constants.h" #include "storm/adapters/RationalFunctionAdapter.h" @@ -24,6 +22,8 @@ namespace storm { namespace storage { using std::size_t; + + // Forward declarations template class DFTGate; @@ -54,41 +54,84 @@ namespace storm { public: - DFTElement(size_t id, std::string const& name) : - mId(id), mName(name) - {} + /*! + * Constructor. + * @param id Id. + * @param name Name. + */ + DFTElement(size_t id, std::string const& name) : mId(id), mName(name) { + } - virtual ~DFTElement() {} + /*! + * Destructor. + */ + virtual ~DFTElement() { + } - /** - * Returns the id + /*! + * Get id. + * @return Id. */ virtual size_t id() const { return mId; } - virtual DFTElementType type() const = 0; + /*! + * Set id. + * @param id Id. + */ + virtual void setId(size_t id) { + this->mId = id; + } - virtual void setRank(size_t rank) { - mRank = rank; + /*! + * Get name. + * @return Name. + */ + virtual std::string const& name() const { + return mName; } - + + + /*! + * Get type. + * @return Type. + */ + virtual DFTElementType type() const = 0; + + /*! + * Get rank. + * @return Rank. + */ virtual size_t rank() const { return mRank; } - + + /*! + * Set rank. + * @param rank Rank. + */ + virtual void setRank(size_t rank) { + this->mRank = rank; + } + virtual bool isConstant() const { return false; } - - virtual bool isGate() const { + + /*! + * Checks whether the element is a basic element. + * @return True iff element is a BE. + */ + virtual bool isBasicElement() const { return false; } - /** - * Returns true if the element is a BE + /*! + * Check wether the element is a gate. + * @return True iff element is a gate. */ - virtual bool isBasicElement() const { + virtual bool isGate() const { return false; } @@ -107,17 +150,7 @@ namespace storm { return false; } - virtual void setId(size_t newId) { - mId = newId; - } - /** - * Returns the name - */ - virtual std::string const& name() const { - return mName; - } - bool addParent(DFTGatePointer const& e) { if(std::find(mParents.begin(), mParents.end(), e) != mParents.end()) { return false; @@ -260,8 +293,6 @@ namespace storm { virtual std::size_t nrChildren() const = 0; - virtual std::string toString() const = 0; - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const; /** @@ -292,14 +323,23 @@ namespace storm { return type() == other.type(); } + /*! + * Print information about element to string. + * @return Element information. + */ + virtual std::string toString() const = 0; + protected: // virtual bool checkIsomorphicSubDftHelper(DFTElement const& otherElem, std::vector>& mapping, std::vector const& order ) const = 0; }; - - - + + + template + inline std::ostream& operator<<(std::ostream& os, DFTElement const& element) { + return os << element.toString(); + } template bool equalType(DFTElement const& e1, DFTElement const& e2) { diff --git a/src/storm-dft/storage/dft/elements/DFTOr.h b/src/storm-dft/storage/dft/elements/DFTOr.h index d614b095a..f45bb4b5b 100644 --- a/src/storm-dft/storage/dft/elements/DFTOr.h +++ b/src/storm-dft/storage/dft/elements/DFTOr.h @@ -36,10 +36,6 @@ namespace storm { } }; - template - inline std::ostream& operator<<(std::ostream& os, DFTOr const& gate) { - return os << gate.toString(); - } } } diff --git a/src/storm-dft/storage/dft/elements/DFTPand.h b/src/storm-dft/storage/dft/elements/DFTPand.h index 21cda29a9..7b03b7196 100644 --- a/src/storm-dft/storage/dft/elements/DFTPand.h +++ b/src/storm-dft/storage/dft/elements/DFTPand.h @@ -55,11 +55,6 @@ namespace storm { protected: bool inclusive; }; - - template - inline std::ostream& operator<<(std::ostream& os, DFTPand const& gate) { - return os << gate.toString(); - } } } diff --git a/src/storm-dft/storage/dft/elements/DFTPor.h b/src/storm-dft/storage/dft/elements/DFTPor.h index 857e19714..1e92384cd 100644 --- a/src/storm-dft/storage/dft/elements/DFTPor.h +++ b/src/storm-dft/storage/dft/elements/DFTPor.h @@ -52,10 +52,5 @@ namespace storm { bool inclusive; }; - template - inline std::ostream& operator<<(std::ostream& os, DFTPor const& gate) { - return os << gate.toString(); - } - } } diff --git a/src/storm-dft/storage/dft/elements/DFTRestriction.h b/src/storm-dft/storage/dft/elements/DFTRestriction.h index d4efde050..10392e05c 100644 --- a/src/storm-dft/storage/dft/elements/DFTRestriction.h +++ b/src/storm-dft/storage/dft/elements/DFTRestriction.h @@ -106,21 +106,6 @@ namespace storm { } } - - virtual std::string toString() const override { - std::stringstream stream; - stream << "{" << this->name() << "} " << typestring() << "( "; - typename DFTElementVector::const_iterator it = mChildren.begin(); - stream << (*it)->name(); - ++it; - while(it != mChildren.end()) { - stream << ", " << (*it)->name(); - ++it; - } - stream << ")"; - return stream.str(); - } - virtual bool checkDontCareAnymore(storm::storage::DFTState& state, DFTStateSpaceGenerationQueues& queues) const override { return false; } @@ -155,11 +140,24 @@ namespace storm { return false; } - + virtual std::string toString() const override { + std::stringstream stream; + stream << "{" << this->name() << "} " << this->typestring() << "( "; + auto it = this->children().begin(); + stream << (*it)->name(); + ++it; + while(it != this->children().end()) { + stream << ", " << (*it)->name(); + ++it; + } + stream << ")"; + return stream.str(); + } }; + template class DFTSeq : public DFTRestriction { diff --git a/src/storm-dft/storage/dft/elements/DFTSpare.h b/src/storm-dft/storage/dft/elements/DFTSpare.h index 8593c6fd1..7584a1f94 100644 --- a/src/storm-dft/storage/dft/elements/DFTSpare.h +++ b/src/storm-dft/storage/dft/elements/DFTSpare.h @@ -105,5 +105,6 @@ namespace storm { }; + } } diff --git a/src/storm-dft/storage/dft/elements/DFTVot.h b/src/storm-dft/storage/dft/elements/DFTVot.h index 0b03954ca..791926a97 100644 --- a/src/storm-dft/storage/dft/elements/DFTVot.h +++ b/src/storm-dft/storage/dft/elements/DFTVot.h @@ -71,10 +71,5 @@ namespace storm { } }; - template - inline std::ostream& operator<<(std::ostream& os, DFTVot const& gate) { - return os << gate.toString(); - } - } } diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 144981117..60a4d04e5 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -122,14 +122,11 @@ namespace storm { // Check which type the element is and call the corresponding translate-function. switch (dftElement->type()) { - case storm::storage::DFTElementType::BE: - translateBE(std::static_pointer_cast const>(dftElement)); + case storm::storage::DFTElementType::BE_EXP: + translateBEExponential(std::static_pointer_cast const>(dftElement)); break; - case storm::storage::DFTElementType::CONSTF: - translateCONSTF(dftElement); - break; - case storm::storage::DFTElementType::CONSTS: - translateCONSTS(dftElement); + case storm::storage::DFTElementType::BE_CONST: + translateBEConst(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::AND: translateAND(std::static_pointer_cast const>(dftElement)); @@ -163,7 +160,7 @@ namespace storm { translateSeq(std::static_pointer_cast const>(dftElement)); break; default: - STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown."); + STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "DFT type '" << dftElement->type() << "' not known."); break; } } @@ -171,8 +168,7 @@ namespace storm { } template - void DftToGspnTransformator::translateBE( - std::shared_ptr const> dftBE) { + void DftToGspnTransformator::translateBEExponential(std::shared_ptr const> dftBE) { double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; @@ -260,35 +256,30 @@ namespace storm { } template - void DftToGspnTransformator::translateCONSTF( - std::shared_ptr const> dftConstF) { - double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x; - double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y; - - addFailedPlace(dftConstF, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0), true); - - if (!smart || mDft.isRepresentative(dftConstF->id())) { - addUnavailablePlace(dftConstF, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0), false); - } - } - - template - void DftToGspnTransformator::translateCONSTS( - std::shared_ptr const> dftConstS) { - double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x; - double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y; + void DftToGspnTransformator::translateBEConst(std::shared_ptr const> dftConst) { + double xcenter = mDft.getElementLayoutInfo(dftConst->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftConst->id()).y; - size_t capacity = 0; // It cannot contain a token, because it cannot fail. + if (dftConst->failed()) { + // Constant failed BE + addFailedPlace(dftConst, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0), true); - uint64_t failedPlace = builder.addPlace(capacity, 0, dftConstS->name() + STR_FAILED); - assert(failedPlaces.size() == dftConstS->id()); - failedPlaces.push_back(failedPlace); - builder.setPlaceLayoutInfo(failedPlace, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); + if (!smart || mDft.isRepresentative(dftConst->id())) { + addUnavailablePlace(dftConst, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0), false); + } + } else { + // Constant failsafe BE + size_t capacity = 0; // It cannot contain a token, because it cannot fail. + uint64_t failedPlace = builder.addPlace(capacity, 0, dftConst->name() + STR_FAILED); + assert(failedPlaces.size() == dftConst->id()); + failedPlaces.push_back(failedPlace); + builder.setPlaceLayoutInfo(failedPlace, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); - if (!smart || mDft.isRepresentative(dftConstS->id())) { - uint64_t unavailablePlace = builder.addPlace(capacity, 0, dftConstS->name() + "_unavail"); - unavailablePlaces.emplace(dftConstS->id(), unavailablePlace); - builder.setPlaceLayoutInfo(unavailablePlace, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); + if (!smart || mDft.isRepresentative(dftConst->id())) { + uint64_t unavailablePlace = builder.addPlace(capacity, 0, dftConst->name() + "_unavail"); + unavailablePlaces.emplace(dftConst->id(), unavailablePlace); + builder.setPlaceLayoutInfo(unavailablePlace, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); + } } } diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 0e60866fc..72b6d1831 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -62,25 +62,18 @@ namespace storm { void translateGSPNElements(); /*! - * Translate a GSPN Basic Event. + * Translate an exponential BE. * - * @param dftBE The Basic Event. + * @param dftBE The exponential Basic Event. */ - void translateBE(std::shared_ptr const> dftBE); + void translateBEExponential(std::shared_ptr const> dftBE); /*! - * Translate a GSPN CONSTF (Constant Failure, a Basic Event that has already failed). + * Translate a constant BE * - * @param dftPor The CONSTF Basic Event. + * @param dftConst The constant Basic Event. */ - void translateCONSTF(std::shared_ptr const> dftConstF); - - /*! - * Translate a GSPN CONSTS (Constant Save, a Basic Event that cannot fail). - * - * @param dftPor The CONSTS Basic Event. - */ - void translateCONSTS(std::shared_ptr const> dftConstS); + void translateBEConst(std::shared_ptr const> dftConst); /*! * Translate a GSPN AND.