From 752f20a65f12ce065f36cd3e66bc61ae341551e8 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 18 Nov 2016 10:34:31 +0100 Subject: [PATCH] removed transformators for now --- .../dft/DftToGspnTransformator.cpp | 845 ------------------ .../dft/DftToGspnTransformator.h | 170 ---- 2 files changed, 1015 deletions(-) delete mode 100644 src/transformations/dft/DftToGspnTransformator.cpp delete mode 100644 src/transformations/dft/DftToGspnTransformator.h diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp deleted file mode 100644 index 68114bf94..000000000 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ /dev/null @@ -1,845 +0,0 @@ -#include "src/transformations/dft/DftToGspnTransformator.h" -#include "src/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); - - // 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)); - break; - case storm::storage::DFTElementType::OR: - drawOR(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::VOT: - drawVOT(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::PAND: - drawPAND(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::SPARE: - drawSPARE(std::static_pointer_cast const>(dftElement)); - break; - case storm::storage::DFTElementType::POR: - drawPOR(std::static_pointer_cast const>(dftElement)); - 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)); - break; - case storm::storage::DFTElementType::CONSTF: - drawCONSTF(dftElement); - break; - case storm::storage::DFTElementType::CONSTS: - drawCONSTS(dftElement); - break; - case storm::storage::DFTElementType::PDEP: - drawPDEP(std::static_pointer_cast const>(dftElement)); - break; - default: - STORM_LOG_ASSERT(false, "DFT type unknown."); - break; - } - } - } - - template - void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE) { - uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); - uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); - 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(tActive, beFailed); - } - - template - void DftToGspnTransformator::drawAND(std::shared_ptr const> dftAnd) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED); - assert(failedNodes.size() == dftAnd->id()); - failedNodes.push_back(nodeFailed); - uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd) , 0.0, dftAnd->name() + STR_FAILING ); - builder.addInhibitionArc(nodeFailed, tAndFailed); - builder.addOutputArc(tAndFailed, nodeFailed); - 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) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED); - assert(failedNodes.size() == dftOr->id()); - failedNodes.push_back(nodeFailed); - 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); - assert(failedNodes.size() > child->id()); - builder.addInputArc(failedNodes[child->id()], tNodeFailed); - ++i; - } - } - - template - void DftToGspnTransformator::drawVOT(std::shared_ptr const> dftVot) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED); - assert(failedNodes.size() == dftVot->id()); - failedNodes.push_back(nodeFailed); - 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); - 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) { - uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED); - assert(failedNodes.size() == dftPand->id()); - failedNodes.push_back(nodeFailed); - 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); - 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); - - } - -// -// storm::gspn::Place placePANDFailed; -// placePANDFailed.setName(dftPand->name() + STR_FAILED); -// placePANDFailed.setNumberOfInitialTokens(0); -// mGspn.addPlace(placePANDFailed); -// -// storm::gspn::Place placePANDFailsave; -// placePANDFailsave.setName(dftPand->name() + STR_FAILSAVE); -// placePANDFailsave.setNumberOfInitialTokens(0); -// mGspn.addPlace(placePANDFailsave); -// -// storm::gspn::ImmediateTransition immediateTransitionPANDFailing; -// immediateTransitionPANDFailing.setName(dftPand->name() + STR_FAILING); -// immediateTransitionPANDFailing.setPriority(priority); -// immediateTransitionPANDFailing.setWeight(0.0); -// immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailed, 1); -// immediateTransitionPANDFailing.setInhibitionArcMultiplicity(placePANDFailsave, 1); -// immediateTransitionPANDFailing.setOutputArcMultiplicity(placePANDFailed, 1); -// mGspn.addImmediateTransition(immediateTransitionPANDFailing); -// -// for (std::size_t i = 0; i < dftPand->nrChildren() -1; i++) { -// storm::gspn::ImmediateTransition immediateTransitionPANDFailsave; -// immediateTransitionPANDFailsave.setName(dftPand->name() + "_" + std::to_string(i) + STR_FAILSAVING); -// immediateTransitionPANDFailsave.setPriority(priority); -// immediateTransitionPANDFailsave.setWeight(0.0); -// immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1); -// immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1); -// mGspn.addImmediateTransition(immediateTransitionPANDFailsave); -// } - } -// - template - void DftToGspnTransformator::drawSPARE(std::shared_ptr const> dftSpare) { -// 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) { -// uint_fast64_t priority = getPriority(0, dftPor); -// -// storm::gspn::Place placePORFailed; -// placePORFailed.setName(dftPor->name() + STR_FAILED); -// placePORFailed.setNumberOfInitialTokens(0); -// mGspn.addPlace(placePORFailed); -// -// storm::gspn::Place placePORFailsave; -// placePORFailsave.setName(dftPor->name() + STR_FAILSAVE); -// placePORFailsave.setNumberOfInitialTokens(0); -// mGspn.addPlace(placePORFailsave); -// -// storm::gspn::ImmediateTransition immediateTransitionPORFailing; -// immediateTransitionPORFailing.setName(dftPor->name() + STR_FAILING); -// immediateTransitionPORFailing.setPriority(priority); -// immediateTransitionPORFailing.setWeight(0.0); -// immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailed, 1); -// immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailsave, 1); -// immediateTransitionPORFailing.setOutputArcMultiplicity(placePORFailed, 1); -// mGspn.addImmediateTransition(immediateTransitionPORFailing); -// -// storm::gspn::ImmediateTransition immediateTransitionPORFailsave; -// immediateTransitionPORFailsave.setName(dftPor->name() + STR_FAILSAVING); -// immediateTransitionPORFailsave.setPriority(priority); -// immediateTransitionPORFailsave.setWeight(0.0); -// immediateTransitionPORFailsave.setInhibitionArcMultiplicity(placePORFailsave, 1); -// immediateTransitionPORFailsave.setOutputArcMultiplicity(placePORFailsave, 1); -// mGspn.addImmediateTransition(immediateTransitionPORFailsave); - } -// - template - void DftToGspnTransformator::drawCONSTF(std::shared_ptr const> dftConstF) { -// 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) { -// 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)) { -// // 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 - 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/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h deleted file mode 100644 index 3b29f40d6..000000000 --- a/src/transformations/dft/DftToGspnTransformator.h +++ /dev/null @@ -1,170 +0,0 @@ -#pragma once - -#include -#include "src/storage/gspn/GSPN.h" -#include "src/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); - - /* - * Draw a Petri net AND. - * - * @param dftAnd The AND gate. - */ - void drawAND(std::shared_ptr const> dftAnd); - - /* - * Draw a Petri net OR. - * - * @param dftOr The OR gate. - */ - void drawOR(std::shared_ptr const> dftOr); - - /* - * Draw a Petri net VOT. - * - * @param dftVot The VOT gate. - */ - void drawVOT(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). - * - * @param dftPand The PAND gate. - */ - void drawPAND(std::shared_ptr const> dftPand); - - /* - * Draw a Petri net SPARE. - * - * @param dftSpare The SPARE gate. - */ - void drawSPARE(std::shared_ptr const> dftSpare); - - /* - * 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); - - /* - * 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); - - /* - * 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); - - /* - * Draw a Petri net PDEP (FDEP is included with a firerate of 1). - */ - void drawPDEP(std::shared_ptr const>(dftDependency)); - - /* - * 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); - - - storm::storage::DFT const& mDft; - storm::gspn::GspnBuilder builder; - std::vector failedNodes; - - 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. - - - }; - } - } -} -