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

Added dependency don't care support

tempestpy_adaptions
Alexander Bork 7 years ago
parent
57ad89adea
commit
8a6bd4d72f
1 changed files with 82 additions and 2 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. 84
      src/storm-dft/transformations/DftToGspnTransformator.cpp

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

@ -136,10 +136,41 @@ namespace storm {
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 5.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 5.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
builder.addInhibitionArc(dontCarePlace, tActive);
builder.addInhibitionArc(dontCarePlace, tPassive);
//Propagation for dependencies
if (!smart || dftBE->hasIngoingDependencies()) {
uint64_t dependencyPropagationPlace = builder.addPlace(defaultPriority, 0,
dftBE->name() + "_dependency_prop");
dependencyPropagationPlaces.emplace(dftBE->id(), dependencyPropagationPlace);
builder.setPlaceLayoutInfo(dependencyPropagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
dftBE->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
builder.addInhibitionArc(dependencyPropagationPlace, tPropagationFailed);
builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, dependencyPropagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
dftBE->name() +
"_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare,
storm::gspn::LayoutInfo(xcenter + 14.0, ycenter + 6.0));
builder.addInhibitionArc(dependencyPropagationPlace, tPropagationDontCare);
builder.addInputArc(dependencyPropagationPlace, tPropagationDontCare);
builder.addOutputArc(tPropagationDontCare, dontCarePlace);
builder.addOutputArc(tPropagationDontCare, dependencyPropagationPlace);
}
} else { } else {
builder.addInhibitionArc(failedPlace, tDontCare); builder.addInhibitionArc(failedPlace, tDontCare);
builder.addOutputArc(tDontCare, failedPlace); builder.addOutputArc(tDontCare, failedPlace);
} }
} }
if (!smart || dftBE->nrRestrictions() > 0) { if (!smart || dftBE->nrRestrictions() > 0) {
@ -154,6 +185,7 @@ namespace storm {
builder.addOutputArc(tActive, unavailablePlace); builder.addOutputArc(tActive, unavailablePlace);
builder.addOutputArc(tPassive, unavailablePlace); builder.addOutputArc(tPassive, unavailablePlace);
} }
} }
template<typename ValueType> template<typename ValueType>
@ -203,7 +235,6 @@ namespace storm {
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 (dontCareElements.count(dftAnd->id())) {
if (dftAnd->id() != mDft.getTopLevelIndex()) { if (dftAnd->id() != mDft.getTopLevelIndex()) {
u_int64_t tDontCare = addDontcareTransition(dftAnd, u_int64_t tDontCare = addDontcareTransition(dftAnd,
@ -845,8 +876,9 @@ namespace storm {
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;
uint64_t failedPlace = 0;
if (!smart) { if (!smart) {
addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
failedPlace = addFailedPlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0)); addUnavailablePlace(dftDependency, storm::gspn::LayoutInfo(xcenter + 16.0, ycenter - 8.0));
} }
@ -898,6 +930,54 @@ namespace storm {
builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id())); builder.addOutputArc(tForwardFailure, unavailablePlaces.at(child->id()));
} }
} }
// Don't Care TODO LAYOUTING
if (dontCareElements.count(dftDependency->id())) {
u_int64_t tDontCare = addDontcareTransition(dftDependency,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter));
if (!mergedDCFailed) {
u_int64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
dftDependency->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 5.0));
builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace);
// Add the arcs for the dependent events
for (auto const &dependentEvent : dftDependency->dependentEvents()) {
if (dontCareElements.count(dependentEvent->id())) {
u_int64_t dependentEventPropagation = dependencyPropagationPlaces.at(
dependentEvent->id());
builder.addInputArc(dependentEventPropagation, tDontCare);
builder.addOutputArc(tDontCare, dependentEventPropagation);
}
}
// Add the arcs for the trigger
uint64_t triggerDontCare = dontcareTransitions.at(dftDependency->triggerEvent()->id());
builder.addInputArc(dontCarePlace, triggerDontCare);
builder.addOutputArc(triggerDontCare, dontCarePlace);
} else {
if (failedPlace == 0) {
failedPlace = addFailedPlace(dftDependency,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0));
}
builder.addInhibitionArc(failedPlace, tDontCare);
builder.addOutputArc(tDontCare, failedPlace);
// Add the arcs for the dependent events
for (auto const &dependentEvent : dftDependency->dependentEvents()) {
if (dontCareElements.count(dependentEvent->id())) {
u_int64_t dependentEventFailed = failedPlaces.at(dependentEvent->id());
builder.addInputArc(dependentEventFailed, tDontCare);
builder.addOutputArc(tDontCare, dependentEventFailed);
}
}
// Add the arcs for the trigger
uint64_t triggerDontCare = dontcareTransitions.at(dftDependency->triggerEvent()->id());
builder.addInputArc(failedPlace, triggerDontCare);
builder.addOutputArc(triggerDontCare, failedPlace);
}
}
} }
template<typename ValueType> template<typename ValueType>

Write Preview
Loading…
Cancel
Save