From 9a54448dc8c1af5b16528f6dab84b4f9baa75f07 Mon Sep 17 00:00:00 2001 From: mdeutschen Date: Mon, 12 Sep 2016 16:02:49 +0200 Subject: [PATCH] Starting implementation of SPARE Former-commit-id: b718fac76cce447883c658b498b3b56ac245929a --- .../dft/DftToGspnTransformator.cpp | 85 ++++++++++++++++++- .../dft/DftToGspnTransformator.h | 4 +- 2 files changed, 86 insertions(+), 3 deletions(-) diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index b5f2e714c..486e872c0 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -88,7 +88,7 @@ namespace storm { uint_fast64_t priority = getPriority(0, dftBE); storm::gspn::Place placeBEActivated; - placeBEActivated.setName(dftBE->name() + "_activated"); + placeBEActivated.setName(dftBE->name() + STR_ACTIVATED); placeBEActivated.setNumberOfInitialTokens(isBEActive(dftBE) ? 1 : 0); mGspn.addPlace(placeBEActivated); @@ -212,7 +212,74 @@ namespace storm { template void DftToGspnTransformator::drawSPARE(std::shared_ptr const> dftSpare) { // TODO: Implement. - STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The transformation of a SPARE is not yet implemented."); + + uint_fast64_t priority = getPriority(0, dftSpare); + + storm::gspn::Place placeSPAREActivated; + placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED); + placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare)); + mGspn.addPlace(placeSPAREActivated); + + storm::gspn::ImmediateTransition immediateTransitionPCActivating; + immediateTransitionPCActivating.setName(dftSpare->children()[0]->name() + STR_ACTIVATING); + immediateTransitionPCActivating.setPriority(priority); + immediateTransitionPCActivating.setWeight(0.0); + immediateTransitionPCActivating.setInputArcMultiplicity(placeSPAREActivated, 1); + immediateTransitionPCActivating.setOutputArcMultiplicity(placeSPAREActivated, 1); + mGspn.addImmediateTransition(immediateTransitionPCActivating); + + auto children = dftSpare->children(); + + // Repeat for every spare child (every child that is not the first!). + for (std::size_t i = 1; i < children.size(); i++) { + auto placeChildClaimedPreexist = mGspn.getPlace(children[i]->name() + "_claimed"); + + if (!placeChildClaimedPreexist.first) { // Only draw this place if it doesn't exist jet. + storm::gspn::Place placeChildClaimed; + placeChildClaimed.setName(children[i]->name() + "_claimed"); + placeChildClaimed.setNumberOfInitialTokens(0); + mGspn.addPlace(placeChildClaimed); + + storm::gspn::ImmediateTransition immediateTransitionSpareChildActivating; + immediateTransitionSpareChildActivating.setName(dftSpare->children()[i]->name() + STR_ACTIVATING); + immediateTransitionSpareChildActivating.setPriority(priority); + immediateTransitionSpareChildActivating.setWeight(0.0); + immediateTransitionSpareChildActivating.setInputArcMultiplicity(placeChildClaimed, 1); + immediateTransitionSpareChildActivating.setOutputArcMultiplicity(placeChildClaimed, 1); + mGspn.addImmediateTransition(immediateTransitionSpareChildActivating); + } + + auto placeChildClaimedExist = mGspn.getPlace(children[i]->name() + "_claimed"); + + storm::gspn::Place placeSPAREClaimedChild; + placeSPAREClaimedChild.setName(dftSpare->name() + "_claimed_" + children[i]->name()); + placeSPAREClaimedChild.setNumberOfInitialTokens(0); + mGspn.addPlace(placeSPAREClaimedChild); + + storm::gspn::Place placeSPAREChildConsumed; + placeSPAREChildConsumed.setName(children[i]->name() + "_consumed"); // TODO: If its the last child, this label must be "SPARE_failed". + placeSPAREChildConsumed.setNumberOfInitialTokens(0); + mGspn.addPlace(placeSPAREChildConsumed); + + storm::gspn::ImmediateTransition immediateTransitionChildConsuming1; + immediateTransitionChildConsuming1.setName(dftSpare->children()[i]->name() + "_consuming1"); + immediateTransitionChildConsuming1.setPriority(priority); + immediateTransitionChildConsuming1.setWeight(0.0); + immediateTransitionChildConsuming1.setOutputArcMultiplicity(placeSPAREChildConsumed, 1); + immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1); + immediateTransitionChildConsuming1.setInhibitionArcMultiplicity(placeSPAREClaimedChild, 1); + mGspn.addImmediateTransition(immediateTransitionChildConsuming1); + + storm::gspn::ImmediateTransition immediateTransitionChildConsuming2; + immediateTransitionChildConsuming2.setName(dftSpare->children()[i]->name() + "_consuming2"); + immediateTransitionChildConsuming2.setPriority(priority); + immediateTransitionChildConsuming2.setWeight(0.0); + immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREChildConsumed, 1); + immediateTransitionChildConsuming2.setInhibitionArcMultiplicity(placeSPAREChildConsumed, 1); + immediateTransitionChildConsuming2.setOutputArcMultiplicity(placeSPAREClaimedChild, 1); + immediateTransitionChildConsuming2.setInputArcMultiplicity(placeSPAREClaimedChild, 1); + mGspn.addImmediateTransition(immediateTransitionChildConsuming2); + } } template @@ -377,7 +444,21 @@ namespace storm { break; } case storm::storage::DFTElementType::SPARE: + { + // TODO: Implement. + + // Check if child is a primary or spare child. + auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); + + if (child == children[0]) { // Primary child. + // TODO: Draw line from "FC_activating" to every BE, that is connected to the primary child. + } + else { // Spare child. + + } + break; + } case storm::storage::DFTElementType::POR: { auto children = std::static_pointer_cast const>(mDft.getElement(parents[j]))->children(); diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index aa65e5199..3f1e09636 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -38,7 +38,9 @@ namespace storm { 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. - + static constexpr const char* STR_ACTIVATED = "_activated"; // Name standard for place which indicates the activity. + static constexpr const char* STR_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity. + /*! * Write Gspn to file or console. *