diff --git a/examples/dft/pand2.dft b/examples/dft/pand2.dft new file mode 100644 index 000000000..c2e875bda --- /dev/null +++ b/examples/dft/pand2.dft @@ -0,0 +1,6 @@ +toplevel "A"; +"A" pand "B" "C" "D" "E"; +"B" lambda=0.4 dorm=0.3; +"C" lambda=0.2 dorm=0.3; +"D" lambda=0.1 dorm=0.3; +"E" lambda=0.05 dorm=0.3; diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 98b159acf..20598293e 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -16,6 +16,8 @@ namespace storm { mGspn = storm::gspn::GSPN(); mGspn.setName("DftToGspnTransformation"); + // TODO: Reconsider priorities! + // Loop through every DFT element and draw them as a GSPN. drawGSPNElements(); @@ -187,15 +189,15 @@ namespace storm { immediateTransitionPANDFailing.setOutputArcMultiplicity(placePANDFailed, 1); mGspn.addImmediateTransition(immediateTransitionPANDFailing); - storm::gspn::ImmediateTransition immediateTransitionPANDFailsave; - immediateTransitionPANDFailsave.setName(dftPand->name() + STR_FAILSAVING); - immediateTransitionPANDFailsave.setPriority(1); - immediateTransitionPANDFailsave.setWeight(0.0); - immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1); - immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1); - mGspn.addImmediateTransition(immediateTransitionPANDFailsave); - - // TODO: Extend for more than 2 children. + for (std::size_t i = 0; i < dftPand->nrChildren() -1; i++) { + storm::gspn::ImmediateTransition immediateTransitionPANDFailsave; + immediateTransitionPANDFailsave.setName(dftPand->name() + "_" + std::to_string(i) + STR_FAILSAVING); + immediateTransitionPANDFailsave.setPriority(1); + immediateTransitionPANDFailsave.setWeight(0.0); + immediateTransitionPANDFailsave.setInhibitionArcMultiplicity(placePANDFailsave, 1); + immediateTransitionPANDFailsave.setOutputArcMultiplicity(placePANDFailsave, 1); + mGspn.addImmediateTransition(immediateTransitionPANDFailsave); + } } template @@ -313,22 +315,38 @@ namespace storm { case storm::storage::DFTElementType::PAND: { auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); - auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING); - auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING); auto childExit = mGspn.getPlace(child->name() + STR_FAILED); + auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING); - if (pandEntry.first && pandEntry2.first && childExit.first) { // Only add arcs if the objects have been found. + if (childExit.first && pandEntry.first) { // Only add arcs if the objects have been found. + pandEntry.second->setInputArcMultiplicity(childExit.second, 1); + pandEntry.second->setOutputArcMultiplicity(childExit.second, 1); + if (children[0] == child) { // Current element is primary child. - pandEntry.second->setInputArcMultiplicity(childExit.second, 1); - pandEntry.second->setOutputArcMultiplicity(childExit.second, 1); - pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); + auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_0" + STR_FAILSAVING); + if (pandEntry2.first) { + pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); + } } - else if (children[1] == child) { // Current element is secondary child. - pandEntry.second->setInputArcMultiplicity(childExit.second, 1); - pandEntry.second->setOutputArcMultiplicity(childExit.second, 1); - pandEntry2.second->setInputArcMultiplicity(childExit.second, 1); - pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1); + else { // Current element is not the primary child. + for (std::size_t k = 1; k < children.size(); k++) { + if (children[k] == child) { + auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k - 1)) + STR_FAILSAVING); + auto pandEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k)) + STR_FAILSAVING); + + if (pandEntry2.first) { + pandEntry2.second->setInputArcMultiplicity(childExit.second, 1); + pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1); + } + + if (pandEntry3.first) { + pandEntry3.second->setInhibitionArcMultiplicity(childExit.second, 1); + } + + continue; + } + } } } @@ -350,7 +368,7 @@ namespace storm { porEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); } - else { // Current element is a child, that is not the primary child. + else { // Current element is not the primary child. porEntry2.second->setInputArcMultiplicity(childExit.second, 1); porEntry2.second->setOutputArcMultiplicity(childExit.second, 1); } diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 338ec622f..58ed48a7c 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -91,7 +91,8 @@ namespace storm { void drawVOT(std::shared_ptr const> dftVot); /* - * Draw a Petri net PAND. + * Draw a Petri net PAND. + * This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless). * * @param dftPand The PAND gate. */ @@ -106,6 +107,7 @@ namespace storm { /* * Draw a Petri net POR. + * This POR is inklusive (children are allowed to fail simultaneously and the POR will fail nevertheless). * * @param dftPor The POR gate. */