From 306eb8a9ccbbd14d357b0a352d0bdec96b41a0a3 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Fri, 11 Mar 2016 15:13:24 +0100
Subject: [PATCH] Construct state from bit vector

Former-commit-id: 705af6d503fafdc8520e5769511f8802144bded8
---
 examples/dft/mcs.dft         | 22 ++++++++++++++++++++++
 src/storage/dft/DFTState.cpp | 28 +++++++++++++++++++++++++---
 2 files changed, 47 insertions(+), 3 deletions(-)
 create mode 100644 examples/dft/mcs.dft

diff --git a/examples/dft/mcs.dft b/examples/dft/mcs.dft
new file mode 100644
index 000000000..733a7a599
--- /dev/null
+++ b/examples/dft/mcs.dft
@@ -0,0 +1,22 @@
+toplevel "n12";
+"n12" or "n1" "n103" "n7";
+"n103" wsp "n106" "n14";
+"n7" and "n18" "n26";
+"n26" or "n28" "n19" "n23";
+"n19" wsp "n16" "n13";
+"n23" wsp "n0" "n17";
+"n18" or "n15" "n9" "n3";
+"n3" wsp "n2" "n17";
+"n9" wsp "n8" "n27";
+"n16" lambda=8.0 dorm=0.0;
+"n0" lambda=0.003 dorm=0.0;
+"n13" lambda=8.0 dorm=0.5;
+"n2" lambda=0.003 dorm=0.0;
+"n17" lambda=0.003 dorm=0.5;
+"n15" lambda=0.05 dorm=0.0;
+"n106" lambda=1.2 dorm=0.0;
+"n14" lambda=0.6 dorm=0.0;
+"n1" lambda=2.0E-4 dorm=0.0;
+"n27" lambda=8.0 dorm=0.5;
+"n8" lambda=8.0 dorm=0.0;
+"n28" lambda=0.05 dorm=0.0;
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index b7061b9b2..c17bad0b6 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -25,10 +25,32 @@ namespace storm {
         
         template<typename ValueType>
         DFTState<ValueType>::DFTState(storm::storage::BitVector const& status, DFT<ValueType> const& dft, DFTStateGenerationInfo const& stateGenerationInfo, size_t id) : mStatus(status), mId(id), mDft(dft), mStateGenerationInfo(stateGenerationInfo) {
-            // TODO implement
-            assert(false);
+            
+            for(size_t index = 0; index < mDft.nrElements(); ++index) {
+                // Initialize currently failable BE
+                if (mDft.isBasicElement(index) && isOperational(index)) {
+                    if (!mDft.getBasicElement(index)->isColdBasicElement() || !mDft.hasRepresentant(index) || isActive(mDft.getRepresentant(index)->id())) {
+                        mIsCurrentlyFailableBE.push_back(index);
+                        STORM_LOG_TRACE("Currently failable: " << mDft.getBasicElement(index)->toString());
+                    }
+                } else if (mDft.getElement(index)->isSpareGate()) {
+                    // Initialize used representants
+                    uint_fast64_t useId = uses(index);
+                    mUsedRepresentants.push_back(useId);
+                    STORM_LOG_TRACE("Spare " << index << " uses " << useId);
+                }
+            }
+            
+            // Initialize failable dependencies
+            for (size_t dependencyId : mDft.getDependencies()) {
+                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(dependencyId);
+                assert(dependencyId == dependency->id());
+                if (hasFailed(dependency->triggerEvent()->id()) && getElementState(dependency->dependentEvent()->id()) == DFTElementState::Operational) {
+                    mFailableDependencies.push_back(dependencyId);
+                    STORM_LOG_TRACE("New dependency failure: " << dependency->toString());
+                }
+            }
         }
-        
 
         template<typename ValueType>
         DFTElementState DFTState<ValueType>::getElementState(size_t id) const {