diff --git a/src/storm-dft/generator/DftNextStateGenerator.cpp b/src/storm-dft/generator/DftNextStateGenerator.cpp index 245a448ef..7b86d1faa 100644 --- a/src/storm-dft/generator/DftNextStateGenerator.cpp +++ b/src/storm-dft/generator/DftNextStateGenerator.cpp @@ -112,7 +112,7 @@ namespace storm { newState->updateFailableDependencies(next->id()); } - if(newState->isInvalid()) { + if(newState->isInvalid() || (nextBE->isTransient() && !newState->hasFailed(mDft.getTopLevelIndex()))) { // Continue with next possible state ++currentFailable; continue; diff --git a/src/storm-dft/parser/DFTGalileoParser.cpp b/src/storm-dft/parser/DFTGalileoParser.cpp index 38dec9bf0..c81c2767a 100644 --- a/src/storm-dft/parser/DFTGalileoParser.cpp +++ b/src/storm-dft/parser/DFTGalileoParser.cpp @@ -124,7 +124,7 @@ namespace storm { } else if (boost::starts_with(tokens[1], "lambda=")) { ValueType failureRate = parseRationalExpression(tokens[1].substr(7)); ValueType dormancyFactor = parseRationalExpression(tokens[2].substr(5)); - success = builder.addBasicElement(name, failureRate, dormancyFactor); + success = builder.addBasicElement(name, failureRate, dormancyFactor, false); // TODO set transient BEs } else { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Type name: " << tokens[1] << " not recognized."); success = false; diff --git a/src/storm-dft/parser/DFTJsonParser.cpp b/src/storm-dft/parser/DFTJsonParser.cpp index ac4e094ff..0d6f312f2 100644 --- a/src/storm-dft/parser/DFTJsonParser.cpp +++ b/src/storm-dft/parser/DFTJsonParser.cpp @@ -100,7 +100,11 @@ namespace storm { } else if (type == "be") { ValueType failureRate = parseRationalExpression(data.at("rate")); ValueType dormancyFactor = parseRationalExpression(data.at("dorm")); - success = builder.addBasicElement(name, failureRate, dormancyFactor); + bool transient = false; + if (data.count("transient") > 0) { + transient = data.at("transient"); + } + success = builder.addBasicElement(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/DFTBuilder.cpp b/src/storm-dft/storage/dft/DFTBuilder.cpp index 66beaa387..88abc9665 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.cpp +++ b/src/storm-dft/storage/dft/DFTBuilder.cpp @@ -272,7 +272,7 @@ namespace storm { if (be->canFail()) { dormancyFactor = be->passiveFailureRate() / be->activeFailureRate(); } - addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor); + addBasicElement(be->name(), be->activeFailureRate(), dormancyFactor, be->isTransient()); break; } case DFTElementType::CONSTF: diff --git a/src/storm-dft/storage/dft/DFTBuilder.h b/src/storm-dft/storage/dft/DFTBuilder.h index 598c1d765..42713e601 100644 --- a/src/storm-dft/storage/dft/DFTBuilder.h +++ b/src/storm-dft/storage/dft/DFTBuilder.h @@ -105,7 +105,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()); + addBasicElement(nameAdditional, storm::utility::zero(), storm::utility::zero(), false); // First consider probabilistic dependency addDepElement(name + "_pdep", {children.front(), nameAdditional}, probability); // Then consider dependencies to the children if probabilistic dependency failed @@ -168,12 +168,12 @@ namespace storm { return true; } - bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor) { + bool addBasicElement(std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) { //TODO Matthias: collect constraints for SMT solving //failureRate > 0 //0 <= dormancyFactor <= 1 - mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor); + mElements[name] = std::make_shared>(mNextId++, name, failureRate, dormancyFactor, transient); return true; } diff --git a/src/storm-dft/storage/dft/elements/DFTBE.h b/src/storm-dft/storage/dft/elements/DFTBE.h index 3be82d9f1..6bb234b4e 100644 --- a/src/storm-dft/storage/dft/elements/DFTBE.h +++ b/src/storm-dft/storage/dft/elements/DFTBE.h @@ -11,10 +11,11 @@ namespace storm { ValueType mActiveFailureRate; ValueType mPassiveFailureRate; DFTDependencyVector mIngoingDependencies; + bool mTransient; public: - DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor) : - DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate) + DFTBE(size_t id, std::string const& name, ValueType failureRate, ValueType dormancyFactor, bool transient = false) : + DFTElement(id, name), mActiveFailureRate(failureRate), mPassiveFailureRate(dormancyFactor * failureRate), mTransient(transient) {} DFTElementType type() const override { @@ -32,6 +33,10 @@ namespace storm { ValueType const& passiveFailureRate() const { return mPassiveFailureRate; } + + bool isTransient() const { + return mTransient; + } bool canFail() const { return !storm::utility::isZero(mActiveFailureRate);