sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

some cleaning and minor additions to dft->gspn translation

tempestpy_adaptions
sjunges 8 years ago
committed by Sebastian Junges
parent
faee1dfeee
commit
297f3ff480
2 changed files with 18 additions and 472 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 468
      src/storm/transformations/dft/DftToGspnTransformator.cpp
  2. 22
      src/storm/transformations/dft/DftToGspnTransformator.h

468
src/storm/transformations/dft/DftToGspnTransformator.cpp
View File

@ -22,16 +22,10 @@ namespace storm {
// Loop through every DFT element and draw them as a GSPN. // Loop through every DFT element and draw them as a GSPN.
drawGSPNElements(); 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). // Draw restrictions into the GSPN (i.e. SEQ or MUTEX).
drawGSPNRestrictions();
//drawGSPNRestrictions();
// Write GSPN to file. // Write GSPN to file.
writeGspn(true); writeGspn(true);
} }
@ -227,7 +221,6 @@ namespace storm {
builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs);
builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs);
builder.addOutputArc(tfs, nodeFS); builder.addOutputArc(tfs, nodeFS);
} }
} }
// //
@ -241,7 +234,7 @@ namespace storm {
unavailableNode = addUnavailableNode(dftSpare); unavailableNode = addUnavailableNode(dftSpare);
} }
uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED); uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED);
activeNodes.emplace(dftBE->id(), beActive);
activeNodes.emplace(dftSpare->id(), spareActive);
std::vector<uint64_t> cucNodes; std::vector<uint64_t> cucNodes;
@ -277,116 +270,16 @@ namespace storm {
builder.addInputArc(failedNodes.at(child->id()), tnextcl); builder.addInputArc(failedNodes.at(child->id()), tnextcl);
builder.addOutputArc(tnextcl, failedNodes.at(child->id())); builder.addOutputArc(tnextcl, failedNodes.at(child->id()));
nextclTransitions.push_back(tnextcl); nextclTransitions.push_back(tnextcl);
++j; ++j;
} }
builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed);
builder.addOutputArc(nextclTransitions.back(), nodeFailed); builder.addOutputArc(nextclTransitions.back(), nodeFailed);
if (isRepresentative) { if (isRepresentative) {
builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode);
builder.addOutputArc(nextclTransitions.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<storm::gspn::GSPN::WeightType> 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<storm::gspn::GSPN::WeightType> 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<storm::gspn::GSPN::WeightType> 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<storm::gspn::GSPN::WeightType> 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<storm::gspn::GSPN::WeightType> 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 <typename ValueType> template <typename ValueType>
@ -415,10 +308,11 @@ namespace storm {
// //
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF, bool isRepresentative) { void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> 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 <typename ValueType> template <typename ValueType>
@ -452,228 +346,14 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
uint64_t unavailableNode = builder.addPlace(defaultCapacity, 1, dftElement->name() + "_unavailable");
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, bool initialAvailable) {
uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable");
assert(unavailableNode != 0); assert(unavailableNode != 0);
unavailableNodes.emplace(dftElement->id(), unavailableNode); unavailableNodes.emplace(dftElement->id(), unavailableNode);
return unavailableNode; return unavailableNode;
} }
// //
template <typename ValueType>
void DftToGspnTransformator<ValueType>::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<storm::storage::DFTPand<ValueType> 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<storm::storage::DFTSpare<ValueType> const>(mDft.getElement(parents[j]))->children();
//
// if (child == children[0]) { // Primary child.
// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
//
// std::vector<int> 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<int> 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<storm::storage::DFTPand<ValueType> 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 <typename ValueType> template <typename ValueType>
bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
@ -715,34 +395,7 @@ namespace storm {
{ {
return mDft.maxRank() - dftElement->rank(); return mDft.maxRank() - dftElement->rank();
} }
template <typename ValueType>
void DftToGspnTransformator<ValueType>::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<storm::storage::DFTDependency<ValueType> 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<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameDependent() + STR_FAILED);
//
// if (dependent.first) { // Only add arcs if the objects have been found.
// depEntry.second->setOutputArcMultiplicity(dependent.second, 1);
// }
// }
// }
}
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() { void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
@ -800,96 +453,7 @@ namespace storm {
// } // }
// } // }
} }
template <typename ValueType>
std::vector<int> DftToGspnTransformator<ValueType>::getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// std::vector<int> ids;
//
// switch (dftElement->type()) {
// case storm::storage::DFTElementType::AND:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::OR:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::VOT:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::PAND:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::SPARE:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> 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<int> newIds = getAllBEIDsOfElement(children[i]);
// ids.insert(ids.end(), newIds.begin(), newIds.end());
// }
// break;
// }
// case storm::storage::DFTElementType::POR:
// {
// auto children = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->children();
//
// for (std::size_t i = 0; i < children.size(); i++) {
// std::vector<int> 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 <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) { void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) {
if (toFile) { if (toFile) {

22
src/storm/transformations/dft/DftToGspnTransformator.h
View File

@ -40,17 +40,6 @@ namespace storm {
* Draw all elements of the GSPN. * Draw all elements of the GSPN.
*/ */
void drawGSPNElements(); 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). * 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. * @param dftElement The element whose priority shall be determined.
*/ */
uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement); uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> 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<int> getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement);
uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement);
uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, bool initialAvailable = true);
storm::storage::DFT<ValueType> const& mDft; storm::storage::DFT<ValueType> const& mDft;
storm::gspn::GspnBuilder builder; storm::gspn::GspnBuilder builder;

Write Preview
Loading…
Cancel
Save