Dont Care Propagation and SEQ are now sound (but more DCs can be propagated with some care)

Former-commit-id: 96288dd8d9

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));

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) {

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) {

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;
             }

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;

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;
                         }