From 45290f5c492d9deb5b4b86c27ac114a5dc48d4a7 Mon Sep 17 00:00:00 2001 From: mdeutschen Date: Wed, 14 Sep 2016 14:29:05 +0200 Subject: [PATCH] SPAREs with unshared children working Former-commit-id: 93f2e3f83025bfc8c60cc7872d658b73ac703443 --- src/transformations/dft/DftToGspnTransformator.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 358fd85d1..88fc0becb 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -502,11 +502,18 @@ namespace storm { } } else { // A spare child. - // TODO: Draw line from "SC_activating" to every BE, that is connected to the spare child. - + auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING); + std::vector ids = getAllBEIDsOfElement(child); + for (std::size_t k = 0; k < ids.size(); k++) { + auto childEntry = mGspn.getPlace(mDft.getElement(ids[k])->name() + STR_ACTIVATED); + + if (spareExit.first && childEntry.first) { // Only add arcs if the objects have been found. + spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1); + spareExit.second->setOutputArcMultiplicity(childEntry.second, 1); + } + } - // TODO: End. auto childExit = mGspn.getPlace(child->name() + STR_FAILED); auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name()); auto spareEntry2 = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);