sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
Browse Source

Refactored DftToGspnTransformator

main
Matthias Volk 7 years ago
parent
9452506b4c
commit
ec8304c386
2 changed files with 469 additions and 448 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 695
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  2. 160
      src/storm-dft/transformations/DftToGspnTransformator.h

695
src/storm-dft/transformations/DftToGspnTransformator.cpp
View File

@ -20,65 +20,64 @@ namespace storm {
this->smart = smart;
builder.setGspnName("DftToGspnTransformation");
// Loop through every DFT element and draw them as a GSPN.
drawGSPNElements();
// Translate all GSPN elements
translateGSPNElements();
// Draw restrictions into the GSPN (i.e. SEQ or MUTEX).
// Create initial template
// TODO
//drawGSPNRestrictions();
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() {
assert(failedNodes.size() > mDft.getTopLevelIndex());
return failedNodes[mDft.getTopLevelIndex()];
STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(), "Failed place for top level element does not exist.");
return failedPlaces.at(mDft.getTopLevelIndex());
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNElements() {
gspn::GSPN* DftToGspnTransformator<ValueType>::obtainGSPN() {
return builder.buildGspn();
}
// Loop through every DFT element and draw them as a GSPN.
template <typename ValueType>
void DftToGspnTransformator<ValueType>::translateGSPNElements() {
// Loop through every DFT element and create its corresponding GSPN template.
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.
// Check which type the element is and call the corresponding translate-function.
switch (dftElement->type()) {
case storm::storage::DFTElementType::BE:
translateBE(std::static_pointer_cast<storm::storage::DFTBE<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::CONSTF:
translateCONSTF(dftElement);
break;
case storm::storage::DFTElementType::CONSTS:
translateCONSTS(dftElement);
break;
case storm::storage::DFTElementType::AND:
drawAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement), isRepresentative);
translateAND(std::static_pointer_cast<storm::storage::DFTAnd<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::OR:
drawOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement), isRepresentative);
translateOR(std::static_pointer_cast<storm::storage::DFTOr<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::VOT:
drawVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement), isRepresentative);
translateVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement));
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);
translatePAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement), std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->isInclusive());
break;
case storm::storage::DFTElementType::POR:
drawPOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement), isRepresentative);
break;
case storm::storage::DFTElementType::SEQ:
drawSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement));
translatePOR(std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement), std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(dftElement)->isInclusive());
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);
case storm::storage::DFTElementType::SPARE:
translateSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::PDEP:
drawPDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
translatePDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
break;
case storm::storage::DFTElementType::SEQ:
translateSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement));
break;
default:
STORM_LOG_ASSERT(false, "DFT type " << dftElement->type() << " unknown.");
@ -89,282 +88,282 @@ namespace storm {
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative) {
uint64_t beActive = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
activeNodes.emplace(dftBE->id(), beActive);
uint64_t beFailed = builder.addPlace(defaultCapacity, 0, dftBE->name() + STR_FAILED);
void DftToGspnTransformator<ValueType>::translateBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y;
builder.setPlaceLayoutInfo(beActive, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter));
builder.setPlaceLayoutInfo(beFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
uint64_t disabledNode = 0;
if (!smart || dftBE->nrRestrictions() > 0) {
disabledNode = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter-9.0, ycenter));
}
uint64_t failedPlace = addFailedPlace(dftBE, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
uint64_t unavailableNode = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter));
}
uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
activePlaces.emplace(dftBE->id(), activePlace);
builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter));
assert(failedNodes.size() == dftBE->id());
failedNodes.push_back(beFailed);
uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing");
builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
builder.addInputArc(beActive, tActive);
builder.addInhibitionArc(beFailed, tActive);
builder.addOutputArc(tActive, beActive);
builder.addOutputArc(tActive, beFailed);
builder.addInputArc(activePlace, tActive);
builder.addInhibitionArc(failedPlace, tActive);
builder.addOutputArc(tActive, activePlace);
builder.addOutputArc(tActive, failedPlace);
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing");
builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
builder.addInhibitionArc(beActive, tPassive);
builder.addInhibitionArc(beFailed, tPassive);
builder.addOutputArc(tPassive, beFailed);
builder.addInhibitionArc(activePlace, tPassive);
builder.addInhibitionArc(failedPlace, tPassive);
builder.addOutputArc(tPassive, failedPlace);
if (!smart || dftBE->nrRestrictions() > 0) {
builder.addInhibitionArc(disabledNode, tActive);
builder.addInhibitionArc(disabledNode, tPassive);
uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter-9.0, ycenter));
builder.addInhibitionArc(disabledPlace, tActive);
builder.addInhibitionArc(disabledPlace, tPassive);
}
if (!smart || isRepresentative) {
builder.addOutputArc(tActive, unavailableNode);
builder.addOutputArc(tPassive, unavailableNode);
if (!smart || mDft.isRepresentative(dftBE->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter+9.0, ycenter));
builder.addOutputArc(tActive, unavailablePlace);
builder.addOutputArc(tPassive, unavailablePlace);
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::translateCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y;
addFailedPlace(dftConstF, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0), true);
if (!smart || mDft.isRepresentative(dftConstF->id())) {
addUnavailablePlace(dftConstF, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0), false);
}
}
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);
void DftToGspnTransformator<ValueType>::translateCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS) {
double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y;
size_t capacity = 0; // It cannot contain a token, because it cannot fail.
uint64_t failedPlace = builder.addPlace(capacity, 0, dftConstS->name() + STR_FAILED);
assert(failedPlaces.size() == dftConstS->id());
failedPlaces.push_back(failedPlace);
builder.setPlaceLayoutInfo(failedPlace, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
if (!smart || mDft.isRepresentative(dftConstS->id())) {
uint64_t unavailablePlace = builder.addPlace(capacity, 0, dftConstS->name() + "_unavail");
unavailablePlaces.emplace(dftConstS->id(), unavailablePlace);
builder.setPlaceLayoutInfo(unavailablePlace, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::translateAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t unavailableNode = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
}
uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING );
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0));
builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace);
uint64_t tAndFailed = builder.addImmediateTransition( getFailPriority(dftAnd), 0.0, dftAnd->name() + STR_FAILING );
builder.setTransitionLayoutInfo(tAndFailed, storm::gspn::LayoutInfo(xcenter, ycenter+3.0));
builder.addInhibitionArc(nodeFailed, tAndFailed);
builder.addOutputArc(tAndFailed, nodeFailed);
if (!smart || isRepresentative) {
builder.addOutputArc(tAndFailed, unavailableNode);
if (!smart || mDft.isRepresentative(dftAnd->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
for (auto const& child : dftAnd->children()) {
assert(failedNodes.size() > child->id());
builder.addInputArc(failedNodes[child->id()], tAndFailed);
builder.addOutputArc(tAndFailed, failedNodes[child->id()]);
builder.addInputArc(getFailedPlace(child), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(child));
}
}
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);
void DftToGspnTransformator<ValueType>::translateOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y;
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t unavailableNode = 0;
uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
bool isRepresentative = mDft.isRepresentative(dftOr->id());
uint64_t unavailablePlace = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
}
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.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0));
builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addOutputArc(tNodeFailed, nodeFailed);
for (size_t i = 0; i < dftOr->nrChildren(); ++i) {
auto const& child = dftOr->children().at(i);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftOr), 0.0, dftOr->name() + STR_FAILING + std::to_string(i) );
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0));
builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace);
if (!smart || isRepresentative) {
builder.addOutputArc(tNodeFailed, unavailableNode);
builder.addOutputArc(tFailed, unavailablePlace);
}
assert(failedNodes.size() > child->id());
builder.addInputArc(failedNodes[child->id()], tNodeFailed);
builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
++i;
builder.addInputArc(getFailedPlace(child), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(child));
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot, bool isRepresentative) {
void DftToGspnTransformator<ValueType>::translateVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
// TODO: finish layouting
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftVot->name() + STR_FAILED);
assert(failedNodes.size() == dftVot->id());
failedNodes.push_back(nodeFailed);
double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y;
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t unavailableNode = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftVot, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
}
uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter-3.0));
uint64_t nodeCollector = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector");
builder.setPlaceLayoutInfo(nodeCollector, storm::gspn::LayoutInfo(xcenter, ycenter));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
builder.addOutputArc(tFailed, failedPlace);
builder.addInhibitionArc(failedPlace, tFailed);
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
builder.addOutputArc(tNodeFailed, nodeFailed);
if (!smart || isRepresentative) {
builder.addOutputArc(tNodeFailed, unavailableNode);
if (!smart || mDft.isRepresentative(dftVot->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter+6.0, ycenter-3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addInputArc(nodeCollector, tNodeFailed, 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 collectorPlace = builder.addPlace(dftVot->nrChildren(), 0, dftVot->name() + "_collector");
builder.setPlaceLayoutInfo(collectorPlace, storm::gspn::LayoutInfo(xcenter, ycenter));
builder.addInputArc(collectorPlace, tFailed, dftVot->threshold());
for (size_t i = 0; i < dftVot->nrChildren(); ++i) {
auto const& child = dftVot->children().at(i);
uint64_t childNextPlace = builder.addPlace(defaultCapacity, 1, dftVot->name() + "_child_next" + 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);
builder.addOutputArc(tCollect, failedNodes[child->id()]);
++i;
builder.addOutputArc(tCollect, collectorPlace);
builder.addInputArc(childNextPlace, tCollect);
builder.addInputArc(getFailedPlace(child), tCollect);
builder.addOutputArc(tCollect, getFailedPlace(child));
}
}
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);
void DftToGspnTransformator<ValueType>::translatePAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive) {
double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y;
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0));
uint64_t unavailableNode = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftPand, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0));
}
uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0));
uint64_t tNodeFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tNodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0));
builder.addInhibitionArc(nodeFailed, tNodeFailed);
builder.addOutputArc(tNodeFailed, nodeFailed);
if (!smart || isRepresentative) {
builder.addOutputArc(tNodeFailed, unavailableNode);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0));
builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace);
if (!smart || mDft.isRepresentative(dftPand->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
if(dftPand->isInclusive()) {
if (inclusive) {
// Inclusive PAND
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + STR_FAILSAVE);
builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
builder.addInhibitionArc(failSafePlace, tFailed);
builder.addInhibitionArc(nodeFS, tNodeFailed);
// Transition for failed
// Transitions for failed place
for (auto const& child : dftPand->children()) {
builder.addInputArc(failedNodes[child->id()], tNodeFailed);
builder.addOutputArc(tNodeFailed, failedNodes[child->id()]);
builder.addInputArc(getFailedPlace(child), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(child));
}
// Transitions for fail-safe
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.setTransitionLayoutInfo(tfs, storm::gspn::LayoutInfo(xcenter-6.0+j*3.0, ycenter+3.0));
builder.addInputArc(failedNodes[dftPand->children().at(j)->id()], tfs);
builder.addOutputArc(tfs, failedNodes[dftPand->children().at(j)->id()]);
builder.addInhibitionArc(failedNodes[dftPand->children().at(j-1)->id()], tfs);
builder.addOutputArc(tfs, nodeFS);
builder.addInhibitionArc(nodeFS, tfs);
// Transitions for fail-safe place
for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) {
auto const& child = dftPand->children().at(i);
uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILSAVING + std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter-6.0+i*3.0, ycenter+3.0));
builder.addInputArc(getFailedPlace(child), tFailSafe);
builder.addOutputArc(tFailSafe, getFailedPlace(child));
builder.addInhibitionArc(getFailedPlace(dftPand->children().at(i-1)), tFailSafe);
builder.addOutputArc(tFailSafe, failSafePlace);
builder.addInhibitionArc(failSafePlace, tFailSafe);
}
} else {
// Exclusive PAND
uint64_t fi = 0;
uint64_t tn = 0;
for(uint64_t j = 0; j < dftPand->nrChildren(); ++j) {
auto const& child = dftPand->children()[j];
if (j > 0) {
builder.addInhibitionArc(failedNodes.at(child->id()), tn);
}
if (j != dftPand->nrChildren() - 1) {
uint64_t failSafeXPlace = 0;
uint64_t tFailSafeX = 0;
for (size_t i = 0; i < dftPand->nrChildren(); ++i) {
auto const& child = dftPand->children().at(i);
if (i > 0) {
// Set inhibition arc to previous transition
builder.addInhibitionArc(getFailedPlace(child), tFailSafeX);
}
if (i < dftPand->nrChildren() - 1) {
// Not last child
tn = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(j));
builder.setTransitionLayoutInfo(tn, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0));
tFailSafeX = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING + "_" +std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafeX, storm::gspn::LayoutInfo(xcenter-3.0, ycenter+3.0));
} else {
// Last child
tn = tNodeFailed;
}
builder.addInputArc(failedNodes.at(child->id()), tn);
builder.addOutputArc(tn, failedNodes.at(child->id()));
if (j > 0) {
builder.addInputArc(fi, tn);
tFailSafeX = tFailed;
}
if (j != dftPand->nrChildren() - 1) {
fi = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(j));
builder.setPlaceLayoutInfo(fi, storm::gspn::LayoutInfo(xcenter-3.0+j*3.0, ycenter));
builder.addOutputArc(tn, fi);
builder.addInputArc(getFailedPlace(child), tFailSafeX);
builder.addOutputArc(tFailSafeX, getFailedPlace(child));
if (i > 0) {
builder.addInputArc(failSafeXPlace, tFailSafeX);
}
if (i < dftPand->nrChildren() - 1) {
// Add fail-safe X place
failSafeXPlace = builder.addPlace(defaultCapacity, 0, dftPand->name() + "_F_" + std::to_string(i));
builder.setPlaceLayoutInfo(failSafeXPlace, storm::gspn::LayoutInfo(xcenter-3.0+i*3.0, ycenter));
builder.addOutputArc(tFailSafeX, failSafeXPlace);
builder.addInhibitionArc(failSafeXPlace, tFailSafeX);
}
}
}
}
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);
failedNodes.push_back(nodeFailed);
void DftToGspnTransformator<ValueType>::translatePOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive) {
double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y;
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0));
uint64_t unavailableNode = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0));
}
uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter+3.0, ycenter-3.0));
uint64_t tfail = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tfail, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0));
builder.addOutputArc(tfail, nodeFailed);
builder.addInhibitionArc(nodeFailed, tfail);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter+3.0, ycenter+3.0));
builder.addOutputArc(tFailed, failedPlace);
builder.addInhibitionArc(failedPlace, tFailed);
builder.addInputArc(failedNodes.at(dftPor->children().front()->id()), tfail);
builder.addOutputArc(tfail, failedNodes.at(dftPor->children().front()->id()));
// Arcs from first child
builder.addInputArc(getFailedPlace(dftPor->children().front()), tFailed);
builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front()));
if(!smart || isRepresentative) {
builder.addOutputArc(tfail, unavailableNode);
if (!smart || mDft.isRepresentative(dftPor->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter+9.0, ycenter-3.0));
builder.addOutputArc(tFailed, unavailablePlace);
}
if(dftPor->isInclusive()) {
if (inclusive) {
// Inclusive POR
uint64_t nodeFS = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE);
builder.setPlaceLayoutInfo(nodeFS, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
uint64_t failSafePlace = builder.addPlace(defaultCapacity, 0, dftPor->name() + STR_FAILSAVE);
builder.setPlaceLayoutInfo(failSafePlace, storm::gspn::LayoutInfo(xcenter-3.0, ycenter-3.0));
builder.addInhibitionArc(nodeFS, tfail);
uint64_t j = 0;
for (auto const& child : dftPor->children()) {
if(j > 0) {
uint64_t tfailsf = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(j));
builder.setTransitionLayoutInfo(tfailsf, storm::gspn::LayoutInfo(xcenter-3.0+j*3.0, ycenter+3.0));
builder.addInputArc(failedNodes.at(child->id()), tfailsf);
builder.addOutputArc(tfailsf, failedNodes.at(child->id()));
builder.addOutputArc(tfailsf, nodeFS);
builder.addInhibitionArc(nodeFS, tfailsf);
builder.addInhibitionArc(failedNodes.at(dftPor->children().front()->id()), tfailsf);
}
++j;
builder.addInhibitionArc(failSafePlace, tFailed);
// For all children except the first one
for (size_t i = 1; i < dftPor->nrChildren(); ++i) {
auto const& child = dftPor->children().at(i);
uint64_t tFailSafe = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILSAVING + std::to_string(i));
builder.setTransitionLayoutInfo(tFailSafe, storm::gspn::LayoutInfo(xcenter-3.0+i*3.0, ycenter+3.0));
builder.addInputArc(getFailedPlace(child), tFailSafe);
builder.addOutputArc(tFailSafe, getFailedPlace(child));
builder.addOutputArc(tFailSafe, failSafePlace);
builder.addInhibitionArc(failSafePlace, tFailSafe);
builder.addInhibitionArc(getFailedPlace(dftPor->children().front()), tFailSafe);
}
} else {
// Exclusive POR
uint64_t j = 0;
// For all children except the first one
for (auto const& child : dftPor->children()) {
if(j > 0) {
builder.addInhibitionArc(failedNodes.at(child->id()), tfail);
}
++j;
builder.addInhibitionArc(getFailedPlace(child), tFailed);
}
}
@ -372,212 +371,199 @@ namespace storm {
}
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);
void DftToGspnTransformator<ValueType>::translateSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y;
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
uint64_t unavailableNode = 0;
uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
bool isRepresentative = mDft.isRepresentative(dftSpare->id());
uint64_t unavailablePlace = 0;
if (!smart || isRepresentative) {
unavailableNode = addUnavailableNode(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
}
uint64_t spareActive = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED);
builder.setPlaceLayoutInfo(spareActive, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-12.0));
activeNodes.emplace(dftSpare->id(), spareActive);
std::vector<uint64_t> nextclTransitions;
std::vector<uint64_t> nextconsiderTransitions;
uint64_t j = 0;
for(auto const& child : dftSpare->children()) {
uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED);
builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter-20.0, ycenter-12.0));
activePlaces.emplace(dftSpare->id(), activePlace);
std::vector<uint64_t> tNextClaims;
std::vector<uint64_t> tNextConsiders;
for (size_t i = 0; i < dftSpare->nrChildren(); ++i) {
auto const& child = dftSpare->children().at(i);
// Consider next child
size_t nodeConsider = builder.addPlace(defaultCapacity, j == 0 ? 1 : 0, dftSpare->name()+ "_consider_" + child->name());
builder.setPlaceLayoutInfo(nodeConsider, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter-8.0));
size_t considerPlace = builder.addPlace(defaultCapacity, i == 0 ? 1 : 0, dftSpare->name()+ "_consider_" + child->name());
builder.setPlaceLayoutInfo(considerPlace, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter-8.0));
if (j > 0) {
if (i > 0) {
// Set output transition from previous next_claim
builder.addOutputArc(nextclTransitions.back(), nodeConsider);
builder.addOutputArc(tNextClaims.back(), considerPlace);
// Set output transition from previous cannot_claim
builder.addOutputArc(nextconsiderTransitions.back(), nodeConsider);
builder.addOutputArc(tNextConsiders.back(), considerPlace);
}
// Cannot claim child
uint64_t tnextconsider = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name());
builder.setTransitionLayoutInfo(tnextconsider, storm::gspn::LayoutInfo(xcenter-7.0+j*14.0, ycenter-8.0));
builder.addInputArc(nodeConsider, tnextconsider);
builder.addInputArc(unavailableNodes.at(child->id()), tnextconsider);
builder.addOutputArc(tnextconsider, unavailableNodes.at(child->id()));
nextconsiderTransitions.push_back(tnextconsider);
uint64_t tConsiderNext = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_cannot_claim_" + child->name());
builder.setTransitionLayoutInfo(tConsiderNext, storm::gspn::LayoutInfo(xcenter-7.0+i*14.0, ycenter-8.0));
builder.addInputArc(considerPlace, tConsiderNext);
builder.addInputArc(unavailablePlaces.at(child->id()), tConsiderNext);
builder.addOutputArc(tConsiderNext, unavailablePlaces.at(child->id()));
tNextConsiders.push_back(tConsiderNext);
// Claimed child
size_t nodeCUC = builder.addPlace(defaultCapacity, 0, dftSpare->name() + "_claimed_" + child->name());
builder.setPlaceLayoutInfo(nodeCUC, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter+5.0));
uint64_t tclaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name());
builder.setTransitionLayoutInfo(tclaim, storm::gspn::LayoutInfo(xcenter-15.0+j*14.0, ycenter));
builder.addInhibitionArc(unavailableNodes.at(child->id()), tclaim);
builder.addInputArc(nodeConsider, tclaim);
builder.addOutputArc(tclaim, nodeCUC);
builder.addOutputArc(tclaim, unavailableNodes.at(child->id()));
size_t claimedPlace = builder.addPlace(defaultCapacity, 0, dftSpare->name() + "_claimed_" + child->name());
builder.setPlaceLayoutInfo(claimedPlace, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter+5.0));
uint64_t tClaim = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_claim_" + child->name());
builder.setTransitionLayoutInfo(tClaim, storm::gspn::LayoutInfo(xcenter-15.0+i*14.0, ycenter));
builder.addInhibitionArc(unavailablePlaces.at(child->id()), tClaim);
builder.addInputArc(considerPlace, tClaim);
builder.addOutputArc(tClaim, claimedPlace);
builder.addOutputArc(tClaim, unavailablePlaces.at(child->id()));
// Claim next
uint64_t tnextcl = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(j));
builder.setTransitionLayoutInfo(tnextcl, storm::gspn::LayoutInfo(xcenter-7.0+j*14.0, ycenter+5.0));
builder.addInputArc(nodeCUC, tnextcl);
builder.addInputArc(failedNodes.at(child->id()), tnextcl);
builder.addOutputArc(tnextcl, failedNodes.at(child->id()));
nextclTransitions.push_back(tnextcl);
++j;
// Activate all nodes in spare module
uint64_t tClaimNext = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0, dftSpare->name() + "_next_claim_" + std::to_string(i));
builder.setTransitionLayoutInfo(tClaimNext, storm::gspn::LayoutInfo(xcenter-7.0+i*14.0, ycenter+5.0));
builder.addInputArc(claimedPlace, tClaimNext);
builder.addInputArc(getFailedPlace(child), tClaimNext);
builder.addOutputArc(tClaimNext, getFailedPlace(child));
tNextClaims.push_back(tClaimNext);
// Activate all elements in spare module
uint64_t l = 0;
for (uint64_t k : mDft.module(child->id())) {
uint64_t tactive = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(j) + "_" + std::to_string(k));
builder.setTransitionLayoutInfo(tactive, storm::gspn::LayoutInfo(xcenter-18.0+(j+l)*3, ycenter-12.0));
builder.addInhibitionArc(activeNodes.at(k), tactive);
builder.addInputArc(nodeCUC, tactive);
builder.addInputArc(spareActive, tactive);
builder.addOutputArc(tactive, nodeCUC);
builder.addOutputArc(tactive, spareActive);
builder.addOutputArc(tactive, activeNodes.at(k));
uint64_t tActivate = builder.addImmediateTransition(defaultPriority, 0.0, dftSpare->name() + "_activate_" + std::to_string(i) + "_" + std::to_string(k));
builder.setTransitionLayoutInfo(tActivate, storm::gspn::LayoutInfo(xcenter-18.0+(i+l)*3, ycenter-12.0));
builder.addInhibitionArc(activePlaces.at(k), tActivate);
builder.addInputArc(claimedPlace, tActivate);
builder.addInputArc(activePlace, tActivate);
builder.addOutputArc(tActivate, claimedPlace);
builder.addOutputArc(tActivate, activePlace);
builder.addOutputArc(tActivate, activePlaces.at(k));
++l;
}
}
// Set arcs to failed
builder.addOutputArc(nextconsiderTransitions.back(), nodeFailed);
builder.addOutputArc(nextclTransitions.back(), nodeFailed);
builder.addOutputArc(tNextConsiders.back(), failedPlace);
builder.addOutputArc(tNextClaims.back(), failedPlace);
if (!smart || isRepresentative) {
builder.addOutputArc(nextconsiderTransitions.back(), unavailableNode);
builder.addOutputArc(nextclTransitions.back(), unavailableNode);
builder.addOutputArc(tNextConsiders.back(), unavailablePlace);
builder.addOutputArc(tNextClaims.back(), unavailablePlace);
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF, bool isRepresentative) {
failedNodes.push_back(builder.addPlace(defaultCapacity, 1, dftConstF->name() + STR_FAILED));
uint64_t unavailableNode = 0;
if (isRepresentative) {
// TODO set position
unavailableNode = addUnavailableNode(dftConstF, storm::gspn::LayoutInfo(0, 0), false);
}
}
//
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) {
void DftToGspnTransformator<ValueType>::translatePDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency) {
double xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;
if (!smart) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftDependency->name() + STR_FAILED);
failedNodes.push_back(nodeFailed);
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
addUnavailableNode(dftDependency, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
}
uint64_t forwardPlace = 0;
if (dftDependency->probability() < 1.0) {
// PDEP
forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward");
builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0));
uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin");
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()));
uint64_t forwardPlace = builder.addPlace(defaultCapacity, 0, dftDependency->name() + "_forward");
builder.setPlaceLayoutInfo(forwardPlace, storm::gspn::LayoutInfo(xcenter+1.0, ycenter+2.0));
uint64_t tStartFlip = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip");
builder.addInputArc(coinPlace, tStartFlip);
builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip);
builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent()));
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, dftDependency->probability(), "_win_flip");
builder.addInputArc(flipPlace, t2);
builder.addOutputArc(t2, forwardPlace);
if (dftDependency->probability() < 1.0) {
uint64_t t3 = builder.addImmediateTransition(defaultPriority, 1 - dftDependency->probability(), "_loose_flip");
builder.addInputArc(flipPlace, t3);
}
builder.addOutputArc(tStartFlip, flipPlace);
uint64_t tWinFlip = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip");
builder.addInputArc(flipPlace, tWinFlip);
builder.addOutputArc(tWinFlip, forwardPlace);
uint64_t tLooseFlip = builder.addImmediateTransition(defaultPriority, storm::utility::one<ValueType>() - dftDependency->probability(), "_loose_flip");
builder.addInputArc(flipPlace, tLooseFlip);
} else {
builder.addOutputArc(t1, forwardPlace);
// FDEP
forwardPlace = getFailedPlace(dftDependency->triggerEvent());
}
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);
for (auto const& child : dftDependency->dependentEvents()) {
uint64_t tForwardFailure = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + child->name());
builder.addInputArc(forwardPlace, tForwardFailure);
builder.addOutputArc(tForwardFailure, forwardPlace);
builder.addOutputArc(tForwardFailure, getFailedPlace(child));
builder.addInhibitionArc(getFailedPlace(child), tForwardFailure);
if (!smart || child->nrRestrictions() > 0) {
builder.addInhibitionArc(disabledPlaces.at(child->id()), tForwardFailure);
}
if (!smart || mDft.isRepresentative(depEv->id())) {
builder.addOutputArc(tx, unavailableNodes.at(depEv->id()));
if (!smart || mDft.isRepresentative(child->id())) {
builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id()));
}
}
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq) {
void DftToGspnTransformator<ValueType>::translateSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq) {
STORM_LOG_THROW(dftSeq->allChildrenBEs(), storm::exceptions::NotImplementedException, "Sequence enforcers with gates as children are currently not supported");
double xcenter = mDft.getElementLayoutInfo(dftSeq->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftSeq->id()).y;
if (!smart) {
uint64_t nodeFailed = builder.addPlace(defaultCapacity, 0, dftSeq->name() + STR_FAILED);
failedNodes.push_back(nodeFailed);
builder.setPlaceLayoutInfo(nodeFailed, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
addUnavailableNode(dftSeq, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
addFailedPlace(dftSeq, storm::gspn::LayoutInfo(xcenter+10.0, ycenter-8.0));
addUnavailablePlace(dftSeq, storm::gspn::LayoutInfo(xcenter+16.0, ycenter-8.0));
}
uint64_t j = 0;
uint64_t tEnable = 0;
uint64_t nextPlace = 0;
for(auto const& child : dftSeq->children()) {
nextPlace = builder.addPlace(defaultCapacity, j==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name());
builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter-5.0+j*3.0, ycenter-3.0));
if (j>0) {
for (size_t i = 0; i < dftSeq->nrChildren(); ++i) {
auto const& child = dftSeq->children().at(i);
nextPlace = builder.addPlace(defaultCapacity, i==0 ? 1 : 0, dftSeq->name() + "_next_" + child->name());
builder.setPlaceLayoutInfo(nextPlace, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter-3.0));
if (i>0) {
builder.addOutputArc(tEnable, nextPlace);
}
tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" +child->name());
builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter-5.0+j*3.0, ycenter+3.0));
builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter-5.0+i*3.0, ycenter+3.0));
builder.addInputArc(nextPlace, tEnable);
builder.addInputArc(disabledNodes.at(child->id()), tEnable);
if (j>0) {
builder.addInputArc(failedNodes.at(dftSeq->children().at(j-1)->id()), tEnable);
builder.addInputArc(disabledPlaces.at(child->id()), tEnable);
if (i>0) {
builder.addInputArc(getFailedPlace(dftSeq->children().at(i-1)), tEnable);
}
++j;
}
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) {
uint64_t unavailableNode = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail");
assert(unavailableNode != 0);
unavailableNodes.emplace(dftElement->id(), unavailableNode);
builder.setPlaceLayoutInfo(unavailableNode, layoutInfo);
return unavailableNode;
uint64_t DftToGspnTransformator<ValueType>::addFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialFailed) {
uint64_t failedPlace = builder.addPlace(defaultCapacity, initialFailed ? 1 : 0, dftElement->name() + STR_FAILED);
assert(failedPlaces.size() == dftElement->id());
failedPlaces.push_back(failedPlace);
builder.setPlaceLayoutInfo(failedPlace, layoutInfo);
return failedPlace;
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addUnavailablePlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable) {
uint64_t unavailablePlace = builder.addPlace(defaultCapacity, initialAvailable ? 0 : 1, dftElement->name() + "_unavail");
unavailablePlaces.emplace(dftElement->id(), unavailablePlace);
builder.setPlaceLayoutInfo(unavailablePlace, layoutInfo);
return unavailablePlace;
}
template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe, storm::gspn::LayoutInfo const& layoutInfo) {
uint64_t disabledNode = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled");
assert(disabledNode != 0);
disabledNodes.emplace(dftBe->id(), disabledNode);
builder.setPlaceLayoutInfo(disabledNode, layoutInfo);
return disabledNode;
uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled");
disabledPlaces.emplace(dftBe->id(), disabledPlace);
builder.setPlaceLayoutInfo(disabledPlace, layoutInfo);
return disabledPlace;
}
template <typename ValueType>
@ -595,20 +581,9 @@ namespace storm {
}
template <typename ValueType>
void DftToGspnTransformator<ValueType>::drawGSPNRestrictions() {
// TODO
}
template <typename ValueType>
gspn::GSPN* DftToGspnTransformator<ValueType>::obtainGSPN() {
return builder.buildGspn();
}
// Explicitly instantiate the class.
template class DftToGspnTransformator<double>;
#ifdef STORM_HAVE_CARL
// template class DftToGspnTransformator<storm::RationalFunction>;
#endif

