|
|
@ -11,6 +11,7 @@ namespace storm { |
|
|
|
template<typename ValueType> |
|
|
|
std::shared_ptr<storm::storage::DFT<ValueType>> |
|
|
|
DftTransformator<ValueType>::transformUniqueFailedBe(storm::storage::DFT<ValueType> const &dft) { |
|
|
|
STORM_LOG_DEBUG("Start transformation UniqueFailedBe"); |
|
|
|
storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true); |
|
|
|
// NOTE: if probabilities for constant BEs are introduced, change this to vector of tuples (name, prob)
|
|
|
|
std::vector<std::string> failedBEs; |
|
|
@ -19,7 +20,6 @@ namespace storm { |
|
|
|
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i); |
|
|
|
switch (element->type()) { |
|
|
|
case storm::storage::DFTElementType::BE_EXP: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]"); |
|
|
|
auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|
|
|
element); |
|
|
|
builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), |
|
|
@ -30,62 +30,47 @@ namespace storm { |
|
|
|
auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|
|
|
element); |
|
|
|
if (be_const->canFail()) { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const failed)]"); |
|
|
|
STORM_LOG_TRACE("Transform " + element->name() + " [BE (const failed)]"); |
|
|
|
failedBEs.push_back(be_const->name()); |
|
|
|
} else { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const failsafe)]"); |
|
|
|
} |
|
|
|
// All original constant BEs are set to failsafe, failed BEs are later triggered by a new element
|
|
|
|
builder.addBasicElementConst(be_const->name(), false); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::AND: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [AND]"); |
|
|
|
builder.addAndElement(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::OR: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [OR]"); |
|
|
|
builder.addOrElement(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::VOT: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [VOT]"); |
|
|
|
auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element); |
|
|
|
builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::PAND: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [PAND]"); |
|
|
|
auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element); |
|
|
|
builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::POR: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [POR]"); |
|
|
|
auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element); |
|
|
|
builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::SPARE: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [SPARE]"); |
|
|
|
builder.addSpareElement(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::PDEP: { |
|
|
|
auto dep = std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>( |
|
|
|
element); |
|
|
|
if (dep->isFDEP()) { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [FDEP]"); |
|
|
|
} else { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]"); |
|
|
|
} |
|
|
|
builder.addDepElement(dep->name(), getChildrenVector(dep), dep->probability()); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::SEQ: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]"); |
|
|
|
builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::MUTEX: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [MUTEX]"); |
|
|
|
builder.addMutex(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
default: |
|
|
@ -99,27 +84,29 @@ namespace storm { |
|
|
|
|
|
|
|
// Introduce new constantly failed BE and FDEPs to trigger all failures
|
|
|
|
if (!failedBEs.empty()) { |
|
|
|
STORM_LOG_TRACE("Add Unique_Constant_Failure [BE (const failed)]"); |
|
|
|
builder.addBasicElementConst("Unique_Constant_Failure", true); |
|
|
|
failedBEs.insert(std::begin(failedBEs), "Unique_Constant_Failure"); |
|
|
|
STORM_LOG_TRACE("Add Failure_Trigger [FDEP]"); |
|
|
|
builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one<ValueType>()); |
|
|
|
} |
|
|
|
|
|
|
|
builder.setTopLevel(dft.getTopLevelGate()->name()); |
|
|
|
|
|
|
|
STORM_LOG_DEBUG("Transformation UniqueFailedBe complete!"); |
|
|
|
STORM_LOG_DEBUG("Transformation UniqueFailedBe complete"); |
|
|
|
return std::make_shared<storm::storage::DFT<ValueType>>(builder.build()); |
|
|
|
} |
|
|
|
|
|
|
|
template<typename ValueType> |
|
|
|
std::shared_ptr<storm::storage::DFT<ValueType>> |
|
|
|
DftTransformator<ValueType>::transformBinaryFDEPs(storm::storage::DFT<ValueType> const &dft) { |
|
|
|
STORM_LOG_DEBUG("Start transformation BinaryFDEPs"); |
|
|
|
storm::builder::DFTBuilder<ValueType> builder = storm::builder::DFTBuilder<ValueType>(true); |
|
|
|
|
|
|
|
for (size_t i = 0; i < dft.nrElements(); ++i) { |
|
|
|
std::shared_ptr<storm::storage::DFTElement<ValueType> const> element = dft.getElement(i); |
|
|
|
switch (element->type()) { |
|
|
|
case storm::storage::DFTElementType::BE_EXP: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]"); |
|
|
|
auto be_exp = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|
|
|
element); |
|
|
|
builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), |
|
|
@ -129,39 +116,32 @@ namespace storm { |
|
|
|
case storm::storage::DFTElementType::BE_CONST: { |
|
|
|
auto be_const = std::static_pointer_cast<storm::storage::BEExponential<ValueType> const>( |
|
|
|
element); |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [BE (const)]"); |
|
|
|
// All original constant BEs are set to failsafe, failed BEs are later triggered by a new element
|
|
|
|
builder.addBasicElementConst(be_const->name(), be_const->canFail()); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::AND: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [AND]"); |
|
|
|
builder.addAndElement(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::OR: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [OR]"); |
|
|
|
builder.addOrElement(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::VOT: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [VOT]"); |
|
|
|
auto vot = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(element); |
|
|
|
builder.addVotElement(vot->name(), vot->threshold(), getChildrenVector(vot)); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::PAND: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [PAND]"); |
|
|
|
auto pand = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(element); |
|
|
|
builder.addPandElement(pand->name(), getChildrenVector(pand), pand->isInclusive()); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::POR: { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [POR]"); |
|
|
|
auto por = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(element); |
|
|
|
builder.addPandElement(por->name(), getChildrenVector(por), por->isInclusive()); |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::SPARE: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [SPARE]"); |
|
|
|
builder.addSpareElement(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::PDEP: { |
|
|
@ -169,11 +149,13 @@ namespace storm { |
|
|
|
element); |
|
|
|
auto children = getChildrenVector(dep); |
|
|
|
if (!storm::utility::isOne(dep->probability())) { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [PDEP]"); |
|
|
|
if (children.size() > 2) { |
|
|
|
STORM_LOG_TRACE("Transform " + element->name() + " [PDEP]"); |
|
|
|
// Introduce additional element for first capturing the probabilistic dependency
|
|
|
|
std::string nameAdditional = dep->name() + "_additional"; |
|
|
|
STORM_LOG_TRACE("Add auxilliary BE " << nameAdditional); |
|
|
|
builder.addBasicElementConst(nameAdditional, false); |
|
|
|
STORM_LOG_TRACE("Add " << dep->name() << "_pdep [PDEP]"); |
|
|
|
// First consider probabilistic dependency
|
|
|
|
builder.addDepElement(dep->name() + "_pdep", {children.front(), nameAdditional}, |
|
|
|
dep->probability()); |
|
|
@ -185,6 +167,7 @@ namespace storm { |
|
|
|
if (builder.nameInUse(nameDep)) { |
|
|
|
STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); |
|
|
|
} |
|
|
|
STORM_LOG_TRACE("Add " << nameDep << " [FDEP]"); |
|
|
|
builder.addDepElement(nameDep, {dep->name() + "_additional", child}, |
|
|
|
storm::utility::one<ValueType>()); |
|
|
|
++i; |
|
|
@ -193,7 +176,6 @@ namespace storm { |
|
|
|
builder.addDepElement(dep->name(), children, dep->probability()); |
|
|
|
} |
|
|
|
} else { |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [FDEP]"); |
|
|
|
// Add dependencies
|
|
|
|
for (size_t i = 1; i < children.size(); ++i) { |
|
|
|
std::string nameDep; |
|
|
@ -201,6 +183,8 @@ namespace storm { |
|
|
|
nameDep = dep->name(); |
|
|
|
} else { |
|
|
|
nameDep = dep->name() + "_" + std::to_string(i); |
|
|
|
STORM_LOG_TRACE("Transform " + element->name() + " [FDEP]"); |
|
|
|
STORM_LOG_TRACE("Add " + nameDep + " [FDEP]"); |
|
|
|
} |
|
|
|
if (builder.nameInUse(nameDep)) { |
|
|
|
STORM_LOG_ERROR("Element with name '" << nameDep << "' already exists."); |
|
|
@ -214,11 +198,9 @@ namespace storm { |
|
|
|
break; |
|
|
|
} |
|
|
|
case storm::storage::DFTElementType::SEQ: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]"); |
|
|
|
builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
case storm::storage::DFTElementType::MUTEX: |
|
|
|
STORM_LOG_DEBUG("Transform " + element->name() + " [MUTEX]"); |
|
|
|
builder.addMutex(element->name(), getChildrenVector(element)); |
|
|
|
break; |
|
|
|
default: |
|
|
@ -231,7 +213,7 @@ namespace storm { |
|
|
|
|
|
|
|
builder.setTopLevel(dft.getTopLevelGate()->name()); |
|
|
|
|
|
|
|
STORM_LOG_DEBUG("Transformation BinaryFDEPs complete!"); |
|
|
|
STORM_LOG_DEBUG("Transformation BinaryFDEPs complete"); |
|
|
|
return std::make_shared<storm::storage::DFT<ValueType>>(builder.build()); |
|
|
|
} |
|
|
|
|
|
|
|