diff --git a/examples/dft/spare10.dft b/examples/dft/spare10.dft new file mode 100644 index 000000000..663bd85a2 --- /dev/null +++ b/examples/dft/spare10.dft @@ -0,0 +1,11 @@ +toplevel "SPARE"; +"SPARE" wsp "PC" "FSC" "SSC"; +"PC" or "A" "B"; +"B" or "C" "D" "E"; +"FSC" lambda=0.5 dorm=0.3; +"SSC" lambda=0.5 dorm=0.3; +"A" lambda=0.5 dorm=0.3; +"C" lambda=0.5 dorm=0.3; +"D" lambda=0.5 dorm=0.3; +"E" lambda=0.5 dorm=0.3; + diff --git a/src/transformations/dft/DftToGspnTransformator.cpp b/src/transformations/dft/DftToGspnTransformator.cpp index 403907f6f..358fd85d1 100644 --- a/src/transformations/dft/DftToGspnTransformator.cpp +++ b/src/transformations/dft/DftToGspnTransformator.cpp @@ -472,13 +472,21 @@ namespace storm { } case storm::storage::DFTElementType::SPARE: { - // TODO: Implement. - // Check if current 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. + 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); + } + } // Draw lines from "primary child_failed" to SPARE. auto childExit = mGspn.getPlace(child->name() + STR_FAILED); @@ -496,6 +504,9 @@ namespace storm { else { // A spare child. // TODO: Draw line from "SC_activating" to every BE, that is connected to the spare child. + + + // 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); @@ -789,17 +800,91 @@ namespace storm { } template - std::vector DftToGspnTransformator::getAllBEIDsOfElement(std::vector ids, std::shared_ptr const> dftElement) { - std::vector newIds; + std::vector DftToGspnTransformator::getAllBEIDsOfElement(std::shared_ptr const> dftElement) { + std::vector ids; - if (dftElement->type() == storm::storage::DFTElementType::BE) { - newIds.push_back(dftElement->id()); - } - else { - // TODO: Check all children: If they are BEs, add them to the list. Else, check the children again. + switch (dftElement->type()) { + case storm::storage::DFTElementType::AND: + { + auto children = std::static_pointer_cast const>(dftElement)->children(); + + for (std::size_t i = 0; i < children.size(); i++) { + std::vector newIds = getAllBEIDsOfElement(children[i]); + ids.insert(ids.end(), newIds.begin(), newIds.end()); + } + break; + } + case storm::storage::DFTElementType::OR: + { + auto children = std::static_pointer_cast const>(dftElement)->children(); + + for (std::size_t i = 0; i < children.size(); i++) { + std::vector newIds = getAllBEIDsOfElement(children[i]); + ids.insert(ids.end(), newIds.begin(), newIds.end()); + } + break; + } + case storm::storage::DFTElementType::VOT: + { + auto children = std::static_pointer_cast const>(dftElement)->children(); + + for (std::size_t i = 0; i < children.size(); i++) { + std::vector newIds = getAllBEIDsOfElement(children[i]); + ids.insert(ids.end(), newIds.begin(), newIds.end()); + } + break; + } + case storm::storage::DFTElementType::PAND: + { + auto children = std::static_pointer_cast const>(dftElement)->children(); + + for (std::size_t i = 0; i < children.size(); i++) { + std::vector newIds = getAllBEIDsOfElement(children[i]); + ids.insert(ids.end(), newIds.begin(), newIds.end()); + } + break; + } + case storm::storage::DFTElementType::SPARE: + { + auto children = std::static_pointer_cast const>(dftElement)->children(); + + for (std::size_t i = 0; i < children.size(); i++) { + std::vector newIds = getAllBEIDsOfElement(children[i]); + ids.insert(ids.end(), newIds.begin(), newIds.end()); + } + break; + } + case storm::storage::DFTElementType::POR: + { + auto children = std::static_pointer_cast const>(dftElement)->children(); + + for (std::size_t i = 0; i < children.size(); i++) { + std::vector newIds = getAllBEIDsOfElement(children[i]); + ids.insert(ids.end(), newIds.begin(), newIds.end()); + } + break; + } + case storm::storage::DFTElementType::BE: + case storm::storage::DFTElementType::CONSTF: + case storm::storage::DFTElementType::CONSTS: + { + ids.push_back(dftElement->id()); + break; + } + case storm::storage::DFTElementType::SEQ: + case storm::storage::DFTElementType::MUTEX: + case storm::storage::DFTElementType::PDEP: + { + break; + } + default: + { + STORM_LOG_ASSERT(false, "DFT type unknown."); + break; + } } - return newIds; + return ids; } template diff --git a/src/transformations/dft/DftToGspnTransformator.h b/src/transformations/dft/DftToGspnTransformator.h index fcfe24139..5602e9d50 100644 --- a/src/transformations/dft/DftToGspnTransformator.h +++ b/src/transformations/dft/DftToGspnTransformator.h @@ -205,7 +205,7 @@ namespace storm { * * @param dftElement The element which */ - std::vector getAllBEIDsOfElement(std::vector ids, std::shared_ptr const> dftElement); + std::vector getAllBEIDsOfElement(std::shared_ptr const> dftElement); }; } }