160
src/storm-dft/transformations/DftToGspnTransformator.h
View File

@ -33,101 +33,106 @@ namespace storm {
*/
gspn::GSPN* obtainGSPN();
/*!
* Get failed place id of top level element.
*/
uint64_t toplevelFailedPlaceId();
private:
/*
* Draw all elements of the GSPN.
/*!
* Translate all elements of the GSPN.
*/
void translateGSPNElements();
/*!
* Translate a GSPN Basic Event.
*
* @param dftBE The Basic Event.
*/
void drawGSPNElements();
void translateBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE);
/*
* Draw restrictions between the elements of the GSPN (i.e. SEQ or MUTEX).
/*!
* Translate a GSPN CONSTF (Constant Failure, a Basic Event that has already failed).
*
* @param dftPor The CONSTF Basic Event.
*/
void drawGSPNRestrictions();
void translateCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF);
/*
* Draw a Petri net Basic Event.
/*!
* Translate a GSPN CONSTS (Constant Save, a Basic Event that cannot fail).
*
* @param dftBE The Basic Event.
* @param dftPor The CONSTS Basic Event.
*/
void drawBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE, bool isRepresentative);
void translateCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS);
/*
* Draw a Petri net AND.
/*!
* Translate a GSPN AND.
*
* @param dftAnd The AND gate.
*/
void drawAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd, bool isRepresentative);
void translateAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd);
/*
* Draw a Petri net OR.
/*!
* Translate a GSPN OR.
*
* @param dftOr The OR gate.
*/
void drawOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr, bool isRepresentative);
void translateOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr);
/*
* Draw a Petri net VOT.
/*!
* Translate a GSPN VOT.
*
* @param dftVot The VOT gate.
*/
void drawVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot, bool isRepresentative);
void translateVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot);
/*
* Draw a Petri net PAND.
* This PAND is inklusive (children are allowed to fail simultaneously and the PAND will fail nevertheless).
/*!
* Translate a GSPN PAND.
*
* @param dftPand The PAND gate.
* @param inclusive Flag wether the PAND is inclusive (children are allowed to fail simultaneously and the PAND will fail nevertheless)
*/
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);
void translatePAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive = true);
/*
* Draw a Petri net POR.
* This POR is inklusive (children are allowed to fail simultaneously and the POR will fail nevertheless).
/*!
* Translate a GSPN POR.
*
* @param dftPor The POR gate.
* @param inclusive Flag wether the POR is inclusive (children are allowed to fail simultaneously and the POR will fail nevertheless)
*/
void drawPOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool isRepresentative);
void translatePOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive = true);
/*
* Draw a Petri net CONSTF (Constant Failure, a Basic Event that has already failed).
/*!
* Translate a GSPN SPARE.
*
* @param dftPor The CONSTF Basic Event.
* @param dftSpare The SPARE gate.
*/
void drawCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF, bool isRepresentative);
void translateSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare);
/*
* Draw a Petri net CONSTS (Constant Save, a Basic Event that cannot fail).
/*!
* Translate a GSPN PDEP (FDEP is included with a probability of 1).
*
* @param dftPor The CONSTS Basic Event.
* @param dftDependency The PDEP gate.
*/
void drawCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS, bool isRepresentative);
void translatePDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency);
/*
* Draw a Petri net PDEP (FDEP is included with a firerate of 1).
/*!
* Translate a GSPN SEQ.
*
* @param dftSeq The SEQ gate.
*/
void drawPDEP(std::shared_ptr<storm::storage::DFTDependency<ValueType> const> dftDependency);
void translateSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq);
void drawSeq(std::shared_ptr<storm::storage::DFTSeq<ValueType> const> dftSeq);
/*
* Return true if BE is active (corresponding place contains one initial token) or false if BE is inactive (corresponding place contains no initial token).
/*!
* Check if the element is active intially.
*
* @param dFTElement DFT element.
*
* @return True iff element is active initially.
*/
bool isActiveInitially(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.
*
@ -137,16 +142,57 @@ namespace storm {
*/
uint64_t getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dFTElement);
uint64_t addUnavailableNode(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true);
/*!
* Add failed place for an element.
*
* @param dftElement Element.
* @param layoutInfo Information about layout.
* @param initialFailed Flag indicating whether the element is initially failed.
*
* @return Id of added failed place.
*/
uint64_t addFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialFailed = false);
/*!
* Add unavailable place for element.
*
* @param dftElement Element.
* @param layoutInfo Information about layout.
* @param initialAvailable Flag indicating whether the element is available initially.
*
* @return Id of added unavailable place.
*/
uint64_t addUnavailablePlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const& layoutInfo, bool initialAvailable = true);
/*!
* Add disabled place for element.
*
* @param dftBe Basic Element.
* @param layoutInfo Information about layout.
*
* @return Id of added disabled place.
*/
uint64_t addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe, storm::gspn::LayoutInfo const& layoutInfo);
/*!
* Get failed place for element.
*
* @param dftElement Element.
*
* @return Id of failed place corresponding to the given element.
*/
uint64_t getFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
return failedPlaces.at(dftElement->id());
}
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;
std::map<uint64_t, uint64_t> disabledNodes;
// Interface places for DFT elements
std::vector<uint64_t> failedPlaces;
std::map<uint64_t, uint64_t> unavailablePlaces;
std::map<uint64_t, uint64_t> activePlaces;
std::map<uint64_t, uint64_t> disabledPlaces;
bool smart;
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.

Write Preview
Loading…
Cancel
Save