From ec8304c38650936e8873de633a0261d8bedcda26 Mon Sep 17 00:00:00 2001 From: Matthias Volk Date: Thu, 1 Feb 2018 18:07:28 +0100 Subject: [PATCH] Refactored DftToGspnTransformator --- .../DftToGspnTransformator.cpp | 733 +++++++++--------- .../transformations/DftToGspnTransformator.h | 184 +++-- 2 files changed, 469 insertions(+), 448 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index bd8fe53b9..7a2b0f360 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -20,66 +20,65 @@ namespace storm { this->smart = smart; builder.setGspnName("DftToGspnTransformation"); - // Loop through every DFT element and draw them as a GSPN. - drawGSPNElements(); + // Translate all GSPN elements + translateGSPNElements(); - // Draw restrictions into the GSPN (i.e. SEQ or MUTEX). + // Create initial template // TODO - //drawGSPNRestrictions(); } template uint64_t DftToGspnTransformator::toplevelFailedPlaceId() { - assert(failedNodes.size() > mDft.getTopLevelIndex()); - return failedNodes[mDft.getTopLevelIndex()]; + STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(), "Failed place for top level element does not exist."); + return failedPlaces.at(mDft.getTopLevelIndex()); + } + + template + gspn::GSPN* DftToGspnTransformator::obtainGSPN() { + return builder.buildGspn(); } template - void DftToGspnTransformator::drawGSPNElements() { - - // Loop through every DFT element and draw them as a GSPN. - for (std::size_t i = 0; i < mDft.nrElements(); i++) { + void DftToGspnTransformator::translateGSPNElements() { + // Loop through every DFT element and create its corresponding GSPN template. + for (std::size_t i = 0; i < mDft.nrElements(); i++) { auto dftElement = mDft.getElement(i); - bool isRepresentative = mDft.isRepresentative(i); - - // Check which type the element is and call the corresponding drawing-function. + + // Check which type the element is and call the corresponding translate-function. switch (dftElement->type()) { - case storm::storage::DFTElementType::AND: - drawAND(std::static_pointer_cast const>(dftElement), isRepresentative); + case storm::storage::DFTElementType::BE: + translateBE(std::static_pointer_cast const>(dftElement)); + break; + case storm::storage::DFTElementType::CONSTF: + translateCONSTF(dftElement); + break; + case storm::storage::DFTElementType::CONSTS: + translateCONSTS(dftElement); + break; + case storm::storage::DFTElementType::AND: + translateAND(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::OR: - drawOR(std::static_pointer_cast const>(dftElement), isRepresentative); + translateOR(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::VOT: - drawVOT(std::static_pointer_cast const>(dftElement), isRepresentative); + translateVOT(std::static_pointer_cast const>(dftElement)); break; case storm::storage::DFTElementType::PAND: - drawPAND(std::static_pointer_cast const>(dftElement), isRepresentative); + translatePAND(std::static_pointer_cast const>(dftElement), std::static_pointer_cast const>(dftElement)->isInclusive()); break; + case storm::storage::DFTElementType::POR: + translatePOR(std::static_pointer_cast const>(dftElement), std::static_pointer_cast const>(dftElement)->isInclusive()); + break; case storm::storage::DFTElementType::SPARE: - drawSPARE(std::static_pointer_cast const>(dftElement), isRepresentative); - break; - case storm::storage::DFTElementType::POR: - drawPOR(std::static_pointer_cast const>(dftElement), isRepresentative); + translateSPARE(std::static_pointer_cast const>(dftElement)); break; + case storm::storage::DFTElementType::PDEP: + translatePDEP(std::static_pointer_cast const>(dftElement)); + break; case storm::storage::DFTElementType::SEQ: - drawSeq(std::static_pointer_cast const>(dftElement)); + translateSeq(std::static_pointer_cast const>(dftElement)); break; - case storm::storage::DFTElementType::MUTEX: - // No method call needed here. MUTEX only consists of restrictions, which are handled later. - break; - case storm::storage::DFTElementType::BE: - drawBE(std::static_pointer_cast const>(dftElement), isRepresentative); - break; - case storm::storage::DFTElementType::CONSTF: - drawCONSTF(dftElement, isRepresentative); - break; - case storm::storage::DFTElementType::CONSTS: - drawCONSTS(dftElement, isRepresentative); - break; - case storm::storage::DFTElementType::PDEP: - drawPDEP(std::static_pointer_cast const>(dftElement)); - break; default: STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown."); break; @@ -89,282 +88,282 @@ namespace storm { } template - void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE, bool isRepresentative) { - uint64_t beActive = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); - activeNodes.emplace(dftBE->id(), beActive); - uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); - + void DftToGspnTransformator::translateBE(std::shared_ptr const> dftBE) { double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; - builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); - builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); - - uint64_t disabledNode = 0; - if (!smart || dftBE->nrRestrictions() > 0) { - disabledNode = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter-9.0, ycenter)); - } - - uint64_t unavailableNode = 0; - if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter)); - } - - assert(failedNodes.size() == dftBE->id()); - failedNodes.push_back(beFailed); + + uint64_t failedPlace = addFailedPlace(dftBE, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); + + uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); + activePlaces.emplace(dftBE->id(), activePlace); + builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); + uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing"); builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); - builder.addInputArc(beActive, tActive); - builder.addInhibitionArc(beFailed, tActive); - builder.addOutputArc(tActive, beActive); - builder.addOutputArc(tActive, beFailed); + builder.addInputArc(activePlace, tActive); + builder.addInhibitionArc(failedPlace, tActive); + builder.addOutputArc(tActive, activePlace); + builder.addOutputArc(tActive, failedPlace); + uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing"); builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); - builder.addInhibitionArc(beActive, tPassive); - builder.addInhibitionArc(beFailed, tPassive); - builder.addOutputArc(tPassive, beFailed); + builder.addInhibitionArc(activePlace, tPassive); + builder.addInhibitionArc(failedPlace, tPassive); + builder.addOutputArc(tPassive, failedPlace); if (!smart || dftBE->nrRestrictions() > 0) { - builder.addInhibitionArc(disabledNode, tActive); - builder.addInhibitionArc(disabledNode, tPassive); + uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter-9.0, ycenter)); + builder.addInhibitionArc(disabledPlace, tActive); + builder.addInhibitionArc(disabledPlace, tPassive); } - if (!smart || isRepresentative) { - builder.addOutputArc(tActive, unavailableNode); - builder.addOutputArc(tPassive, unavailableNode); + if (!smart || mDft.isRepresentative(dftBE->id())) { + uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter)); + builder.addOutputArc(tActive, unavailablePlace); + builder.addOutputArc(tPassive, unavailablePlace); + } + } + + template + void DftToGspnTransformator::translateCONSTF(std::shared_ptr const> dftConstF) { + double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y; + + addFailedPlace(dftConstF, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0), true); + + if (!smart || mDft.isRepresentative(dftConstF->id())) { + addUnavailablePlace(dftConstF, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0), false); + } + } + + template + void DftToGspnTransformator::translateCONSTS(std::shared_ptr const> dftConstS) { + double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x; + double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y; + + size_t capacity = 0; // It cannot contain a token, because it cannot fail. + + uint64_t failedPlace = builder.addPlace(capacity, 0, dftConstS->name() + STR_FAILED); + assert(failedPlaces.size() == dftConstS->id()); + failedPlaces.push_back(failedPlace); + builder.setPlaceLayoutInfo(failedPlace, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); + + if (!smart || mDft.isRepresentative(dftConstS->id())) { + uint64_t unavailablePlace = builder.addPlace(capacity, 0, dftConstS->name() + "_unavail"); + unavailablePlaces.emplace(dftConstS->id(), unavailablePlace); + builder.setPlaceLayoutInfo(unavailablePlace, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); } } - - template - void DftToGspnTransformator::drawAND(std::shared_ptr const> dftAnd, bool isRepresentative) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED); - assert(failedNodes.size() == dftAnd->id()); - failedNodes.push_back(nodeFailed); + template + void DftToGspnTransformator::translateAND(std::shared_ptr const> dftAnd) { double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); - uint64_t unavailableNode = 0; - if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); - } + uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); - - uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING ); - builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); - builder.addInhibitionArc(nodeFailed, tAndFailed); - builder.addOutputArc(tAndFailed, nodeFailed); - if (!smart || isRepresentative) { - builder.addOutputArc(tAndFailed, unavailableNode); + uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING ); + builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); + builder.addInhibitionArc(failedPlace, tFailed); + builder.addOutputArc(tFailed, failedPlace); + + if (!smart || mDft.isRepresentative(dftAnd->id())) { + uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); + builder.addOutputArc(tFailed, unavailablePlace); } + for (auto const& child : dftAnd->children()) { - assert(failedNodes.size() > child->id()); - builder.addInputArc(failedNodes[child->id()], tAndFailed); - builder.addOutputArc(tAndFailed, failedNodes[child->id()]); + builder.addInputArc(getFailedPlace(child), tFailed); + builder.addOutputArc(tFailed, getFailedPlace(child)); } } template - void DftToGspnTransformator::drawOR(std::shared_ptr const> dftOr, bool isRepresentative) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED); - assert(failedNodes.size() == dftOr->id()); - failedNodes.push_back(nodeFailed); - + void DftToGspnTransformator::translateOR(std::shared_ptr const> dftOr) { double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x; double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y; - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); - uint64_t unavailableNode = 0; + uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); + + bool isRepresentative = mDft.isRepresentative(dftOr->id()); + uint64_t unavailablePlace = 0; if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); + unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); } - uint64_t i = 0; - for (auto const& child : dftOr->children()) { - uint64_t tNodeFailed = builder.addImmediateTransition( getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i) ); - builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0)); - builder.addInhibitionArc(nodeFailed, tNodeFailed); - builder.addOutputArc(tNodeFailed, nodeFailed); + for (size_t i = 0; i < dftOr->nrChildren(); ++i) { + auto const& child = dftOr->children().at(i); + uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i) ); + builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0)); + builder.addInhibitionArc(failedPlace, tFailed); + builder.addOutputArc(tFailed, failedPlace); if (!smart || isRepresentative) { - builder.addOutputArc(tNodeFailed, unavailableNode); + builder.addOutputArc(tFailed, unavailablePlace); } - assert(failedNodes.size() > child->id()); - builder.addInputArc(failedNodes[child->id()], tNodeFailed); - builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); - ++i; + builder.addInputArc(getFailedPlace(child), tFailed); + builder.addOutputArc(tFailed, getFailedPlace(child)); } } template - void DftToGspnTransformator::drawVOT(std::shared_ptr const> dftVot, bool isRepresentative) { + void DftToGspnTransformator::translateVOT(std::shared_ptr const> dftVot) { // TODO: finish layouting - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED); - assert(failedNodes.size() == dftVot->id()); - failedNodes.push_back(nodeFailed); double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x; double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y; - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); - uint64_t unavailableNode = 0; - if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftVot, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); - } - - uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector"); - builder.setPlaceLayoutInfo(nodeCollector, storm::gspn::LayoutInfo(xcenter, ycenter)); + uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); - uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING); - builder.addOutputArc(tNodeFailed, nodeFailed); - if (!smart || isRepresentative) { - builder.addOutputArc(tNodeFailed, unavailableNode); + uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING); + builder.addOutputArc(tFailed, failedPlace); + builder.addInhibitionArc(failedPlace, tFailed); + + if (!smart || mDft.isRepresentative(dftVot->id())) { + uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); + builder.addOutputArc(tFailed, unavailablePlace); } - builder.addInhibitionArc(nodeFailed, tNodeFailed); - builder.addInputArc(nodeCollector, tNodeFailed, dftVot->threshold()); - uint64_t i = 0; - for (auto const& child : dftVot->children()) { - uint64_t childInhibPlace = builder.addPlace(1, 0, dftVot->name() + "_child_fail_inhib" + std::to_string(i)); + + uint64_t collectorPlace = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector"); + builder.setPlaceLayoutInfo(collectorPlace, storm::gspn::LayoutInfo(xcenter, ycenter)); + builder.addInputArc(collectorPlace, tFailed, dftVot->threshold()); + + for (size_t i = 0; i < dftVot->nrChildren(); ++i) { + auto const& child = dftVot->children().at(i); + uint64_t childNextPlace = builder.addPlace(defaultCapacity, 1, dftVot->name() + "_child_next" + std::to_string(i)); + uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i)); - builder.addOutputArc(tCollect, nodeCollector); - builder.addOutputArc(tCollect, childInhibPlace); - builder.addInhibitionArc(childInhibPlace, tCollect); - builder.addInputArc(failedNodes[child->id()], tCollect); - builder.addOutputArc(tCollect, failedNodes[child->id()]); - ++i; + builder.addOutputArc(tCollect, collectorPlace); + builder.addInputArc(childNextPlace, tCollect); + builder.addInputArc(getFailedPlace(child), tCollect); + builder.addOutputArc(tCollect, getFailedPlace(child)); } } template - void DftToGspnTransformator::drawPAND(std::shared_ptr const> dftPand, bool isRepresentative) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED); - assert(failedNodes.size() == dftPand->id()); - failedNodes.push_back(nodeFailed); - + void DftToGspnTransformator::translatePAND(std::shared_ptr const> dftPand, bool inclusive) { double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x; double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y; - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); - uint64_t unavailableNode = 0; - if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftPand, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); - } - - uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING); - builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0)); - builder.addInhibitionArc(nodeFailed, tNodeFailed); - builder.addOutputArc(tNodeFailed, nodeFailed); - if (!smart || isRepresentative) { - builder.addOutputArc(tNodeFailed, unavailableNode); + uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); + + uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING); + builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0)); + builder.addInhibitionArc(failedPlace, tFailed); + builder.addOutputArc(tFailed, failedPlace); + + if (!smart || mDft.isRepresentative(dftPand->id())) { + uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); + builder.addOutputArc(tFailed, unavailablePlace); } - if(dftPand->isInclusive()) { + if (inclusive) { // Inclusive PAND - uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE); - builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); + uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE); + builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); - builder.addInhibitionArc(nodeFS, tNodeFailed); - // Transition for failed + builder.addInhibitionArc(failSafePlace, tFailed); + + // Transitions for failed place for (auto const& child : dftPand->children()) { - builder.addInputArc(failedNodes[child->id()], tNodeFailed); - builder.addOutputArc(tNodeFailed, failedNodes[child->id()]); + builder.addInputArc(getFailedPlace(child), tFailed); + builder.addOutputArc(tFailed, getFailedPlace(child)); } - // Transitions for fail-safe - for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) { - uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j)); - builder.setTransitionLayoutInfo(tfs, storm::gspn::LayoutInfo(xcenter-6.0+j*3.0, ycenter+3.0)); - - builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); - builder.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]); - builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); - builder.addOutputArc(tfs, nodeFS); - builder.addInhibitionArc(nodeFS, tfs); - + // Transitions for fail-safe place + for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) { + auto const& child = dftPand->children().at(i); + uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(i)); + builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter-6.0+i*3.0, ycenter+3.0)); + + builder.addInputArc(getFailedPlace(child), tFailSafe); + builder.addOutputArc(tFailSafe, getFailedPlace(child)); + builder.addInhibitionArc(getFailedPlace(dftPand->children().at(i-1)), tFailSafe); + builder.addOutputArc(tFailSafe, failSafePlace); + builder.addInhibitionArc(failSafePlace, tFailSafe); } } else { // Exclusive PAND - uint64_t fi = 0; - uint64_t tn = 0; - for(uint64_t j = 0; j < dftPand->nrChildren(); ++j) { - auto const& child = dftPand->children()[j]; - if (j > 0) { - builder.addInhibitionArc(failedNodes.at(child->id()), tn); + uint64_t failSafeXPlace = 0; + uint64_t tFailSafeX = 0; + for (size_t i = 0; i < dftPand->nrChildren(); ++i) { + auto const& child = dftPand->children().at(i); + + if (i > 0) { + // Set inhibition arc to previous transition + builder.addInhibitionArc(getFailedPlace(child), tFailSafeX); } - if (j != dftPand->nrChildren() - 1) { + + if (i < dftPand->nrChildren() - 1) { // Not last child - tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j)); - builder.setTransitionLayoutInfo(tn, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0)); + tFailSafeX = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(i)); + builder.setTransitionLayoutInfo(tFailSafeX, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0)); } else { // Last child - tn = tNodeFailed; + tFailSafeX = tFailed; } - builder.addInputArc(failedNodes.at(child->id()), tn); - builder.addOutputArc(tn, failedNodes.at(child->id())); - if (j > 0) { - builder.addInputArc(fi, tn); + builder.addInputArc(getFailedPlace(child), tFailSafeX); + builder.addOutputArc(tFailSafeX, getFailedPlace(child)); + + if (i > 0) { + builder.addInputArc(failSafeXPlace, tFailSafeX); } - if (j != dftPand->nrChildren() - 1) { - fi = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(j)); - builder.setPlaceLayoutInfo(fi, storm::gspn::LayoutInfo(xcenter-3.0+j*3.0, ycenter)); - builder.addOutputArc(tn, fi); + + if (i < dftPand->nrChildren() - 1) { + // Add fail-safe X place + failSafeXPlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(i)); + builder.setPlaceLayoutInfo(failSafeXPlace, storm::gspn::LayoutInfo(xcenter-3.0+i*3.0, ycenter)); + builder.addOutputArc(tFailSafeX, failSafeXPlace); + builder.addInhibitionArc(failSafeXPlace, tFailSafeX); } - } } } template - void DftToGspnTransformator::drawPOR(std::shared_ptr const> dftPor, bool isRepresentative) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILED); - failedNodes.push_back(nodeFailed); - + void DftToGspnTransformator::translatePOR(std::shared_ptr const> dftPor, bool inclusive) { double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x; double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y; - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); - uint64_t unavailableNode = 0; - if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); - } + uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); - uint64_t tfail = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING); - builder.setTransitionLayoutInfo(tfail, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0)); - builder.addOutputArc(tfail, nodeFailed); - builder.addInhibitionArc(nodeFailed, tfail); + uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING); + builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0)); + builder.addOutputArc(tFailed, failedPlace); + builder.addInhibitionArc(failedPlace, tFailed); - builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail); - builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id())); + // Arcs from first child + builder.addInputArc(getFailedPlace(dftPor->children().front()), tFailed); + builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front())); - if(!smart || isRepresentative) { - builder.addOutputArc(tfail, unavailableNode); + if (!smart || mDft.isRepresentative(dftPor->id())) { + uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); + builder.addOutputArc(tFailed, unavailablePlace); } - if(dftPor->isInclusive()) { + if (inclusive) { // Inclusive POR - uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); - builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); - - builder.addInhibitionArc(nodeFS, tfail); - uint64_t j = 0; - for (auto const& child : dftPor->children()) { - if(j > 0) { - uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); - builder.setTransitionLayoutInfo(tfailsf, storm::gspn::LayoutInfo(xcenter-3.0+j*3.0, ycenter+3.0)); - builder.addInputArc(failedNodes.at(child->id()), tfailsf); - builder.addOutputArc(tfailsf, failedNodes.at(child->id())); - builder.addOutputArc(tfailsf, nodeFS); - builder.addInhibitionArc(nodeFS, tfailsf); - builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf); - } - ++j; + uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); + builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); + + builder.addInhibitionArc(failSafePlace, tFailed); + + // For all children except the first one + for (size_t i = 1; i < dftPor->nrChildren(); ++i) { + auto const& child = dftPor->children().at(i); + uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(i)); + builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter-3.0+i*3.0, ycenter+3.0)); + + builder.addInputArc(getFailedPlace(child), tFailSafe); + builder.addOutputArc(tFailSafe, getFailedPlace(child)); + builder.addOutputArc(tFailSafe, failSafePlace); + builder.addInhibitionArc(failSafePlace, tFailSafe); + builder.addInhibitionArc(getFailedPlace(dftPor->children().front()), tFailSafe); } } else { // Exclusive POR - uint64_t j = 0; + + // For all children except the first one for (auto const& child : dftPor->children()) { - if(j > 0) { - builder.addInhibitionArc(failedNodes.at(child->id()), tfail); - } - ++j; + builder.addInhibitionArc(getFailedPlace(child), tFailed); } } @@ -372,212 +371,199 @@ namespace storm { } template - void DftToGspnTransformator::drawSPARE(std::shared_ptr const> dftSpare, bool isRepresentative) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_FAILED); - failedNodes.push_back(nodeFailed); - + void DftToGspnTransformator::translateSPARE(std::shared_ptr const> dftSpare) { double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x; double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y; - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); - uint64_t unavailableNode = 0; + uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); + + bool isRepresentative = mDft.isRepresentative(dftSpare->id()); + uint64_t unavailablePlace = 0; if (!smart || isRepresentative) { - unavailableNode = addUnavailableNode(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); + unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); } - uint64_t spareActive = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED); - builder.setPlaceLayoutInfo(spareActive, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-12.0)); - activeNodes.emplace(dftSpare->id(), spareActive); + + uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED); + builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-12.0)); + activePlaces.emplace(dftSpare->id(), activePlace); - std::vector nextclTransitions; - std::vector nextconsiderTransitions; - uint64_t j = 0; - for(auto const& child : dftSpare->children()) { + std::vector tNextClaims; + std::vector tNextConsiders; + for (size_t i = 0; i < dftSpare->nrChildren(); ++i) { + auto const& child = dftSpare->children().at(i); // Consider next child - size_t nodeConsider = builder.addPlace(defaultCapacity, j == 0 ? 1 : 0, dftSpare->name()+ "_consider_" + child->name()); - builder.setPlaceLayoutInfo(nodeConsider, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter-8.0)); + size_t considerPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSpare->name()+ "_consider_" + child->name()); + builder.setPlaceLayoutInfo(considerPlace, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter-8.0)); - if (j > 0) { + if (i > 0) { // Set output transition from previous next_claim - builder.addOutputArc(nextclTransitions.back(), nodeConsider); + builder.addOutputArc(tNextClaims.back(), considerPlace); // Set output transition from previous cannot_claim - builder.addOutputArc(nextconsiderTransitions.back(), nodeConsider); + builder.addOutputArc(tNextConsiders.back(), considerPlace); } // Cannot claim child - uint64_t tnextconsider = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name()); - builder.setTransitionLayoutInfo(tnextconsider, storm::gspn::LayoutInfo(xcenter-7.0+j*14.0, ycenter-8.0)); - builder.addInputArc(nodeConsider, tnextconsider); - builder.addInputArc(unavailableNodes.at(child->id()), tnextconsider); - builder.addOutputArc(tnextconsider, unavailableNodes.at(child->id())); - nextconsiderTransitions.push_back(tnextconsider); + uint64_t tConsiderNext = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name()); + builder.setTransitionLayoutInfo(tConsiderNext, storm::gspn::LayoutInfo(xcenter-7.0+i*14.0, ycenter-8.0)); + builder.addInputArc(considerPlace, tConsiderNext); + builder.addInputArc(unavailablePlaces.at(child->id()), tConsiderNext); + builder.addOutputArc(tConsiderNext, unavailablePlaces.at(child->id())); + tNextConsiders.push_back(tConsiderNext); // Claimed child - size_t nodeCUC = builder.addPlace(defaultCapacity, 0, dftSpare->name() + "_claimed_" + child->name()); - builder.setPlaceLayoutInfo(nodeCUC, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter+5.0)); - uint64_t tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); - builder.setTransitionLayoutInfo(tclaim, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter)); - builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim); - builder.addInputArc(nodeConsider, tclaim); - builder.addOutputArc(tclaim, nodeCUC); - builder.addOutputArc(tclaim, unavailableNodes.at(child->id())); + size_t claimedPlace = builder.addPlace(defaultCapacity, 0, dftSpare->name() + "_claimed_" + child->name()); + builder.setPlaceLayoutInfo(claimedPlace, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter+5.0)); + uint64_t tClaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); + builder.setTransitionLayoutInfo(tClaim, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter)); + builder.addInhibitionArc(unavailablePlaces.at(child->id()), tClaim); + builder.addInputArc(considerPlace, tClaim); + builder.addOutputArc(tClaim, claimedPlace); + builder.addOutputArc(tClaim, unavailablePlaces.at(child->id())); // Claim next - uint64_t tnextcl = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(j)); - builder.setTransitionLayoutInfo(tnextcl, storm::gspn::LayoutInfo(xcenter-7.0+j*14.0, ycenter+5.0)); - builder.addInputArc(nodeCUC, tnextcl); - builder.addInputArc(failedNodes.at(child->id()), tnextcl); - builder.addOutputArc(tnextcl, failedNodes.at(child->id())); - nextclTransitions.push_back(tnextcl); - - ++j; - // Activate all nodes in spare module + uint64_t tClaimNext = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(i)); + builder.setTransitionLayoutInfo(tClaimNext, storm::gspn::LayoutInfo(xcenter-7.0+i*14.0, ycenter+5.0)); + builder.addInputArc(claimedPlace, tClaimNext); + builder.addInputArc(getFailedPlace(child), tClaimNext); + builder.addOutputArc(tClaimNext, getFailedPlace(child)); + tNextClaims.push_back(tClaimNext); + + // Activate all elements in spare module uint64_t l = 0; for (uint64_t k : mDft.module(child->id())) { - uint64_t tactive = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(j) + "_" + std::to_string(k)); - builder.setTransitionLayoutInfo(tactive, storm::gspn::LayoutInfo(xcenter-18.0+(j+l)*3, ycenter-12.0)); - builder.addInhibitionArc(activeNodes.at(k), tactive); - builder.addInputArc(nodeCUC, tactive); - builder.addInputArc(spareActive, tactive); - builder.addOutputArc(tactive, nodeCUC); - builder.addOutputArc(tactive, spareActive); - builder.addOutputArc(tactive, activeNodes.at(k)); + uint64_t tActivate = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(i) + "_" + std::to_string(k)); + builder.setTransitionLayoutInfo(tActivate, storm::gspn::LayoutInfo(xcenter-18.0+(i+l)*3, ycenter-12.0)); + builder.addInhibitionArc(activePlaces.at(k), tActivate); + builder.addInputArc(claimedPlace, tActivate); + builder.addInputArc(activePlace, tActivate); + builder.addOutputArc(tActivate, claimedPlace); + builder.addOutputArc(tActivate, activePlace); + builder.addOutputArc(tActivate, activePlaces.at(k)); ++l; } } // Set arcs to failed - builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); - builder.addOutputArc(nextclTransitions.back(), nodeFailed); + builder.addOutputArc(tNextConsiders.back(), failedPlace); + builder.addOutputArc(tNextClaims.back(), failedPlace); if (!smart || isRepresentative) { - builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); - builder.addOutputArc(nextclTransitions.back(), unavailableNode); + builder.addOutputArc(tNextConsiders.back(), unavailablePlace); + builder.addOutputArc(tNextClaims.back(), unavailablePlace); } } template - void DftToGspnTransformator::drawCONSTF(std::shared_ptr const> dftConstF, bool isRepresentative) { - failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED)); - uint64_t unavailableNode = 0; - if (isRepresentative) { - // TODO set position - unavailableNode = addUnavailableNode(dftConstF, storm::gspn::LayoutInfo(0, 0), false); - } - - } -// - template - void DftToGspnTransformator::drawCONSTS(std::shared_ptr const> dftConstS, bool isRepresentative) { -// storm::gspn::Place placeCONSTSFailed; -// placeCONSTSFailed.setName(dftConstS->name() + STR_FAILED); -// placeCONSTSFailed.setNumberOfInitialTokens(0); -// placeCONSTSFailed.setCapacity(0); // It cannot contain a token, because it cannot fail. -// mGspn.addPlace(placeCONSTSFailed); - } -// - template - void DftToGspnTransformator::drawPDEP(std::shared_ptr const> dftDependency) { + void DftToGspnTransformator::translatePDEP(std::shared_ptr const> dftDependency) { double xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x; double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y; if (!smart) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftDependency->name() + STR_FAILED); - failedNodes.push_back(nodeFailed); - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); - addUnavailableNode(dftDependency, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); + addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); + addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); } - uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin"); - builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0)); - uint64_t t1 = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip"); - - builder.addInputArc(coinPlace, t1); - builder.addInputArc(failedNodes.at(dftDependency->triggerEvent()->id()), t1); - builder.addOutputArc(t1, failedNodes.at(dftDependency->triggerEvent()->id())); - uint64_t forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward"); - builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0)); - - if (!smart || dftDependency->probability() < 1.0) { + uint64_t forwardPlace = 0; + if (dftDependency->probability() < 1.0) { + // PDEP + forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward"); + builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0)); + + uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin"); + builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0)); + + uint64_t tStartFlip = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip"); + builder.addInputArc(coinPlace, tStartFlip); + builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip); + builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent())); + uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip"); - builder.addOutputArc(t1, flipPlace); - builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0)); - uint64_t t2 = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip"); - builder.addInputArc(flipPlace, t2); - builder.addOutputArc(t2, forwardPlace); - if (dftDependency->probability() < 1.0) { - uint64_t t3 = builder.addImmediateTransition(defaultPriority, 1 - dftDependency->probability(), "_loose_flip"); - builder.addInputArc(flipPlace, t3); - } + builder.addOutputArc(tStartFlip, flipPlace); + + uint64_t tWinFlip = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip"); + builder.addInputArc(flipPlace, tWinFlip); + builder.addOutputArc(tWinFlip, forwardPlace); + + uint64_t tLooseFlip = builder.addImmediateTransition(defaultPriority, storm::utility::one() - dftDependency->probability(), "_loose_flip"); + builder.addInputArc(flipPlace, tLooseFlip); } else { - builder.addOutputArc(t1, forwardPlace); + // FDEP + forwardPlace = getFailedPlace(dftDependency->triggerEvent()); } - for(auto const& depEv : dftDependency->dependentEvents()) { - uint64_t tx = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + depEv->name()); - builder.addInputArc(forwardPlace, tx); - builder.addOutputArc(tx, forwardPlace); - builder.addOutputArc(tx, failedNodes.at(depEv->id())); - builder.addInhibitionArc(failedNodes.at(depEv->id()), tx); - if (!smart || depEv->nrRestrictions() > 0) { - builder.addInhibitionArc(disabledNodes.at(depEv->id()), tx); + + for (auto const& child : dftDependency->dependentEvents()) { + uint64_t tForwardFailure = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + child->name()); + builder.addInputArc(forwardPlace, tForwardFailure); + builder.addOutputArc(tForwardFailure, forwardPlace); + builder.addOutputArc(tForwardFailure, getFailedPlace(child)); + builder.addInhibitionArc(getFailedPlace(child), tForwardFailure); + if (!smart || child->nrRestrictions() > 0) { + builder.addInhibitionArc(disabledPlaces.at(child->id()), tForwardFailure); } - if (!smart || mDft.isRepresentative(depEv->id())) { - builder.addOutputArc(tx, unavailableNodes.at(depEv->id())); + if (!smart || mDft.isRepresentative(child->id())) { + builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id())); } } } template - void DftToGspnTransformator::drawSeq(std::shared_ptr const> dftSeq) { + void DftToGspnTransformator::translateSeq(std::shared_ptr const> dftSeq) { STORM_LOG_THROW(dftSeq->allChildrenBEs(), storm::exceptions::NotImplementedException, "Sequence enforcers with gates as children are currently not supported"); double xcenter = mDft.getElementLayoutInfo(dftSeq->id()).x; double ycenter = mDft.getElementLayoutInfo(dftSeq->id()).y; if (!smart) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftSeq->name() + STR_FAILED); - failedNodes.push_back(nodeFailed); - builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); - addUnavailableNode(dftSeq, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); + addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); + addUnavailablePlace(dftSeq, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); } - uint64_t j = 0; uint64_t tEnable = 0; uint64_t nextPlace = 0; - for(auto const& child : dftSeq->children()) { - nextPlace = builder.addPlace(defaultCapacity, j==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name()); - builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter-5.0+j*3.0, ycenter-3.0)); - if (j>0) { + for (size_t i = 0; i < dftSeq->nrChildren(); ++i) { + auto const& child = dftSeq->children().at(i); + + nextPlace = builder.addPlace(defaultCapacity, i==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name()); + builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter-3.0)); + + if (i>0) { builder.addOutputArc(tEnable, nextPlace); } tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" +child->name()); - builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter-5.0+j*3.0, ycenter+3.0)); - + builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0)); builder.addInputArc(nextPlace, tEnable); - builder.addInputArc(disabledNodes.at(child->id()), tEnable); - if (j>0) { - builder.addInputArc(failedNodes.at(dftSeq->children().at(j-1)->id()), tEnable); + builder.addInputArc(disabledPlaces.at(child->id()), tEnable); + if (i>0) { + builder.addInputArc(getFailedPlace(dftSeq->children().at(i-1)), tEnable); } - ++j; } } - + template - uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) { - uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail"); - assert(unavailableNode != 0); - unavailableNodes.emplace(dftElement->id(), unavailableNode); - builder.setPlaceLayoutInfo(unavailableNode, layoutInfo); - return unavailableNode; + uint64_t DftToGspnTransformator::addFailedPlace(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialFailed) { + uint64_t failedPlace = builder.addPlace(defaultCapacity, initialFailed ? 1 : 0, dftElement->name() + STR_FAILED); + assert(failedPlaces.size() == dftElement->id()); + failedPlaces.push_back(failedPlace); + builder.setPlaceLayoutInfo(failedPlace, layoutInfo); + return failedPlace; + } + + + template + uint64_t DftToGspnTransformator::addUnavailablePlace(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) { + uint64_t unavailablePlace = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail"); + unavailablePlaces.emplace(dftElement->id(), unavailablePlace); + builder.setPlaceLayoutInfo(unavailablePlace, layoutInfo); + return unavailablePlace; } template uint64_t DftToGspnTransformator::addDisabledPlace(std::shared_ptr > dftBe, storm::gspn::LayoutInfo const& layoutInfo) { - uint64_t disabledNode = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled"); - assert(disabledNode != 0); - disabledNodes.emplace(dftBe->id(), disabledNode); - builder.setPlaceLayoutInfo(disabledNode, layoutInfo); - return disabledNode; + uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled"); + disabledPlaces.emplace(dftBe->id(), disabledPlace); + builder.setPlaceLayoutInfo(disabledPlace, layoutInfo); + return disabledPlace; } template @@ -594,20 +580,9 @@ namespace storm { //return mDft.maxRank() - dftElement->rank() + 2; } - - template - void DftToGspnTransformator::drawGSPNRestrictions() { - // TODO - } - template - gspn::GSPN* DftToGspnTransformator::obtainGSPN() { - return builder.buildGspn(); - } - // Explicitly instantiate the class. template class DftToGspnTransformator; - #ifdef STORM_HAVE_CARL // template class DftToGspnTransformator; diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index f9e576bbc..3d49505c9 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -33,101 +33,106 @@ namespace storm { */ gspn::GSPN* obtainGSPN(); - + /*! + * Get failed place id of top level element. + */ uint64_t toplevelFailedPlaceId(); private: - /* - * Draw all elements of the GSPN. + /*! + * Translate all elements of the GSPN. */ - void drawGSPNElements(); + void translateGSPNElements(); - /* - * Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). - */ - void drawGSPNRestrictions(); - - /* - * Draw a Petri net Basic Event. + /*! + * Translate a GSPN Basic Event. * * @param dftBE The Basic Event. */ - void drawBE(std::shared_ptr const> dftBE, bool isRepresentative); - - /* - * Draw a Petri net AND. + void translateBE(std::shared_ptr const> dftBE); + + /*! + * Translate a GSPN CONSTF (Constant Failure, a Basic Event that has already failed). + * + * @param dftPor The CONSTF Basic Event. + */ + void translateCONSTF(std::shared_ptr const> dftConstF); + + /*! + * Translate a GSPN CONSTS (Constant Save, a Basic Event that cannot fail). + * + * @param dftPor The CONSTS Basic Event. + */ + void translateCONSTS(std::shared_ptr const> dftConstS); + + /*! + * Translate a GSPN AND. * * @param dftAnd The AND gate. */ - void drawAND(std::shared_ptr const> dftAnd, bool isRepresentative); + void translateAND(std::shared_ptr const> dftAnd); - /* - * Draw a Petri net OR. + /*! + * Translate a GSPN OR. * * @param dftOr The OR gate. */ - void drawOR(std::shared_ptr const> dftOr, bool isRepresentative); + void translateOR(std::shared_ptr const> dftOr); - /* - * Draw a Petri net VOT. + /*! + * Translate a GSPN VOT. * * @param dftVot The VOT gate. */ - void drawVOT(std::shared_ptr const> dftVot, bool isRepresentative); + void translateVOT(std::shared_ptr const> dftVot); - /* - * Draw a Petri net PAND. - * This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless). - * + /*! + * Translate a GSPN PAND. + * * @param dftPand The PAND gate. + * @param inclusive Flag wether the PAND is inclusive (children are allowed to fail simultaneously and the PAND will fail nevertheless) */ - void drawPAND(std::shared_ptr const> dftPand, bool isRepresentative); - - /* - * Draw a Petri net SPARE. + void translatePAND(std::shared_ptr const> dftPand, bool inclusive = true); + + /*! + * Translate a GSPN POR. + * + * @param dftPor The POR gate. + * @param inclusive Flag wether the POR is inclusive (children are allowed to fail simultaneously and the POR will fail nevertheless) + */ + void translatePOR(std::shared_ptr const> dftPor, bool inclusive = true); + + /*! + * Translate a GSPN SPARE. * * @param dftSpare The SPARE gate. */ - void drawSPARE(std::shared_ptr const> dftSpare, bool isRepresentative); - - /* - * Draw a Petri net POR. - * This POR is inklusive (children are allowed to fail simultaneously and the POR will fail nevertheless). - * - * @param dftPor The POR gate. - */ - void drawPOR(std::shared_ptr const> dftPor, bool isRepresentative); - - /* - * Draw a Petri net CONSTF (Constant Failure, a Basic Event that has already failed). - * - * @param dftPor The CONSTF Basic Event. - */ - void drawCONSTF(std::shared_ptr const> dftConstF, bool isRepresentative); - - /* - * Draw a Petri net CONSTS (Constant Save, a Basic Event that cannot fail). - * - * @param dftPor The CONSTS Basic Event. - */ - void drawCONSTS(std::shared_ptr const> dftConstS, bool isRepresentative); - - /* - * Draw a Petri net PDEP (FDEP is included with a firerate of 1). - */ - void drawPDEP(std::shared_ptr const> dftDependency); + void translateSPARE(std::shared_ptr const> dftSpare); + + /*! + * Translate a GSPN PDEP (FDEP is included with a probability of 1). + * + * @param dftDependency The PDEP gate. + */ + void translatePDEP(std::shared_ptr const> dftDependency); - - void drawSeq(std::shared_ptr const> dftSeq); + /*! + * Translate a GSPN SEQ. + * + * @param dftSeq The SEQ gate. + */ + void translateSeq(std::shared_ptr const> dftSeq); - /* - * Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token). + /*! + * Check if the element is active intially. * * @param dFTElement DFT element. + * + * @return True iff element is active initially. */ bool isActiveInitially(std::shared_ptr const> dFTElement); - /* + /*! * Get the priority of the element. * The priority is two times the length of the shortest path to the top event. * @@ -137,16 +142,57 @@ namespace storm { */ uint64_t getFailPriority(std::shared_ptr const> dFTElement); - uint64_t addUnavailableNode(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true); - + /*! + * Add failed place for an element. + * + * @param dftElement Element. + * @param layoutInfo Information about layout. + * @param initialFailed Flag indicating whether the element is initially failed. + * + * @return Id of added failed place. + */ + uint64_t addFailedPlace(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialFailed = false); + + /*! + * Add unavailable place for element. + * + * @param dftElement Element. + * @param layoutInfo Information about layout. + * @param initialAvailable Flag indicating whether the element is available initially. + * + * @return Id of added unavailable place. + */ + uint64_t addUnavailablePlace(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true); + + /*! + * Add disabled place for element. + * + * @param dftBe Basic Element. + * @param layoutInfo Information about layout. + * + * @return Id of added disabled place. + */ uint64_t addDisabledPlace(std::shared_ptr const> dftBe, storm::gspn::LayoutInfo const& layoutInfo); + + /*! + * Get failed place for element. + * + * @param dftElement Element. + * + * @return Id of failed place corresponding to the given element. + */ + uint64_t getFailedPlace(std::shared_ptr const> dftElement) { + return failedPlaces.at(dftElement->id()); + } storm::storage::DFT const& mDft; storm::gspn::GspnBuilder builder; - std::vector failedNodes; - std::map unavailableNodes; - std::map activeNodes; - std::map disabledNodes; + + // Interface places for DFT elements + std::vector failedPlaces; + std::map unavailablePlaces; + std::map activePlaces; + std::map disabledPlaces; bool smart; static constexpr const char* STR_FAILING = "_failing"; // Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.