Handle PDEP in createSuccessorState as well

src/storm-dft/generator/DftNextStateGenerator.cpp

@@ -159,14 +159,13 @@ namespace storm {
                 // Set transitions
                 if (exploreDependencies) {
                     // Failure is due to dependency -> add non-deterministic choice if necessary
-                    ValueType probability = mDft.getDependency(*iterFailable)->probability();
+                    ValueType probability = dependency->probability();
                     choice.addProbability(newStateId, probability);
                     STORM_LOG_TRACE("Added transition to " << newStateId << " with probability " << probability);
 
                     if (!storm::utility::isOne(probability)) {
                         // Add transition to state where dependency was unsuccessful
-                        DFTStatePointer unsuccessfulState = state->copy();
-                        unsuccessfulState->letDependencyBeUnsuccessful(*iterFailable);
+                        DFTStatePointer unsuccessfulState = createSuccessorState(state, nextBE, dependency, false);
                         // Add state
                         StateType unsuccessfulStateId = stateToIdCallback(unsuccessfulState);
                         ValueType remainingProbability = storm::utility::one<ValueType>() - probability;
@@ -221,9 +220,19 @@ namespace storm {
         }
 
         template<typename ValueType, typename StateType>
-        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency) const {
+        typename DftNextStateGenerator<ValueType, StateType>::DFTStatePointer DftNextStateGenerator<ValueType, StateType>::createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const>& failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const>& triggeringDependency, bool dependencySuccessful) const {
             // Construct new state as copy from original one
             DFTStatePointer newState = state->copy();
+
+            if (!dependencySuccessful) {
+                // Dependency was unsuccessful -> no BE fails
+                STORM_LOG_ASSERT(triggeringDependency != nullptr, "Dependency is not given");
+                STORM_LOG_TRACE("With the unsuccessful triggering of PDEP: " << triggeringDependency->name() << " [" << triggeringDependency->id() << "]" << " in " << mDft.getStateString(state));
+                newState->letDependencyBeUnsuccessful(triggeringDependency);
+                return newState;
+            }
+
+
             STORM_LOG_TRACE("With the failure of: " << failedBE->name() << " [" << failedBE->id() << "]" << (triggeringDependency != nullptr ? " (through dependency " + triggeringDependency->name() + " [" + std::to_string(triggeringDependency->id()) + ")]" : "") << " in " << mDft.getStateString(state));
 
             newState->letBEFail(failedBE, triggeringDependency);

src/storm-dft/generator/DftNextStateGenerator.h

@@ -61,10 +61,12 @@ namespace storm {
              * @param state Current state.
              * @param failedBE BE which fails next.
              * @param triggeringDependency Dependency which triggered the failure (or nullptr if BE failed on its own).
+             * @param dependencySuccessful Whether the triggering dependency was successful.
+             *              If the dependency is unsuccessful, failedBE does not fail and only the depedendy is marked as failed.
              * 
              * @return Successor state.
              */
-            DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency) const;
+            DFTStatePointer createSuccessorState(DFTStatePointer const state, std::shared_ptr<storm::storage::DFTBE<ValueType> const> &failedBE, std::shared_ptr<storm::storage::DFTDependency<ValueType> const> &triggeringDependency, bool dependencySuccessful = true) const;
 
             /**
              * Propagate the failures in a given state if the given BE fails

src/storm-dft/storage/dft/DFTState.cpp

@@ -343,10 +343,10 @@ namespace storm {
         }
  
         template<typename ValueType>
-        void DFTState<ValueType>::letDependencyBeUnsuccessful(size_t id) {
+        void DFTState<ValueType>::letDependencyBeUnsuccessful(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency) {
             STORM_LOG_ASSERT(failableElements.hasDependencies(), "Index invalid.");
-            std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(id);
-            failableElements.removeDependency(id);
+            STORM_LOG_ASSERT(!dependency->isFDEP(), "Dependency is not a PDEP.");
+            failableElements.removeDependency(dependency->id());
             setDependencyUnsuccessful(dependency->id());
         }
 

src/storm-dft/storage/dft/DFTState.h

@@ -247,9 +247,9 @@ namespace storm {
             
             /**
              * Sets the dependency as unsuccesful meaning no BE will fail.
-             * @param index Index of dependency to fail.
+             * @param dependency Dependency.
              */
-            void letDependencyBeUnsuccessful(size_t index = 0);
+            void letDependencyBeUnsuccessful(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency);
             
             /**
              * Order the state in decreasing order using the symmetries.