From 8ef9b8a57673fa380bf1c2dbbb31e6b2a10f3756 Mon Sep 17 00:00:00 2001 From: Sebastian Junges Date: Thu, 15 Dec 2016 11:26:34 +0100 Subject: [PATCH] pdeps now fully working --- .../DftToGspnTransformator.cpp | 101 +++++++----------- 1 file changed, 36 insertions(+), 65 deletions(-) diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 0d145ef0c..12d85e000 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -433,24 +433,48 @@ namespace storm { double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;; uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin"); - uint64_t flipPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_flip"); - uint64_t forwardPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_forward"); + builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0)); uint64_t t1 = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip"); + builder.addInputArc(coinPlace, t1); builder.addInputArc(failedNodes.at(dftDependency->triggerEvent()->id()), t1); builder.addOutputArc(t1, failedNodes.at(dftDependency->triggerEvent()->id())); - builder.addOutputArc(t1, flipPlace); - uint64_t t2 = builder.addImmediateTransition(defaultPriority + 1, dftDependency->probability(), "_win_flip"); - builder.addInputArc(flipPlace, t2); - builder.addOutputArc(t2, forwardPlace); - if (dftDependency->probability() < 1.0) { - uint64_t t3 = builder.addImmediateTransition(defaultPriority + 1, 1 - dftDependency->probability(), "_loose_flip"); - builder.addInputArc(flipPlace, t3); + uint64_t forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward"); + builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0)); + + if (!smart || dftDependency->probability() < 1.0) { + uint64_t flipPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_flip"); + builder.addOutputArc(t1, flipPlace); + + builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0)); + uint64_t t2 = builder.addImmediateTransition(defaultPriority + 1, dftDependency->probability(), "_win_flip"); + builder.addInputArc(flipPlace, t2); + builder.addOutputArc(t2, forwardPlace); + if (dftDependency->probability() < 1.0) { + uint64_t t3 = builder.addImmediateTransition(defaultPriority + 1, 1 - dftDependency->probability(), "_loose_flip"); + builder.addInputArc(flipPlace, t3); + } + } else { + builder.addOutputArc(t1, forwardPlace); + } + for(auto const& depEv : dftDependency->dependentEvents()) { + uint64_t tx = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + depEv->name()); + builder.addInputArc(forwardPlace, tx); + builder.addOutputArc(tx, forwardPlace); + builder.addOutputArc(tx, failedNodes.at(depEv->id())); + builder.addInhibitionArc(failedNodes.at(depEv->id()), tx); + if (!smart || depEv->nrRestrictions() > 0) { + builder.addInhibitionArc(disabledNodes.at(depEv->id()), tx); + } + if (!smart || mDft.isRepresentative(depEv->id())) { + builder.addOutputArc(tx, unavailableNodes.at(depEv->id())); + } + } - builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter-5.0, ycenter+2.0)); - builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter-2.0, ycenter+2.0)); - builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0)); + + + } @@ -536,59 +560,6 @@ namespace storm { template void DftToGspnTransformator::drawGSPNRestrictions() { -// for (std::size_t i = 0; i < mDft.nrElements(); i++) { -// auto dftElement = mDft.getElement(i); -// -// if (dftElement->isRestriction()) { -// switch (dftElement->type()) { -// case storm::storage::DFTElementType::SEQ: -// { -// auto children = mDft.getRestriction(i)->children(); -// -// for (std::size_t j = 0; j < children.size() - 1; j++) { -// auto suppressor = mGspn.getPlace(children[j]->name() + STR_FAILED); -// -// switch (children[j + 1]->type()) { -// case storm::storage::DFTElementType::BE: // If suppressed is a BE, add 2 arcs to timed transitions. -// { -// auto suppressedActive = mGspn.getTimedTransition(children[j + 1]->name() + "_activeFailing"); -// auto suppressedPassive = mGspn.getTimedTransition(children[j + 1]->name() + "_passiveFailing"); -// -// if (suppressor.first && suppressedActive.first && suppressedPassive.first) { // Only add arcs if the objects have been found. -// suppressedActive.second->setInputArcMultiplicity(suppressor.second, 1); -// suppressedActive.second->setOutputArcMultiplicity(suppressor.second, 1); -// suppressedPassive.second->setInputArcMultiplicity(suppressor.second, 1); -// suppressedPassive.second->setOutputArcMultiplicity(suppressor.second, 1); -// } -// break; -// } -// default: // If supressed is not a BE, add single arc to immediate transition. -// { -// auto suppressed = mGspn.getImmediateTransition(children[j + 1]->name() + STR_FAILING); -// -// if (suppressor.first && suppressed.first) { // Only add arcs if the objects have been found. -// suppressed.second->setInputArcMultiplicity(suppressor.second, 1); -// suppressed.second->setOutputArcMultiplicity(suppressor.second, 1); -// } -// break; -// } -// } -// } -// break; -// } -// case storm::storage::DFTElementType::MUTEX: -// { -// // MUTEX is not implemented by the DFTGalileoParser yet. Nothing to do here. -// STORM_LOG_ASSERT(false, "MUTEX is not supported by DftToGspnTransformator."); -// break; -// } -// default: -// { -// break; -// } -// } -// } -// } } template