Nested SPAREs working. Hence, SPARE is completely implemented

Former-commit-id: 443ddc971a

examples/dft/spare11.dft

@@ -0,0 +1,11 @@
+toplevel "OR";
+"OR" or "A" "B";
+"A" wsp "AND" "C";
+"B" wsp "C" "R" "S";
+"C" wsp "Q" "R";
+"AND" and "P" "Q";
+"P" lambda=0.1 dorm=0.9;
+"Q" lambda=0.2 dorm=0.8;
+"R" lambda=0.3 dorm=0.7;
+"S" lambda=0.4 dorm=0.6;
+

src/transformations/dft/DftToGspnTransformator.cpp

@@ -213,6 +213,8 @@ namespace storm {
             void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {	
 				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));
@@ -225,6 +227,7 @@ namespace storm {
 				immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1);
 				immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1);
 				mGspn.addImmediateTransition(immediateTransitionPCActivating);
+				*/
 				
 				auto children = dftSpare->children();
 				
@@ -663,8 +666,6 @@ namespace storm {
 			template <typename ValueType>
             bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement)
 			{
-				// TODO: This method must be tested again after SPAREs are implemented.
-				
 				// If element is the top element, return true.
 				if (dftElement->id() == mDft.getTopLevelIndex()) {
 					return true;

src/transformations/dft/DftToGspnTransformator.h

@@ -201,7 +201,7 @@ namespace storm {
 				 uint_fast64_t getPriority(uint_fast64_t priority, std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
 				 
 				 /*
-				  * Return all ids of BEs, that are successors of the given element.
+				  * 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 
 				  */