From 222c59a939f2017760b2613128ffb087203f6cc9 Mon Sep 17 00:00:00 2001 From: mdeutschen Date: Fri, 12 Aug 2016 16:15:25 +0200 Subject: [PATCH] Implementation of VOTE transformation Former-commit-id: 177525ba3606fe8733f19910f06fa210ccc56c9d --- examples/dft/voting3.dft | 7 ++ .../dft/DftToGspnTransformator.cpp | 103 ++++++++++++++++-- .../dft/DftToGspnTransformator.h | 42 +++++++ 3 files changed, 142 insertions(+), 10 deletions(-) create mode 100644 examples/dft/voting3.dft diff --git a/examples/dft/voting3.dft b/examples/dft/voting3.dft new file mode 100644 index 000000000..73fc341b2 --- /dev/null +++ b/examples/dft/voting3.dft @@ -0,0 +1,7 @@ +toplevel "A"; +"A" 3of5 "B" "C" "D" "E" "F"; +"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; diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 1ce3a5cf7..dd2791cc0 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -15,9 +15,6 @@ namespace storm { void DftToGspnTransformator::transform() { mGspn = storm::gspn::GSPN(); mGspn.setName("DftToGspnTransformation"); - - // TODO: Do I need to check if every DFT element has an unique name? - // TODO: GSPN elements are picked by their name in method drawGSPNConnections(), so this might cause problems... // Loop through every DFT element and draw them as a GSPN. drawGSPNElements(); @@ -84,7 +81,7 @@ namespace storm { void DftToGspnTransformator::drawBE(std::shared_ptr const> dftBE) { storm::gspn::Place placeBEActivated; placeBEActivated.setName(dftBE->name() + "_activated"); - placeBEActivated.setNumberOfInitialTokens(false ? 1 : 0); // TODO: How can I check if BE is activated? + placeBEActivated.setNumberOfInitialTokens(false ? 1 : 0); // TODO: Check if BE is spare child of a SPARE. mGspn.addPlace(placeBEActivated); storm::gspn::Place placeBEFailed; @@ -149,7 +146,21 @@ namespace storm { template void DftToGspnTransformator::drawVOT(std::shared_ptr const> dftVot) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a VOT is not yet implemented."); + storm::gspn::Place placeVOTFailed; + placeVOTFailed.setName(dftVot->name() + STR_FAILED); + 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(1); + immediateTransitionVOTFailing.setWeight(0.0); + immediateTransitionVOTFailing.setInhibitionArcMultiplicity(placeVOTFailed, 1); + immediateTransitionVOTFailing.setOutputArcMultiplicity(placeVOTFailed, 1); + mGspn.addImmediateTransition(immediateTransitionVOTFailing); + } } template @@ -180,14 +191,11 @@ namespace storm { immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1); immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1); mGspn.addImmediateTransition(immediateTransitionPANDFailsave); - - // TODO: Are PANDs with more than two children possible? } template void DftToGspnTransformator::drawSPARE(std::shared_ptr const> dftSpare) { STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented."); - // TODO: What are the codewords for SPAREs in a *.dft file? hsp, wsp and csp? } template @@ -201,7 +209,8 @@ namespace storm { placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED); placeCONSTFFailed.setNumberOfInitialTokens(1); mGspn.addPlace(placeCONSTFFailed); - // TODO: What is the codeword for CONSTF in a *.dft file? + + // TODO: Not tested because there is no corresponding DFT element yet. } template @@ -211,7 +220,8 @@ namespace storm { placeCONSTSFailed.setNumberOfInitialTokens(0); placeCONSTSFailed.setCapacity(0); // It cannot contain a token, because it cannot fail. mGspn.addPlace(placeCONSTSFailed); - // TODO: What is the codeword for CONSTS in a *.dft file? + + // TODO: Not tested because there is no corresponding DFT element yet. } template @@ -246,7 +256,25 @@ namespace storm { break; } 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(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); + } + } + } break; + } case storm::storage::DFTElementType::PAND: { auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); @@ -306,6 +334,61 @@ 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 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; + combinationUtil(output, childrenIds, subsets, 0, children.size() - 1, 0, threshold); + + // 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 void DftToGspnTransformator::writeGspn(bool toFile) { if (toFile) { diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 21ba259ab..78a5d7b1f 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -115,6 +115,48 @@ namespace storm { * @param dftPor The CONSTS Basic Event. */ void drawCONSTS(std::shared_ptr const> dftConstS); + + /* + * 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 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); + + /* + * 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); }; } }