Parse PDEPs

Former-commit-id: 623afd494f

examples/dft/pdep.dft

@@ -0,0 +1,12 @@
+// From Junges2015
+// Example 3.19
+
+toplevel "SF";
+"SF" or "A" "B" "PDEP";
+"A" pand "S" "MA";
+"B" and "MA" "MB";
+"PDEP" pdep=0.2 "MA" "S";
+
+"S" lambda=0.5 dorm=0;
+"MA" lambda=0.5 dorm=0;
+"MB" lambda=0.5 dorm=0;

src/parser/DFTGalileoParser.cpp

@@ -106,8 +106,11 @@ namespace storm {
                         success = builder.addPandElement(name, childNames);
                     } 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, storm::utility::one<ValueType>());
+                    } else if (tokens[1] == "fdep") {
+                        success = builder.addDepElement(name, childNames, storm::utility::one<ValueType>());
+                    } else if (boost::starts_with(tokens[1], "pdep=")) {
+                        ValueType probability = parseRationalExpression(tokens[1].substr(5));
+                        success = builder.addDepElement(name, childNames, probability);
                     } 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,28 +53,36 @@ namespace storm {
                 return addStandardGate(name, children, DFTElementTypes::SPARE);
             }
             
-            bool addFDepElement(std::string const& name, std::vector<std::string> const& children, ValueType probability) {
+            bool addDepElement(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;
                 }
+
+                if (storm::utility::isZero(probability)) {
+                    // Element is superfluous
+                    return true;
+                }
                 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;
+                    //TODO Matthias: introduce additional element for probability and then add pdeps with probability 1 to children
+                    std::cerr << "Probability != 1 for more than one child currently not supported." << std::endl;
+                    return false;
                 }
 
                 for (size_t i = 1; i < children.size(); ++i) {
-                    std::string nameFdep = name + "_" + std::to_string(i);
-                    if(mElements.count(nameFdep) != 0) {
+                    std::string nameDep = name + "_" + std::to_string(i);
+                    if(mElements.count(nameDep) != 0) {
                         // Element with that name already exists.
+                        std::cerr << "Element with name: " << nameDep << " already exists." << std::endl;
                         return false;
                     }
-                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameFdep, trigger, children[i], storm::utility::one<ValueType>());
+                    assert(storm::utility::isOne(probability) || children.size() == 2);
+                    DFTDependencyPointer element = std::make_shared<DFTDependency<ValueType>>(mNextId++, nameDep, trigger, children[i], probability);
                     mElements[element->name()] = element;
                     mDependencies.push_back(element);
                 }

src/storage/dft/DFTElements.h

@@ -431,8 +431,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)) {
+                bool fdep = storm::utility::isOne(mProbability);
+                stream << "{" << this->name() << "} " << (fdep ? "FDEP" : "PDEP") << "(" << mTriggerEvent->name() << " => " << mDependentEvent->name() << ")";
+                if (!fdep) {
                     stream << " with probability " << mProbability;
                 }
                 return stream.str();