Use map to avoid recalculation of VOTE associations

Former-commit-id: 2c680f89b6

examples/dft/voting3.dft

@@ -1,7 +1,11 @@
 toplevel "A";
-"A" 3of5 "B" "C" "D" "E" "F";
+"A" 5of9 "B" "C" "D" "E" "F" "G" "H" "I" "J";
 "B" lambda=0.1 dorm=0;
 "C" lambda=0.2 dorm=0;
 "D" lambda=0.3 dorm=0;
 "E" lambda=0.4 dorm=0;
 "F" lambda=0.5 dorm=0;
+"G" lambda=0.5 dorm=0;
+"H" lambda=0.5 dorm=0;
+"I" lambda=0.5 dorm=0;
+"J" lambda=0.5 dorm=0;

examples/dft/voting_mix.dft

@@ -0,0 +1,9 @@
+toplevel "A";
+"A" and "B" "F";
+"B" 2of3 "C" "D" "E";
+"C" lambda=0.1 dorm=0;
+"D" lambda=0.2 dorm=0;
+"E" lambda=0.3 dorm=0;
+"F" 2of3 "G" "H" "C";
+"G" lambda=0.4 dorm=0;
+"H" lambda=0.5 dorm=0;

src/transformations/dft/DftToGspnTransformator.cpp

@@ -261,7 +261,7 @@ namespace storm {
 								if (childExit.first) {
 									// Get all associations of the child to all immediate transitions of the VOTE.
 									auto children = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(mDft.getElement(parents[j]))->children();
-									auto associations = getVOTEEntryAssociation(child->id(), 
+									auto associations = getVOTEEntryAssociation(parents[j], child->id(), 
 										std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(mDft.getElement(parents[j]))->threshold(), children);
 									
 									// Draw.
@@ -347,7 +347,7 @@ namespace storm {
             }
             
            	template <typename ValueType>
-            std::vector<int> DftToGspnTransformator<ValueType>::getVOTEEntryAssociation(int childId, int threshold, std::vector<std::shared_ptr<storm::storage::DFTElement<ValueType>>> children) {
+            std::vector<int> DftToGspnTransformator<ValueType>::getVOTEEntryAssociation(int parentId, int childId, int threshold, std::vector<std::shared_ptr<storm::storage::DFTElement<ValueType>>> children) {
 				// Fetch all ids of the children.
 				std::vector<int> childrenIds(children.size());
 				for (std::size_t i = 0; i < children.size(); i++) {
@@ -357,7 +357,15 @@ namespace storm {
 				// Get all subsets of the 'children' of size 'threshold'.
 				std::vector<int> subsets(threshold);
 				std::vector<int> output;
-				combinationUtil(output, childrenIds, subsets, 0, children.size() - 1, 0, threshold);
+				
+				// Check if output for this VOTE already exists. If yes, use it instead recalculating.
+				if (mVoteAssociations.find(parentId) == mVoteAssociations.end()) { // Could not find parentId in map.
+					combinationUtil(output, childrenIds, subsets, 0, children.size() - 1, 0, threshold);
+					mVoteAssociations.insert ( std::pair<int, std::vector<int> > (parentId, output) );
+				}
+				else { // Could find parentId in map, use already computed output.
+					output = mVoteAssociations.find(parentId)->second;
+				}
 				
 				// Check which subset contains the id 'childId' and add the subset-number to the association.
 				std::vector<int> associations;

src/transformations/dft/DftToGspnTransformator.h

@@ -32,6 +32,8 @@ namespace storm {
                 storm::storage::DFT<ValueType> const& mDft;
                 storm::gspn::GSPN mGspn;
 				
+				std::map<int, std::vector<int> > mVoteAssociations; 			// Used to avoid multiple calculations for the same VOTE. 
+				
 				static constexpr const char* STR_FAILING = "_failing";			// Name standard for transitions that point towards a place, which in turn indicates the failure of a gate.
 				static constexpr const char* STR_FAILED = "_failed";			// Name standard for place which indicates the failure of a gate.
                 
@@ -143,13 +145,15 @@ namespace storm {
 				 * 'A' is contained in subset 0 and subset 1, so this method returns {0, 1}. 
 				 * This means that BE 'A' needs to be connected with the immediate transitions 'VOTE_0_failing' and 'VOTE_1_failing'.
 				 * 
+				 * @param parentId Id of the parent.
+				 * 
 				 * @param childId Id of the child.
 				 * 
 				 * @param threshold The threshold of the VOTE.
 				 * 
 				 * @param children All children of the VOTE.
 				 */
-				 std::vector<int> getVOTEEntryAssociation(int childId, int threshold, std::vector<std::shared_ptr<storm::storage::DFTElement<ValueType>>> children);
+				 std::vector<int> getVOTEEntryAssociation(int parentId, int childId, int threshold, std::vector<std::shared_ptr<storm::storage::DFTElement<ValueType>>> children);
 				 
 				 /*
 				  * Helper-method for getVOTEEntryAssociation().