From df28d8ef84a10b305b909036b0538e7c7a6b57ae Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Mon, 11 May 2020 14:27:19 +0200
Subject: [PATCH] Added getUnreliability() for BEs

---
 .../storage/dft/elements/BEConst.cpp          | 16 +++++++++
 src/storm-dft/storage/dft/elements/BEConst.h  |  2 ++
 .../storage/dft/elements/BEExponential.cpp    | 24 ++++++++++++++
 .../storage/dft/elements/BEExponential.h      | 10 +++---
 src/storm-dft/storage/dft/elements/DFTBE.cpp  | 33 +++++++++++++++++++
 src/storm-dft/storage/dft/elements/DFTBE.h    | 27 ++++++---------
 src/test/storm-dft/CMakeLists.txt             |  2 +-
 src/test/storm-dft/storage/DftBETest.cpp      | 29 ++++++++++++++++
 8 files changed, 119 insertions(+), 24 deletions(-)
 create mode 100644 src/storm-dft/storage/dft/elements/BEConst.cpp
 create mode 100644 src/storm-dft/storage/dft/elements/BEExponential.cpp
 create mode 100644 src/storm-dft/storage/dft/elements/DFTBE.cpp
 create mode 100644 src/test/storm-dft/storage/DftBETest.cpp

diff --git a/src/storm-dft/storage/dft/elements/BEConst.cpp b/src/storm-dft/storage/dft/elements/BEConst.cpp
new file mode 100644
index 000000000..cb2457a04
--- /dev/null
+++ b/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
diff --git a/src/storm-dft/storage/dft/elements/BEConst.h b/src/storm-dft/storage/dft/elements/BEConst.h
index 050cdf51e..3f0cdd949 100644
--- a/src/storm-dft/storage/dft/elements/BEConst.h
+++ b/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;
diff --git a/src/storm-dft/storage/dft/elements/BEExponential.cpp b/src/storm-dft/storage/dft/elements/BEExponential.cpp
new file mode 100644
index 000000000..a93113e31
--- /dev/null
+++ b/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>;
+
+    }
+}
diff --git a/src/storm-dft/storage/dft/elements/BEExponential.h b/src/storm-dft/storage/dft/elements/BEExponential.h
index 71786fda8..e29d44642 100644
--- a/src/storm-dft/storage/dft/elements/BEExponential.h
+++ b/src/storm-dft/storage/dft/elements/BEExponential.h
@@ -50,14 +50,12 @@ 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 {
-                    return this->passiveFailureRate() / this->activeFailureRate();
-                }
+                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.
              * @return True iff BE is transient.
diff --git a/src/storm-dft/storage/dft/elements/DFTBE.cpp b/src/storm-dft/storage/dft/elements/DFTBE.cpp
new file mode 100644
index 000000000..369039547
--- /dev/null
+++ b/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>;
+
+    }
+}
diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h
index 899ece201..1dd2d91d0 100644
--- a/src/storm-dft/storage/dft/elements/DFTBE.h
+++ b/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)) {
diff --git a/src/test/storm-dft/CMakeLists.txt b/src/test/storm-dft/CMakeLists.txt
index a0e96ee36..a2ef04a4b 100644
--- a/src/test/storm-dft/CMakeLists.txt
+++ b/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)
diff --git a/src/test/storm-dft/storage/DftBETest.cpp b/src/test/storm-dft/storage/DftBETest.cpp
new file mode 100644
index 000000000..38c2f2112
--- /dev/null
+++ b/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));
+    }
+
+}