From 2291569bc7792ac73e15e9cc48566d92b4aa31f8 Mon Sep 17 00:00:00 2001
From: mdeutschen <michael.deutschen@rwth-aachen.de>
Date: Wed, 17 Aug 2016 12:01:04 +0200
Subject: [PATCH] Added transformation for SEQ
Former-commit-id: b9bb2beba5705f818033e36d072eb6439a2a1069
---
.../dft/DftToGspnTransformator.cpp | 42 ++++++++++++++++++-
.../dft/DftToGspnTransformator.h | 5 +++
2 files changed, 45 insertions(+), 2 deletions(-)
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 <typename ValueType>
+ void DftToGspnTransformator<ValueType>::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 <typename ValueType>
void DftToGspnTransformator<ValueType>::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.
*