Added probabilities for FDeps

Former-commit-id: c679ebb321

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));

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);
                 }

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();
             }