Added getUnreliability() for BEs

src/storm-dft/storage/dft/elements/BEConst.cpp

@@ -0,0 +1,16 @@
+#include "BEConst.h"
+
+namespace storm {
+    namespace storage {
+
+        template <typename ValueType>
+        ValueType BEConst<ValueType>::getUnreliability(ValueType time) const {
+            return failed() ? storm::utility::one<ValueType>() : storm::utility::zero<ValueType>();
+        }
+
+        // Explicitly instantiate the class.
+        template class BEConst<double>;
+        template class BEConst<RationalFunction>;
+
+    } // namespace storage
+} // namespace storm

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

@@ -39,6 +39,8 @@ namespace storm {
                 return this->failed();
             }
 
+            ValueType getUnreliability(ValueType time) const override;
+
             bool isTypeEqualTo(DFTElement<ValueType> const& other) const override {
                 if (!DFTElement<ValueType>::isTypeEqualTo(other)) {
                     return false;

src/storm-dft/storage/dft/elements/BEExponential.cpp

@@ -0,0 +1,24 @@
+#include "BEExponential.h"
+
+#include "storm/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace storage {
+
+        template <>
+        double BEExponential<double>::getUnreliability(double time) const {
+            // 1 - e^(-lambda * t)
+            return 1 - exp(-this->activeFailureRate() * time);
+        }
+
+        template <typename ValueType>
+        ValueType BEExponential<ValueType>::getUnreliability(ValueType time) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Computing cumulative failure probability not supported for this data type.");
+        }
+
+        // Explicitly instantiate the class.
+        template class BEExponential<double>;
+        template class BEExponential<RationalFunction>;
+
+    }
+}

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

@@ -50,13 +50,11 @@ namespace storm {
              * @return Dormancy factor.
              */
             ValueType dormancyFactor() const {
-                if (storm::utility::isZero<ValueType>(this->activeFailureRate())) {
-                    // Return default value of 1
-                    return storm::utility::one<ValueType>();
-                } else {
+                STORM_LOG_ASSERT(!storm::utility::isZero<ValueType>(this->activeFailureRate()), "Active failure rate of non-const BE should not be zero.");
                 return this->passiveFailureRate() / this->activeFailureRate();
             }
-            }
+
+            ValueType getUnreliability(ValueType time) const override;
 
             /*!
              * Return whether the BE experiences transient failures.

src/storm-dft/storage/dft/elements/DFTBE.cpp

@@ -0,0 +1,33 @@
+#include "DFTBE.h"
+
+#include "storm-dft/storage/dft/elements/DFTGate.h"
+#include "storm-dft/storage/dft/elements/DFTDependency.h"
+
+namespace storm {
+    namespace storage {
+
+        template <typename ValueType>
+        void DFTBE<ValueType>::extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const {
+            if (elemsInSubtree.count(this->id())) {
+                return;
+            }
+            DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+            if (elemsInSubtree.empty()) {
+                // Parent in the subDFT, i.e., it is *not* a subDFT
+                return;
+            }
+            for (auto const& inDep : ingoingDependencies()) {
+                inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
+                if (elemsInSubtree.empty()) {
+                    // Parent in the subDFT, i.e., it is *not* a subDFT
+                    return;
+                }
+            }
+        }
+
+        // Explicitly instantiate the class.
+        template class DFTBE<double>;
+        template class DFTBE<RationalFunction>;
+
+    }
+}

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

@@ -36,6 +36,15 @@ namespace storm {
                 return 0;
             }
 
+           /*!
+             * Return the unreliability of the BE up to the given time point.
+             * Computes the cumulative distribution function F(x) for time x.
+             * Note that the computation assumes the BE is always active.
+             *
+             * @return Cumulative failure probability.
+             */
+            virtual ValueType getUnreliability(ValueType time) const = 0;
+
             /*!
              * Return whether the BE can fail.
              * @return True iff BE is not failsafe.
@@ -73,23 +82,7 @@ namespace storm {
                 return true;
             }
 
-            void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override {
-                if (elemsInSubtree.count(this->id())) {
-                    return;
-                }
-                DFTElement<ValueType>::extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
-                if (elemsInSubtree.empty()) {
-                    // Parent in the subDFT, i.e., it is *not* a subDFT
-                    return;
-                }
-                for (auto const& inDep : ingoingDependencies()) {
-                    inDep->extendSubDft(elemsInSubtree, parentsOfSubRoot, blockParents, sparesAsLeaves);
-                    if (elemsInSubtree.empty()) {
-                        // Parent in the subDFT, i.e., it is *not* a subDFT
-                        return;
-                    }
-                }
-            }
+            void extendSubDft(std::set<size_t>& elemsInSubtree, std::vector<size_t> const& parentsOfSubRoot, bool blockParents, bool sparesAsLeaves) const override;
 
             bool checkDontCareAnymore(storm::storage::DFTState<ValueType>& state, DFTStateSpaceGenerationQueues<ValueType>& queues) const override {
                 if (DFTElement<ValueType>::checkDontCareAnymore(state, queues)) {

src/test/storm-dft/CMakeLists.txt

@@ -9,7 +9,7 @@ register_source_groups_from_filestructure("${ALL_FILES}" test)
 # Note that the tests also need the source files, except for the main file
 include_directories(${GTEST_INCLUDE_DIR})
 
-foreach (testsuite api)
+foreach (testsuite api storage)
 
 	  file(GLOB_RECURSE TEST_${testsuite}_FILES ${STORM_TESTS_BASE_PATH}/${testsuite}/*.h ${STORM_TESTS_BASE_PATH}/${testsuite}/*.cpp)
       add_executable (test-dft-${testsuite} ${TEST_${testsuite}_FILES} ${STORM_TESTS_BASE_PATH}/storm-test.cpp)

src/test/storm-dft/storage/DftBETest.cpp

@@ -0,0 +1,29 @@
+#include "test/storm_gtest.h"
+#include "storm-config.h"
+
+#include "storm-dft/storage/dft/DFTElements.h"
+
+namespace {
+
+    TEST(DftBETest, FailureConstant) {
+        storm::storage::BEConst<double> be(0, "Test", true);
+        EXPECT_TRUE(be.failed());
+        EXPECT_TRUE(be.canFail());
+    
+        EXPECT_EQ(1, be.getUnreliability(0));
+        EXPECT_EQ(1, be.getUnreliability(10));
+    }
+
+    TEST(DftBETest, FailureExponential) {
+        storm::storage::BEExponential<double> be(0, "Test", 3, 0.5);
+            
+        EXPECT_TRUE(be.canFail());
+        EXPECT_EQ(1.5, be.passiveFailureRate());
+    
+        EXPECT_EQ(0, be.getUnreliability(0));
+        EXPECT_FLOAT_EQ(0.7768698399, be.getUnreliability(0.5));
+        EXPECT_FLOAT_EQ(0.9502129316, be.getUnreliability(1));
+        EXPECT_FLOAT_EQ(0.9975212478, be.getUnreliability(2));
+    }
+
+}