From a781df35c291e34c52ff443456fb65f7c76b73c2 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Sun, 31 Jan 2016 17:21:13 +0100
Subject: [PATCH] Use passive failure rate if BE is not used

Former-commit-id: fdc4a6687bb658f26585391e6d5ce7f811dabea0
---
 src/builder/ExplicitDFTModelBuilder.cpp | 21 +++++++++++++--------
 src/storage/dft/DFT.cpp                 |  9 +++++----
 src/storage/dft/DFT.h                   |  9 +++++++++
 3 files changed, 27 insertions(+), 12 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index 107baa4bb..811d0fdcb 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/src/builder/ExplicitDFTModelBuilder.cpp
@@ -127,31 +127,36 @@ namespace storm {
                         next->checkDontCareAnymore(newState, queues);
                     }
 
-                    auto it = mStates.find(newState);
-                    if (it == mStates.end()) {
+                    auto itState = mStates.find(newState);
+                    if (itState == mStates.end()) {
                         // New state
                         newState.setId(newIndex++);
                         auto itInsert = mStates.insert(newState);
                         assert(itInsert.second);
-                        it = itInsert.first;
+                        itState = itInsert.first;
                         STORM_LOG_TRACE("New state " << mDft.getStateString(newState));
 
                         // Add state to search
                         stateQueue.push(newState);
                     } else {
                         // State already exists
-                        STORM_LOG_TRACE("State " << mDft.getStateString(*it) << " already exists");
+                        STORM_LOG_TRACE("State " << mDft.getStateString(*itState) << " already exists");
                     }
 
-                    // Set transition
-                    ValueType rate = nextBE->activeFailureRate();
-                    auto resultFind = outgoingTransitions.find(it->getId());
+                    // Set failure rate according to usage
+                    bool isUsed = true;
+                    if (mDft.hasRepresentant(nextBE->id())) {
+                        isUsed = newState.isUsed(nextBE->id());
+                    }
+                    STORM_LOG_TRACE("BE " << nextBE->name() << " is " << (isUsed ? "used" : "not used"));
+                    ValueType rate = isUsed ? nextBE->activeFailureRate() : nextBE->passiveFailureRate();
+                    auto resultFind = outgoingTransitions.find(itState->getId());
                     if (resultFind != outgoingTransitions.end()) {
                         // Add to existing transition
                         resultFind->second += rate;
                     } else {
                         // Insert new transition
-                        outgoingTransitions.insert(std::make_pair(it->getId(), rate));
+                        outgoingTransitions.insert(std::make_pair(itState->getId(), rate));
                     }
                     sum += rate;
                 } // end while failing BE
diff --git a/src/storage/dft/DFT.cpp b/src/storage/dft/DFT.cpp
index 0b8c99685..ae4ec62eb 100644
--- a/src/storage/dft/DFT.cpp
+++ b/src/storage/dft/DFT.cpp
@@ -29,6 +29,7 @@ namespace storm {
                         for(auto const& modelem : module) {
                             if(mElements[modelem]->isSpareGate() || mElements[modelem]->isBasicElement()) {
                                 sparesAndBes.push_back(modelem);
+                                mRepresentants.insert(std::make_pair(modelem, spareReprs->id()));
                             }
                         }
                         mSpareModules.insert(std::make_pair(spareReprs->id(), sparesAndBes));
@@ -131,12 +132,12 @@ namespace storm {
             stream << "(" << state.getId() << ") ";
             for (auto const& elem : mElements) {
                 stream << state.getElementStateInt(elem->id());
-                /*if(elem->isSpareGate()) {
+                if(elem->isSpareGate()) {
                     if(state.isActiveSpare(elem->id())) {
-                        os << " actively";
+                        stream << " actively";
                     }
-                    os << " using " << state.uses(elem->id());
-                }*/
+                    stream << " using " << state.uses(elem->id());
+                }
             }
             return stream.str();
         }
diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 0f39e3ddc..17d6c7fd5 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -50,6 +50,7 @@ namespace storm {
             std::vector<size_t> mTopModule;
             std::vector<size_t> mIdToFailureIndex;
             std::map<size_t, size_t> mUsageIndex;
+            std::map<size_t, size_t> mRepresentants;
             
         public:
             DFT(DFTElementVector const& elements, DFTElementPointer const& tle);
@@ -154,6 +155,14 @@ namespace storm {
                 return elements;
             }
 
+            bool hasRepresentant(size_t id) const {
+                return mRepresentants.find(id) != mRepresentants.end();
+            }
+
+            DFTElementPointer getRepresentant(size_t id) const {
+                assert(hasRepresentant(id));
+                return getElement(mRepresentants.find(id)->second);
+            }
 
             bool hasFailed(DFTState<ValueType> const& state) const {
                 return state.hasFailed(mTopLevelIndex);