From 7697254635f201e2007c8320b29daeeeeb78ca58 Mon Sep 17 00:00:00 2001
From: Matthias Volk <matthias.volk@cs.rwth-aachen.de>
Date: Tue, 13 Nov 2018 14:42:24 +0100
Subject: [PATCH] Fixed computation of dormancy factor for lambda=0

---
 src/storm-dft/builder/DFTBuilder.cpp          | 6 +-----
 src/storm-dft/storage/dft/DftJsonExporter.cpp | 3 +--
 src/storm-dft/storage/dft/elements/DFTBE.h    | 9 +++++++++
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp
index a333c3cd6..747075ef3 100644
--- a/src/storm-dft/builder/DFTBuilder.cpp
+++ b/src/storm-dft/builder/DFTBuilder.cpp
@@ -268,11 +268,7 @@ namespace storm {
                 case storm::storage::DFTElementType::BE:
                 {
                     std::shared_ptr<storm::storage::DFTBE<ValueType>> be = std::static_pointer_cast<storm::storage::DFTBE<ValueType>>(element);
-                    ValueType dormancyFactor = storm::utility::zero<ValueType>();
-                    if (be->canFail()) {
-                        dormancyFactor = be->passiveFailureRate() / be->activeFailureRate();
-                    }
-                    addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient());
+                    addBasicElement(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient());
                     break;
                 }
                 case storm::storage::DFTElementType::CONSTF:
diff --git a/src/storm-dft/storage/dft/DftJsonExporter.cpp b/src/storm-dft/storage/dft/DftJsonExporter.cpp
index 608d01aca..a99335a96 100644
--- a/src/storm-dft/storage/dft/DftJsonExporter.cpp
+++ b/src/storm-dft/storage/dft/DftJsonExporter.cpp
@@ -88,8 +88,7 @@ namespace storm {
                 stream << be->activeFailureRate();
                 nodeData["rate"] = stream.str();
                 stream.str(std::string()); // Clear stringstream
-                ValueType dormancy = be->passiveFailureRate() / be->activeFailureRate();
-                stream << dormancy;
+                stream << be->dormancyFactor();
                 nodeData["dorm"] = stream.str();
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Element of type '" << element->type() << "' is not supported.");
diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h
index 6bb234b4e..84f05b5b1 100644
--- a/src/storm-dft/storage/dft/elements/DFTBE.h
+++ b/src/storm-dft/storage/dft/elements/DFTBE.h
@@ -34,6 +34,15 @@ namespace storm {
                 return mPassiveFailureRate;
             }
 
+            ValueType dormancyFactor() const {
+                if (storm::utility::isZero<ValueType>(this->activeFailureRate())) {
+                    // Return default value of 0
+                    return storm::utility::zero<ValueType>();
+                } else {
+                    return this->passiveFailureRate() / this->activeFailureRate();
+                }
+            }
+
             bool isTransient() const {
                 return mTransient;
             }