diff --git a/src/storm-dft/transformations/DftTransformator.cpp b/src/storm-dft/transformations/DftTransformator.cpp index 97428b6b6..473f4249b 100644 --- a/src/storm-dft/transformations/DftTransformator.cpp +++ b/src/storm-dft/transformations/DftTransformator.cpp @@ -11,6 +11,7 @@ namespace storm { template std::shared_ptr> DftTransformator::transformUniqueFailedBe(storm::storage::DFT const &dft) { + STORM_LOG_DEBUG("Start transformation UniqueFailedBe"); storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true); // NOTE: if probabilities for constant BEs are introduced, change this to vector of tuples (name, prob) std::vector failedBEs; @@ -19,7 +20,6 @@ namespace storm { std::shared_ptr 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 const>( element); builder.addBasicElementExponential(be_exp->name(), be_exp->activeFailureRate(), @@ -30,62 +30,47 @@ namespace storm { auto be_const = std::static_pointer_cast 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 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(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()); } builder.setTopLevel(dft.getTopLevelGate()->name()); - STORM_LOG_DEBUG("Transformation UniqueFailedBe complete!"); + STORM_LOG_DEBUG("Transformation UniqueFailedBe complete"); return std::make_shared>(builder.build()); } template std::shared_ptr> DftTransformator::transformBinaryFDEPs(storm::storage::DFT const &dft) { + STORM_LOG_DEBUG("Start transformation BinaryFDEPs"); storm::builder::DFTBuilder builder = storm::builder::DFTBuilder(true); for (size_t i = 0; i < dft.nrElements(); ++i) { std::shared_ptr 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 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 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 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: { @@ -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()); ++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>(builder.build()); }