diff --git a/src/storm-dft-cli/storm-dyftee.cpp b/src/storm-dft-cli/storm-dyftee.cpp index 6ed375d79..71f5cea86 100644 --- a/src/storm-dft-cli/storm-dyftee.cpp +++ b/src/storm-dft-cli/storm-dyftee.cpp @@ -4,6 +4,7 @@ #include "storm/cli/cli.h" #include "storm/exceptions/BaseException.h" #include "storm/utility/macros.h" +#include "storm/transformations/dft/DftToGspnTransformator.h" #include "storm/settings/modules/GeneralSettings.h" #include "storm/settings/modules/CoreSettings.h" @@ -78,6 +79,11 @@ template storm::gspn::GSPN transformDFT(std::string filename) { storm::parser::DFTGalileoParser parser; storm::storage::DFT dft = parser.parseDFT(filename); +<<<<<<< f8986fe6139bddaf5068477b0f70ac1f806f8576:src/storm-dft-cli/storm-dyftee.cpp +======= + storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); + gspnTransformator.transform(); +>>>>>>> updated dft->gspn translation to now have basis support for spares:src/storm/storm-dyftee.cpp } /*! diff --git a/src/storm/transformations/dft/DftToGspnTransformator.cpp b/src/storm/transformations/dft/DftToGspnTransformator.cpp new file mode 100644 index 000000000..4331e0c62 --- /dev/null +++ b/src/storm/transformations/dft/DftToGspnTransformator.cpp @@ -0,0 +1,923 @@ +#include "DftToGspnTransformator.h" +#include "storm/exceptions/NotImplementedException.h" +#include + +namespace storm { + namespace transformations { + namespace dft { + + // Prevent some magic constants + static constexpr const uint64_t defaultPriority = 0; + static constexpr const uint64_t defaultCapacity = 0; + + template + DftToGspnTransformator::DftToGspnTransformator(storm::storage::DFT const& dft) : mDft(dft) { + // Intentionally left empty. + } + + template + void DftToGspnTransformator::transform() { + + builder.setGspnName("DftToGspnTransformation"); + + // Loop through every DFT element and draw them as a GSPN. + drawGSPNElements(); + + // When all DFT elements are drawn, draw the connections between them. + drawGSPNConnections(); + + // Draw functional/probability dependencies into the GSPN. + drawGSPNDependencies(); + + // Draw restrictions into the GSPN (i.e. SEQ or MUTEX). + drawGSPNRestrictions(); + + // Write GSPN to file. + writeGspn(true); + } + + 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++) { + auto dftElement = mDft.getElement(i); + bool isRepresentative = mDft.isRepresentative(i); + + // Check which type the element is and call the corresponding drawing-function. + switch (dftElement->type()) { + case storm::storage::DFTElementType::AND: + drawAND(std::static_pointer_cast const>(dftElement), isRepresentative); + break; + case storm::storage::DFTElementType::OR: + drawOR(std::static_pointer_cast const>(dftElement), isRepresentative); + break; + case storm::storage::DFTElementType::VOT: + drawVOT(std::static_pointer_cast const>(dftElement), isRepresentative); + break; + case storm::storage::DFTElementType::PAND: + drawPAND(std::static_pointer_cast const>(dftElement), isRepresentative); + 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); + break; + case storm::storage::DFTElementType::SEQ: + // No method call needed here. SEQ only consists of restrictions, which are handled later. + 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), isRepresentative); + break; + default: + STORM_LOG_ASSERT(false, "DFT type unknown."); + break; + } + } + + } + + template + void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE, bool isRepresentative) { + + uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); + activeNodes.emplace(dftBE->id(), beActive); + uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); + + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftBE); + } + + assert(failedNodes.size() == dftBE->id()); + failedNodes.push_back(beFailed); + uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing"); + builder.addInputArc(beActive, tActive); + builder.addInhibitionArc(beFailed, tActive); + builder.addOutputArc(tActive, beActive); + builder.addOutputArc(tActive, beFailed); + uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing"); + builder.addInhibitionArc(beActive, tPassive); + builder.addInhibitionArc(beFailed, tPassive); + builder.addOutputArc(tPassive, beFailed); + + if (isRepresentative) { + builder.addOutputArc(tActive, unavailableNode); + builder.addOutputArc(tPassive, unavailableNode); + } + } + + 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); + + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftAnd); + } + + + uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd) , 0.0, dftAnd->name() + STR_FAILING ); + builder.addInhibitionArc(nodeFailed, tAndFailed); + builder.addOutputArc(tAndFailed, nodeFailed); + if (isRepresentative) { + builder.addOutputArc(tAndFailed, unavailableNode); + } + for(auto const& child : dftAnd->children()) { + assert(failedNodes.size() > child->id()); + builder.addInputArc(failedNodes[child->id()], tAndFailed); + } + + } + + 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); + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftOr); + } + + 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.addInhibitionArc(nodeFailed, tNodeFailed); + builder.addOutputArc(tNodeFailed, nodeFailed); + if (isRepresentative) { + builder.addOutputArc(tNodeFailed, unavailableNode); + } + assert(failedNodes.size() > child->id()); + builder.addInputArc(failedNodes[child->id()], tNodeFailed); + ++i; + } + } + + template + void DftToGspnTransformator::drawVOT(std::shared_ptr const> dftVot, bool isRepresentative) { + uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED); + assert(failedNodes.size() == dftVot->id()); + failedNodes.push_back(nodeFailed); + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftVot); + } + + uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector"); + uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING); + builder.addOutputArc(tNodeFailed, nodeFailed); + if (isRepresentative) { + builder.addOutputArc(tNodeFailed, unavailableNode); + } + builder.addInhibitionArc(nodeFailed, tNodeFailed); + builder.addInputArc(nodeCollector, tNodeFailed, dftVot->threshold()); + builder.addOutputArc(tNodeFailed, nodeCollector, 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 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); + ++i; + } + } + + 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); + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftPand); + } + + uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE); + uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING); + builder.addInhibitionArc(nodeFailed, tNodeFailed); + builder.addInhibitionArc(nodeFS, tNodeFailed); + builder.addOutputArc(tNodeFailed, nodeFailed); + if (isRepresentative) { + builder.addOutputArc(tNodeFailed, nodeFailed); + } + for(auto const& child : dftPand->children()) { + builder.addInputArc(failedNodes[child->id()], tNodeFailed); + } + 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.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); + builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); + builder.addOutputArc(tfs, nodeFS); + + } + } +// + 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); + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftSpare); + } + uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED); + activeNodes.emplace(dftBE->id(), beActive); + + + std::vector cucNodes; + std::vector nextClaimNodes; + std::vector nextclTransitions; + std::vector nextconsiderTransitions; + uint64_t j = 0; + for(auto const& child : dftSpare->children()) { + if (j > 0) { + nextClaimNodes.push_back(builder.addPlace(defaultCapacity, 0, dftSpare->name()+ "_consider_" + child->name())); + + builder.addOutputArc(nextclTransitions.back(), nextClaimNodes.back(), 1); + if (j > 1) { + builder.addOutputArc(nextconsiderTransitions.back(), nextClaimNodes.back()); + } + + uint64_t tnextconsider = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name()); + builder.addInputArc(nextClaimNodes.back(), tnextconsider); + builder.addInputArc(unavailableNodes.at(child->id()), tnextconsider); + nextconsiderTransitions.push_back(tnextconsider); + + } + cucNodes.push_back(builder.addPlace(defaultCapacity, j == 0 ? 1 : 0, dftSpare->name() + "_claimed_" + child->name())); + if (j > 0) { + uint64 tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); + builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim); + builder.addInputArc(nextClaimNodes.back(), tclaim); + builder.addOutputArc(tclaim, cucNodes.back()); + } + uint64_t tnextcl = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(j)); + builder.addInputArc(cucNodes.back(), tnextcl); + builder.addOutputArc(tnextcl, cucNodes.back()); + builder.addInputArc(failedNodes.at(child->id()), tnextcl); + builder.addOutputArc(tnextcl, failedNodes.at(child->id())); + nextclTransitions.push_back(tnextcl); + + + ++j; + } + builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); + builder.addOutputArc(nextclTransitions.back(), nodeFailed); + + if (isRepresentative) { + builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); + builder.addOutputArc(nextclTransitions.back(), unavailableNode); + } + + +// uint_fast64_t priority = getPriority(0, dftSpare); +// +// // This codeblock can be removed later, when I am 100% sure it is not needed anymore. +// /* +// storm::gspn::Place placeSPAREActivated; +// placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED); +// placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare)); +// mGspn.addPlace(placeSPAREActivated); +// +// storm::gspn::ImmediateTransition immediateTransitionPCActivating; +// immediateTransitionPCActivating.setName(dftSpare->children()[0]->name() + STR_ACTIVATING); +// immediateTransitionPCActivating.setPriority(priority); +// immediateTransitionPCActivating.setWeight(0.0); +// immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1); +// immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1); +// mGspn.addImmediateTransition(immediateTransitionPCActivating); +// */ +// +// auto children = dftSpare->children(); +// +// // Draw places and transitions that belong to each spare child. +// for (std::size_t i = 1; i < children.size(); i++) { +// auto placeChildClaimedPreexist = mGspn.getPlace(children[i]->name() + "_claimed"); +// +// if (!placeChildClaimedPreexist.first) { // Only draw this place if it doesn't exist jet. +// storm::gspn::Place placeChildClaimed; +// placeChildClaimed.setName(children[i]->name() + "_claimed"); +// placeChildClaimed.setNumberOfInitialTokens(0); +// mGspn.addPlace(placeChildClaimed); +// +// storm::gspn::ImmediateTransition immediateTransitionSpareChildActivating; +// immediateTransitionSpareChildActivating.setName(children[i]->name() + STR_ACTIVATING); +// immediateTransitionSpareChildActivating.setPriority(priority); +// immediateTransitionSpareChildActivating.setWeight(0.0); +// immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1); +// immediateTransitionSpareChildActivating.setOutputArcMultiplicity(placeChildClaimed, 1); +// mGspn.addImmediateTransition(immediateTransitionSpareChildActivating); +// } +// +// auto placeChildClaimedExist = mGspn.getPlace(children[i]->name() + "_claimed"); +// +// storm::gspn::Place placeSPAREClaimedChild; +// placeSPAREClaimedChild.setName(dftSpare->name() + "_claimed_" + children[i]->name()); +// placeSPAREClaimedChild.setNumberOfInitialTokens(0); +// mGspn.addPlace(placeSPAREClaimedChild); +// +// storm::gspn::ImmediateTransition immediateTransitionChildClaiming; +// immediateTransitionChildClaiming.setName(dftSpare->name() + "_claiming_" + children[i]->name()); +// immediateTransitionChildClaiming.setPriority(priority + 1); // Higher priority needed! +// immediateTransitionChildClaiming.setWeight(0.0); +// immediateTransitionChildClaiming.setInhibitionArcMultiplicity(placeChildClaimedExist.second, 1); +// immediateTransitionChildClaiming.setOutputArcMultiplicity(placeChildClaimedExist.second, 1); +// immediateTransitionChildClaiming.setOutputArcMultiplicity(placeSPAREClaimedChild, 1); +// mGspn.addImmediateTransition(immediateTransitionChildClaiming); +// +// storm::gspn::Place placeSPAREChildConsumed; +// if (i < children.size() - 1) { +// placeSPAREChildConsumed.setName(dftSpare->name() + "_" + children[i]->name() + "_consumed"); +// } +// else { +// placeSPAREChildConsumed.setName(dftSpare->name() + STR_FAILED); +// } +// placeSPAREChildConsumed.setNumberOfInitialTokens(0); +// mGspn.addPlace(placeSPAREChildConsumed); +// +// storm::gspn::ImmediateTransition immediateTransitionChildConsuming1; +// immediateTransitionChildConsuming1.setName(dftSpare->name() + "_" + children[i]->name() + "_consuming1"); +// immediateTransitionChildConsuming1.setPriority(priority); +// immediateTransitionChildConsuming1.setWeight(0.0); +// immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1); +// immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1); +// immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREClaimedChild, 1); +// mGspn.addImmediateTransition(immediateTransitionChildConsuming1); +// +// storm::gspn::ImmediateTransition immediateTransitionChildConsuming2; +// immediateTransitionChildConsuming2.setName(dftSpare->name() + "_" + children[i]->name() + "_consuming2"); +// immediateTransitionChildConsuming2.setPriority(priority); +// immediateTransitionChildConsuming2.setWeight(0.0); +// immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1); +// immediateTransitionChildConsuming2.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1); +// immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREClaimedChild, 1); +// immediateTransitionChildConsuming2.setInputArcMultiplicity(placeSPAREClaimedChild, 1); +// mGspn.addImmediateTransition(immediateTransitionChildConsuming2); +// } +// +// // Draw connections between all spare childs. +// for (std::size_t i = 1; i < children.size() - 1; i++) { +// auto placeSPAREChildConsumed = mGspn.getPlace(dftSpare->name() + "_" + children[i]->name() + "_consumed"); +// auto immediateTransitionChildClaiming = mGspn.getImmediateTransition(dftSpare->name() + "_claiming_" + children[i + 1]->name()); +// auto immediateTransitionChildConsuming1 = mGspn.getImmediateTransition(dftSpare->name() + "_" + children[i + 1]->name() + "_consuming1"); +// +// immediateTransitionChildClaiming.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1); +// immediateTransitionChildClaiming.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1); +// +// immediateTransitionChildConsuming1.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1); +// immediateTransitionChildConsuming1.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1); +// } + } +// + template + void DftToGspnTransformator::drawPOR(std::shared_ptr const> dftPor, bool isRepresentative) { + uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILED); + uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); + + + uint64_t tfail = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING); + builder.addInhibitionArc(nodeFS, tfail); + builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail); + builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id())); + builder.addOutputArc(tfail, nodeFailed); + builder.addInhibitionArc(nodeFailed, tfail); + uint64_t j = 0; + for (auto const& child : dftPor->children()) { + uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); + builder.addInputArc(failedNodes.at(child->id()), tfailsf); + builder.addOutputArc(tfailsf, failedNodes.at(child->id())); + // TODO +// builder.addInhibitionArc(<#const uint_fast64_t &from#>, <#const uint_fast64_t &to#>) + ++j; + } + } + +// + template + void DftToGspnTransformator::drawCONSTF(std::shared_ptr const> dftConstF, bool isRepresentative) { +// storm::gspn::Place placeCONSTFFailed; +// placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED); +// placeCONSTFFailed.setNumberOfInitialTokens(1); +// mGspn.addPlace(placeCONSTFFailed); + } +// + 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, bool isRepresentative) { +// // Only draw dependency, if it wasn't drawn before. +// std::string gateName = dftDependency->name().substr(0, dftDependency->name().find("_")); +// auto exists = mGspn.getPlace(gateName + STR_FAILED); +// if (!exists.first) { +// storm::gspn::Place placeDEPFailed; +// placeDEPFailed.setName(gateName + STR_FAILED); +// placeDEPFailed.setNumberOfInitialTokens(0); +// mGspn.addPlace(placeDEPFailed); +// +// storm::gspn::TimedTransition timedTransitionDEPFailure; +// timedTransitionDEPFailure.setName(gateName + STR_FAILING); +// timedTransitionDEPFailure.setPriority(getPriority(0, dftDependency)); +// timedTransitionDEPFailure.setRate(dftDependency->probability()); +// timedTransitionDEPFailure.setOutputArcMultiplicity(placeDEPFailed, 1); +// timedTransitionDEPFailure.setInhibitionArcMultiplicity(placeDEPFailed, 1); +// mGspn.addTimedTransition(timedTransitionDEPFailure); +// } + } + + template + uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement) { + uint64_t unavailableNode = builder.addPlace(defaultCapacity, 1, dftElement->name() + "_unavailable"); + assert(unavailableNode != 0); + unavailableNodes.emplace(dftElement->id(), unavailableNode); + return unavailableNode; + } +// + template + void DftToGspnTransformator::drawGSPNConnections() { +// // Check for every element, if they have parents (all will have at least 1, except the top event). +// for (std::size_t i = 0; i < mDft.nrElements(); i++) { +// auto child = mDft.getElement(i); +// auto parents = child->parentIds(); +// +// // Draw a connection to every parent. +// for (std::size_t j = 0; j < parents.size(); j++) { +// // Check the type of the parent and act accordingly (every parent gate has different entry points...). +// switch (mDft.getElement(parents[j])->type()) { +// case storm::storage::DFTElementType::AND: +// { +// auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING); +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// if (andEntry.first && childExit.first) { // Only add arcs if the objects have been found. +// andEntry.second->setInputArcMultiplicity(childExit.second, 1); +// andEntry.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// break; +// } +// case storm::storage::DFTElementType::OR: +// { +// auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + STR_FAILING); +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// if (orEntry.first && childExit.first) { // Only add arcs if the objects have been found. +// orEntry.second->setInputArcMultiplicity(childExit.second, 1); +// orEntry.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// break; +// } +// case storm::storage::DFTElementType::VOT: +// { +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// auto parentEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_collecting"); +// +// if (childExit.first && parentEntry.first) { // Only add arcs if the objects have been found. +// parentEntry.second->setInputArcMultiplicity(childExit.second, 1); +// parentEntry.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// +// break; +// } +// case storm::storage::DFTElementType::PAND: +// { +// auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING); +// +// if (childExit.first && pandEntry.first) { // Only add arcs if the objects have been found. +// pandEntry.second->setInputArcMultiplicity(childExit.second, 1); +// pandEntry.second->setOutputArcMultiplicity(childExit.second, 1); +// +// if (children[0] == child) { // Current element is primary child. +// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_0" + STR_FAILSAVING); +// +// if (pandEntry2.first) { +// pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); +// } +// } +// else { // Current element is not the primary child. +// for (std::size_t k = 1; k < children.size(); k++) { +// if (children[k] == child) { +// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k - 1)) + STR_FAILSAVING); +// auto pandEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k)) + STR_FAILSAVING); +// +// if (pandEntry2.first) { +// pandEntry2.second->setInputArcMultiplicity(childExit.second, 1); +// pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// +// if (pandEntry3.first) { +// pandEntry3.second->setInhibitionArcMultiplicity(childExit.second, 1); +// } +// +// continue; +// } +// } +// } +// } +// +// break; +// } +// case storm::storage::DFTElementType::SPARE: +// { +// // Check if current child is a primary or spare child. +// auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); +// +// if (child == children[0]) { // Primary child. +// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING); +// +// std::vector ids = getAllBEIDsOfElement(child); +// for (std::size_t k = 0; k < ids.size(); k++) { +// auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED); +// +// if (spareExit.first && childEntry.first) { // Only add arcs if the objects have been found. +// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1); +// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1); +// } +// } +// +// // Draw lines from "primary child_failed" to SPARE. +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + children[1]->name()); +// auto spareEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + children[1]->name() + "_consuming1"); +// +// if (childExit.first && spareEntry.first && spareEntry2.first) { // Only add arcs if the objects have been found. +// spareEntry.second->setInputArcMultiplicity(childExit.second, 1); +// spareEntry.second->setOutputArcMultiplicity(childExit.second, 1); +// +// spareEntry2.second->setInputArcMultiplicity(childExit.second, 1); +// spareEntry2.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// } +// else { // A spare child. +// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING); +// auto spareExit2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name()); +// +// std::vector ids = getAllBEIDsOfElement(child); +// for (std::size_t k = 0; k < ids.size(); k++) { +// auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED); +// +// if (spareExit.first && spareExit2.first && childEntry.first) { // Only add arcs if the objects have been found. +// if (!spareExit.second->existsInhibitionArc(childEntry.second)) { +// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1); +// } +// if (!spareExit.second->existsOutputArc(childEntry.second)) { +// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1); +// } +// if (!spareExit2.second->existsInhibitionArc(childEntry.second)) { +// spareExit2.second->setInhibitionArcMultiplicity(childEntry.second, 1); +// } +// } +// } +// +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name()); +// auto spareEntry2 = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING); +// auto spareEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_consuming2"); +// +// if (childExit.first && spareEntry.first && spareEntry2.first && spareEntry3.first) { // Only add arcs if the objects have been found. +// spareEntry.second->setInhibitionArcMultiplicity(childExit.second, 1); +// +// if (!spareEntry2.second->existsInhibitionArc(childExit.second)) { +// spareEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); +// } +// +// spareEntry3.second->setInputArcMultiplicity(childExit.second, 1); +// spareEntry3.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// } +// +// break; +// } +// case storm::storage::DFTElementType::POR: +// { +// auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); +// auto porEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING); +// auto porEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING); +// auto childExit = mGspn.getPlace(child->name() + STR_FAILED); +// +// if (porEntry.first && porEntry2.first && childExit.first) { // Only add arcs if the objects have been found. +// if (children[0] == child) { // Current element is primary child. +// porEntry.second->setInputArcMultiplicity(childExit.second, 1); +// porEntry.second->setOutputArcMultiplicity(childExit.second, 1); +// porEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); +// +// } +// else { // Current element is not the primary child. +// porEntry2.second->setInputArcMultiplicity(childExit.second, 1); +// porEntry2.second->setOutputArcMultiplicity(childExit.second, 1); +// } +// } +// +// break; +// } +// case storm::storage::DFTElementType::SEQ: +// { +// // Sequences are realized with restrictions. Nothing to do here. +// break; +// } +// case storm::storage::DFTElementType::MUTEX: +// { +// // MUTEX are realized with restrictions. Nothing to do here. +// break; +// } +// case storm::storage::DFTElementType::BE: +// { +// // The parent is never a Basic Event. +// break; +// } +// case storm::storage::DFTElementType::CONSTF: +// { +// // The parent is never a Basic Event. +// break; +// } +// case storm::storage::DFTElementType::CONSTS: +// { +// // The parent is never a Basic Event. +// break; +// } +// case storm::storage::DFTElementType::PDEP: +// { +// // The parent is never a DEP. Hence the connections must be drawn somewhere else. +// break; +// } +// default: +// { +// STORM_LOG_ASSERT(false, "DFT type unknown."); +// break; +// } +// } +// } +// } + } + + template + bool DftToGspnTransformator::isBEActive(std::shared_ptr const> dftElement) + { + // If element is the top element, return true. + if (dftElement->id() == mDft.getTopLevelIndex()) { + return true; + } + else { // Else look at all parents. + auto parents = dftElement->parents(); + std::vector pathValidities; + + for (std::size_t i = 0; i < parents.size(); i++) { + // Add all parents to the vector, except if the parent is a SPARE and the current element is an inactive child of the SPARE. + if (parents[i]->type() == storm::storage::DFTElementType::SPARE) { + auto children = std::static_pointer_cast const>(parents[i])->children(); + if (children[0]->id() != dftElement->id()) { + continue; + } + } + + pathValidities.push_back(isBEActive(parents[i])); + } + + // Check all vector entries. If one is true, a "valid" path has been found. + for (std::size_t i = 0; i < pathValidities.size(); i++) { + if (pathValidities[i]) { + return true; + } + } + } + + // No "valid" path found. BE is inactive. + return false; + } + + template + uint64_t DftToGspnTransformator::getFailPriority(std::shared_ptr const> dftElement) + { + return mDft.maxRank() - dftElement->rank(); + } + + template + void DftToGspnTransformator::drawGSPNDependencies() { +// for (std::size_t i = 0; i < mDft.nrElements(); i++) { +// auto dftElement = mDft.getElement(i); +// +// if (dftElement->isDependency()) { +// std::string gateName = dftElement->name().substr(0, dftElement->name().find("_")); +// auto depEntry = mGspn.getTimedTransition(gateName + STR_FAILING); +// auto trigger = mGspn.getPlace(std::static_pointer_cast const>(dftElement)->nameTrigger() + STR_FAILED); +// +// if (depEntry.first && trigger.first) { // Only add arcs if the objects have been found. +// if (!depEntry.second->existsInputArc(trigger.second)) { +// depEntry.second->setInputArcMultiplicity(trigger.second, 1); +// } +// if (!depEntry.second->existsOutputArc(trigger.second)){ +// depEntry.second->setOutputArcMultiplicity(trigger.second, 1); +// } +// } +// +// auto dependent = mGspn.getPlace(std::static_pointer_cast const>(dftElement)->nameDependent() + STR_FAILED); +// +// if (dependent.first) { // Only add arcs if the objects have been found. +// depEntry.second->setOutputArcMultiplicity(dependent.second, 1); +// } +// } +// } + } + + template + void DftToGspnTransformator::drawGSPNRestrictions() { +// for (std::size_t i = 0; i < mDft.nrElements(); i++) { +// auto dftElement = mDft.getElement(i); +// +// if (dftElement->isRestriction()) { +// switch (dftElement->type()) { +// case storm::storage::DFTElementType::SEQ: +// { +// auto children = mDft.getRestriction(i)->children(); +// +// for (std::size_t j = 0; j < children.size() - 1; j++) { +// auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED); +// +// switch (children[j + 1]->type()) { +// case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions. +// { +// auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing"); +// auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing"); +// +// if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found. +// suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1); +// suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1); +// suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1); +// suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1); +// } +// break; +// } +// default: // If supressed is not a BE, add single arc to immediate transition. +// { +// auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING); +// +// if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found. +// suppressed.second->setInputArcMultiplicity(suppressor.second, 1); +// suppressed.second->setOutputArcMultiplicity(suppressor.second, 1); +// } +// break; +// } +// } +// } +// break; +// } +// case storm::storage::DFTElementType::MUTEX: +// { +// // MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here. +// STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator."); +// break; +// } +// default: +// { +// break; +// } +// } +// } +// } + } + + template + std::vector DftToGspnTransformator::getAllBEIDsOfElement(std::shared_ptr const> dftElement) { +// std::vector ids; +// +// switch (dftElement->type()) { +// case storm::storage::DFTElementType::AND: +// { +// auto children = std::static_pointer_cast const>(dftElement)->children(); +// +// for (std::size_t i = 0; i < children.size(); i++) { +// std::vector newIds = getAllBEIDsOfElement(children[i]); +// ids.insert(ids.end(), newIds.begin(), newIds.end()); +// } +// break; +// } +// case storm::storage::DFTElementType::OR: +// { +// auto children = std::static_pointer_cast const>(dftElement)->children(); +// +// for (std::size_t i = 0; i < children.size(); i++) { +// std::vector newIds = getAllBEIDsOfElement(children[i]); +// ids.insert(ids.end(), newIds.begin(), newIds.end()); +// } +// break; +// } +// case storm::storage::DFTElementType::VOT: +// { +// auto children = std::static_pointer_cast const>(dftElement)->children(); +// +// for (std::size_t i = 0; i < children.size(); i++) { +// std::vector newIds = getAllBEIDsOfElement(children[i]); +// ids.insert(ids.end(), newIds.begin(), newIds.end()); +// } +// break; +// } +// case storm::storage::DFTElementType::PAND: +// { +// auto children = std::static_pointer_cast const>(dftElement)->children(); +// +// for (std::size_t i = 0; i < children.size(); i++) { +// std::vector newIds = getAllBEIDsOfElement(children[i]); +// ids.insert(ids.end(), newIds.begin(), newIds.end()); +// } +// break; +// } +// case storm::storage::DFTElementType::SPARE: +// { +// auto children = std::static_pointer_cast const>(dftElement)->children(); +// +// // Only regard the primary child of a SPARE. The spare childs are not allowed to be listed here. +// for (std::size_t i = 0; i < 1; i++) { +// std::vector newIds = getAllBEIDsOfElement(children[i]); +// ids.insert(ids.end(), newIds.begin(), newIds.end()); +// } +// break; +// } +// case storm::storage::DFTElementType::POR: +// { +// auto children = std::static_pointer_cast const>(dftElement)->children(); +// +// for (std::size_t i = 0; i < children.size(); i++) { +// std::vector newIds = getAllBEIDsOfElement(children[i]); +// ids.insert(ids.end(), newIds.begin(), newIds.end()); +// } +// break; +// } +// case storm::storage::DFTElementType::BE: +// case storm::storage::DFTElementType::CONSTF: +// case storm::storage::DFTElementType::CONSTS: +// { +// ids.push_back(dftElement->id()); +// break; +// } +// case storm::storage::DFTElementType::SEQ: +// case storm::storage::DFTElementType::MUTEX: +// case storm::storage::DFTElementType::PDEP: +// { +// break; +// } +// default: +// { +// STORM_LOG_ASSERT(false, "DFT type unknown."); +// break; +// } +// } +// +// return ids; + } + + template + void DftToGspnTransformator::writeGspn(bool toFile) { + if (toFile) { + // Writing to file + std::ofstream file; + file.open("gspn.dot"); + storm::gspn::GSPN* gspn = builder.buildGspn(); + gspn->writeDotToStream(file); + delete gspn; + file.close(); + } else { + // Writing to console + storm::gspn::GSPN* gspn = builder.buildGspn(); + gspn->writeDotToStream(std::cout); + delete gspn; + } + } + + // Explicitly instantiate the class. + template class DftToGspnTransformator; + + + #ifdef STORM_HAVE_CARL + // template class DftToGspnTransformator; + #endif + + } // namespace dft + } // namespace transformations +} // namespace storm + + diff --git a/src/storm/transformations/dft/DftToGspnTransformator.h b/src/storm/transformations/dft/DftToGspnTransformator.h new file mode 100644 index 000000000..76250bfbf --- /dev/null +++ b/src/storm/transformations/dft/DftToGspnTransformator.h @@ -0,0 +1,174 @@ +#pragma once + +#include "storm/storage/dft/DFT.h" +#include "storm/storage/gspn/GSPN.h" +#include "storm/storage/gspn/GspnBuilder.h" + +namespace storm { + namespace transformations { + namespace dft { + + /*! + * Transformator for DFT -> GSPN. + */ + template + class DftToGspnTransformator { + + public: + /*! + * Constructor. + * + * @param dft DFT + */ + DftToGspnTransformator(storm::storage::DFT const& dft); + + /*! + * Transform the DFT to a GSPN. + */ + void transform(); + + private: + /*! + * Write Gspn to file or console. + * + * @param toFile If true, the GSPN will be written to a file, otherwise it will + be written to the console. + */ + void writeGspn(bool toFile); + + /* + * Draw all elements of the GSPN. + */ + void drawGSPNElements(); + + /* + * Draw the connections between the elements of the GSPN. + */ + void drawGSPNConnections(); + + /* + * Draw functional/probability dependencies into the GSPN. + */ + void drawGSPNDependencies(); + + /* + * Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). + */ + void drawGSPNRestrictions(); + + /* + * Draw a Petri net Basic Event. + * + * @param dftBE The Basic Event. + */ + void drawBE(std::shared_ptr const> dftBE, bool isRepresentative); + + /* + * Draw a Petri net AND. + * + * @param dftAnd The AND gate. + */ + void drawAND(std::shared_ptr const> dftAnd, bool isRepresentative); + + /* + * Draw a Petri net OR. + * + * @param dftOr The OR gate. + */ + void drawOR(std::shared_ptr const> dftOr, bool isRepresentative); + + /* + * Draw a Petri net VOT. + * + * @param dftVot The VOT gate. + */ + void drawVOT(std::shared_ptr const> dftVot, bool isRepresentative); + + /* + * Draw a Petri net PAND. + * This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless). + * + * @param dftPand The PAND gate. + */ + void drawPAND(std::shared_ptr const> dftPand, bool isRepresentative); + + /* + * Draw a Petri net 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, bool isRepresentative); + + /* + * Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token). + * + * @param dFTElement DFT element. + */ + bool isBEActive(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. + * + * @param priority The priority of the gate. Top Event has priority 0, its children 2, its grandchildren 4, ... + * + * @param dftElement The element whose priority shall be determined. + */ + uint64_t getFailPriority(std::shared_ptr const> dFTElement); + + /* + * Return all ids of BEs, that are successors of the given element and that are not the spare childs of a SPARE. + * + * @param dftElement The element which + */ + std::vector getAllBEIDsOfElement(std::shared_ptr const> dftElement); + + + uint64_t addUnavailableNode(std::shared_ptr const> dftElement); + + storm::storage::DFT const& mDft; + storm::gspn::GspnBuilder builder; + std::vector failedNodes; + std::map unavailableNodes; + std::map activeNodes; + + 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. + static constexpr const char* STR_FAILED = "_failed"; // Name standard for place which indicates the failure of a gate. + static constexpr const char* STR_FAILSAVING = "_failsaving"; // Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate. + static constexpr const char* STR_FAILSAVE = "_failsave"; // Name standard for place which indicates the failsave state of a gate. + static constexpr const char* STR_ACTIVATED = "_activated"; // Name standard for place which indicates the activity. + static constexpr const char* STR_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity. + + + }; + } + } +} +