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

Fixed layout for PDEP GSPN template and added Don't Care support for SPARE elements

main
Alexander Bork 7 years ago
parent
8a6bd4d72f
commit
a2d8faece0
1 changed files with 72 additions and 9 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. 81
      src/storm-dft/transformations/DftToGspnTransformator.cpp

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

@ -145,13 +145,12 @@ namespace storm {
uint64_t dependencyPropagationPlace = builder.addPlace(defaultPriority, 0, uint64_t dependencyPropagationPlace = builder.addPlace(defaultPriority, 0,
dftBE->name() + "_dependency_prop"); dftBE->name() + "_dependency_prop");
dependencyPropagationPlaces.emplace(dftBE->id(), dependencyPropagationPlace); dependencyPropagationPlaces.emplace(dftBE->id(), dependencyPropagationPlace);
builder.setPlaceLayoutInfo(dependencyPropagationPlace, builder.setPlaceLayoutInfo(dependencyPropagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 5.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0, uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
dftBE->name() + "_prop_fail"); dftBE->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
storm::gspn::LayoutInfo(xcenter + 8.0, ycenter));
builder.addInhibitionArc(dependencyPropagationPlace, tPropagationFailed); builder.addInhibitionArc(dependencyPropagationPlace, tPropagationFailed);
builder.addInputArc(failedPlace, tPropagationFailed); builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, failedPlace);
@ -160,7 +159,7 @@ namespace storm {
dftBE->name() + dftBE->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter));
builder.addInhibitionArc(dependencyPropagationPlace, tPropagationDontCare); builder.addInhibitionArc(dependencyPropagationPlace, tPropagationDontCare);
builder.addInputArc(dependencyPropagationPlace, tPropagationDontCare); builder.addInputArc(dependencyPropagationPlace, tPropagationDontCare);
builder.addOutputArc(tPropagationDontCare, dontCarePlace); builder.addOutputArc(tPropagationDontCare, dontCarePlace);
@ -864,6 +863,71 @@ namespace storm {
builder.addOutputArc(tNextConsiders.back(), failedPlace); builder.addOutputArc(tNextConsiders.back(), failedPlace);
builder.addOutputArc(tNextClaims.back(), failedPlace); builder.addOutputArc(tNextClaims.back(), failedPlace);
// Don't Care Mechanism
if (dontCareElements.count(dftSpare->id())) {
if (dftSpare->id() != mDft.getTopLevelIndex()) {
u_int64_t tDontCare = addDontcareTransition(dftSpare,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
dftSpare->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,
dftSpare->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
dftSpare->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,
dftSpare->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 : dftSpare->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 : dftSpare->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(failedPlace, childDontCare);
builder.addOutputArc(childDontCare, failedPlace);
}
}
}
} else {
// If SPARE is TLE, simple failure propagation suffices
for (auto const &child : dftSpare->children()) {
if (dontCareElements.count(child->id())) {
u_int64_t childDontCare = dontcareTransitions.at(child->id());
builder.addInputArc(failedPlace, childDontCare);
builder.addOutputArc(childDontCare, failedPlace);
}
}
}
}
if (!smart || isRepresentative) { if (!smart || isRepresentative) {
builder.addOutputArc(tNextConsiders.back(), unavailablePlace); builder.addOutputArc(tNextConsiders.back(), unavailablePlace);
builder.addOutputArc(tNextClaims.back(), unavailablePlace); builder.addOutputArc(tNextClaims.back(), unavailablePlace);
@ -931,15 +995,14 @@ namespace storm {
} }
} }
// Don't Care TODO LAYOUTING
// Don't Care
if (dontCareElements.count(dftDependency->id())) { if (dontCareElements.count(dftDependency->id())) {
u_int64_t tDontCare = addDontcareTransition(dftDependency, u_int64_t tDontCare = addDontcareTransition(dftDependency,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter));
storm::gspn::LayoutInfo(xcenter + 3.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
u_int64_t dontCarePlace = builder.addPlace(defaultPriority, 0, u_int64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
dftDependency->name() + STR_DONTCARE); dftDependency->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 5.0));
builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 4.0, ycenter));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
// Add the arcs for the dependent events // Add the arcs for the dependent events
@ -958,7 +1021,7 @@ namespace storm {
} else { } else {
if (failedPlace == 0) { if (failedPlace == 0) {
failedPlace = addFailedPlace(dftDependency, failedPlace = addFailedPlace(dftDependency,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
storm::gspn::LayoutInfo(xcenter + 4.0, ycenter));
} }
builder.addInhibitionArc(failedPlace, tDontCare); builder.addInhibitionArc(failedPlace, tDontCare);
builder.addOutputArc(tDontCare, failedPlace); builder.addOutputArc(tDontCare, failedPlace);

Write Preview
Loading…
Cancel
Save