Set dependencies to dont care after dependent event has failed

Former-commit-id: 506f5c3107

examples/dft/pdep_symmetry.dft

@@ -2,8 +2,8 @@ toplevel "A";
 "A" and "B" "B'";
 "B" and "C" "D" "PDEP";
 "B'" and "C'" "D'" "PDEP'";
-"PDEP" pdep=0.6 "B" "C";
-"PDEP'" pdep=0.6 "B'" "C'";
+"PDEP" pdep=0.6 "C" "D";
+"PDEP'" pdep=0.6 "C'" "D'";
 "C" lambda=0.5 dorm=0;
 "D" lambda=0.5 dorm=0;
 "C'" lambda=0.5 dorm=0;

src/builder/ExplicitDFTModelBuilder.cpp

@@ -227,6 +227,7 @@ namespace storm {
                     // Update failable dependencies
                     if (!dftFailed) {
                         newState->updateFailableDependencies(nextBE->id());
+                        newState->updateDontCareDependencies(nextBE->id());
                     }
                     
                     uint_fast64_t newStateId;

src/storage/dft/DFTState.cpp

@@ -142,14 +142,21 @@ namespace storm {
         
         template<typename ValueType>
         void DFTState<ValueType>::setDependencySuccessful(size_t id) {
-            // No distinction between successful dependency and no dependency at all
-            // => we do not set bit
-            //mStatus.set(mStateGenerationInfo.mIdToStateIndex(id));
+            // Only distinguish between passive and dont care dependencies
+            //mStatus.set(mStateGenerationInfo.getStateIndex(id));
+            setDependencyDontCare(id);
         }
 
         template<typename ValueType>
         void DFTState<ValueType>::setDependencyUnsuccessful(size_t id) {
-            mStatus.set(mStateGenerationInfo.getStateIndex(id)+1);
+            // Only distinguish between passive and dont care dependencies
+            //mStatus.set(mStateGenerationInfo.getStateIndex(id)+1);
+            setDependencyDontCare(id);
+        }
+        
+        template<typename ValueType>
+        void DFTState<ValueType>::setDependencyDontCare(size_t id) {
+            mStatus.setFromInt(mStateGenerationInfo.getStateIndex(id), 2, static_cast<uint_fast64_t>(DFTDependencyState::DontCare));
         }
 
         template<typename ValueType>
@@ -176,6 +183,17 @@ namespace storm {
             }
             return nrFailableDependencies() > 0;
         }
+        
+        template<typename ValueType>
+        void DFTState<ValueType>::updateDontCareDependencies(size_t id) {
+            assert(mDft.isBasicElement(id));
+            assert(hasFailed(id));
+            
+            for (auto dependency : mDft.getBasicElement(id)->ingoingDependencies()) {
+                assert(dependency->dependentEvent()->id() == id);
+                setDependencyDontCare(dependency->id());
+            }
+        }
 
         template<typename ValueType>
         std::pair<std::shared_ptr<DFTBE<ValueType> const>, bool> DFTState<ValueType>::letNextBEFail(size_t index)

src/storage/dft/DFTState.h

@@ -79,6 +79,8 @@ namespace storm {
 
             void setDependencyUnsuccessful(size_t id);
 
+            void setDependencyDontCare(size_t id);
+
             void beNoLongerFailable(size_t id);
             
             void activate(size_t repr);
@@ -162,6 +164,12 @@ namespace storm {
              * @return true if failable dependent events exist
              */
             bool updateFailableDependencies(size_t id);
+            
+            /**
+             * Sets all dependencies dont care whose dependent event is the newly failed BE.
+             * @param id Id of the newly failed element
+             */
+            void updateDontCareDependencies(size_t id);
 
             /**
              * Sets the next BE as failed