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<storm::storage::DFTSpare<ValueType>>(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<ValueType>::copyElement(DFTElementPointer element) {
std::vector<std::string> children;
switch (element->type()) {
+ case storm::storage::DFTElementType::BE:
+ copyBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(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<storm::storage::DFTGate<ValueType>>(element), children);
break;
}
- case storm::storage::DFTElementType::BE_EXP:
- {
- auto beExp = std::static_pointer_cast<storm::storage::BEExponential<ValueType>>(element);
- addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient());
- break;
- }
- case storm::storage::DFTElementType::BE_CONST:
- {
- auto beConst = std::static_pointer_cast<storm::storage::BEConst<ValueType>>(element);
- addBasicElementConst(beConst->name(), beConst->failed());
- break;
- }
case storm::storage::DFTElementType::PDEP:
{
DFTDependencyPointer dependency = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(element);
@@ -304,6 +294,27 @@ namespace storm {
}
}
+ template<typename ValueType>
+ void DFTBuilder<ValueType>::copyBE(DFTBEPointer be) {
+ switch (be->beType()) {
+ case storm::storage::BEType::CONSTANT:
+ {
+ auto beConst = std::static_pointer_cast<storm::storage::BEConst<ValueType>>(be);
+ addBasicElementConst(beConst->name(), beConst->failed());
+ break;
+ }
+ case storm::storage::BEType::EXPONENTIAL:
+ {
+ auto beExp = std::static_pointer_cast<storm::storage::BEExponential<ValueType>>(be);
+ addBasicElementExponential(beExp->name(), beExp->activeFailureRate(), beExp->dormancyFactor(), beExp->isTransient());
+ break;
+ }
+ default:
+ STORM_LOG_ASSERT(false, "BE type not known.");
+ break;
+ }
+ }
+
template<typename ValueType>
void DFTBuilder<ValueType>::copyGate(DFTGatePointer gate, std::vector<std::string> 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<storm::storage::DFTElement<ValueType>>;
using DFTElementVector = std::vector<DFTElementPointer>;
+ using DFTBEPointer = std::shared_ptr<storm::storage::DFTBE<ValueType>>;
using DFTGatePointer = std::shared_ptr<storm::storage::DFTGate<ValueType>>;
using DFTGateVector = std::vector<DFTGatePointer>;
using DFTDependencyPointer = std::shared_ptr<storm::storage::DFTDependency<ValueType>>;
@@ -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<storm::storage::DFTBE<ValueType> 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<storm::storage::BEConst<ValueType> 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<storm::storage::BEExponential<ValueType> 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<storm::storage::BEExponential<ValueType> 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<storm::storage::BEConst<double> 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<storm::storage::DFTBE<double> 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<storm::storage::BEConst<double> 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<std::shared_ptr<SmtConstraint>> triggerConstraints;
for (size_t i = 0; i < dft.nrElements(); ++i) {
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
- if (element->type() == storm::storage::DFTElementType::BE_CONST) {
+ if (element->isBasicElement()) {
auto be = std::static_pointer_cast<storm::storage::DFTBE<double> const>(element);
- triggerConstraints.clear();
- for (auto const &dependency : be->ingoingDependencies()) {
- triggerConstraints.push_back(std::make_shared<IsConstantValue>(
- timePointVariables.at(dependency->triggerEvent()->id()), notFailed));
- }
- if (!triggerConstraints.empty()) {
- constraints.push_back(std::make_shared<Implies>(
- std::make_shared<IsConstantValue>(timePointVariables.at(be->id()), notFailed),
- std::make_shared<And>(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<IsConstantValue>(timePointVariables.at(dependency->triggerEvent()->id()), notFailed));
+ }
+ if (!triggerConstraints.empty()) {
+ constraints.push_back(std::make_shared<Implies>(std::make_shared<IsConstantValue>(timePointVariables.at(be->id()), notFailed), std::make_shared<And>(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<storm::storage::DFTBE<ValueType>>(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<DFTBE<ValueType>> be = std::static_pointer_cast<DFTBE<ValueType>>(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<BEExponential<ValueType>>(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 DFTBE<ValueType>> 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<BEExponential<ValueType> const>(be);
- beColour[beExp->id()] = BEColourClass<ValueType>(beExp->type(), beExp->activeFailureRate(), beExp->passiveFailureRate(), beExp->nrParents());
+ auto beConst = std::static_pointer_cast<BEConst<ValueType> const>(be);
+ beColour[beConst->id()] = BEColourClass<ValueType>(beConst->beType(), beConst->failed(), beConst->nrParents());
break;
}
- case storm::storage::DFTElementType::BE_CONST:
+ case storm::storage::BEType::EXPONENTIAL:
{
- auto beConst = std::static_pointer_cast<BEConst<ValueType> const>(be);
- beColour[beConst->id()] = BEColourClass<ValueType>(beConst->type(), beConst->failed(), beConst->nrParents());
+ auto beExp = std::static_pointer_cast<BEExponential<ValueType> const>(be);
+ beColour[beExp->id()] = BEColourClass<ValueType>(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 DFTDependency<ValueType>> const& dep) {
// TODO this can be improved for n-ary dependencies.
std::shared_ptr<DFTBE<ValueType> 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<BEExponential<ValueType> const>(be);
- depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), beExp->activeFailureRate());
+ auto beConst = std::static_pointer_cast<BEConst<ValueType> const>(be);
+ depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), beConst->failed() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>());
break;
}
- case storm::storage::DFTElementType::BE_CONST:
+ case storm::storage::BEType::EXPONENTIAL:
{
- auto beConst = std::static_pointer_cast<BEConst<ValueType> const>(be);
- depColour[dep->id()] = std::pair<ValueType, ValueType>(dep->probability(), beConst->failed() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>());
+ auto beExp = std::static_pointer_cast<BEExponential<ValueType> const>(be);
+ depColour[dep->id()] = std::pair<ValueType, ValueType>(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<uint_fast64_t>(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<const DFTBE<ValueType>> 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<BEExponential<ValueType> 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<typename ValueType>
ValueType DFTState<ValueType>::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<storm::storage::BEExponential<ValueType> 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<const DFTBE<ValueType>> 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<BEExponential<ValueType> 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<DFTBE<ValueType> const> be = std::static_pointer_cast<DFTBE<ValueType> 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<BEConst<ValueType> const>(be);
+ std::stringstream stream;
+ nodeData["distribution"] = "const";
+ nodeData["failed"] = beConst->failed();
+ break;
+ }
+ case storm::storage::BEType::EXPONENTIAL:
{
auto beExp = std::static_pointer_cast<BEExponential<ValueType> 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<BEConst<ValueType> 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<ValueType>(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<storm::storage::BEExponential<ValueType> const>(dftElement));
- break;
- case storm::storage::DFTElementType::BE_CONST:
- translateBEConst(std::static_pointer_cast<storm::storage::BEConst<ValueType> const>(dftElement));
+ case storm::storage::DFTElementType::BE:
+ translateBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::AND:
translateAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement));
@@ -167,6 +164,21 @@ namespace storm {
}
+ template<typename ValueType>
+ void DftToGspnTransformator<ValueType>::translateBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
+ switch (dftBE->beType()) {
+ case storm::storage::BEType::CONSTANT:
+ translateBEConst(std::static_pointer_cast<storm::storage::BEConst<ValueType> const>(dftBE));
+ break;
+ case storm::storage::BEType::EXPONENTIAL:
+ translateBEExponential(std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>(dftBE));
+ break;
+ default:
+ STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "BE type '" << dftBE->beType() << "' not known.");
+ break;
+ }
+ }
+
template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateBEExponential(std::shared_ptr<storm::storage::BEExponential<ValueType> 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<storm::storage::DFTBE<ValueType> 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<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
switch (element->type()) {
- case storm::storage::DFTElementType::BE_EXP: {
- auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> 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<storm::storage::BEExponential<ValueType> 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<storm::storage::DFTBE<ValueType> const>(element);
+ switch (be->beType()) {
+ case storm::storage::BEType::CONSTANT: {
+ auto beConst = std::static_pointer_cast<storm::storage::BEConst<ValueType> 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<storm::storage::BEExponential<ValueType> 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<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i);
switch (element->type()) {
- case storm::storage::DFTElementType::BE_EXP: {
- auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> 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<storm::storage::BEExponential<ValueType> 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<storm::storage::DFTBE<ValueType> const>(element);
+ switch (be->beType()) {
+ case storm::storage::BEType::CONSTANT: {
+ auto beConst = std::static_pointer_cast<storm::storage::BEConst<ValueType> const>(element);
+ builder.addBasicElementConst(beConst->name(), beConst->canFail());
+ break;
+ }
+ case storm::storage::BEType::EXPONENTIAL: {
+ auto beExp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> 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<storm::storage::DFTElement<double> 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<storm::storage::DFTBE<double> 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<storm::storage::DFTElement<double> 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<storm::storage::DFTBE<double> 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
+}