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

Added dontCare transformation support for BE, AND and OR DFT elements.

main
Alexander Nikolai Bork 8 years ago
parent
c9b66b2492
commit
875764c472
2 changed files with 353 additions and 96 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Unified View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 393
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  2. 56
      src/storm-dft/transformations/DftToGspnTransformator.h

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

@ -11,12 +11,14 @@ namespace storm {
static constexpr const uint64_t defaultCapacity = 1; static constexpr const uint64_t defaultCapacity = 1;
template<typename ValueType> template<typename ValueType>
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const &dft) : mDft(dft) {
DftToGspnTransformator<ValueType>::DftToGspnTransformator(storm::storage::DFT<ValueType> const &dft) : mDft(
dft) {
// Intentionally left empty. // Intentionally left empty.
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::transform(std::set<uint64_t> const &dontCareElements, bool smart, bool mergeDCFailed) {
void DftToGspnTransformator<ValueType>::transform(std::set<uint64_t> const &dontCareElements, bool smart,
bool mergeDCFailed) {
this->dontCareElements = dontCareElements; this->dontCareElements = dontCareElements;
this->smart = smart; this->smart = smart;
this->mergedDCFailed = mergeDCFailed; this->mergedDCFailed = mergeDCFailed;
@ -31,7 +33,8 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() { uint64_t DftToGspnTransformator<ValueType>::toplevelFailedPlaceId() {
STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(), "Failed place for top level element does not exist.");
STORM_LOG_ASSERT(failedPlaces.size() > mDft.getTopLevelIndex(),
"Failed place for top level element does not exist.");
return failedPlaces.at(mDft.getTopLevelIndex()); return failedPlaces.at(mDft.getTopLevelIndex());
} }
@ -67,18 +70,23 @@ namespace storm {
translateVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement)); translateVOT(std::static_pointer_cast<storm::storage::DFTVot<ValueType> const>(dftElement));
break; break;
case storm::storage::DFTElementType::PAND: case storm::storage::DFTElementType::PAND:
translatePAND(std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement),
std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement)->isInclusive());
translatePAND(
std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(dftElement),
std::static_pointer_cast<storm::storage::DFTPand<ValueType> const>(
dftElement)->isInclusive());
break; break;
case storm::storage::DFTElementType::POR: case storm::storage::DFTElementType::POR:
translatePOR(std::static_pointer_cast<storm::storage::DFTPor<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());
std::static_pointer_cast<storm::storage::DFTPor<ValueType> const>(
dftElement)->isInclusive());
break; break;
case storm::storage::DFTElementType::SPARE: case storm::storage::DFTElementType::SPARE:
translateSPARE(std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement));
translateSPARE(
std::static_pointer_cast<storm::storage::DFTSpare<ValueType> const>(dftElement));
break; break;
case storm::storage::DFTElementType::PDEP: case storm::storage::DFTElementType::PDEP:
translatePDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(dftElement));
translatePDEP(std::static_pointer_cast<storm::storage::DFTDependency<ValueType> const>(
dftElement));
break; break;
case storm::storage::DFTElementType::SEQ: case storm::storage::DFTElementType::SEQ:
translateSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement)); translateSeq(std::static_pointer_cast<storm::storage::DFTSeq<ValueType> const>(dftElement));
@ -92,29 +100,48 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateBE(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
void DftToGspnTransformator<ValueType>::translateBE(
std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBE) {
double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y;
uint64_t failedPlace = addFailedPlace(dftBE, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); uint64_t failedPlace = addFailedPlace(dftBE, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0, dftBE->name() + STR_ACTIVATED);
uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftBE) ? 1 : 0,
dftBE->name() + STR_ACTIVATED);
activePlaces.emplace(dftBE->id(), activePlace); activePlaces.emplace(dftBE->id(), activePlace);
builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter)); builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 3.0, ycenter));
uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(), dftBE->name() + "_activeFailing");
uint64_t tActive = builder.addTimedTransition(defaultPriority, dftBE->activeFailureRate(),
dftBE->name() + "_activeFailing");
builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); builder.setTransitionLayoutInfo(tActive, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
builder.addInputArc(activePlace, tActive); builder.addInputArc(activePlace, tActive);
builder.addInhibitionArc(failedPlace, tActive); builder.addInhibitionArc(failedPlace, tActive);
builder.addOutputArc(tActive, activePlace); builder.addOutputArc(tActive, activePlace);
builder.addOutputArc(tActive, failedPlace); builder.addOutputArc(tActive, failedPlace);
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(), dftBE->name() + "_passiveFailing");
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(),
dftBE->name() + "_passiveFailing");
builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); builder.setTransitionLayoutInfo(tPassive, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
builder.addInhibitionArc(activePlace, tPassive); builder.addInhibitionArc(activePlace, tPassive);
builder.addInhibitionArc(failedPlace, tPassive); builder.addInhibitionArc(failedPlace, tPassive);
builder.addOutputArc(tPassive, failedPlace); builder.addOutputArc(tPassive, failedPlace);
if (dontCareElements.count(dftBE->id()) && dftBE->id() != mDft.getTopLevelIndex()) {
u_int64_t tDontCare = addDontcareTransition(dftBE,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter));
if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0, dftBE->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 5.0));
builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace);
} else {
builder.addInhibitionArc(failedPlace, tDontCare);
builder.addOutputArc(tDontCare, failedPlace);
}
}
if (!smart || dftBE->nrRestrictions() > 0) { if (!smart || dftBE->nrRestrictions() > 0) {
uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter - 9.0, ycenter)); uint64_t disabledPlace = addDisabledPlace(dftBE, storm::gspn::LayoutInfo(xcenter - 9.0, ycenter));
builder.addInhibitionArc(disabledPlace, tActive); builder.addInhibitionArc(disabledPlace, tActive);
@ -122,14 +149,16 @@ namespace storm {
} }
if (!smart || mDft.isRepresentative(dftBE->id())) { if (!smart || mDft.isRepresentative(dftBE->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftBE, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter));
uint64_t unavailablePlace = addUnavailablePlace(dftBE,
storm::gspn::LayoutInfo(xcenter + 9.0, ycenter));
builder.addOutputArc(tActive, unavailablePlace); builder.addOutputArc(tActive, unavailablePlace);
builder.addOutputArc(tPassive, unavailablePlace); builder.addOutputArc(tPassive, unavailablePlace);
} }
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateCONSTF(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
void DftToGspnTransformator<ValueType>::translateCONSTF(
std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstF) {
double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x; double xcenter = mDft.getElementLayoutInfo(dftConstF->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y; double ycenter = mDft.getElementLayoutInfo(dftConstF->id()).y;
@ -141,7 +170,8 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateCONSTS(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS) {
void DftToGspnTransformator<ValueType>::translateCONSTS(
std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftConstS) {
double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x; double xcenter = mDft.getElementLayoutInfo(dftConstS->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y; double ycenter = mDft.getElementLayoutInfo(dftConstS->id()).y;
@ -160,19 +190,85 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateAND(std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
void DftToGspnTransformator<ValueType>::translateAND(
std::shared_ptr<storm::storage::DFTAnd<ValueType> const> dftAnd) {
double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y;
uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, 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);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftAnd), 0.0,
dftAnd->name() + STR_FAILING);
builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0)); builder.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter, ycenter + 3.0));
builder.addInhibitionArc(failedPlace, tFailed); builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace); builder.addOutputArc(tFailed, failedPlace);
//TODO Make it smart
if (dontCareElements.count(dftAnd->id())) {
if (dftAnd->id() != mDft.getTopLevelIndex()) {
u_int64_t tDontCare = addDontcareTransition(dftAnd,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
dftAnd->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace);
//Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftAnd->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
dftAnd->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
builder.addInhibitionArc(propagationPlace, tPropagationFailed);
builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, propagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
dftAnd->name() +
"_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare,
storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
builder.addInputArc(dontCarePlace, tPropagationDontCare);
builder.addOutputArc(tPropagationDontCare, dontCarePlace);
builder.addOutputArc(tPropagationDontCare, propagationPlace);
for (auto const &child : dftAnd->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(propagationPlace, childDontCare);
builder.addOutputArc(childDontCare, propagationPlace);
}
}
} else {
builder.addInhibitionArc(failedPlace, tDontCare);
builder.addOutputArc(tDontCare, failedPlace);
for (auto const &child : dftAnd->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(failedPlace, childDontCare);
builder.addOutputArc(childDontCare, failedPlace);
}
}
}
} else {
// If AND is TLE, simple failure propagation suffices
for (auto const &child : dftAnd->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(failedPlace, childDontCare);
builder.addOutputArc(childDontCare, failedPlace);
}
}
}
}
if (!smart || mDft.isRepresentative(dftAnd->id())) { if (!smart || mDft.isRepresentative(dftAnd->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftAnd, storm::gspn::LayoutInfo(xcenter + 6.0,
ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace); builder.addOutputArc(tFailed, unavailablePlace);
} }
@ -183,22 +279,87 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateOR(std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
void DftToGspnTransformator<ValueType>::translateOR(
std::shared_ptr<storm::storage::DFTOr<ValueType> const> dftOr) {
double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x; double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y; double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y;
uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
if (dontCareElements.count(dftOr->id())) {
if (dftOr->id() != mDft.getTopLevelIndex()) {
u_int64_t tDontCare = addDontcareTransition(dftOr,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0, dftOr->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace);
//Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftOr->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
dftOr->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
builder.addInhibitionArc(propagationPlace, tPropagationFailed);
builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, propagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
dftOr->name() +
"_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare,
storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
builder.addInhibitionArc(propagationPlace, tPropagationDontCare);
builder.addInputArc(dontCarePlace, tPropagationDontCare);
builder.addOutputArc(tPropagationDontCare, dontCarePlace);
builder.addOutputArc(tPropagationDontCare, propagationPlace);
for (auto const &child : dftOr->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(propagationPlace, childDontCare);
builder.addOutputArc(childDontCare, propagationPlace);
}
}
} else {
builder.addInhibitionArc(failedPlace, tDontCare);
builder.addOutputArc(tDontCare, failedPlace);
for (auto const &child : dftOr->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(failedPlace, childDontCare);
builder.addOutputArc(childDontCare, failedPlace);
}
}
}
} else {
// If OR is TLE, simple failure propagation suffices
for (auto const &child : dftOr->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(failedPlace, childDontCare);
builder.addOutputArc(childDontCare, failedPlace);
}
}
}
}
bool isRepresentative = mDft.isRepresentative(dftOr->id()); bool isRepresentative = mDft.isRepresentative(dftOr->id());
uint64_t unavailablePlace = 0; uint64_t unavailablePlace = 0;
if (!smart || isRepresentative) { if (!smart || isRepresentative) {
unavailablePlace = addUnavailablePlace(dftOr, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
unavailablePlace = addUnavailablePlace(dftOr,
storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
} }
for (size_t i = 0; i < dftOr->nrChildren(); ++i) { for (size_t i = 0; i < dftOr->nrChildren(); ++i) {
auto const &child = dftOr->children().at(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));
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.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace); builder.addOutputArc(tFailed, failedPlace);
if (!smart || isRepresentative) { if (!smart || isRepresentative) {
@ -210,7 +371,8 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateVOT(std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
void DftToGspnTransformator<ValueType>::translateVOT(
std::shared_ptr<storm::storage::DFTVot<ValueType> const> dftVot) {
// TODO: finish layouting // TODO: finish layouting
double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x; double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x;
@ -218,12 +380,14 @@ namespace storm {
uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0, dftVot->name() + STR_FAILING);
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftVot), 0.0,
dftVot->name() + STR_FAILING);
builder.addOutputArc(tFailed, failedPlace); builder.addOutputArc(tFailed, failedPlace);
builder.addInhibitionArc(failedPlace, tFailed); builder.addInhibitionArc(failedPlace, tFailed);
if (!smart || mDft.isRepresentative(dftVot->id())) { if (!smart || mDft.isRepresentative(dftVot->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter + 6.0, ycenter - 3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftVot, storm::gspn::LayoutInfo(xcenter + 6.0,
ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace); builder.addOutputArc(tFailed, unavailablePlace);
} }
@ -233,9 +397,12 @@ namespace storm {
for (size_t i = 0; i < dftVot->nrChildren(); ++i) { for (size_t i = 0; i < dftVot->nrChildren(); ++i) {
auto const &child = dftVot->children().at(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 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));
uint64_t tCollect = builder.addImmediateTransition(getFailPriority(dftVot), 0.0,
dftVot->name() + "_child_collect" +
std::to_string(i));
builder.addOutputArc(tCollect, collectorPlace); builder.addOutputArc(tCollect, collectorPlace);
builder.addInputArc(childNextPlace, tCollect); builder.addInputArc(childNextPlace, tCollect);
builder.addInputArc(getFailedPlace(child), tCollect); builder.addInputArc(getFailedPlace(child), tCollect);
@ -244,19 +411,22 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translatePAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive) {
void DftToGspnTransformator<ValueType>::translatePAND(
std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive) {
double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x; double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y; double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y;
uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0)); uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPand), 0.0, dftPand->name() + STR_FAILING);
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.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0));
builder.addInhibitionArc(failedPlace, tFailed); builder.addInhibitionArc(failedPlace, tFailed);
builder.addOutputArc(tFailed, failedPlace); builder.addOutputArc(tFailed, failedPlace);
if (!smart || mDft.isRepresentative(dftPand->id())) { if (!smart || mDft.isRepresentative(dftPand->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftPand, storm::gspn::LayoutInfo(xcenter + 9.0,
ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace); builder.addOutputArc(tFailed, unavailablePlace);
} }
@ -275,8 +445,11 @@ namespace storm {
// Transitions for fail-safe place // Transitions for fail-safe place
for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) { for (uint64_t i = 1; i < dftPand->nrChildren(); ++i) {
auto const &child = dftPand->children().at(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));
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.addInputArc(getFailedPlace(child), tFailSafe);
builder.addOutputArc(tFailSafe, getFailedPlace(child)); builder.addOutputArc(tFailSafe, getFailedPlace(child));
@ -298,8 +471,11 @@ namespace storm {
if (i < dftPand->nrChildren() - 1) { if (i < dftPand->nrChildren() - 1) {
// Not last child // Not last child
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));
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 { } else {
// Last child // Last child
tFailSafeX = tFailed; tFailSafeX = tFailed;
@ -313,8 +489,10 @@ namespace storm {
if (i < dftPand->nrChildren() - 1) { if (i < dftPand->nrChildren() - 1) {
// Add fail-safe X place // 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));
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.addOutputArc(tFailSafeX, failSafeXPlace);
builder.addInhibitionArc(failSafeXPlace, tFailSafeX); builder.addInhibitionArc(failSafeXPlace, tFailSafeX);
} }
@ -323,13 +501,15 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translatePOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive) {
void DftToGspnTransformator<ValueType>::translatePOR(
std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive) {
double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x; double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y; double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y;
uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0)); uint64_t failedPlace = addFailedPlace(dftPor, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0));
uint64_t tFailed = builder.addImmediateTransition(getFailPriority(dftPor), 0.0, dftPor->name() + STR_FAILING);
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.setTransitionLayoutInfo(tFailed, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter + 3.0));
builder.addOutputArc(tFailed, failedPlace); builder.addOutputArc(tFailed, failedPlace);
builder.addInhibitionArc(failedPlace, tFailed); builder.addInhibitionArc(failedPlace, tFailed);
@ -339,7 +519,8 @@ namespace storm {
builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front())); builder.addOutputArc(tFailed, getFailedPlace(dftPor->children().front()));
if (!smart || mDft.isRepresentative(dftPor->id())) { if (!smart || mDft.isRepresentative(dftPor->id())) {
uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter + 9.0, ycenter - 3.0));
uint64_t unavailablePlace = addUnavailablePlace(dftPor, storm::gspn::LayoutInfo(xcenter + 9.0,
ycenter - 3.0));
builder.addOutputArc(tFailed, unavailablePlace); builder.addOutputArc(tFailed, unavailablePlace);
} }
@ -353,8 +534,11 @@ namespace storm {
// For all children except the first one // For all children except the first one
for (size_t i = 1; i < dftPor->nrChildren(); ++i) { for (size_t i = 1; i < dftPor->nrChildren(); ++i) {
auto const &child = dftPor->children().at(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));
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.addInputArc(getFailedPlace(child), tFailSafe);
builder.addOutputArc(tFailSafe, getFailedPlace(child)); builder.addOutputArc(tFailSafe, getFailedPlace(child));
@ -375,7 +559,8 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translateSPARE(std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
void DftToGspnTransformator<ValueType>::translateSPARE(
std::shared_ptr<storm::storage::DFTSpare<ValueType> const> dftSpare) {
double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x; double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y; double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y;
@ -384,10 +569,12 @@ namespace storm {
bool isRepresentative = mDft.isRepresentative(dftSpare->id()); bool isRepresentative = mDft.isRepresentative(dftSpare->id());
uint64_t unavailablePlace = 0; uint64_t unavailablePlace = 0;
if (!smart || isRepresentative) { if (!smart || isRepresentative) {
unavailablePlace = addUnavailablePlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
unavailablePlace = addUnavailablePlace(dftSpare,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
} }
uint64_t activePlace = builder.addPlace(defaultCapacity, isActiveInitially(dftSpare) ? 1 : 0, dftSpare->name() + STR_ACTIVATED);
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)); builder.setPlaceLayoutInfo(activePlace, storm::gspn::LayoutInfo(xcenter - 20.0, ycenter - 12.0));
activePlaces.emplace(dftSpare->id(), activePlace); activePlaces.emplace(dftSpare->id(), activePlace);
@ -396,8 +583,10 @@ namespace storm {
for (size_t i = 0; i < dftSpare->nrChildren(); ++i) { for (size_t i = 0; i < dftSpare->nrChildren(); ++i) {
auto const &child = dftSpare->children().at(i); auto const &child = dftSpare->children().at(i);
// Consider next child // Consider next child
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));
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 (i > 0) { if (i > 0) {
// Set output transition from previous next_claim // Set output transition from previous next_claim
@ -407,26 +596,36 @@ namespace storm {
} }
// Cannot claim child // Cannot claim child
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));
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(considerPlace, tConsiderNext);
builder.addInputArc(unavailablePlaces.at(child->id()), tConsiderNext); builder.addInputArc(unavailablePlaces.at(child->id()), tConsiderNext);
builder.addOutputArc(tConsiderNext, unavailablePlaces.at(child->id())); builder.addOutputArc(tConsiderNext, unavailablePlaces.at(child->id()));
tNextConsiders.push_back(tConsiderNext); tNextConsiders.push_back(tConsiderNext);
// Claimed child // Claimed child
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));
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.addInhibitionArc(unavailablePlaces.at(child->id()), tClaim);
builder.addInputArc(considerPlace, tClaim); builder.addInputArc(considerPlace, tClaim);
builder.addOutputArc(tClaim, claimedPlace); builder.addOutputArc(tClaim, claimedPlace);
builder.addOutputArc(tClaim, unavailablePlaces.at(child->id())); builder.addOutputArc(tClaim, unavailablePlaces.at(child->id()));
// Claim next // Claim next
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));
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(claimedPlace, tClaimNext);
builder.addInputArc(getFailedPlace(child), tClaimNext); builder.addInputArc(getFailedPlace(child), tClaimNext);
builder.addOutputArc(tClaimNext, getFailedPlace(child)); builder.addOutputArc(tClaimNext, getFailedPlace(child));
@ -435,8 +634,12 @@ namespace storm {
// Activate all elements in spare module // Activate all elements in spare module
uint64_t l = 0; uint64_t l = 0;
for (uint64_t k : mDft.module(child->id())) { for (uint64_t k : mDft.module(child->id())) {
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));
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.addInhibitionArc(activePlaces.at(k), tActivate);
builder.addInputArc(claimedPlace, tActivate); builder.addInputArc(claimedPlace, tActivate);
builder.addInputArc(activePlace, tActivate); builder.addInputArc(activePlace, tActivate);
@ -458,7 +661,8 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::translatePDEP(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 xcenter = mDft.getElementLayoutInfo(dftDependency->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y; double ycenter = mDft.getElementLayoutInfo(dftDependency->id()).y;
@ -476,7 +680,8 @@ namespace storm {
uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin"); uint64_t coinPlace = builder.addPlace(defaultCapacity, 1, dftDependency->name() + "_coin");
builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter - 5.0, ycenter + 2.0)); builder.setPlaceLayoutInfo(coinPlace, storm::gspn::LayoutInfo(xcenter - 5.0, ycenter + 2.0));
uint64_t tStartFlip = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_start_flip");
uint64_t tStartFlip = builder.addImmediateTransition(defaultPriority, 0.0,
dftDependency->name() + "_start_flip");
builder.addInputArc(coinPlace, tStartFlip); builder.addInputArc(coinPlace, tStartFlip);
builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip); builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip);
builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent())); builder.addOutputArc(tStartFlip, getFailedPlace(dftDependency->triggerEvent()));
@ -485,11 +690,14 @@ namespace storm {
builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter - 2.0, ycenter + 2.0)); builder.setPlaceLayoutInfo(flipPlace, storm::gspn::LayoutInfo(xcenter - 2.0, ycenter + 2.0));
builder.addOutputArc(tStartFlip, flipPlace); builder.addOutputArc(tStartFlip, flipPlace);
uint64_t tWinFlip = builder.addImmediateTransition(defaultPriority, dftDependency->probability(), "_win_flip");
uint64_t tWinFlip = builder.addImmediateTransition(defaultPriority, dftDependency->probability(),
"_win_flip");
builder.addInputArc(flipPlace, tWinFlip); builder.addInputArc(flipPlace, tWinFlip);
builder.addOutputArc(tWinFlip, forwardPlace); builder.addOutputArc(tWinFlip, forwardPlace);
uint64_t tLooseFlip = builder.addImmediateTransition(defaultPriority, storm::utility::one<ValueType>() - dftDependency->probability(), "_loose_flip");
uint64_t tLooseFlip = builder.addImmediateTransition(defaultPriority,
storm::utility::one<ValueType>() -
dftDependency->probability(), "_loose_flip");
builder.addInputArc(flipPlace, tLooseFlip); builder.addInputArc(flipPlace, tLooseFlip);
} else { } else {
// FDEP // FDEP
@ -497,7 +705,9 @@ namespace storm {
} }
for (auto const &child : dftDependency->dependentEvents()) { for (auto const &child : dftDependency->dependentEvents()) {
uint64_t tForwardFailure = builder.addImmediateTransition(defaultPriority, 0.0, dftDependency->name() + "_propagate_" + child->name());
uint64_t tForwardFailure = builder.addImmediateTransition(defaultPriority, 0.0,
dftDependency->name() + "_propagate_" +
child->name());
builder.addInputArc(forwardPlace, tForwardFailure); builder.addInputArc(forwardPlace, tForwardFailure);
builder.addOutputArc(tForwardFailure, forwardPlace); builder.addOutputArc(tForwardFailure, forwardPlace);
builder.addOutputArc(tForwardFailure, getFailedPlace(child)); builder.addOutputArc(tForwardFailure, getFailedPlace(child));
@ -512,8 +722,10 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
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");
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 xcenter = mDft.getElementLayoutInfo(dftSeq->id()).x;
double ycenter = mDft.getElementLayoutInfo(dftSeq->id()).y; double ycenter = mDft.getElementLayoutInfo(dftSeq->id()).y;
@ -527,14 +739,18 @@ namespace storm {
for (size_t i = 0; i < dftSeq->nrChildren(); ++i) { for (size_t i = 0; i < dftSeq->nrChildren(); ++i) {
auto const &child = dftSeq->children().at(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));
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) { if (i > 0) {
builder.addOutputArc(tEnable, nextPlace); builder.addOutputArc(tEnable, nextPlace);
} }
tEnable = builder.addImmediateTransition(defaultPriority, 0.0, dftSeq->name() + "_unblock_" + child->name());
builder.setTransitionLayoutInfo(tEnable, storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
tEnable = builder.addImmediateTransition(defaultPriority, 0.0,
dftSeq->name() + "_unblock_" + child->name());
builder.setTransitionLayoutInfo(tEnable,
storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
builder.addInputArc(nextPlace, tEnable); builder.addInputArc(nextPlace, tEnable);
builder.addInputArc(disabledPlaces.at(child->id()), tEnable); builder.addInputArc(disabledPlaces.at(child->id()), tEnable);
if (i > 0) { if (i > 0) {
@ -546,9 +762,12 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
uint64_t 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);
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()); assert(failedPlaces.size() == dftElement->id());
failedPlaces.push_back(failedPlace); failedPlaces.push_back(failedPlace);
builder.setPlaceLayoutInfo(failedPlace, layoutInfo); builder.setPlaceLayoutInfo(failedPlace, layoutInfo);
@ -557,9 +776,11 @@ namespace storm {
template<typename ValueType> 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");
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); unavailablePlaces.emplace(dftElement->id(), unavailablePlace);
builder.setPlaceLayoutInfo(unavailablePlace, layoutInfo); builder.setPlaceLayoutInfo(unavailablePlace, layoutInfo);
return unavailablePlace; return unavailablePlace;
@ -567,21 +788,39 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
uint64_t uint64_t
DftToGspnTransformator<ValueType>::addDisabledPlace(std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe, storm::gspn::LayoutInfo const &layoutInfo) {
uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(), dftBe->name() + "_dabled");
DftToGspnTransformator<ValueType>::addDisabledPlace(
std::shared_ptr<const storm::storage::DFTBE<ValueType> > dftBe,
storm::gspn::LayoutInfo const &layoutInfo) {
uint64_t disabledPlace = builder.addPlace(dftBe->nrRestrictions(), dftBe->nrRestrictions(),
dftBe->name() + "_dabled");
disabledPlaces.emplace(dftBe->id(), disabledPlace); disabledPlaces.emplace(dftBe->id(), disabledPlace);
builder.setPlaceLayoutInfo(disabledPlace, layoutInfo); builder.setPlaceLayoutInfo(disabledPlace, layoutInfo);
return disabledPlace; return disabledPlace;
} }
template<typename ValueType> template<typename ValueType>
bool DftToGspnTransformator<ValueType>::isActiveInitially(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
uint64_t
DftToGspnTransformator<ValueType>::addDontcareTransition(
std::shared_ptr<const storm::storage::DFTElement<ValueType> > dftElement,
storm::gspn::LayoutInfo const &layoutInfo) {
uint64_t dontcareTransition = builder.addImmediateTransition(defaultPriority, 0.0,
dftElement->name() + STR_DONTCARE +
"_transition");
dontcareTransitions.emplace(dftElement->id(), dontcareTransition);
builder.setTransitionLayoutInfo(dontcareTransition, layoutInfo);
return dontcareTransition;
}
template<typename ValueType>
bool DftToGspnTransformator<ValueType>::isActiveInitially(
std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// If element is in the top module, return true. // If element is in the top module, return true.
return !mDft.hasRepresentant(dftElement->id()); return !mDft.hasRepresentant(dftElement->id());
} }
template<typename ValueType> template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
uint64_t DftToGspnTransformator<ValueType>::getFailPriority(
std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// Temporariliy use one priority for all // Temporariliy use one priority for all
return defaultPriority; return defaultPriority;
//return mDft.maxRank() - dftElement->rank() + 2; //return mDft.maxRank() - dftElement->rank() + 2;

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

@ -20,7 +20,7 @@ namespace storm {
* *
* @param dft DFT * @param dft DFT
*/ */
DftToGspnTransformator(storm::storage::DFT<ValueType> const& dft);
DftToGspnTransformator(storm::storage::DFT<ValueType> const &dft);
/*! /*!
* Transform the DFT to a GSPN. * Transform the DFT to a GSPN.
@ -30,14 +30,15 @@ namespace storm {
* Smart semantics will only generate necessary parts of the GSPNs. * Smart semantics will only generate necessary parts of the GSPNs.
* @param mergeDCFailed Flag indicating if Don't Care places and Failed places should be merged. * @param mergeDCFailed Flag indicating if Don't Care places and Failed places should be merged.
*/ */
void transform(std::set<uint64_t> const& dontCareElements, bool smart = true, bool mergeDCFailed = true);
void
transform(std::set<uint64_t> const &dontCareElements, bool smart = true, bool mergeDCFailed = true);
/*! /*!
* Extract Gspn by building * Extract Gspn by building
* *
*/ */
gspn::GSPN* obtainGSPN();
gspn::GSPN *obtainGSPN();
/*! /*!
* Get failed place id of top level element. * Get failed place id of top level element.
*/ */
@ -97,7 +98,8 @@ namespace storm {
* @param dftPand The PAND gate. * @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) * @param inclusive Flag wether the PAND is inclusive (children are allowed to fail simultaneously and the PAND will fail nevertheless)
*/ */
void translatePAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive = true);
void
translatePAND(std::shared_ptr<storm::storage::DFTPand<ValueType> const> dftPand, bool inclusive = true);
/*! /*!
* Translate a GSPN POR. * Translate a GSPN POR.
@ -105,7 +107,8 @@ namespace storm {
* @param dftPor The POR gate. * @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) * @param inclusive Flag wether the POR is inclusive (children are allowed to fail simultaneously and the POR will fail nevertheless)
*/ */
void translatePOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive = true);
void
translatePOR(std::shared_ptr<storm::storage::DFTPor<ValueType> const> dftPor, bool inclusive = true);
/*! /*!
* Translate a GSPN SPARE. * Translate a GSPN SPARE.
@ -157,7 +160,8 @@ namespace storm {
* @return Id of added failed place. * @return Id of added failed place.
*/ */
uint64_t uint64_t
addFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const &layoutInfo, bool initialFailed = false);
addFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement,
storm::gspn::LayoutInfo const &layoutInfo, bool initialFailed = false);
/*! /*!
* Add unavailable place for element. * Add unavailable place for element.
@ -168,7 +172,8 @@ namespace storm {
* *
* @return Id of added unavailable place. * @return Id of added unavailable place.
*/ */
uint64_t addUnavailablePlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement, storm::gspn::LayoutInfo const &layoutInfo,
uint64_t addUnavailablePlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement,
storm::gspn::LayoutInfo const &layoutInfo,
bool initialAvailable = true); bool initialAvailable = true);
/*! /*!
@ -179,7 +184,19 @@ namespace storm {
* *
* @return Id of added disabled place. * @return Id of added disabled place.
*/ */
uint64_t addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe, storm::gspn::LayoutInfo const& layoutInfo);
uint64_t addDisabledPlace(std::shared_ptr<storm::storage::DFTBE<ValueType> const> dftBe,
storm::gspn::LayoutInfo const &layoutInfo);
/*!
* Add don't care place for element.
*
* @param dftBe Basic Element.
* @param layoutInfo Information about layout.
*
* @return Id of added don't care place.
*/
uint64_t addDontcareTransition(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement,
storm::gspn::LayoutInfo const &layoutInfo);
/*! /*!
* Get failed place for element. * Get failed place for element.
@ -191,8 +208,8 @@ namespace storm {
uint64_t getFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) { uint64_t getFailedPlace(std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
return failedPlaces.at(dftElement->id()); return failedPlaces.at(dftElement->id());
} }
storm::storage::DFT<ValueType> const& mDft;
storm::storage::DFT<ValueType> const &mDft;
storm::gspn::GspnBuilder builder; storm::gspn::GspnBuilder builder;
// Transformation options // Transformation options
@ -208,14 +225,15 @@ namespace storm {
std::map<uint64_t, uint64_t> unavailablePlaces; std::map<uint64_t, uint64_t> unavailablePlaces;
std::map<uint64_t, uint64_t> activePlaces; std::map<uint64_t, uint64_t> activePlaces;
std::map<uint64_t, uint64_t> disabledPlaces; std::map<uint64_t, uint64_t> disabledPlaces;
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_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity.
static constexpr const char* STR_ACTIVATED = "_active"; // Name standard for place which indicates the activity.
static constexpr const char* STR_DONTCARE = "_dontcare"; // Name standard for place which indicates Don't Care.
std::map<uint64_t, uint64_t> dontcareTransitions;
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_ACTIVATING = "_activating"; // Name standard for transition that point towards a place, which in turn indicates its activity.
static constexpr const char *STR_ACTIVATED = "_active"; // Name standard for place which indicates the activity.
static constexpr const char *STR_DONTCARE = "_dontcare"; // Name standard for place which indicates Don't Care.
}; };
} }
} }

Write Preview
Loading…
Cancel
Save