Started on support for constant failed/failsafe BEs

src/storm-dft/builder/DFTBuilder.cpp

@@ -273,14 +273,16 @@ namespace storm {
                 case storm::storage::DFTElementType::BE:
                 {
                     std::shared_ptr<storm::storage::DFTBE<ValueType>> be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(element);
-                    addBasicElement(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient());
+                    addBasicElementExponential(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient());
                     break;
                 }
                 case storm::storage::DFTElementType::CONSTF:
                 case storm::storage::DFTElementType::CONSTS:
-                    // TODO
-                    STORM_LOG_ASSERT(false, "Const elements not supported.");
+                {
+                    std::shared_ptr<storm::storage::DFTConst<ValueType>> be = std::static_pointer_cast<storm::storage::DFTConst<ValueType>>(element);
+                    addBasicElementConst(be->name(), be->failed());
                     break;
+                }
                 case storm::storage::DFTElementType::PDEP:
                 {
                     DFTDependencyPointer dependency = std::static_pointer_cast<storm::storage::DFTDependency<ValueType>>(element);

src/storm-dft/builder/DFTBuilder.h

@@ -8,6 +8,8 @@
 #include "storm-dft/storage/dft/DFTElements.h"
 #include "storm-dft/storage/dft/elements/DFTRestriction.h"
 #include "storm-dft/storage/dft/DFTLayoutInfo.h"
+#include "storm/exceptions/NotSupportedException.h"
+
 
 namespace storm {
     namespace storage {
@@ -109,7 +111,7 @@ namespace storm {
                 if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) {
                     // Introduce additional element for first capturing the probabilistic dependency
                     std::string nameAdditional = name + "_additional";
-                    addBasicElement(nameAdditional, storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>(), false);
+                    addBasicElementConst(nameAdditional, false);
                     // First consider probabilistic dependency
                     addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability);
                     // Then consider dependencies to the children if probabilistic dependency failed
@@ -167,15 +169,42 @@ namespace storm {
                 mChildNames[element] = children;
                 return true;
             }
-            
-            bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) {
+
+            bool addBasicElementConst(std::string const& name, bool failed) {
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
+                    return false;
+                }
+                mElements[name] = std::make_shared<storm::storage::DFTConst<ValueType>>(mNextId++, name, failed);
+                return true;
+            }
+
+            bool addBasicElementProbability(std::string const& name, ValueType probability, ValueType dormancyFactor, bool transient = false) {
+                //0 <= dormancyFactor <= 1
+                if (nameInUse(name)) {
+                    STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
+                    return false;
+                }
+                if (storm::utility::isZero<ValueType>(probability)) {
+                    return addBasicElementConst(name, false);
+                } else if (storm::utility::isOne<ValueType>(probability)) {
+                    return addBasicElementConst(name, true);
+                }
+                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant probability distribution is not supported for basic element '" << name << "'.");
+                return false;
+            }
+
+            bool addBasicElementExponential(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) {
                 //TODO Matthias: collect constraints for SMT solving
-                //failureRate > 0
                 //0 <= dormancyFactor <= 1
                 if (nameInUse(name)) {
                     STORM_LOG_ERROR("Element with name '" << name << "' already exists.");
                     return false;
                 }
+                if (storm::utility::isZero<ValueType>(failureRate)) {
+                    return addBasicElementConst(name, false);
+                }
+
                 mElements[name] = std::make_shared<storm::storage::DFTBE<ValueType>>(mNextId++, name, failureRate, dormancyFactor, transient);
                 return true;
             }

src/storm-dft/parser/DFTGalileoParser.cpp

@@ -297,26 +297,29 @@ namespace storm {
 
             switch (distribution) {
                 case Constant:
+                    if (storm::utility::isZero(firstValDistribution) || storm::utility::isOne(firstValDistribution)) {
+                        return builder.addBasicElementProbability(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
+                    }
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant distribution is not supported for basic element '" << name << "' in line " << lineNo << ".");
                     break;
                 case Exponential:
-                    return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
+                    return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
                     break;
                 case Erlang:
                     if (erlangPhases == 1) {
                         // Erlang distribution reduces to exponential distribution
-                        return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
+                        return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
                     } else {
                         // Model Erlang distribution by using SEQ over BEs instead.
                         // For each phase a BE is added, then the SEQ ensures the ordered failure.
                         STORM_LOG_WARN("Erlang distribution for basic element '" << name << "' in line " << lineNo << " is modelled by SEQ gate and BEs.");
                         std::string origName = parseName(name);
                         std::vector<std::string> childNames;
-                        bool success = builder.addBasicElement(origName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
+                        bool success = builder.addBasicElementExponential(origName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
                         for (size_t i = 0; i < erlangPhases - 1; ++i) {
                             std::string beName = origName + "_" + std::to_string(i);
                             childNames.push_back(beName);
-                            success = success && builder.addBasicElement(beName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
+                            success = success && builder.addBasicElementExponential(beName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs
                         }
                         childNames.push_back(origName);
                         return success && builder.addSequenceEnforcer(origName + "_seq", childNames);
@@ -325,7 +328,7 @@ namespace storm {
                 case Weibull:
                     if (storm::utility::isOne<ValueType>(secondValDistribution)) {
                         // Weibull distribution reduces to exponential distribution
-                        return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
+                        return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Weibull distribution is not supported for basic element '" << name << "' in line " << lineNo << ".");
                     }

src/storm-dft/parser/DFTJsonParser.cpp

@@ -93,13 +93,14 @@ 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");
                     }
-                    success = builder.addBasicElement(name, failureRate, dormancyFactor, transient);
+                    success = builder.addBasicElementExponential(name, failureRate, dormancyFactor, transient);
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << "  not recognized.");
                     success = false;

src/storm-dft/storage/dft/elements/DFTConst.h

@@ -27,15 +27,20 @@ namespace storm {
                 return mFailed;
             }
             
-            virtual bool isConstant() const {
+            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<ValueType> const& other) const override {
                 if(!DFTElement<ValueType>::isTypeEqualTo(other)) return false;
                 DFTConst<ValueType> const& otherCNST = static_cast<DFTConst<ValueType> const&>(other);
@@ -43,5 +48,11 @@ namespace storm {
             }
 
         };
+
+        template<typename ValueType>
+        inline std::ostream& operator<<(std::ostream& os, DFTConst<ValueType> const& be) {
+            return os << "{" << be.name() << "} BE(const " << (be.failed() ? "failed" : "failsafe") << ")";
+        }
+
     }
 }