Implementation of simple and incomplete isBEActive()

Former-commit-id: 13ae5b0f31

examples/dft/be.dft

@@ -0,0 +1,2 @@
+toplevel "A";
+"A" lambda=0.5 dorm=0.3;

src/transformations/dft/DftToGspnTransformator.cpp

@@ -87,7 +87,7 @@ namespace storm {
             void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
 				storm::gspn::Place placeBEActivated;
 				placeBEActivated.setName(dftBE->name() + "_activated");
-				placeBEActivated.setNumberOfInitialTokens(true ? 1 : 0); // TODO: Check if BE is spare child of a SPARE.
+				placeBEActivated.setNumberOfInitialTokens(isBEActive(dftBE) ? 1 : 0); // TODO: Check if BE is spare child of a SPARE.
 				mGspn.addPlace(placeBEActivated);
 				
 				storm::gspn::Place placeBEFailed;
@@ -496,6 +496,29 @@ namespace storm {
 				}
 			}
 			
+			template <typename ValueType>
+            bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE)
+			{
+				// TODO: Fix for higher lvl layers, maybe recursive?
+				
+				// Check all paths to the top event.
+				// If all paths are intervened by a SPARE, and the BE is never the primary child, it is not activated.
+				
+				if (dftBE->id() == mDft.getTopLevelIndex()) {
+					return true;
+				}
+				
+				auto parents = dftBE->parents();
+				for (std::size_t i = 0; i < parents.size(); i++) {
+					if (parents[i]->id() == mDft.getTopLevelIndex()) {
+						return true;
+					}
+				}
+				
+				// No "valid" path found. BE is inactive.
+				return false;
+			}
+			
 			template <typename ValueType>
             void DftToGspnTransformator<ValueType>::drawGSPNDependencies() {
 				for (std::size_t i = 0; i < mDft.nrElements(); i++) {

src/transformations/dft/DftToGspnTransformator.h

@@ -180,6 +180,8 @@ namespace storm {
 				  * http://www.geeksforgeeks.org/print-all-possible-combinations-of-r-elements-in-a-given-array-of-size-n/
 				  */
 				 void combinationUtil(std::vector<int> &output, std::vector<int> childrenIds, std::vector<int> subsets, int start, int end, int index, int threshold);
+				 
+				 bool isBEActive(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE);
             };
         }
     }