diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index 8b000ac4d..d70c15ec0 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -15,9 +15,9 @@ namespace storm { for (size_t i = 0; i < mDft.nrElements(); ++i) { std::shared_ptr const> element = mDft.getElement(i); - STORM_LOG_DEBUG("Transform " + element->name()); switch (element->type()) { case storm::storage::DFTElementType::BE_EXP: { + STORM_LOG_DEBUG("Transform " + element->name() + " [BE (exp)]"); auto be_exp = std::static_pointer_cast const>( element); builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), @@ -28,43 +28,58 @@ namespace storm { auto be_const = std::static_pointer_cast const>( element); if (be_const->canFail()) { + STORM_LOG_DEBUG("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 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 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 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 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(element), dep->probability()); break; } case storm::storage::DFTElementType::SEQ: + STORM_LOG_DEBUG("Transform " + element->name() + " [SEQ]"); builder.addSequenceEnforcer(element->name(), getChildrenVector(element)); break; default: @@ -75,6 +90,11 @@ namespace storm { } // At this point the DFT is an exact copy of the original, except for all constant failure probabilities being 0 + if (!failedBEs.empty()) { + builder.addBasicElementConst("Unique_Constant_Failure", true); + failedBEs.insert(std::begin(failedBEs), "Unique_Constant_Failure"); + builder.addDepElement("Failure_Trigger", failedBEs, storm::utility::one()); + } builder.setTopLevel(mDft.getTopLevelGate()->name()); @@ -85,7 +105,6 @@ namespace storm { template std::vector DftTransformator::getChildrenVector( std::shared_ptr const> element) { - STORM_LOG_DEBUG("Get children for " + element->name()); std::vector res; if (element->isDependency()) { // Dependencies have to be handled separately @@ -99,7 +118,6 @@ namespace storm { element); for (auto const &child : elementWithChildren->children()) { res.push_back(child->name()); - STORM_LOG_DEBUG("Got child " + child->name()); } } return res;