diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index e05b13210..1e17b0c5d 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -29,7 +29,9 @@ namespace storm { template<> void transformToGSPN(storm::storage::DFT const& dft) { + // TODO make choosable bool smart = true; + bool mergeDCFailed = true; // Set Don't Care elements std::set dontCareElements; @@ -43,7 +45,7 @@ namespace storm { // Transform to GSPN storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); - gspnTransformator.transform(dontCareElements, smart); + gspnTransformator.transform(dontCareElements, smart, mergeDCFailed); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index a9b761c52..d6e54cf5f 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -5,48 +5,49 @@ namespace storm { namespace transformations { namespace dft { - + // Prevent some magic constants static constexpr const uint64_t defaultPriority = 1; static constexpr const uint64_t defaultCapacity = 1; - template - DftToGspnTransformator::DftToGspnTransformator(storm::storage::DFT const& dft) : mDft(dft) { + template + DftToGspnTransformator::DftToGspnTransformator(storm::storage::DFT const &dft) : mDft(dft) { // Intentionally left empty. } - template - void DftToGspnTransformator::transform(std::set const& dontCareElements, bool smart) { + template + void DftToGspnTransformator::transform(std::set const &dontCareElements, bool smart, bool mergeDCFailed) { this->dontCareElements = dontCareElements; this->smart = smart; + this->mergedDCFailed = mergeDCFailed; builder.setGspnName("DftToGspnTransformation"); - - // Translate all GSPN elements + + // Translate all GSPN elements translateGSPNElements(); // Create initial template // TODO } - + template uint64_t DftToGspnTransformator::toplevelFailedPlaceId() { 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() { + template + gspn::GSPN *DftToGspnTransformator::obtainGSPN() { return builder.buildGspn(); } - - template + + template void DftToGspnTransformator::translateGSPNElements() { - // Loop through every DFT element and create its corresponding GSPN template. + // 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); + auto dftElement = mDft.getElement(i); - // Check which type the element is and call the corresponding translate-function. - switch (dftElement->type()) { + // Check which type the element is and call the corresponding translate-function. + switch (dftElement->type()) { case storm::storage::DFTElementType::BE: translateBE(std::static_pointer_cast const>(dftElement)); break; @@ -57,38 +58,40 @@ namespace storm { translateCONSTS(dftElement); break; case storm::storage::DFTElementType::AND: - translateAND(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::OR: - translateOR(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::VOT: - translateVOT(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::PAND: - translatePAND(std::static_pointer_cast const>(dftElement), std::static_pointer_cast const>(dftElement)->isInclusive()); - break; + translateAND(std::static_pointer_cast const>(dftElement)); + break; + case storm::storage::DFTElementType::OR: + translateOR(std::static_pointer_cast const>(dftElement)); + break; + case storm::storage::DFTElementType::VOT: + translateVOT(std::static_pointer_cast const>(dftElement)); + break; + case storm::storage::DFTElementType::PAND: + 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()); + translatePOR(std::static_pointer_cast const>(dftElement), + std::static_pointer_cast const>(dftElement)->isInclusive()); + break; + case storm::storage::DFTElementType::SPARE: + translateSPARE(std::static_pointer_cast const>(dftElement)); break; - case storm::storage::DFTElementType::SPARE: - 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: + case storm::storage::DFTElementType::SEQ: translateSeq(std::static_pointer_cast const>(dftElement)); break; - default: - STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown."); - break; - } - } - - } - - template + default: + STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown."); + break; + } + } + + } + + template void DftToGspnTransformator::translateBE(std::shared_ptr const> dftBE) { double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; @@ -111,21 +114,21 @@ namespace storm { builder.addInhibitionArc(activePlace, tPassive); builder.addInhibitionArc(failedPlace, tPassive); builder.addOutputArc(tPassive, failedPlace); - + if (!smart || dftBE->nrRestrictions() > 0) { - uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter-9.0, ycenter)); + uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter - 9.0, ycenter)); builder.addInhibitionArc(disabledPlace, tActive); builder.addInhibitionArc(disabledPlace, tPassive); } - + if (!smart || mDft.isRepresentative(dftBE->id())) { - uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter)); + uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter)); builder.addOutputArc(tActive, unavailablePlace); builder.addOutputArc(tPassive, unavailablePlace); } } - template + template void DftToGspnTransformator::translateCONSTF(std::shared_ptr const> dftConstF) { double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x; double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y; @@ -137,7 +140,7 @@ namespace storm { } } - template + template void DftToGspnTransformator::translateCONSTS(std::shared_ptr const> dftConstS) { double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x; double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y; @@ -156,46 +159,46 @@ namespace storm { } } - template + template void DftToGspnTransformator::translateAND(std::shared_ptr const> dftAnd) { double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; - uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); + uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); - uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING ); - builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0)); + 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)); + uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0)); builder.addOutputArc(tFailed, unavailablePlace); } - for (auto const& child : dftAnd->children()) { + for (auto const &child : dftAnd->children()) { builder.addInputArc(getFailedPlace(child), tFailed); builder.addOutputArc(tFailed, getFailedPlace(child)); } - } + } - template + template void DftToGspnTransformator::translateOR(std::shared_ptr const> dftOr) { double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x; double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y; - uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter-3.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) { - unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0)); + unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0)); } - - 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)); + + 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) { @@ -204,23 +207,23 @@ namespace storm { builder.addInputArc(getFailedPlace(child), tFailed); builder.addOutputArc(tFailed, getFailedPlace(child)); } - } - - template + } + + template void DftToGspnTransformator::translateVOT(std::shared_ptr const> dftVot) { // TODO: finish layouting double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x; double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y; - uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter-3.0)); + uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); 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)); + uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0)); builder.addOutputArc(tFailed, unavailablePlace); } @@ -228,8 +231,8 @@ namespace storm { 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); + 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)); @@ -238,46 +241,46 @@ namespace storm { builder.addInputArc(getFailedPlace(child), tCollect); builder.addOutputArc(tCollect, getFailedPlace(child)); } - } + } - template + template void DftToGspnTransformator::translatePAND(std::shared_ptr const> dftPand, bool inclusive) { double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x; double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y; - uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); + 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)); + 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)); + uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0)); builder.addOutputArc(tFailed, unavailablePlace); } if (inclusive) { // Inclusive PAND uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE); - builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); + builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter - 3.0)); builder.addInhibitionArc(failSafePlace, tFailed); // Transitions for failed place - for (auto const& child : dftPand->children()) { + for (auto const &child : dftPand->children()) { builder.addInputArc(getFailedPlace(child), tFailed); builder.addOutputArc(tFailed, getFailedPlace(child)); } // Transitions for fail-safe place for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) { - auto const& child = dftPand->children().at(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.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.addInhibitionArc(getFailedPlace(dftPand->children().at(i - 1)), tFailSafe); builder.addOutputArc(tFailSafe, failSafePlace); builder.addInhibitionArc(failSafePlace, tFailSafe); } @@ -286,7 +289,7 @@ namespace storm { uint64_t failSafeXPlace = 0; uint64_t tFailSafeX = 0; for (size_t i = 0; i < dftPand->nrChildren(); ++i) { - auto const& child = dftPand->children().at(i); + auto const &child = dftPand->children().at(i); if (i > 0) { // Set inhibition arc to previous transition @@ -295,8 +298,8 @@ namespace storm { if (i < dftPand->nrChildren() - 1) { // Not last child - 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)); + 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 tFailSafeX = tFailed; @@ -311,7 +314,7 @@ namespace storm { 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.setPlaceLayoutInfo(failSafeXPlace, storm::gspn::LayoutInfo(xcenter - 3.0 + i * 3.0, ycenter)); builder.addOutputArc(tFailSafeX, failSafeXPlace); builder.addInhibitionArc(failSafeXPlace, tFailSafeX); } @@ -319,15 +322,15 @@ namespace storm { } } - template + template void DftToGspnTransformator::translatePOR(std::shared_ptr const> dftPor, bool inclusive) { double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x; double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y; - uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0)); + uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0)); 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.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0)); builder.addOutputArc(tFailed, failedPlace); builder.addInhibitionArc(failedPlace, tFailed); @@ -336,22 +339,22 @@ namespace storm { builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front())); if (!smart || mDft.isRepresentative(dftPor->id())) { - uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0)); + uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0)); builder.addOutputArc(tFailed, unavailablePlace); } if (inclusive) { // Inclusive POR uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); - builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0)); + 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); + 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.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter - 3.0 + i * 3.0, ycenter + 3.0)); builder.addInputArc(getFailedPlace(child), tFailSafe); builder.addOutputArc(tFailSafe, getFailedPlace(child)); @@ -363,38 +366,38 @@ namespace storm { // Exclusive POR // For all children except the first one - for (auto const& child : dftPor->children()) { + for (auto const &child : dftPor->children()) { builder.addInhibitionArc(getFailedPlace(child), tFailed); } } - + } - template + template void DftToGspnTransformator::translateSPARE(std::shared_ptr const> dftSpare) { double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x; double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y; - uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.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) { - unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0)); + unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0)); } 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)); + builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 20.0, ycenter - 12.0)); activePlaces.emplace(dftSpare->id(), activePlace); - + std::vector tNextClaims; std::vector tNextConsiders; for (size_t i = 0; i < dftSpare->nrChildren(); ++i) { - auto const& child = dftSpare->children().at(i); + auto const &child = dftSpare->children().at(i); // Consider next child - 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)); + 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 (i > 0) { // Set output transition from previous next_claim @@ -405,7 +408,7 @@ namespace storm { // Cannot claim child 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.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())); @@ -413,9 +416,9 @@ namespace storm { // Claimed child 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)); + 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.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); @@ -423,7 +426,7 @@ namespace storm { // Claim next 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.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)); @@ -432,8 +435,8 @@ namespace storm { // Activate all elements in spare module uint64_t l = 0; for (uint64_t k : mDft.module(child->id())) { - 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)); + 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); @@ -452,26 +455,26 @@ namespace storm { builder.addOutputArc(tNextConsiders.back(), unavailablePlace); builder.addOutputArc(tNextClaims.back(), unavailablePlace); } - } + } - template + template void DftToGspnTransformator::translatePDEP(std::shared_ptr const> dftDependency) { double xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x; double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y; if (!smart) { - addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); - addUnavailablePlace(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 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)); + 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)); + 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); @@ -479,7 +482,7 @@ namespace storm { builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent())); uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip"); - builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0)); + builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter - 2.0, ycenter + 2.0)); builder.addOutputArc(tStartFlip, flipPlace); uint64_t tWinFlip = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip"); @@ -493,7 +496,7 @@ namespace storm { forwardPlace = getFailedPlace(dftDependency->triggerEvent()); } - for (auto const& child : dftDependency->dependentEvents()) { + 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); @@ -506,43 +509,45 @@ namespace storm { builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id())); } } - } - - template + } + + template 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) { - addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0)); - addUnavailablePlace(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 tEnable = 0; uint64_t nextPlace = 0; for (size_t i = 0; i < dftSeq->nrChildren(); ++i) { - auto const& child = dftSeq->children().at(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)); + 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) { + 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+i*3.0, ycenter+3.0)); + tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" + child->name()); + builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0)); builder.addInputArc(nextPlace, tEnable); builder.addInputArc(disabledPlaces.at(child->id()), tEnable); - if (i>0) { - builder.addInputArc(getFailedPlace(dftSeq->children().at(i-1)), tEnable); + if (i > 0) { + builder.addInputArc(getFailedPlace(dftSeq->children().at(i - 1)), tEnable); } } - + } template - uint64_t DftToGspnTransformator::addFailedPlace(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialFailed) { + 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); @@ -552,42 +557,44 @@ namespace storm { template - uint64_t DftToGspnTransformator::addUnavailablePlace(std::shared_ptr const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) { + 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 + DftToGspnTransformator::addDisabledPlace(std::shared_ptr > dftBe, storm::gspn::LayoutInfo const &layoutInfo) { uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled"); disabledPlaces.emplace(dftBe->id(), disabledPlace); builder.setPlaceLayoutInfo(disabledPlace, layoutInfo); return disabledPlace; } - - template + + template bool DftToGspnTransformator::isActiveInitially(std::shared_ptr const> dftElement) { - // If element is in the top module, return true. + // If element is in the top module, return true. return !mDft.hasRepresentant(dftElement->id()); - } - - template - uint64_t DftToGspnTransformator::getFailPriority(std::shared_ptr const> dftElement) - { + } + + template + uint64_t DftToGspnTransformator::getFailPriority(std::shared_ptr const> dftElement) { // Temporariliy use one priority for all return defaultPriority; //return mDft.maxRank() - dftElement->rank() + 2; - } + } // Explicitly instantiate the class. - template class DftToGspnTransformator; + template + class DftToGspnTransformator; - #ifdef STORM_HAVE_CARL +#ifdef STORM_HAVE_CARL // template class DftToGspnTransformator; - #endif +#endif } // namespace dft } // namespace transformations diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 22ba384c7..038b525bd 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -28,8 +28,9 @@ namespace storm { * @param dontCareElements Set of DFT elements which should have Don't Care propagation. * @param smart Flag indicating if smart semantics should be used. * Smart semantics will only generate necessary parts of the GSPNs. + * @param mergeDCFailed Flag indicating if Don't Care places and Failed places should be merged. */ - void transform(std::set const& dontCareElements, bool smart = true); + void transform(std::set const& dontCareElements, bool smart = true, bool mergeDCFailed = true); /*! * Extract Gspn by building @@ -194,6 +195,7 @@ namespace storm { // Options bool smart; + bool mergedDCFailed; std::set dontCareElements; // Interface places for DFT elements