From f2a8c1be401c0e9a934f597e90220a02b57fd4bc Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Fri, 2 Dec 2016 14:12:19 +0100 Subject: [PATCH] post-rebase fix --- .../DftToGspnTransformator.cpp | 477 +----------------- 1 file changed, 3 insertions(+), 474 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index f63e80f0a..49f58707f 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -221,10 +221,7 @@ 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 + } } // @@ -238,11 +235,7 @@ 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; @@ -278,127 +271,17 @@ 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 @@ -427,18 +310,12 @@ 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 @@ -472,237 +349,13 @@ 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) @@ -744,38 +397,7 @@ 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() { @@ -833,100 +455,7 @@ 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) {