Browse Source
updated dft->gspn translation to now have basis support for spares
tempestpy_adaptions
updated dft->gspn translation to now have basis support for spares
tempestpy_adaptions
Sebastian Junges
8 years ago
3 changed files with 1103 additions and 0 deletions
-
6src/storm-dft-cli/storm-dyftee.cpp
-
923src/storm/transformations/dft/DftToGspnTransformator.cpp
-
174src/storm/transformations/dft/DftToGspnTransformator.h
@ -0,0 +1,923 @@ |
|||||
|
#include "DftToGspnTransformator.h"
|
||||
|
#include "storm/exceptions/NotImplementedException.h"
|
||||
|
#include <memory>
|
||||
|
|
||||
|
namespace storm { |
||||
|
namespace transformations { |
||||
|
namespace dft { |
||||
|
|
||||
|
// Prevent some magic constants
|
||||
|
static constexpr const uint64_t defaultPriority = 0; |
||||
|
static constexpr const uint64_t defaultCapacity = 0; |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft) : mDft(dft) { |
||||
|
// Intentionally left empty.
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::transform() { |
||||
|
|
||||
|
builder.setGspnName("DftToGspnTransformation"); |
||||
|
|
||||
|
// Loop through every DFT element and draw them as a GSPN.
|
||||
|
drawGSPNElements(); |
||||
|
|
||||
|
// When all DFT elements are drawn, draw the connections between them.
|
||||
|
drawGSPNConnections(); |
||||
|
|
||||
|
// Draw functional/probability dependencies into the GSPN.
|
||||
|
drawGSPNDependencies(); |
||||
|
|
||||
|
// Draw restrictions into the GSPN (i.e. SEQ or MUTEX).
|
||||
|
drawGSPNRestrictions(); |
||||
|
|
||||
|
// Write GSPN to file.
|
||||
|
writeGspn(true); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawGSPNElements() { |
||||
|
|
||||
|
|
||||
|
// Loop through every DFT element and draw them as a GSPN.
|
||||
|
for (std::size_t i = 0; i < mDft.nrElements(); i++) { |
||||
|
auto dftElement = mDft.getElement(i); |
||||
|
bool isRepresentative = mDft.isRepresentative(i); |
||||
|
|
||||
|
// Check which type the element is and call the corresponding drawing-function.
|
||||
|
switch (dftElement->type()) { |
||||
|
case storm::storage::DFTElementType::AND: |
||||
|
drawAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::OR: |
||||
|
drawOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::VOT: |
||||
|
drawVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::PAND: |
||||
|
drawPAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::SPARE: |
||||
|
drawSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::POR: |
||||
|
drawPOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::SEQ: |
||||
|
// No method call needed here. SEQ only consists of restrictions, which are handled later.
|
||||
|
break; |
||||
|
case storm::storage::DFTElementType::MUTEX: |
||||
|
// No method call needed here. MUTEX only consists of restrictions, which are handled later.
|
||||
|
break; |
||||
|
case storm::storage::DFTElementType::BE: |
||||
|
drawBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::CONSTF: |
||||
|
drawCONSTF(dftElement, isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::CONSTS: |
||||
|
drawCONSTS(dftElement, isRepresentative); |
||||
|
break; |
||||
|
case storm::storage::DFTElementType::PDEP: |
||||
|
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement), isRepresentative); |
||||
|
break; |
||||
|
default: |
||||
|
STORM_LOG_ASSERT(false, "DFT type unknown."); |
||||
|
break; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative) { |
||||
|
|
||||
|
uint64_t beActive = builder.addPlace(defaultCapacity, isBEActive(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED); |
||||
|
activeNodes.emplace(dftBE->id(), beActive); |
||||
|
uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftBE); |
||||
|
} |
||||
|
|
||||
|
assert(failedNodes.size() == dftBE->id()); |
||||
|
failedNodes.push_back(beFailed); |
||||
|
uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing"); |
||||
|
builder.addInputArc(beActive, tActive); |
||||
|
builder.addInhibitionArc(beFailed, tActive); |
||||
|
builder.addOutputArc(tActive, beActive); |
||||
|
builder.addOutputArc(tActive, beFailed); |
||||
|
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing"); |
||||
|
builder.addInhibitionArc(beActive, tPassive); |
||||
|
builder.addInhibitionArc(beFailed, tPassive); |
||||
|
builder.addOutputArc(tPassive, beFailed); |
||||
|
|
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tActive, unavailableNode); |
||||
|
builder.addOutputArc(tPassive, unavailableNode); |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftAnd->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftAnd->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
|
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftAnd); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd) , 0.0, dftAnd->name() + STR_FAILING ); |
||||
|
builder.addInhibitionArc(nodeFailed, tAndFailed); |
||||
|
builder.addOutputArc(tAndFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tAndFailed, unavailableNode); |
||||
|
} |
||||
|
for(auto const& child : dftAnd->children()) { |
||||
|
assert(failedNodes.size() > child->id()); |
||||
|
builder.addInputArc(failedNodes[child->id()], tAndFailed); |
||||
|
} |
||||
|
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftOr->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftOr->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftOr); |
||||
|
} |
||||
|
|
||||
|
uint64_t i = 0; |
||||
|
for (auto const& child : dftOr->children()) { |
||||
|
uint64_t tNodeFailed = builder.addImmediateTransition( getFailPriority(dftOr) , 0.0, dftOr->name() + STR_FAILING + std::to_string(i) ); |
||||
|
builder.addInhibitionArc(nodeFailed, tNodeFailed); |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tNodeFailed, unavailableNode); |
||||
|
} |
||||
|
assert(failedNodes.size() > child->id()); |
||||
|
builder.addInputArc(failedNodes[child->id()], tNodeFailed); |
||||
|
++i; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftVot->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftVot); |
||||
|
} |
||||
|
|
||||
|
uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector"); |
||||
|
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING); |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tNodeFailed, unavailableNode); |
||||
|
} |
||||
|
builder.addInhibitionArc(nodeFailed, tNodeFailed); |
||||
|
builder.addInputArc(nodeCollector, tNodeFailed, dftVot->threshold()); |
||||
|
builder.addOutputArc(tNodeFailed, nodeCollector, dftVot->threshold()); |
||||
|
uint64_t i = 0; |
||||
|
for (auto const& child : dftVot->children()) { |
||||
|
uint64_t childInhibPlace = builder.addPlace(1, 0, dftVot->name() + "_child_fail_inhib" + std::to_string(i)); |
||||
|
uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + "_child_collect" + std::to_string(i)); |
||||
|
builder.addOutputArc(tCollect, nodeCollector); |
||||
|
builder.addOutputArc(tCollect, childInhibPlace); |
||||
|
builder.addInhibitionArc(childInhibPlace, tCollect); |
||||
|
builder.addInputArc(failedNodes[child->id()], tCollect); |
||||
|
++i; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILED); |
||||
|
assert(failedNodes.size() == dftPand->id()); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftPand); |
||||
|
} |
||||
|
|
||||
|
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE); |
||||
|
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING); |
||||
|
builder.addInhibitionArc(nodeFailed, tNodeFailed); |
||||
|
builder.addInhibitionArc(nodeFS, tNodeFailed); |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(tNodeFailed, nodeFailed); |
||||
|
} |
||||
|
for(auto const& child : dftPand->children()) { |
||||
|
builder.addInputArc(failedNodes[child->id()], tNodeFailed); |
||||
|
} |
||||
|
for (uint64_t j = 1; j < dftPand->nrChildren(); ++j) { |
||||
|
uint64_t tfs = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(j)); |
||||
|
builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs); |
||||
|
builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs); |
||||
|
builder.addOutputArc(tfs, nodeFS); |
||||
|
|
||||
|
} |
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare, bool isRepresentative) { |
||||
|
|
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_FAILED); |
||||
|
failedNodes.push_back(nodeFailed); |
||||
|
uint64_t unavailableNode = 0; |
||||
|
if (isRepresentative) { |
||||
|
unavailableNode = addUnavailableNode(dftSpare); |
||||
|
} |
||||
|
uint64_t spareActive = builder.addPlace(defaultCapacity, 0, dftSpare->name() + STR_ACTIVATED); |
||||
|
activeNodes.emplace(dftBE->id(), beActive); |
||||
|
|
||||
|
|
||||
|
std::vector<uint64_t> cucNodes; |
||||
|
std::vector<uint64_t> nextClaimNodes; |
||||
|
std::vector<uint64_t> nextclTransitions; |
||||
|
std::vector<uint64_t> nextconsiderTransitions; |
||||
|
uint64_t j = 0; |
||||
|
for(auto const& child : dftSpare->children()) { |
||||
|
if (j > 0) { |
||||
|
nextClaimNodes.push_back(builder.addPlace(defaultCapacity, 0, dftSpare->name()+ "_consider_" + child->name())); |
||||
|
|
||||
|
builder.addOutputArc(nextclTransitions.back(), nextClaimNodes.back(), 1); |
||||
|
if (j > 1) { |
||||
|
builder.addOutputArc(nextconsiderTransitions.back(), nextClaimNodes.back()); |
||||
|
} |
||||
|
|
||||
|
uint64_t tnextconsider = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name()); |
||||
|
builder.addInputArc(nextClaimNodes.back(), tnextconsider); |
||||
|
builder.addInputArc(unavailableNodes.at(child->id()), tnextconsider); |
||||
|
nextconsiderTransitions.push_back(tnextconsider); |
||||
|
|
||||
|
} |
||||
|
cucNodes.push_back(builder.addPlace(defaultCapacity, j == 0 ? 1 : 0, dftSpare->name() + "_claimed_" + child->name())); |
||||
|
if (j > 0) { |
||||
|
uint64 tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name()); |
||||
|
builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim); |
||||
|
builder.addInputArc(nextClaimNodes.back(), tclaim); |
||||
|
builder.addOutputArc(tclaim, cucNodes.back()); |
||||
|
} |
||||
|
uint64_t tnextcl = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(j)); |
||||
|
builder.addInputArc(cucNodes.back(), tnextcl); |
||||
|
builder.addOutputArc(tnextcl, cucNodes.back()); |
||||
|
builder.addInputArc(failedNodes.at(child->id()), tnextcl); |
||||
|
builder.addOutputArc(tnextcl, failedNodes.at(child->id())); |
||||
|
nextclTransitions.push_back(tnextcl); |
||||
|
|
||||
|
|
||||
|
++j; |
||||
|
} |
||||
|
builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed); |
||||
|
builder.addOutputArc(nextclTransitions.back(), nodeFailed); |
||||
|
|
||||
|
if (isRepresentative) { |
||||
|
builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode); |
||||
|
builder.addOutputArc(nextclTransitions.back(), unavailableNode); |
||||
|
} |
||||
|
|
||||
|
|
||||
|
// uint_fast64_t priority = getPriority(0, dftSpare);
|
||||
|
//
|
||||
|
// // This codeblock can be removed later, when I am 100% sure it is not needed anymore.
|
||||
|
// /*
|
||||
|
// storm::gspn::Place placeSPAREActivated;
|
||||
|
// placeSPAREActivated.setName(dftSpare->name() + STR_ACTIVATED);
|
||||
|
// placeSPAREActivated.setNumberOfInitialTokens(isBEActive(dftSpare));
|
||||
|
// mGspn.addPlace(placeSPAREActivated);
|
||||
|
//
|
||||
|
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> 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();
|
||||
|
//
|
||||
|
// // Draw places and transitions that belong to each spare child.
|
||||
|
// 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<storm::gspn::GSPN::WeightType> immediateTransitionSpareChildActivating;
|
||||
|
// immediateTransitionSpareChildActivating.setName(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::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildClaiming;
|
||||
|
// immediateTransitionChildClaiming.setName(dftSpare->name() + "_claiming_" + children[i]->name());
|
||||
|
// immediateTransitionChildClaiming.setPriority(priority + 1); // Higher priority needed!
|
||||
|
// immediateTransitionChildClaiming.setWeight(0.0);
|
||||
|
// immediateTransitionChildClaiming.setInhibitionArcMultiplicity(placeChildClaimedExist.second, 1);
|
||||
|
// immediateTransitionChildClaiming.setOutputArcMultiplicity(placeChildClaimedExist.second, 1);
|
||||
|
// immediateTransitionChildClaiming.setOutputArcMultiplicity(placeSPAREClaimedChild, 1);
|
||||
|
// mGspn.addImmediateTransition(immediateTransitionChildClaiming);
|
||||
|
//
|
||||
|
// storm::gspn::Place placeSPAREChildConsumed;
|
||||
|
// if (i < children.size() - 1) {
|
||||
|
// placeSPAREChildConsumed.setName(dftSpare->name() + "_" + children[i]->name() + "_consumed");
|
||||
|
// }
|
||||
|
// else {
|
||||
|
// placeSPAREChildConsumed.setName(dftSpare->name() + STR_FAILED);
|
||||
|
// }
|
||||
|
// placeSPAREChildConsumed.setNumberOfInitialTokens(0);
|
||||
|
// mGspn.addPlace(placeSPAREChildConsumed);
|
||||
|
//
|
||||
|
// storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming1;
|
||||
|
// immediateTransitionChildConsuming1.setName(dftSpare->name() + "_" + 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<storm::gspn::GSPN::WeightType> immediateTransitionChildConsuming2;
|
||||
|
// immediateTransitionChildConsuming2.setName(dftSpare->name() + "_" + 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);
|
||||
|
// }
|
||||
|
//
|
||||
|
// // Draw connections between all spare childs.
|
||||
|
// for (std::size_t i = 1; i < children.size() - 1; i++) {
|
||||
|
// auto placeSPAREChildConsumed = mGspn.getPlace(dftSpare->name() + "_" + children[i]->name() + "_consumed");
|
||||
|
// auto immediateTransitionChildClaiming = mGspn.getImmediateTransition(dftSpare->name() + "_claiming_" + children[i + 1]->name());
|
||||
|
// auto immediateTransitionChildConsuming1 = mGspn.getImmediateTransition(dftSpare->name() + "_" + children[i + 1]->name() + "_consuming1");
|
||||
|
//
|
||||
|
// immediateTransitionChildClaiming.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
|
||||
|
// immediateTransitionChildClaiming.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
|
||||
|
//
|
||||
|
// immediateTransitionChildConsuming1.second->setOutputArcMultiplicity(placeSPAREChildConsumed.second, 1);
|
||||
|
// immediateTransitionChildConsuming1.second->setInputArcMultiplicity(placeSPAREChildConsumed.second, 1);
|
||||
|
// }
|
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool isRepresentative) { |
||||
|
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILED); |
||||
|
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE); |
||||
|
|
||||
|
|
||||
|
uint64_t tfail = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING); |
||||
|
builder.addInhibitionArc(nodeFS, tfail); |
||||
|
builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail); |
||||
|
builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id())); |
||||
|
builder.addOutputArc(tfail, nodeFailed); |
||||
|
builder.addInhibitionArc(nodeFailed, tfail); |
||||
|
uint64_t j = 0; |
||||
|
for (auto const& child : dftPor->children()) { |
||||
|
uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j)); |
||||
|
builder.addInputArc(failedNodes.at(child->id()), tfailsf); |
||||
|
builder.addOutputArc(tfailsf, failedNodes.at(child->id())); |
||||
|
// TODO
|
||||
|
// builder.addInhibitionArc(<#const uint_fast64_t &from#>, <#const uint_fast64_t &to#>)
|
||||
|
++j; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF, bool isRepresentative) { |
||||
|
// storm::gspn::Place placeCONSTFFailed;
|
||||
|
// placeCONSTFFailed.setName(dftConstF->name() + STR_FAILED);
|
||||
|
// placeCONSTFFailed.setNumberOfInitialTokens(1);
|
||||
|
// mGspn.addPlace(placeCONSTFFailed);
|
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS, bool isRepresentative) { |
||||
|
// storm::gspn::Place placeCONSTSFailed;
|
||||
|
// placeCONSTSFailed.setName(dftConstS->name() + STR_FAILED);
|
||||
|
// placeCONSTSFailed.setNumberOfInitialTokens(0);
|
||||
|
// placeCONSTSFailed.setCapacity(0); // It cannot contain a token, because it cannot fail.
|
||||
|
// mGspn.addPlace(placeCONSTSFailed);
|
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency, bool isRepresentative) { |
||||
|
// // Only draw dependency, if it wasn't drawn before.
|
||||
|
// std::string gateName = dftDependency->name().substr(0, dftDependency->name().find("_"));
|
||||
|
// auto exists = mGspn.getPlace(gateName + STR_FAILED);
|
||||
|
// if (!exists.first) {
|
||||
|
// storm::gspn::Place placeDEPFailed;
|
||||
|
// placeDEPFailed.setName(gateName + STR_FAILED);
|
||||
|
// placeDEPFailed.setNumberOfInitialTokens(0);
|
||||
|
// mGspn.addPlace(placeDEPFailed);
|
||||
|
//
|
||||
|
// storm::gspn::TimedTransition<double> timedTransitionDEPFailure;
|
||||
|
// timedTransitionDEPFailure.setName(gateName + STR_FAILING);
|
||||
|
// timedTransitionDEPFailure.setPriority(getPriority(0, dftDependency));
|
||||
|
// timedTransitionDEPFailure.setRate(dftDependency->probability());
|
||||
|
// timedTransitionDEPFailure.setOutputArcMultiplicity(placeDEPFailed, 1);
|
||||
|
// timedTransitionDEPFailure.setInhibitionArcMultiplicity(placeDEPFailed, 1);
|
||||
|
// mGspn.addTimedTransition(timedTransitionDEPFailure);
|
||||
|
// }
|
||||
|
} |
||||
|
|
||||
|
template<typename ValueType> |
||||
|
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) { |
||||
|
uint64_t unavailableNode = builder.addPlace(defaultCapacity, 1, dftElement->name() + "_unavailable"); |
||||
|
assert(unavailableNode != 0); |
||||
|
unavailableNodes.emplace(dftElement->id(), unavailableNode); |
||||
|
return unavailableNode; |
||||
|
} |
||||
|
//
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawGSPNConnections() { |
||||
|
// // Check for every element, if they have parents (all will have at least 1, except the top event).
|
||||
|
// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
|
||||
|
// auto child = mDft.getElement(i);
|
||||
|
// auto parents = child->parentIds();
|
||||
|
//
|
||||
|
// // Draw a connection to every parent.
|
||||
|
// for (std::size_t j = 0; j < parents.size(); j++) {
|
||||
|
// // Check the type of the parent and act accordingly (every parent gate has different entry points...).
|
||||
|
// switch (mDft.getElement(parents[j])->type()) {
|
||||
|
// case storm::storage::DFTElementType::AND:
|
||||
|
// {
|
||||
|
// auto andEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
|
||||
|
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
|
||||
|
// if (andEntry.first && childExit.first) { // Only add arcs if the objects have been found.
|
||||
|
// andEntry.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// andEntry.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::OR:
|
||||
|
// {
|
||||
|
// auto orEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + STR_FAILING);
|
||||
|
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
|
||||
|
// if (orEntry.first && childExit.first) { // Only add arcs if the objects have been found.
|
||||
|
// orEntry.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// orEntry.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::VOT:
|
||||
|
// {
|
||||
|
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
|
||||
|
// auto parentEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_collecting");
|
||||
|
//
|
||||
|
// if (childExit.first && parentEntry.first) { // Only add arcs if the objects have been found.
|
||||
|
// parentEntry.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// parentEntry.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
//
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::PAND:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(mDft.getElement(parents[j]))->children();
|
||||
|
// auto childExit = mGspn.getPlace(child->name() + STR_FAILED);
|
||||
|
// auto pandEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + STR_FAILING);
|
||||
|
//
|
||||
|
// if (childExit.first && pandEntry.first) { // Only add arcs if the objects have been found.
|
||||
|
// pandEntry.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// pandEntry.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
//
|
||||
|
// if (children[0] == child) { // Current element is primary child.
|
||||
|
// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_0" + STR_FAILSAVING);
|
||||
|
//
|
||||
|
// if (pandEntry2.first) {
|
||||
|
// pandEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
// else { // Current element is not the primary child.
|
||||
|
// for (std::size_t k = 1; k < children.size(); k++) {
|
||||
|
// if (children[k] == child) {
|
||||
|
// auto pandEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k - 1)) + STR_FAILSAVING);
|
||||
|
// auto pandEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + std::to_string((k)) + STR_FAILSAVING);
|
||||
|
//
|
||||
|
// if (pandEntry2.first) {
|
||||
|
// pandEntry2.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// pandEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
//
|
||||
|
// if (pandEntry3.first) {
|
||||
|
// pandEntry3.second->setInhibitionArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
//
|
||||
|
// continue;
|
||||
|
// }
|
||||
|
// }
|
||||
|
// }
|
||||
|
// }
|
||||
|
//
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::SPARE:
|
||||
|
// {
|
||||
|
// // Check if current child is a primary or spare child.
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(mDft.getElement(parents[j]))->children();
|
||||
|
//
|
||||
|
// if (child == children[0]) { // Primary child.
|
||||
|
// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
|
||||
|
//
|
||||
|
// std::vector<int> 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);
|
||||
|
// auto spareEntry = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + children[1]->name());
|
||||
|
// auto spareEntry2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + children[1]->name() + "_consuming1");
|
||||
|
//
|
||||
|
// if (childExit.first && spareEntry.first && spareEntry2.first) { // Only add arcs if the objects have been found.
|
||||
|
// spareEntry.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// spareEntry.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
//
|
||||
|
// spareEntry2.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// spareEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
// else { // A spare child.
|
||||
|
// auto spareExit = mGspn.getImmediateTransition(child->name() + STR_ACTIVATING);
|
||||
|
// auto spareExit2 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_claiming_" + child->name());
|
||||
|
//
|
||||
|
// std::vector<int> 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 && spareExit2.first && childEntry.first) { // Only add arcs if the objects have been found.
|
||||
|
// if (!spareExit.second->existsInhibitionArc(childEntry.second)) {
|
||||
|
// spareExit.second->setInhibitionArcMultiplicity(childEntry.second, 1);
|
||||
|
// }
|
||||
|
// if (!spareExit.second->existsOutputArc(childEntry.second)) {
|
||||
|
// spareExit.second->setOutputArcMultiplicity(childEntry.second, 1);
|
||||
|
// }
|
||||
|
// if (!spareExit2.second->existsInhibitionArc(childEntry.second)) {
|
||||
|
// spareExit2.second->setInhibitionArcMultiplicity(childEntry.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
// }
|
||||
|
//
|
||||
|
// 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);
|
||||
|
// auto spareEntry3 = mGspn.getImmediateTransition(mDft.getElement(parents[j])->name() + "_" + child->name() + "_consuming2");
|
||||
|
//
|
||||
|
// if (childExit.first && spareEntry.first && spareEntry2.first && spareEntry3.first) { // Only add arcs if the objects have been found.
|
||||
|
// spareEntry.second->setInhibitionArcMultiplicity(childExit.second, 1);
|
||||
|
//
|
||||
|
// if (!spareEntry2.second->existsInhibitionArc(childExit.second)) {
|
||||
|
// spareEntry2.second->setInhibitionArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
//
|
||||
|
// spareEntry3.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// spareEntry3.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
//
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::POR:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> 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 { // Current element is not the primary child.
|
||||
|
// porEntry2.second->setInputArcMultiplicity(childExit.second, 1);
|
||||
|
// porEntry2.second->setOutputArcMultiplicity(childExit.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
//
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::SEQ:
|
||||
|
// {
|
||||
|
// // Sequences are realized with restrictions. Nothing to do here.
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::MUTEX:
|
||||
|
// {
|
||||
|
// // MUTEX are realized with restrictions. Nothing to do here.
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::BE:
|
||||
|
// {
|
||||
|
// // The parent is never a Basic Event.
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::CONSTF:
|
||||
|
// {
|
||||
|
// // The parent is never a Basic Event.
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::CONSTS:
|
||||
|
// {
|
||||
|
// // The parent is never a Basic Event.
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::PDEP:
|
||||
|
// {
|
||||
|
// // The parent is never a DEP. Hence the connections must be drawn somewhere else.
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// default:
|
||||
|
// {
|
||||
|
// STORM_LOG_ASSERT(false, "DFT type unknown.");
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// }
|
||||
|
// }
|
||||
|
// }
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
bool DftToGspnTransformator<ValueType>::isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) |
||||
|
{ |
||||
|
// If element is the top element, return true.
|
||||
|
if (dftElement->id() == mDft.getTopLevelIndex()) { |
||||
|
return true; |
||||
|
} |
||||
|
else { // Else look at all parents.
|
||||
|
auto parents = dftElement->parents(); |
||||
|
std::vector<bool> pathValidities; |
||||
|
|
||||
|
for (std::size_t i = 0; i < parents.size(); i++) { |
||||
|
// Add all parents to the vector, except if the parent is a SPARE and the current element is an inactive child of the SPARE.
|
||||
|
if (parents[i]->type() == storm::storage::DFTElementType::SPARE) { |
||||
|
auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(parents[i])->children(); |
||||
|
if (children[0]->id() != dftElement->id()) { |
||||
|
continue; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
pathValidities.push_back(isBEActive(parents[i])); |
||||
|
} |
||||
|
|
||||
|
// Check all vector entries. If one is true, a "valid" path has been found.
|
||||
|
for (std::size_t i = 0; i < pathValidities.size(); i++) { |
||||
|
if (pathValidities[i]) { |
||||
|
return true; |
||||
|
} |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// No "valid" path found. BE is inactive.
|
||||
|
return false; |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) |
||||
|
{ |
||||
|
return mDft.maxRank() - dftElement->rank(); |
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::drawGSPNDependencies() { |
||||
|
// for (std::size_t i = 0; i < mDft.nrElements(); i++) {
|
||||
|
// auto dftElement = mDft.getElement(i);
|
||||
|
//
|
||||
|
// if (dftElement->isDependency()) {
|
||||
|
// std::string gateName = dftElement->name().substr(0, dftElement->name().find("_"));
|
||||
|
// auto depEntry = mGspn.getTimedTransition(gateName + STR_FAILING);
|
||||
|
// auto trigger = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameTrigger() + STR_FAILED);
|
||||
|
//
|
||||
|
// if (depEntry.first && trigger.first) { // Only add arcs if the objects have been found.
|
||||
|
// if (!depEntry.second->existsInputArc(trigger.second)) {
|
||||
|
// depEntry.second->setInputArcMultiplicity(trigger.second, 1);
|
||||
|
// }
|
||||
|
// if (!depEntry.second->existsOutputArc(trigger.second)){
|
||||
|
// depEntry.second->setOutputArcMultiplicity(trigger.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
//
|
||||
|
// auto dependent = mGspn.getPlace(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement)->nameDependent() + STR_FAILED);
|
||||
|
//
|
||||
|
// if (dependent.first) { // Only add arcs if the objects have been found.
|
||||
|
// depEntry.second->setOutputArcMultiplicity(dependent.second, 1);
|
||||
|
// }
|
||||
|
// }
|
||||
|
// }
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::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 <typename ValueType> |
||||
|
std::vector<int> DftToGspnTransformator<ValueType>::getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) { |
||||
|
// std::vector<int> ids;
|
||||
|
//
|
||||
|
// switch (dftElement->type()) {
|
||||
|
// case storm::storage::DFTElementType::AND:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement)->children();
|
||||
|
//
|
||||
|
// for (std::size_t i = 0; i < children.size(); i++) {
|
||||
|
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
|
||||
|
// ids.insert(ids.end(), newIds.begin(), newIds.end());
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::OR:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement)->children();
|
||||
|
//
|
||||
|
// for (std::size_t i = 0; i < children.size(); i++) {
|
||||
|
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
|
||||
|
// ids.insert(ids.end(), newIds.begin(), newIds.end());
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::VOT:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement)->children();
|
||||
|
//
|
||||
|
// for (std::size_t i = 0; i < children.size(); i++) {
|
||||
|
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
|
||||
|
// ids.insert(ids.end(), newIds.begin(), newIds.end());
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::PAND:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->children();
|
||||
|
//
|
||||
|
// for (std::size_t i = 0; i < children.size(); i++) {
|
||||
|
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
|
||||
|
// ids.insert(ids.end(), newIds.begin(), newIds.end());
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::SPARE:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement)->children();
|
||||
|
//
|
||||
|
// // Only regard the primary child of a SPARE. The spare childs are not allowed to be listed here.
|
||||
|
// for (std::size_t i = 0; i < 1; i++) {
|
||||
|
// std::vector<int> newIds = getAllBEIDsOfElement(children[i]);
|
||||
|
// ids.insert(ids.end(), newIds.begin(), newIds.end());
|
||||
|
// }
|
||||
|
// break;
|
||||
|
// }
|
||||
|
// case storm::storage::DFTElementType::POR:
|
||||
|
// {
|
||||
|
// auto children = std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->children();
|
||||
|
//
|
||||
|
// for (std::size_t i = 0; i < children.size(); i++) {
|
||||
|
// std::vector<int> 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 ids;
|
||||
|
} |
||||
|
|
||||
|
template <typename ValueType> |
||||
|
void DftToGspnTransformator<ValueType>::writeGspn(bool toFile) { |
||||
|
if (toFile) { |
||||
|
// Writing to file
|
||||
|
std::ofstream file; |
||||
|
file.open("gspn.dot"); |
||||
|
storm::gspn::GSPN* gspn = builder.buildGspn(); |
||||
|
gspn->writeDotToStream(file); |
||||
|
delete gspn; |
||||
|
file.close(); |
||||
|
} else { |
||||
|
// Writing to console
|
||||
|
storm::gspn::GSPN* gspn = builder.buildGspn(); |
||||
|
gspn->writeDotToStream(std::cout); |
||||
|
delete gspn; |
||||
|
} |
||||
|
} |
||||
|
|
||||
|
// Explicitly instantiate the class.
|
||||
|
template class DftToGspnTransformator<double>; |
||||
|
|
||||
|
|
||||
|
#ifdef STORM_HAVE_CARL
|
||||
|
// template class DftToGspnTransformator<storm::RationalFunction>;
|
||||
|
#endif
|
||||
|
|
||||
|
} // namespace dft
|
||||
|
} // namespace transformations
|
||||
|
} // namespace storm
|
||||
|
|
||||
|
|
||||
@ -0,0 +1,174 @@ |
|||||
|
#pragma once |
||||
|
|
||||
|
#include "storm/storage/dft/DFT.h" |
||||
|
#include "storm/storage/gspn/GSPN.h" |
||||
|
#include "storm/storage/gspn/GspnBuilder.h" |
||||
|
|
||||
|
namespace storm { |
||||
|
namespace transformations { |
||||
|
namespace dft { |
||||
|
|
||||
|
/*! |
||||
|
* Transformator for DFT -> GSPN. |
||||
|
*/ |
||||
|
template<typename ValueType> |
||||
|
class DftToGspnTransformator { |
||||
|
|
||||
|
public: |
||||
|
/*! |
||||
|
* Constructor. |
||||
|
* |
||||
|
* @param dft DFT |
||||
|
*/ |
||||
|
DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft); |
||||
|
|
||||
|
/*! |
||||
|
* Transform the DFT to a GSPN. |
||||
|
*/ |
||||
|
void transform(); |
||||
|
|
||||
|
private: |
||||
|
/*! |
||||
|
* Write Gspn to file or console. |
||||
|
* |
||||
|
* @param toFile If true, the GSPN will be written to a file, otherwise it will |
||||
|
be written to the console. |
||||
|
*/ |
||||
|
void writeGspn(bool toFile); |
||||
|
|
||||
|
/* |
||||
|
* Draw all elements of the GSPN. |
||||
|
*/ |
||||
|
void drawGSPNElements(); |
||||
|
|
||||
|
/* |
||||
|
* Draw the connections between the elements of the GSPN. |
||||
|
*/ |
||||
|
void drawGSPNConnections(); |
||||
|
|
||||
|
/* |
||||
|
* Draw functional/probability dependencies into the GSPN. |
||||
|
*/ |
||||
|
void drawGSPNDependencies(); |
||||
|
|
||||
|
/* |
||||
|
* Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX). |
||||
|
*/ |
||||
|
void drawGSPNRestrictions(); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net Basic Event. |
||||
|
* |
||||
|
* @param dftBE The Basic Event. |
||||
|
*/ |
||||
|
void drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net AND. |
||||
|
* |
||||
|
* @param dftAnd The AND gate. |
||||
|
*/ |
||||
|
void drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net OR. |
||||
|
* |
||||
|
* @param dftOr The OR gate. |
||||
|
*/ |
||||
|
void drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net VOT. |
||||
|
* |
||||
|
* @param dftVot The VOT gate. |
||||
|
*/ |
||||
|
void drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net PAND. |
||||
|
* This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless). |
||||
|
* |
||||
|
* @param dftPand The PAND gate. |
||||
|
*/ |
||||
|
void drawPAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net SPARE. |
||||
|
* |
||||
|
* @param dftSpare The SPARE gate. |
||||
|
*/ |
||||
|
void drawSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net POR. |
||||
|
* This POR is inklusive (children are allowed to fail simultaneously and the POR will fail nevertheless). |
||||
|
* |
||||
|
* @param dftPor The POR gate. |
||||
|
*/ |
||||
|
void drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net CONSTF (Constant Failure, a Basic Event that has already failed). |
||||
|
* |
||||
|
* @param dftPor The CONSTF Basic Event. |
||||
|
*/ |
||||
|
void drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net CONSTS (Constant Save, a Basic Event that cannot fail). |
||||
|
* |
||||
|
* @param dftPor The CONSTS Basic Event. |
||||
|
*/ |
||||
|
void drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Draw a Petri net PDEP (FDEP is included with a firerate of 1). |
||||
|
*/ |
||||
|
void drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency, bool isRepresentative); |
||||
|
|
||||
|
/* |
||||
|
* Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token). |
||||
|
* |
||||
|
* @param dFTElement DFT element. |
||||
|
*/ |
||||
|
bool isBEActive(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement); |
||||
|
|
||||
|
/* |
||||
|
* Get the priority of the element. |
||||
|
* The priority is two times the length of the shortest path to the top event. |
||||
|
* |
||||
|
* @param priority The priority of the gate. Top Event has priority 0, its children 2, its grandchildren 4, ... |
||||
|
* |
||||
|
* @param dftElement The element whose priority shall be determined. |
||||
|
*/ |
||||
|
uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement); |
||||
|
|
||||
|
/* |
||||
|
* Return all ids of BEs, that are successors of the given element and that are not the spare childs of a SPARE. |
||||
|
* |
||||
|
* @param dftElement The element which |
||||
|
*/ |
||||
|
std::vector<int> getAllBEIDsOfElement(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement); |
||||
|
|
||||
|
|
||||
|
uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement); |
||||
|
|
||||
|
storm::storage::DFT<ValueType> const& mDft; |
||||
|
storm::gspn::GspnBuilder builder; |
||||
|
std::vector<uint64_t> failedNodes; |
||||
|
std::map<uint64_t, uint64_t> unavailableNodes; |
||||
|
std::map<uint64_t, uint64_t> activeNodes; |
||||
|
|
||||
|
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. |
||||
|
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
Preview
Loading…
Cancel
Save
Reference in new issue