diff --git a/examples/dft/pdep.dft b/examples/dft/pdep.dft new file mode 100644 index 000000000..f8cb0382b --- /dev/null +++ b/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; diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp index 262098a68..c8639ae30 100644 --- a/src/parser/DFTGalileoParser.cpp +++ b/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()); + } else if (tokens[1] == "fdep") { + success = builder.addDepElement(name, childNames, storm::utility::one()); + } 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)); diff --git a/src/storage/dft/DFTBuilder.h b/src/storage/dft/DFTBuilder.h index 9297d90cf..a2422522c 100644 --- a/src/storage/dft/DFTBuilder.h +++ b/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 const& children, ValueType probability) { + bool addDepElement(std::string const& name, std::vector 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>(mNextId++, nameFdep, trigger, children[i], storm::utility::one()); + assert(storm::utility::isOne(probability) || children.size() == 2); + DFTDependencyPointer element = std::make_shared>(mNextId++, nameDep, trigger, children[i], probability); mElements[element->name()] = element; mDependencies.push_back(element); } diff --git a/src/storage/dft/DFTElements.h b/src/storage/dft/DFTElements.h index 063a8a414..9dcc42b8d 100644 --- a/src/storage/dft/DFTElements.h +++ b/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();