From d4cb41a4cfb8171ab2a8af658b21739728a58783 Mon Sep 17 00:00:00 2001 From: mdeutschen Date: Fri, 30 Sep 2016 12:35:16 +0200 Subject: [PATCH] Improved VOTE. Removed unused methods Former-commit-id: d8a832b33b04b2cd281134506526a9b7c7e15002 --- examples/dft/voting4.dft | 5 + .../dft/DftToGspnTransformator.cpp | 124 ++++++------------ .../dft/DftToGspnTransformator.h | 44 ------- 3 files changed, 43 insertions(+), 130 deletions(-) create mode 100644 examples/dft/voting4.dft diff --git a/examples/dft/voting4.dft b/examples/dft/voting4.dft new file mode 100644 index 000000000..4c213b6d4 --- /dev/null +++ b/examples/dft/voting4.dft @@ -0,0 +1,5 @@ +toplevel "A"; +"A" 2of3 "B" "C" "D"; +"B" lambda=0.1 dorm=0; +"C" lambda=0.2 dorm=0; +"D" lambda=0.3 dorm=0; diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index d01cf1fec..c5dc57221 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -163,15 +163,38 @@ namespace storm { placeVOTFailed.setNumberOfInitialTokens(0); mGspn.addPlace(placeVOTFailed); - // Calculate, how many immediate transitions are necessary and draw the needed number. - for (int i = 0; i < calculateBinomialCoefficient(dftVot->nrChildren(), dftVot->threshold()); i++) { - storm::gspn::ImmediateTransition immediateTransitionVOTFailing; - immediateTransitionVOTFailing.setName(dftVot->name() + "_" + std::to_string(i) + STR_FAILING); - immediateTransitionVOTFailing.setPriority(priority); - immediateTransitionVOTFailing.setWeight(0.0); - immediateTransitionVOTFailing.setInhibitionArcMultiplicity(placeVOTFailed, 1); - immediateTransitionVOTFailing.setOutputArcMultiplicity(placeVOTFailed, 1); - mGspn.addImmediateTransition(immediateTransitionVOTFailing); + storm::gspn::Place placeVOTCollector; + placeVOTCollector.setName(dftVot->name() + "_collector"); + placeVOTCollector.setNumberOfInitialTokens(0); + mGspn.addPlace(placeVOTCollector); + + storm::gspn::ImmediateTransition immediateTransitionVOTFailing; + immediateTransitionVOTFailing.setName(dftVot->name() + STR_FAILING); + immediateTransitionVOTFailing.setPriority(priority); + immediateTransitionVOTFailing.setWeight(0.0); + immediateTransitionVOTFailing.setInhibitionArcMultiplicity(placeVOTFailed, 1); + immediateTransitionVOTFailing.setOutputArcMultiplicity(placeVOTFailed, 1); + immediateTransitionVOTFailing.setOutputArcMultiplicity(placeVOTCollector, dftVot->threshold()); // Custom threshold. + immediateTransitionVOTFailing.setInputArcMultiplicity(placeVOTCollector, dftVot->threshold()); // Custom threshold. + mGspn.addImmediateTransition(immediateTransitionVOTFailing); + + auto children = dftVot->children(); + + // Draw transition/place for every child. + for (std::size_t i = 0; i < children.size(); i++) { + storm::gspn::Place placeChildInhibit; + placeChildInhibit.setName(dftVot->name() + "_" + children[i]->name() + "_inhibitor"); + placeChildInhibit.setNumberOfInitialTokens(0); + mGspn.addPlace(placeChildInhibit); + + storm::gspn::ImmediateTransition immediateTransitionCollecting; + immediateTransitionCollecting.setName(dftVot->name() + "_" + children[i]->name() + "_collecting"); + immediateTransitionCollecting.setPriority(priority); + immediateTransitionCollecting.setWeight(0.0); + immediateTransitionCollecting.setInhibitionArcMultiplicity(placeChildInhibit, 1); + immediateTransitionCollecting.setOutputArcMultiplicity(placeChildInhibit, 1); + immediateTransitionCollecting.setOutputArcMultiplicity(placeVOTCollector, 1); + mGspn.addImmediateTransition(immediateTransitionCollecting); } } @@ -414,21 +437,13 @@ namespace storm { case storm::storage::DFTElementType::VOT: { auto childExit = mGspn.getPlace(child->name() + STR_FAILED); - 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(parents[j], child->id(), - std::static_pointer_cast const>(mDft.getElement(parents[j]))->threshold(), children); - - // Draw. - for (std::size_t k = 0; k < associations.size(); k++) { - auto voteEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string(associations[k]) + STR_FAILING); - if (voteEntry.first) { - voteEntry.second->setInputArcMultiplicity(childExit.second, 1); - voteEntry.second->setOutputArcMultiplicity(childExit.second, 1); - } - } + auto parentEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_collecting"); + + if (childExit.first && parentEntry.first) { // Only add arcs if the objects have been found. + parentEntry.second->setInputArcMultiplicity(childExit.second, 1); + parentEntry.second->setOutputArcMultiplicity(childExit.second, 1); } + break; } case storm::storage::DFTElementType::PAND: @@ -600,69 +615,6 @@ namespace storm { } } - template - int DftToGspnTransformator::calculateBinomialCoefficient(int n, int k) { - STORM_LOG_ASSERT(n >= k, "k is not allowed to be larger than n."); - - return factorialFunction(n) / ( factorialFunction(n - k) * factorialFunction(k) ); - } - - template - int DftToGspnTransformator::factorialFunction(int n) { - return (n == 1 || n == 0) ? 1 : factorialFunction(n - 1) * n; - } - - template - 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++) { - childrenIds[i] = children[i]->id(); - } - - // Get all subsets of the 'children' of size 'threshold'. - std::vector subsets(threshold); - std::vector output; - - // 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; - for (std::size_t i = 0; i < output.size(); i++) { - if (childId == output[i]) { - associations.push_back(i / threshold); - } - } - - return associations; - } - - template - void DftToGspnTransformator::combinationUtil(std::vector &output, std::vector childrenIds, std::vector subsets, int start, int end, int index, int threshold) - { - if (index == threshold) - { - for (int j = 0; j < threshold; j++) { - output.push_back(subsets[j]); - } - - return; - } - - for (int i = start; i <= end && end - i + 1 >= threshold - index; i++) - { - subsets[index] = childrenIds[i]; - combinationUtil(output, childrenIds, subsets, i + 1, end, index + 1, threshold); - } - } - template bool DftToGspnTransformator::isBEActive(std::shared_ptr const> dftElement) { diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 081683bfd..2a3da290f 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -139,50 +139,6 @@ namespace storm { */ void drawPDEP(std::shared_ptr const>(dftDependency)); - /* - * Calculate the binomial coefficient: - * n! / ( (n - k)! * k!) - * - * @param n First parameter of binomial coefficient. - * - * @ param k Second parameter of binomial coefficient. - * - */ - int calculateBinomialCoefficient(int n, int k); - - /* - * Calculate the factorial function of n. - * - * @param n The parameter for the factorial function, i.e. n!. - * - */ - int factorialFunction(int n); - - /* - * Return the immediate Transition numbers of the VOTE with which the child has to be connected. - * - * Example: A VOTE2/3 gate has three children BEs: {A, B, C}. - * The subsets of size 2 of {A, B, C} are {{A, B}, {A, C}, {B, C}}. - * '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 parentId, int childId, int threshold, std::vector>> children); - - /* - * Helper-method for getVOTEEntryAssociation(). - * Obtained from / more info at: - * http://www.geeksforgeeks.org/print-all-possible-combinations-of-r-elements-in-a-given-array-of-size-n/ - */ - void combinationUtil(std::vector &output, std::vector childrenIds, std::vector subsets, int start, int end, int index, int threshold); - /* * Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token). *