Distinguish between different BEType and use single BE type in DFTElementTypes

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()) {

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.

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;

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())) {

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");
+                        }
                     }
                 }
             }

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:

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.");
                             }

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);
+        }
+
     }
 }

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;

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.");
                         }

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 {

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;
             }
 
             /*!

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;
             }
 
             /*!

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;
             }

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;

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.
                  *

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:

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;
         }
     }
-}
+}

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());
     }
 
-}
+}