From a6c087f4610a818183146b6f624d3e95dd93de15 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@rwth-aachen.de>
Date: Fri, 26 Feb 2016 17:50:51 +0100
Subject: [PATCH] Dont Care Propagation and SEQ are now sound (but more DCs can
 be propagated with some care)

Former-commit-id: 96288dd8d951caf24325caef0d7eff00cd3e23db
---
 src/storage/dft/DFT.h                    |  4 ++++
 src/storage/dft/DFTState.cpp             | 13 +++++++++++++
 src/storage/dft/DFTState.h               |  7 +++++++
 src/storage/dft/DFTStateGenerationInfo.h |  6 ++++++
 src/storage/dft/elements/DFTElement.cpp  |  5 ++++-
 src/storage/dft/elements/DFTElement.h    |  2 +-
 6 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/src/storage/dft/DFT.h b/src/storage/dft/DFT.h
index 9762def61..22041da85 100644
--- a/src/storage/dft/DFT.h
+++ b/src/storage/dft/DFT.h
@@ -146,6 +146,10 @@ namespace storm {
             bool isDependency(size_t index) const {
                 return getElement(index)->isDependency();
             }
+            
+            bool isRestriction(size_t index) const {
+                return getElement(index)->isRestriction();
+            }
 
             std::shared_ptr<DFTBE<ValueType> const> getBasicElement(size_t index) const {
                 assert(isBasicElement(index));
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 547fdd169..419403d55 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/src/storage/dft/DFTState.cpp
@@ -233,6 +233,19 @@ namespace storm {
             assert(hasFailed(spareId));
             mStatus.setFromInt(mStateGenerationInfo.getSpareUsageIndex(spareId), mStateGenerationInfo.usageInfoBits(), mDft.getMaxSpareChildCount());
         }
+        
+        template<typename ValueType>
+        bool DFTState<ValueType>::hasOperationalPostSeqElements(size_t id) const {
+            assert(!mDft.isDependency(id));
+            assert(!mDft.isRestriction(id));
+            auto const& postIds =  mStateGenerationInfo.seqRestrictionPostElements(id);
+            for(size_t id : postIds) {
+                if(isOperational(id)) {
+                    return true;
+                }
+            }
+            return false;
+        }
 
         template<typename ValueType>
         bool DFTState<ValueType>::claimNew(size_t spareId, size_t currentlyUses, std::vector<std::shared_ptr<DFTElement<ValueType>>> const& children) {
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index ea874cf1b..826e510d5 100644
--- a/src/storage/dft/DFTState.h
+++ b/src/storage/dft/DFTState.h
@@ -177,6 +177,13 @@ namespace storm {
              */
             bool orderBySymmetry();
             
+            /**
+             * Checks whether operational post seq elements are present
+             * @param id
+             * @return 
+             */
+            bool hasOperationalPostSeqElements(size_t id) const;
+            
             std::string getCurrentlyFailableString() const {
                 std::stringstream stream;
                 if (nrFailableDependencies() > 0) {
diff --git a/src/storage/dft/DFTStateGenerationInfo.h b/src/storage/dft/DFTStateGenerationInfo.h
index a89add9bf..4b3ef92c9 100644
--- a/src/storage/dft/DFTStateGenerationInfo.h
+++ b/src/storage/dft/DFTStateGenerationInfo.h
@@ -38,6 +38,12 @@ namespace storm {
                 mSeqRestrictionPostElements[id] = elems;
             }
             
+            std::vector<size_t> const& seqRestrictionPostElements(size_t index) const {
+                assert(mSeqRestrictionPostElements.count(index) > 0);
+                return mSeqRestrictionPostElements.at(index);
+            }
+            
+            
             void addSpareActivationIndex(size_t id, size_t index) {
                 mSpareActivationIndex[id] = index;
             }
diff --git a/src/storage/dft/elements/DFTElement.cpp b/src/storage/dft/elements/DFTElement.cpp
index b71e0672b..0ee8a3cd2 100644
--- a/src/storage/dft/elements/DFTElement.cpp
+++ b/src/storage/dft/elements/DFTElement.cpp
@@ -32,6 +32,10 @@ namespace storm {
                 }
             }
             
+            if(!mRestrictions.empty() && state.hasOperationalPostSeqElements(mId)) {
+                return false;
+            }
+            
             state.setDontCare(mId);
             if (hasParentSpare && !state.isActive(mId)) {
                 // Activate child for consistency in failed spares
@@ -65,7 +69,6 @@ namespace storm {
 
         template<typename ValueType>
         std::vector<size_t> DFTElement<ValueType>::independentSubDft(bool blockParents) const {
-            //std::cout << "INDEPENDENT SUBTREE CALL " << this->id() << std::endl;
             std::vector<size_t> res;
             res.push_back(this->id());
             return res;
diff --git a/src/storage/dft/elements/DFTElement.h b/src/storage/dft/elements/DFTElement.h
index 2d57567e9..2b3b05c98 100644
--- a/src/storage/dft/elements/DFTElement.h
+++ b/src/storage/dft/elements/DFTElement.h
@@ -241,7 +241,7 @@ namespace storm {
                         continue;
                     }
                     auto it = restr->children().cbegin();
-                    for(++it; it != restr->children().cend(); ++it) {
+                    for(; it != restr->children().cend(); ++it) {
                         if((*it)->id() == mId) {
                             break;
                         }