From 8896bc55ddd11bb3b52dd4134e34e75df8257c02 Mon Sep 17 00:00:00 2001
From: Mavo <matthias.volk@rwth-aachen.de>
Date: Mon, 8 Feb 2016 17:50:59 +0100
Subject: [PATCH] Added probabilities for FDeps

Former-commit-id: c679ebb321d742dea13ceb88cea687e46e48fc75
---
 src/parser/DFTGalileoParser.cpp |  2 +-
 src/storage/dft/DFTBuilder.h    | 12 ++++++++++--
 src/storage/dft/DFTElements.h   | 12 ++++++++++--
 3 files changed, 21 insertions(+), 5 deletions(-)

diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp
index d623821e6..d56899d20 100644
--- a/src/parser/DFTGalileoParser.cpp
+++ b/src/parser/DFTGalileoParser.cpp
@@ -107,7 +107,7 @@ namespace storm {
                     } else if (tokens[1] == "wsp" || tokens[1] == "csp") {
                         success = builder.addSpareElement(name, childNames);
                     } else if (boost::starts_with(tokens[1], "fdep")) {
-                        success = builder.addFDepElement(name, childNames);
+                        success = builder.addFDepElement(name, childNames, storm::utility::one<ValueType>());
                     } else if (boost::starts_with(tokens[1], "lambda=")) {
                         ValueType failureRate = parseRationalExpression(tokens[1].substr(7));
                         ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5));
diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h
index 9dfb80ac2..8fc65b0b5 100644
--- a/src/storage/dft/DFTBuilder.h
+++ b/src/storage/dft/DFTBuilder.h
@@ -53,13 +53,21 @@ namespace storm {
                 return addStandardGate(name, children, DFTElementTypes::SPARE);
             }
             
-            bool addFDepElement(std::string const& name, std::vector<std::string> const& children) {
+            bool addFDepElement(std::string const& name, std::vector<std::string> const& children, ValueType probability) {
                 assert(children.size() > 1);
                 if(mElements.count(name) != 0) {
                     // Element with that name already exists.
                     return false;
                 }
                 std::string trigger = children[0];
+
+                //TODO Matthias: collect constraints for SMT solving
+                //0 <= probability <= 1
+                if (!storm::utility::isOne(probability) && children.size() > 2) {
+                    //TODO Matthias: introduce additional element for probability and then add fdeps with probability 1 to children
+                    std::cerr << "Probability != 1 currently not supported." << std::endl;
+                }
+
                 for (size_t i = 1; i < children.size(); ++i) {
                     // TODO Matthias: better code
                     std::stringstream stream;
@@ -69,7 +77,7 @@ namespace storm {
                         // Element with that name already exists.
                         return false;
                     }
-                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, s, trigger, children[i]);
+                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, s, trigger, children[i], storm::utility::one<ValueType>());
                     mElements[element->name()] = element;
                     mDependencies.push_back(element);
                 }
diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h
index d8f9e19b1..063a8a414 100644
--- a/src/storage/dft/DFTElements.h
+++ b/src/storage/dft/DFTElements.h
@@ -371,12 +371,13 @@ namespace storm {
         protected:
             std::string mNameTrigger;
             std::string mNameDependent;
+            ValueType mProbability;
             DFTGatePointer mTriggerEvent;
             DFTBEPointer mDependentEvent;
 
         public:
-            DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent) :
-                DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent)
+            DFTDependency(size_t id, std::string const& name, std::string const& trigger, std::string const& dependent, ValueType probability) :
+                DFTElement<ValueType>(id, name), mNameTrigger(trigger), mNameDependent(dependent), mProbability(probability)
             {
             }
 
@@ -397,6 +398,10 @@ namespace storm {
                 return mNameDependent;
             }
 
+            ValueType probability() {
+                return mProbability;
+            }
+
             DFTGatePointer const& triggerEvent() const {
                 assert(mTriggerEvent);
                 return mTriggerEvent;
@@ -427,6 +432,9 @@ namespace storm {
             virtual std::string toString() const override {
                 std::stringstream stream;
                 stream << "{" << this->name() << "} FDEP(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+                if (!storm::utility::isOne(mProbability)) {
+                    stream << " with probability " << mProbability;
+                }
                 return stream.str();
             }