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

updated dft->gspn translation to now have basis support for spares

tempestpy_adaptions
Sebastian Junges 8 years ago
parent
2b7610244d
commit
0fa736d458
1 changed files with 473 additions and 0 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. 473
      src/storm/transformations/dft/DftToGspnTransformator.cpp

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

@ -221,6 +221,10 @@ 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);
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
=======
>>>>>>> updated dft->gspn translation to now have basis support for spares
} }
} }
// //
@ -234,7 +238,11 @@ 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);
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
activeNodes.emplace(dftSpare->id(), spareActive); activeNodes.emplace(dftSpare->id(), spareActive);
=======
activeNodes.emplace(dftBE->id(), beActive);
>>>>>>> updated dft->gspn translation to now have basis support for spares
std::vector<uint64_t> cucNodes; std::vector<uint64_t> cucNodes;
@ -270,16 +278,127 @@ 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);
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
=======
>>>>>>> updated dft->gspn translation to now have basis support for spares
++j; ++j;
} }
builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed);
builder.addOutputArc(nextclTransitions.back(), nodeFailed); builder.addOutputArc(nextclTransitions.back(), nodeFailed);
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
=======
>>>>>>> updated dft->gspn translation to now have basis support for spares
if (isRepresentative) { if (isRepresentative) {
builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode);
builder.addOutputArc(nextclTransitions.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<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);
// }
>>>>>>> updated dft->gspn translation to now have basis support for spares
} }
// //
template <typename ValueType> template <typename ValueType>
@ -308,11 +427,18 @@ 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) {
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED)); failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED));
uint64_t unavailableNode = 0; uint64_t unavailableNode = 0;
if (isRepresentative) { if (isRepresentative) {
unavailableNode = addUnavailableNode(dftConstF, false); 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 <typename ValueType> template <typename ValueType>
@ -346,14 +472,237 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, bool initialAvailable) { 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"); uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavailable");
=======
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> 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); assert(unavailableNode != 0);
unavailableNodes.emplace(dftElement->id(), unavailableNode); unavailableNodes.emplace(dftElement->id(), unavailableNode);
return unavailableNode; return unavailableNode;
} }
// //
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
=======
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;
// }
// }
// }
// }
}
>>>>>>> updated dft->gspn translation to now have basis support for spares
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)
@ -395,7 +744,38 @@ namespace storm {
{ {
return mDft.maxRank() - dftElement->rank(); return mDft.maxRank() - dftElement->rank();
} }
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
=======
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);
// }
// }
// }
}
>>>>>>> updated dft->gspn translation to now have basis support for spares
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() { void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
@ -453,7 +833,100 @@ namespace storm {
// } // }
// } // }
} }
<<<<<<< fcc5d69a44cb202290c4db3c5b2062ff35da5791
=======
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;
}
>>>>>>> updated dft->gspn translation to now have basis support for spares
template <typename ValueType> template <typename ValueType>
void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) { void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) {
if (toFile) { if (toFile) {

Write Preview
Loading…
Cancel
Save