From 0fa736d4588650eee8d3cddd597a427682d760bd Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Mon, 21 Nov 2016 22:05:10 +0100 Subject: [PATCH] updated dft->gspn translation to now have basis support for spares --- .../dft/DftToGspnTransformator.cpp | 473 ++++++++++++++++++ 1 file changed, 473 insertions(+) diff --git a/src/storm/transformations/dft/DftToGspnTransformator.cpp b/src/storm/transformations/dft/DftToGspnTransformator.cpp index 730656b35..f63e80f0a 100644 --- a/src/storm/transformations/dft/DftToGspnTransformator.cpp +++ b/src/storm/transformations/dft/DftToGspnTransformator.cpp @@ -221,6 +221,10 @@ namespace storm { builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); builder.addOutputArc(tfs, nodeFS); +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + +>>>>>>> updated dft->gspn translation to now have basis support for spares } } // @@ -234,7 +238,11 @@ namespace storm { unavailableNode = addUnavailableNode(dftSpare); } uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED); +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 activeNodes.emplace(dftSpare->id(), spareActive); +======= + activeNodes.emplace(dftBE->id(), beActive); +>>>>>>> updated dft->gspn translation to now have basis support for spares std::vector cucNodes; @@ -270,16 +278,127 @@ namespace storm { builder.addInputArc(failedNodes.at(child->id()), tnextcl); builder.addOutputArc(tnextcl, failedNodes.at(child->id())); nextclTransitions.push_back(tnextcl); +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + + +>>>>>>> updated dft->gspn translation to now have basis support for spares ++j; } builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); builder.addOutputArc(nextclTransitions.back(), nodeFailed); +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + +>>>>>>> updated dft->gspn translation to now have basis support for spares if (isRepresentative) { builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); builder.addOutputArc(nextclTransitions.back(), unavailableNode); } +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + + +// 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); +// } +>>>>>>> updated dft->gspn translation to now have basis support for spares } // template @@ -308,11 +427,18 @@ namespace storm { // template void DftToGspnTransformator::drawCONSTF(std::shared_ptr const> dftConstF, bool isRepresentative) { +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED)); uint64_t unavailableNode = 0; if (isRepresentative) { unavailableNode = addUnavailableNode(dftConstF, false); } +======= +// storm::gspn::Place placeCONSTFFailed; +// placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED); +// placeCONSTFFailed.setNumberOfInitialTokens(1); +// mGspn.addPlace(placeCONSTFFailed); +>>>>>>> updated dft->gspn translation to now have basis support for spares } // template @@ -346,14 +472,237 @@ namespace storm { } template +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement, bool initialAvailable) { uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable"); +======= + uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement) { + uint64_t unavailableNode = builder.addPlace(defaultCapacity, 1, dftElement->name() + "_unavailable"); +>>>>>>> updated dft->gspn translation to now have basis support for spares assert(unavailableNode != 0); unavailableNodes.emplace(dftElement->id(), unavailableNode); return unavailableNode; } // +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + 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; +// } +// } +// } +// } + } +>>>>>>> updated dft->gspn translation to now have basis support for spares template bool DftToGspnTransformator::isBEActive(std::shared_ptr const> dftElement) @@ -395,7 +744,38 @@ namespace storm { { return mDft.maxRank() - dftElement->rank(); } +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + + 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); +// } +// } +// } + } +>>>>>>> updated dft->gspn translation to now have basis support for spares template void DftToGspnTransformator::drawGSPNRestrictions() { @@ -453,7 +833,100 @@ namespace storm { // } // } } +<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791 +======= + + 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; + } + +>>>>>>> updated dft->gspn translation to now have basis support for spares template void DftToGspnTransformator::writeGspn(bool toFile) { if (toFile) {