diff --git a/src/storm-dft/builder/DFTBuilder.cpp b/src/storm-dft/builder/DFTBuilder.cpp index 3bc2cf71b..2c3f4a656 100644 --- a/src/storm-dft/builder/DFTBuilder.cpp +++ b/src/storm-dft/builder/DFTBuilder.cpp @@ -273,14 +273,16 @@ namespace storm { case storm::storage::DFTElementType::BE: { std::shared_ptr> be = std::static_pointer_cast>(element); - addBasicElement(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient()); + addBasicElementExponential(be->name(), be->activeFailureRate(), be->dormancyFactor(), be->isTransient()); break; } case storm::storage::DFTElementType::CONSTF: case storm::storage::DFTElementType::CONSTS: - // TODO - STORM_LOG_ASSERT(false, "Const elements not supported."); + { + std::shared_ptr> be = std::static_pointer_cast>(element); + addBasicElementConst(be->name(), be->failed()); break; + } case storm::storage::DFTElementType::PDEP: { DFTDependencyPointer dependency = std::static_pointer_cast>(element); diff --git a/src/storm-dft/builder/DFTBuilder.h b/src/storm-dft/builder/DFTBuilder.h index 479db529c..2f89b8306 100644 --- a/src/storm-dft/builder/DFTBuilder.h +++ b/src/storm-dft/builder/DFTBuilder.h @@ -8,6 +8,8 @@ #include "storm-dft/storage/dft/DFTElements.h" #include "storm-dft/storage/dft/elements/DFTRestriction.h" #include "storm-dft/storage/dft/DFTLayoutInfo.h" +#include "storm/exceptions/NotSupportedException.h" + namespace storm { namespace storage { @@ -109,7 +111,7 @@ namespace storm { if (binaryDependencies && !storm::utility::isOne(probability) && children.size() > 2) { // Introduce additional element for first capturing the probabilistic dependency std::string nameAdditional = name + "_additional"; - addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero(), false); + addBasicElementConst(nameAdditional, false); // First consider probabilistic dependency addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability); // Then consider dependencies to the children if probabilistic dependency failed @@ -167,15 +169,42 @@ namespace storm { mChildNames[element] = children; return true; } - - bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) { + + bool addBasicElementConst(std::string const& name, bool failed) { + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); + return false; + } + mElements[name] = std::make_shared>(mNextId++, name, failed); + return true; + } + + bool addBasicElementProbability(std::string const& name, ValueType probability, ValueType dormancyFactor, bool transient = false) { + //0 <= dormancyFactor <= 1 + if (nameInUse(name)) { + STORM_LOG_ERROR("Element with name '" << name << "' already exists."); + return false; + } + if (storm::utility::isZero(probability)) { + return addBasicElementConst(name, false); + } else if (storm::utility::isOne(probability)) { + return addBasicElementConst(name, true); + } + STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant probability distribution is not supported for basic element '" << name << "'."); + return false; + } + + bool addBasicElementExponential(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) { //TODO Matthias: collect constraints for SMT solving - //failureRate > 0 //0 <= dormancyFactor <= 1 if (nameInUse(name)) { STORM_LOG_ERROR("Element with name '" << name << "' already exists."); return false; } + if (storm::utility::isZero(failureRate)) { + return addBasicElementConst(name, false); + } + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index ef7faf350..bf1dced78 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -297,26 +297,29 @@ namespace storm { switch (distribution) { case Constant: + if (storm::utility::isZero(firstValDistribution) || storm::utility::isOne(firstValDistribution)) { + return builder.addBasicElementProbability(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs + } STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Constant distribution is not supported for basic element '" << name << "' in line " << lineNo << "."); break; case Exponential: - return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs + return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs break; case Erlang: if (erlangPhases == 1) { // Erlang distribution reduces to exponential distribution - return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs + return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs } else { // Model Erlang distribution by using SEQ over BEs instead. // For each phase a BE is added, then the SEQ ensures the ordered failure. STORM_LOG_WARN("Erlang distribution for basic element '" << name << "' in line " << lineNo << " is modelled by SEQ gate and BEs."); std::string origName = parseName(name); std::vector childNames; - bool success = builder.addBasicElement(origName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs + bool success = builder.addBasicElementExponential(origName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs for (size_t i = 0; i < erlangPhases - 1; ++i) { std::string beName = origName + "_" + std::to_string(i); childNames.push_back(beName); - success = success && builder.addBasicElement(beName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs + success = success && builder.addBasicElementExponential(beName, firstValDistribution, dormancyFactor, false); // TODO set transient BEs } childNames.push_back(origName); return success && builder.addSequenceEnforcer(origName + "_seq", childNames); @@ -325,7 +328,7 @@ namespace storm { case Weibull: if (storm::utility::isOne(secondValDistribution)) { // Weibull distribution reduces to exponential distribution - return builder.addBasicElement(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs + return builder.addBasicElementExponential(parseName(name), firstValDistribution, dormancyFactor, false); // TODO set transient BEs } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Weibull distribution is not supported for basic element '" << name << "' in line " << lineNo << "."); } diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index c9f02b016..23d83fed2 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -93,13 +93,14 @@ namespace storm { ValueType probability = parseRationalExpression(parseJsonNumber(data.at("probability"))); success = builder.addDepElement(name, childNames, probability); } else if (type == "be") { + // TODO support different distributions ValueType failureRate = parseRationalExpression(parseJsonNumber(data.at("rate"))); ValueType dormancyFactor = parseRationalExpression(parseJsonNumber(data.at("dorm"))); bool transient = false; if (data.count("transient") > 0) { transient = data.at("transient"); } - success = builder.addBasicElement(name, failureRate, dormancyFactor, transient); + success = builder.addBasicElementExponential(name, failureRate, dormancyFactor, transient); } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << type << " not recognized."); success = false; diff --git a/src/storm-dft/storage/dft/elements/DFTConst.h b/src/storm-dft/storage/dft/elements/DFTConst.h index 144b5335c..6ff4cd39e 100644 --- a/src/storm-dft/storage/dft/elements/DFTConst.h +++ b/src/storm-dft/storage/dft/elements/DFTConst.h @@ -27,15 +27,20 @@ namespace storm { return mFailed; } - virtual bool isConstant() const { + virtual bool isConstant() const override { return true; } virtual size_t nrChildren() const override { return 0; } - - + + std::string toString() const override { + std::stringstream stream; + stream << *this; + return stream.str(); + } + bool isTypeEqualTo(DFTElement const& other) const override { if(!DFTElement::isTypeEqualTo(other)) return false; DFTConst const& otherCNST = static_cast const&>(other); @@ -43,5 +48,11 @@ namespace storm { } }; + + template + inline std::ostream& operator<<(std::ostream& os, DFTConst const& be) { + return os << "{" << be.name() << "} BE(const " << (be.failed() ? "failed" : "failsafe") << ")"; + } + } }