Extended SEQ to support children which are not BEs

Former-commit-id: 2ed806b4ba

examples/dft/seq6.dft

@@ -0,0 +1,7 @@
+toplevel "A";
+"A" and "B" "C";
+"X" seq "B" "C"
+"B" lambda=0.5 dorm=0.3;
+"C" and "D" "E";
+"D" lambda=0.5 dorm=0.3;
+"E" lambda=0.5 dorm=0.3;

src/transformations/dft/DftToGspnTransformator.cpp

@@ -465,6 +465,10 @@ namespace storm {
 								
 								for (std::size_t j = 0; j < children.size() - 1; j++) {
 									auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED);
+									
+									switch (children[j + 1]->type()) {
+										case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions.
+										{
 											auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing");
 											auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing");
 											
@@ -474,6 +478,19 @@ namespace storm {
 												suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1);
 												suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1);
 											}
+											break;
+										}
+										default: // If supressed is not a BE, add single arc to immediate transition.
+										{
+											auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING);
+											
+											if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found.
+												suppressed.second->setInputArcMultiplicity(suppressor.second, 1);
+												suppressed.second->setOutputArcMultiplicity(suppressor.second, 1);
+											}
+											break;
+										}
+									}
 								}
 								break;
 							}
@@ -485,9 +502,6 @@ namespace storm {
 						}
 					}
 				}
-				
-				// 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>