From 297f3ff48076dbf9b67056c82bc97409ef9fd445 Mon Sep 17 00:00:00 2001 From: sjunges Date: Tue, 22 Nov 2016 09:56:00 +0100 Subject: [PATCH] some cleaning and minor additions to dft->gspn translation --- .../dft/DftToGspnTransformator.cpp | 468 +----------------- .../dft/DftToGspnTransformator.h | 22 +- 2 files changed, 18 insertions(+), 472 deletions(-) diff --git a/src/storm/transformations/dft/DftToGspnTransformator.cpp b/src/storm/transformations/dft/DftToGspnTransformator.cpp index 4331e0c62..730656b35 100644 --- a/src/storm/transformations/dft/DftToGspnTransformator.cpp +++ b/src/storm/transformations/dft/DftToGspnTransformator.cpp @@ -22,16 +22,10 @@ namespace storm { // 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(); - + //drawGSPNRestrictions(); + // Write GSPN to file. writeGspn(true); } @@ -227,7 +221,6 @@ 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); - } } // @@ -241,7 +234,7 @@ namespace storm { unavailableNode = addUnavailableNode(dftSpare); } uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED); - activeNodes.emplace(dftBE->id(), beActive); + activeNodes.emplace(dftSpare->id(), spareActive); std::vector cucNodes; @@ -277,116 +270,16 @@ namespace storm { 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 @@ -415,10 +308,11 @@ namespace storm { // 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); + failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED)); + uint64_t unavailableNode = 0; + if (isRepresentative) { + unavailableNode = addUnavailableNode(dftConstF, false); + } } // template @@ -452,228 +346,14 @@ namespace storm { } template - uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement) { - uint64_t unavailableNode = builder.addPlace(defaultCapacity, 1, dftElement->name() + "_unavailable"); + uint64_t DftToGspnTransformator::addUnavailableNode(std::shared_ptr const> dftElement, bool initialAvailable) { + uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 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) @@ -715,34 +395,7 @@ namespace storm { { 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() { @@ -800,96 +453,7 @@ namespace storm { // } // } } - - 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) { diff --git a/src/storm/transformations/dft/DftToGspnTransformator.h b/src/storm/transformations/dft/DftToGspnTransformator.h index 76250bfbf..1e0d3eb69 100644 --- a/src/storm/transformations/dft/DftToGspnTransformator.h +++ b/src/storm/transformations/dft/DftToGspnTransformator.h @@ -40,17 +40,6 @@ namespace storm { * 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). */ @@ -142,16 +131,9 @@ namespace storm { * @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); + uint64_t addUnavailableNode(std::shared_ptr const> dftElement, bool initialAvailable = true); storm::storage::DFT const& mDft; storm::gspn::GspnBuilder builder;