diff --git a/examples/dft/voting3.dft b/examples/dft/voting3.dft index 73fc341b2..19c6883de 100644 --- a/examples/dft/voting3.dft +++ b/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; diff --git a/examples/dft/voting_mix.dft b/examples/dft/voting_mix.dft new file mode 100644 index 000000000..c599db903 --- /dev/null +++ b/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; diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index dd2791cc0..2d6483c7b 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/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 const>(mDft.getElement(parents[j]))->children(); - auto associations = getVOTEEntryAssociation(child->id(), + auto associations = getVOTEEntryAssociation(parents[j], child->id(), std::static_pointer_cast const>(mDft.getElement(parents[j]))->threshold(), children); // Draw. @@ -347,7 +347,7 @@ namespace storm { } template - std::vector DftToGspnTransformator::getVOTEEntryAssociation(int childId, int threshold, std::vector>> children) { + std::vector DftToGspnTransformator::getVOTEEntryAssociation(int parentId, int childId, int threshold, std::vector>> children) { // Fetch all ids of the children. std::vector 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 subsets(threshold); std::vector 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 > (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 associations; diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 78a5d7b1f..9b826a558 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -32,6 +32,8 @@ namespace storm { storm::storage::DFT const& mDft; storm::gspn::GSPN mGspn; + std::map > 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 getVOTEEntryAssociation(int childId, int threshold, std::vector>> children); + std::vector getVOTEEntryAssociation(int parentId, int childId, int threshold, std::vector>> children); /* * Helper-method for getVOTEEntryAssociation().