From 63b0513f38c74bd06b0254d70df9d32e9636d8ef Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 15 Feb 2016 14:58:26 +0100
Subject: [PATCH] Set probability for pdeps

Former-commit-id: 2ac06e76c007d05cef74fc3028e967910abacb06
---
 src/builder/ExplicitDFTModelBuilder.cpp |  8 +++++---
 src/storage/dft/DFTState.cpp            |  3 +--
 src/storage/dft/DFTState.h              | 11 +++++++++++
 3 files changed, 17 insertions(+), 5 deletions(-)

diff --git a/src/builder/ExplicitDFTModelBuilder.cpp b/src/builder/ExplicitDFTModelBuilder.cpp
index cd2704dc6..723d75920 100644
--- a/src/builder/ExplicitDFTModelBuilder.cpp
+++ b/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;
                     }
diff --git a/src/storage/dft/DFTState.cpp b/src/storage/dft/DFTState.cpp
index 672ca14a7..8714f0130 100644
--- a/src/storage/dft/DFTState.cpp
+++ b/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());
diff --git a/src/storage/dft/DFTState.h b/src/storage/dft/DFTState.h
index 17a9c2d3b..520587a42 100644
--- a/src/storage/dft/DFTState.h
+++ b/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