From 07baef9a7ca184e8c48ce5f2d0dc08adc593f08f Mon Sep 17 00:00:00 2001 From: mdeutschen Date: Mon, 15 Aug 2016 16:43:45 +0200 Subject: [PATCH] Added transformation for 2-input-POR Former-commit-id: 890be90f62094b32741c22064a35706c71ea4b18 --- examples/dft/por2.dft | 4 ++ .../dft/DftToGspnTransformator.cpp | 57 +++++++++++++++++-- .../dft/DftToGspnTransformator.h | 2 + 3 files changed, 59 insertions(+), 4 deletions(-) create mode 100644 examples/dft/por2.dft diff --git a/examples/dft/por2.dft b/examples/dft/por2.dft new file mode 100644 index 000000000..cd37e0c21 --- /dev/null +++ b/examples/dft/por2.dft @@ -0,0 +1,4 @@ +toplevel "A"; +"A" por "B" "C"; +"B" lambda=0.4 dorm=0.0; +"C" lambda=0.2 dorm=0.0; diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 2d6483c7b..a015c0a08 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -171,7 +171,7 @@ namespace storm { mGspn.addPlace(placePANDFailed); storm::gspn::Place placePANDFailsave; - placePANDFailsave.setName(dftPand->name() + "_failsave"); + placePANDFailsave.setName(dftPand->name() + STR_FAILSAVE); placePANDFailsave.setNumberOfInitialTokens(0); mGspn.addPlace(placePANDFailsave); @@ -185,12 +185,14 @@ namespace storm { mGspn.addImmediateTransition(immediateTransitionPANDFailing); storm::gspn::ImmediateTransition immediateTransitionPANDFailsave; - immediateTransitionPANDFailsave.setName(dftPand->name() + "_failsaving"); + 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. } template @@ -200,7 +202,34 @@ namespace storm { template void DftToGspnTransformator::drawPOR(std::shared_ptr const> dftPor) { - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a POR is not yet implemented."); + storm::gspn::Place placePORFailed; + placePORFailed.setName(dftPor->name() + STR_FAILED); + placePORFailed.setNumberOfInitialTokens(0); + mGspn.addPlace(placePORFailed); + + storm::gspn::Place placePORFailsave; + placePORFailsave.setName(dftPor->name() + STR_FAILSAVE); + placePORFailsave.setNumberOfInitialTokens(0); + mGspn.addPlace(placePORFailsave); + + storm::gspn::ImmediateTransition immediateTransitionPORFailing; + immediateTransitionPORFailing.setName(dftPor->name() + STR_FAILING); + immediateTransitionPORFailing.setPriority(1); + immediateTransitionPORFailing.setWeight(0.0); + immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailed, 1); + immediateTransitionPORFailing.setInhibitionArcMultiplicity(placePORFailsave, 1); + immediateTransitionPORFailing.setOutputArcMultiplicity(placePORFailed, 1); + mGspn.addImmediateTransition(immediateTransitionPORFailing); + + storm::gspn::ImmediateTransition immediateTransitionPORFailsave; + immediateTransitionPORFailsave.setName(dftPor->name() + STR_FAILSAVING); + immediateTransitionPORFailsave.setPriority(1); + immediateTransitionPORFailsave.setWeight(0.0); + immediateTransitionPORFailsave.setInhibitionArcMultiplicity(placePORFailsave, 1); + immediateTransitionPORFailsave.setOutputArcMultiplicity(placePORFailsave, 1); + mGspn.addImmediateTransition(immediateTransitionPORFailsave); + + // TODO: Extend for more than 2 children. } template @@ -279,7 +308,7 @@ namespace storm { { 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() + "_failsaving"); + auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING); auto childExit = mGspn.getPlace(child->name() + STR_FAILED); if (pandEntry.first && pandEntry2.first && childExit.first) { // Only add arcs if the objects have been found. @@ -302,7 +331,27 @@ namespace storm { case storm::storage::DFTElementType::SPARE: break; case storm::storage::DFTElementType::POR: + { + auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); + auto porEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING); + auto porEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILSAVING); + auto childExit = mGspn.getPlace(child->name() + STR_FAILED); + + if (porEntry.first && porEntry2.first && childExit.first) { // Only add arcs if the objects have been found. + if (children[0] == child) { // Current element is primary child. + porEntry.second->setInputArcMultiplicity(childExit.second, 1); + porEntry.second->setOutputArcMultiplicity(childExit.second, 1); + porEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1); + + } + else if (children[1] == child) { // Current element is secondary child. + porEntry2.second->setInputArcMultiplicity(childExit.second, 1); + porEntry2.second->setOutputArcMultiplicity(childExit.second, 1); + } + } + break; + } case storm::storage::DFTElementType::SEQ: break; case storm::storage::DFTElementType::MUTEX: diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index 9b826a558..4ff667b51 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -36,6 +36,8 @@ namespace storm { 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. + static constexpr const char* STR_FAILSAVING = "_failsaving"; // Name standard for transition that point towards a place, which in turn indicates the failsave state of a gate. + static constexpr const char* STR_FAILSAVE = "_failsave"; // Name standard for place which indicates the failsave state of a gate. /*! * Write Gspn to file or console.