Set probability for pdeps

Former-commit-id: 2ac06e76c0

src/builder/ExplicitDFTModelBuilder.cpp

@@ -187,7 +187,9 @@ namespace storm {
                     // Set transitions
                     if (hasDependencies) {
                         // Failure is due to dependency -> add non-deterministic choice
-                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), storm::utility::one<ValueType>());
+                        std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dependency = mDft.getDependency(state->getDependencyId(smallest-1));
+                        transitionMatrixBuilder.addNextValue(state->getId() + rowOffset++, newState->getId(), dependency->probability());
+                        STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with probability " << dependency->probability());
                     } else {
                         // Set failure rate according to usage
                         bool isUsed = true;
@@ -203,11 +205,11 @@ namespace storm {
                         if (resultFind != outgoingTransitions.end()) {
                             // Add to existing transition
                             resultFind->second += rate;
-                            STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with " << rate << " to " << resultFind->second);
+                            STORM_LOG_TRACE("Updated transition from " << state->getId() << " to " << resultFind->first << " with rate " << rate << " to new rate " << resultFind->second);
                         } else {
                             // Insert new transition
                             outgoingTransitions.insert(std::make_pair(newState->getId(), rate));
-                            STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with " << rate);
+                            STORM_LOG_TRACE("Added transition from " << state->getId() << " to " << newState->getId() << " with rate " << rate);
                         }
                         exitRate += rate;
                     }

src/storage/dft/DFTState.cpp

@@ -99,8 +99,7 @@ namespace storm {
             STORM_LOG_TRACE("currently failable: " << getCurrentlyFailableString());
             if (nrFailableDependencies() > 0) {
                 // Consider failure due to dependency
-                assert(index < nrFailableDependencies());
-                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(mFailableDependencies[index]);
+                std::shared_ptr<DFTDependency<ValueType> const> dependency = mDft.getDependency(getDependencyId(index));
                 std::pair<std::shared_ptr<DFTBE<ValueType> const>,bool> res(mDft.getBasicElement(dependency->dependentEvent()->id()), true);
                 mFailableDependencies.erase(mFailableDependencies.begin() + index);
                 setFailed(res.first->id());

src/storage/dft/DFTState.h

@@ -6,6 +6,7 @@
 
 #include <sstream>
 #include <memory>
+#include <cassert>
 
 namespace storm {
     namespace storage {
@@ -114,6 +115,16 @@ namespace storm {
             size_t nrFailableDependencies() const {
                 return mFailableDependencies.size();
             }
+            
+            /**
+             * Gets the id of the dependency at index in the list of failable dependencies.
+             * @param index Index in list of failable dependencies.
+             * @return Id of the dependency
+             */
+            size_t getDependencyId(size_t index) const {
+                assert(index < nrFailableDependencies());
+                return mFailableDependencies[index];
+            }
 
             /**
              * Sets all failable BEs due to dependencies from newly failed element