diff --git a/examples/dft/spare11.dft b/examples/dft/spare11.dft new file mode 100644 index 000000000..b3c6e929f --- /dev/null +++ b/examples/dft/spare11.dft @@ -0,0 +1,11 @@ +toplevel "OR"; +"OR" or "A" "B"; +"A" wsp "AND" "C"; +"B" wsp "C" "R" "S"; +"C" wsp "Q" "R"; +"AND" and "P" "Q"; +"P" lambda=0.1 dorm=0.9; +"Q" lambda=0.2 dorm=0.8; +"R" lambda=0.3 dorm=0.7; +"S" lambda=0.4 dorm=0.6; + diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 1bf270536..d01cf1fec 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -213,6 +213,8 @@ namespace storm { void DftToGspnTransformator::drawSPARE(std::shared_ptr const> dftSpare) { uint_fast64_t priority = getPriority(0, dftSpare); + // This codeblock can be removed later, when I am 100% sure it is not needed anymore. + /* storm::gspn::Place placeSPAREActivated; placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED); placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare)); @@ -225,6 +227,7 @@ namespace storm { immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1); immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1); mGspn.addImmediateTransition(immediateTransitionPCActivating); + */ auto children = dftSpare->children(); @@ -663,8 +666,6 @@ namespace storm { template bool DftToGspnTransformator::isBEActive(std::shared_ptr const> dftElement) { - // TODO: This method must be tested again after SPAREs are implemented. - // If element is the top element, return true. if (dftElement->id() == mDft.getTopLevelIndex()) { return true; diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 5602e9d50..081683bfd 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -201,7 +201,7 @@ namespace storm { uint_fast64_t getPriority(uint_fast64_t priority, std::shared_ptr const> dFTElement); /* - * Return all ids of BEs, that are successors of the given element. + * Return all ids of BEs, that are successors of the given element and that are not the spare childs of a SPARE. * * @param dftElement The element which */