diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index be1dd62ab..cc9d7de9c 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -22,8 +22,8 @@ namespace storm { // When all DFT elements are drawn, draw the connections between them. drawGSPNConnections(); - // TODO: For sequences: - // drawGSPNRestrictions(); ? + // Draw restrictions into the GSPN (i.e. SEQ). + drawGSPNRestrictions(); // Write GSPN to file. writeGspn(true); @@ -452,6 +452,44 @@ namespace storm { } } + template + void DftToGspnTransformator::drawGSPNRestrictions() { + for (std::size_t i = 0; i < mDft.nrElements(); i++) { + auto dftElement = mDft.getElement(i); + + if (dftElement->isRestriction()) { + switch (dftElement->type()) { + case storm::storage::DFTElementType::SEQ: + { + auto children = mDft.getRestriction(i)->children(); + + for (std::size_t j = 0; j < children.size() - 1; j++) { + auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED); + auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing"); + auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing"); + + if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found. + suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1); + suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1); + suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1); + suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1); + } + } + break; + } + default: + { + // TODO: Are there other restrictions than SEQ? + break; + } + } + } + } + + // TODO: Check if children are BE or Elements. For BE, you must draw 2 arcs instead of 1 (supposedly)! + // TODO: Are SEQ restricted to BEs? If yes, above TODO can be ignored. + } + template void DftToGspnTransformator::writeGspn(bool toFile) { if (toFile) { diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 4ff667b51..579879792 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -57,6 +57,11 @@ namespace storm { */ void drawGSPNConnections(); + /* + * Draw restrictions between the elements of the GSPN (i.e. SEQ). + */ + void drawGSPNRestrictions(); + /* * Draw a Petri net Basic Event. *