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

Changed DFT element transformation so priorities are used

tempestpy_adaptions
Alexander Bork 7 years ago
parent
480b1fb8e5
commit
fa43e515ee
2 changed files with 64 additions and 56 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. 114
      src/storm-dft/transformations/DftToGspnTransformator.cpp
  2. 2
      src/storm-dft/transformations/DftToGspnTransformator.h

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

@ -17,12 +17,14 @@ namespace storm {
} }
template<typename ValueType> template<typename ValueType>
void DftToGspnTransformator<ValueType>::transform(std::map<uint64_t, uint64_t> const &priorities, std::set<uint64_t> const &dontCareElements, bool smart,
void DftToGspnTransformator<ValueType>::transform(std::map<uint64_t, uint64_t> const &priorities,
std::set<uint64_t> const &dontCareElements, bool smart,
bool mergeDCFailed) { bool mergeDCFailed) {
this->priorities = priorities; this->priorities = priorities;
this->dontCareElements = dontCareElements; this->dontCareElements = dontCareElements;
this->smart = smart; this->smart = smart;
this->mergedDCFailed = false;//mergeDCFailed; this->mergedDCFailed = false;//mergeDCFailed;
this->dontCarePriority = 1;
builder.setGspnName("DftToGspnTransformation"); builder.setGspnName("DftToGspnTransformation");
// Translate all GSPN elements // Translate all GSPN elements
@ -37,7 +39,7 @@ namespace storm {
std::map<uint64_t, uint64_t> priorities; std::map<uint64_t, uint64_t> priorities;
for (std::size_t i = 0; i < mDft.nrElements(); i++) { for (std::size_t i = 0; i < mDft.nrElements(); i++) {
// Give all elements the same priority // Give all elements the same priority
priorities[i] = 1;
priorities[i] = 2;
} }
return priorities; return priorities;
} }
@ -45,7 +47,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());
} }
@ -123,7 +126,7 @@ namespace storm {
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(),
uint64_t tActive = builder.addTimedTransition(getFailPriority(dftBE), dftBE->activeFailureRate(),
dftBE->name() + "_activeFailing"); 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);
@ -131,7 +134,7 @@ namespace storm {
builder.addOutputArc(tActive, activePlace); builder.addOutputArc(tActive, activePlace);
builder.addOutputArc(tActive, failedPlace); builder.addOutputArc(tActive, failedPlace);
uint64_t tPassive = builder.addTimedTransition(defaultPriority, dftBE->passiveFailureRate(),
uint64_t tPassive = builder.addTimedTransition(getFailPriority(dftBE), dftBE->passiveFailureRate(),
dftBE->name() + "_passiveFailing"); 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);
@ -142,7 +145,7 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftBE, u_int64_t tDontCare = addDontcareTransition(dftBE,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0, dftBE->name() + STR_DONTCARE);
uint64_t dontCarePlace = builder.addPlace(1, 0, dftBE->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
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);
@ -153,12 +156,12 @@ namespace storm {
//Propagation for dependencies //Propagation for dependencies
if (!smart || dftBE->hasIngoingDependencies()) { if (!smart || dftBE->hasIngoingDependencies()) {
uint64_t dependencyPropagationPlace = builder.addPlace(defaultPriority, 0,
uint64_t dependencyPropagationPlace = builder.addPlace(1, 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 + 10.0, ycenter - 5.0)); storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 5.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftBE->name() + "_prop_fail"); dftBE->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 8.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 8.0, ycenter));
@ -166,7 +169,7 @@ namespace storm {
builder.addInputArc(failedPlace, tPropagationFailed); builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, dependencyPropagationPlace); builder.addOutputArc(tPropagationFailed, dependencyPropagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftBE->name() + dftBE->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -250,17 +253,16 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftAnd, u_int64_t tDontCare = addDontcareTransition(dftAnd,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
dftAnd->name() + STR_DONTCARE);
uint64_t dontCarePlace = builder.addPlace(1, 0, dftAnd->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
//Propagation //Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftAnd->name() + "_prop");
uint64_t propagationPlace = builder.addPlace(1, 0, dftAnd->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace, builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftAnd->name() + "_prop_fail"); dftAnd->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
@ -268,7 +270,7 @@ namespace storm {
builder.addInputArc(failedPlace, tPropagationFailed); builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, propagationPlace); builder.addOutputArc(tPropagationFailed, propagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftAnd->name() + dftAnd->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -332,16 +334,16 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftOr, u_int64_t tDontCare = addDontcareTransition(dftOr,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0, dftOr->name() + STR_DONTCARE);
uint64_t dontCarePlace = builder.addPlace(1, 0, dftOr->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
//Propagation //Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftOr->name() + "_prop");
uint64_t propagationPlace = builder.addPlace(1, 0, dftOr->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace, builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftOr->name() + "_prop_fail"); dftOr->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
@ -349,7 +351,7 @@ namespace storm {
builder.addInputArc(failedPlace, tPropagationFailed); builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, propagationPlace); builder.addOutputArc(tPropagationFailed, propagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftOr->name() + dftOr->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -455,17 +457,16 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftVot, u_int64_t tDontCare = addDontcareTransition(dftVot,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
dftVot->name() + STR_DONTCARE);
uint64_t dontCarePlace = builder.addPlace(1, 0, dftVot->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
//Propagation //Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftVot->name() + "_prop");
uint64_t propagationPlace = builder.addPlace(1, 0, dftVot->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace, builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftVot->name() + "_prop_fail"); dftVot->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
@ -473,7 +474,7 @@ namespace storm {
builder.addInputArc(failedPlace, tPropagationFailed); builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, propagationPlace); builder.addOutputArc(tPropagationFailed, propagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftVot->name() + dftVot->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -522,7 +523,9 @@ namespace storm {
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,
// Set priority lower if the PAND is exclusive
uint64_t tFailed = builder.addImmediateTransition(
inclusive ? getFailPriority(dftPand) : getFailPriority(dftPand) - 1, 0.0,
dftPand->name() + STR_FAILING); 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);
@ -566,8 +569,8 @@ namespace storm {
dftPand->name() + "_delay_" + previousChild->name()); dftPand->name() + "_delay_" + previousChild->name());
builder.setPlaceLayoutInfo(delayPlace, storm::gspn::LayoutInfo(xcenter - 5.0 + (i - 1) * 3.0, builder.setPlaceLayoutInfo(delayPlace, storm::gspn::LayoutInfo(xcenter - 5.0 + (i - 1) * 3.0,
ycenter + 5.0)); ycenter + 5.0));
//TODO check if priority is set correctly
uint64_t tDelay = builder.addImmediateTransition(getFailPriority(dftPand) + 1, 0.0,
// Priority of delayTransitions needs to be lower than for failsafeTransitions
uint64_t tDelay = builder.addImmediateTransition(getFailPriority(dftPand) - 1, 0.0,
child->name() + "_" + dftPand->name() + child->name() + "_" + dftPand->name() +
"_delayTransition"); "_delayTransition");
builder.setTransitionLayoutInfo(tDelay, builder.setTransitionLayoutInfo(tDelay,
@ -588,14 +591,14 @@ namespace storm {
// Dont Care // Dont Care
if (dontCareElements.count(dftPand->id())) { if (dontCareElements.count(dftPand->id())) {
//Propagation //Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftPand->name() + "_prop");
uint64_t propagationPlace = builder.addPlace(1, 0, dftPand->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace, builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftPand->name() + "_prop_fail"); dftPand->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
uint64_t tPropagationFailsafe = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailsafe = builder.addImmediateTransition(dontCarePriority, 0.0,
dftPand->name() + "_prop_failsafe"); dftPand->name() + "_prop_failsafe");
builder.setTransitionLayoutInfo(tPropagationFailsafe, builder.setTransitionLayoutInfo(tPropagationFailsafe,
storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0));
@ -622,13 +625,13 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftPand, u_int64_t tDontCare = addDontcareTransition(dftPand,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
uint64_t dontCarePlace = builder.addPlace(1, 0,
dftPand->name() + STR_DONTCARE); dftPand->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftPand->name() + dftPand->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -657,7 +660,9 @@ namespace storm {
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,
// Set priority lower if the POR is exclusive
uint64_t tFailed = builder.addImmediateTransition(
inclusive ? getFailPriority(dftPor) : getFailPriority(dftPor) - 1, 0.0,
dftPor->name() + STR_FAILING); 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);
@ -683,8 +688,9 @@ namespace storm {
delayPlace = builder.addPlace(1, 0, dftPor->name() + "_delay"); delayPlace = builder.addPlace(1, 0, dftPor->name() + "_delay");
builder.setPlaceLayoutInfo(delayPlace, storm::gspn::LayoutInfo(xcenter - 5.0, builder.setPlaceLayoutInfo(delayPlace, storm::gspn::LayoutInfo(xcenter - 5.0,
ycenter + 5.0)); ycenter + 5.0));
//TODO check if priority is set correctly
uint64_t tDelay = builder.addImmediateTransition(getFailPriority(dftPor) + 1, 0.0, dftPor->name() +
// priority of delayTransition has to be lower than other priorities
uint64_t tDelay = builder.addImmediateTransition(getFailPriority(dftPor) - 1, 0.0, dftPor->name() +
"_delayTransition"); "_delayTransition");
builder.setTransitionLayoutInfo(tDelay, builder.setTransitionLayoutInfo(tDelay,
storm::gspn::LayoutInfo(xcenter - 5.0, storm::gspn::LayoutInfo(xcenter - 5.0,
@ -719,14 +725,14 @@ namespace storm {
// Dont Care // Dont Care
if (dontCareElements.count(dftPor->id())) { if (dontCareElements.count(dftPor->id())) {
//Propagation //Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0, dftPor->name() + "_prop");
uint64_t propagationPlace = builder.addPlace(1, 0, dftPor->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace, builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftPor->name() + "_prop_fail"); dftPor->name() + "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0));
uint64_t tPropagationFailsafe = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailsafe = builder.addImmediateTransition(dontCarePriority, 0.0,
dftPor->name() + "_prop_failsafe"); dftPor->name() + "_prop_failsafe");
builder.setTransitionLayoutInfo(tPropagationFailsafe, builder.setTransitionLayoutInfo(tPropagationFailsafe,
storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0)); storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0));
@ -753,13 +759,13 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftPor, u_int64_t tDontCare = addDontcareTransition(dftPor,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
uint64_t dontCarePlace = builder.addPlace(1, 0,
dftPor->name() + STR_DONTCARE); dftPor->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftPor->name() + dftPor->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -854,7 +860,7 @@ 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,
uint64_t tActivate = builder.addImmediateTransition(getFailPriority(dftSpare), 0.0,
dftSpare->name() + "_activate_" + dftSpare->name() + "_activate_" +
std::to_string(i) + "_" + std::to_string(i) + "_" +
std::to_string(k)); std::to_string(k));
@ -880,18 +886,18 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftSpare, u_int64_t tDontCare = addDontcareTransition(dftSpare,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter));
if (!mergedDCFailed) { if (!mergedDCFailed) {
uint64_t dontCarePlace = builder.addPlace(defaultPriority, 0,
uint64_t dontCarePlace = builder.addPlace(1, 0,
dftSpare->name() + STR_DONTCARE); dftSpare->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, builder.setPlaceLayoutInfo(dontCarePlace,
storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
builder.addOutputArc(tDontCare, dontCarePlace); builder.addOutputArc(tDontCare, dontCarePlace);
//Propagation //Propagation
uint64_t propagationPlace = builder.addPlace(defaultPriority, 0,
uint64_t propagationPlace = builder.addPlace(1, 0,
dftSpare->name() + "_prop"); dftSpare->name() + "_prop");
builder.setPlaceLayoutInfo(propagationPlace, builder.setPlaceLayoutInfo(propagationPlace,
storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0));
uint64_t tPropagationFailed = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0,
dftSpare->name() + dftSpare->name() +
"_prop_fail"); "_prop_fail");
builder.setTransitionLayoutInfo(tPropagationFailed, builder.setTransitionLayoutInfo(tPropagationFailed,
@ -900,7 +906,7 @@ namespace storm {
builder.addInputArc(failedPlace, tPropagationFailed); builder.addInputArc(failedPlace, tPropagationFailed);
builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, failedPlace);
builder.addOutputArc(tPropagationFailed, propagationPlace); builder.addOutputArc(tPropagationFailed, propagationPlace);
uint64_t tPropagationDontCare = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0,
dftSpare->name() + dftSpare->name() +
"_prop_dontCare"); "_prop_dontCare");
builder.setTransitionLayoutInfo(tPropagationDontCare, builder.setTransitionLayoutInfo(tPropagationDontCare,
@ -966,7 +972,7 @@ 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,
uint64_t tStartFlip = builder.addImmediateTransition(getFailPriority(dftDependency), 0.0,
dftDependency->name() + "_start_flip"); dftDependency->name() + "_start_flip");
builder.addInputArc(coinPlace, tStartFlip); builder.addInputArc(coinPlace, tStartFlip);
builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip); builder.addInputArc(getFailedPlace(dftDependency->triggerEvent()), tStartFlip);
@ -976,12 +982,13 @@ 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(),
uint64_t tWinFlip = builder.addImmediateTransition(getFailPriority(dftDependency) + 1,
dftDependency->probability(),
"_win_flip"); "_win_flip");
builder.addInputArc(flipPlace, tWinFlip); builder.addInputArc(flipPlace, tWinFlip);
builder.addOutputArc(tWinFlip, forwardPlace); builder.addOutputArc(tWinFlip, forwardPlace);
uint64_t tLooseFlip = builder.addImmediateTransition(defaultPriority,
uint64_t tLooseFlip = builder.addImmediateTransition(getFailPriority(dftDependency) + 1,
storm::utility::one<ValueType>() - storm::utility::one<ValueType>() -
dftDependency->probability(), "_loose_flip"); dftDependency->probability(), "_loose_flip");
builder.addInputArc(flipPlace, tLooseFlip); builder.addInputArc(flipPlace, tLooseFlip);
@ -991,7 +998,7 @@ namespace storm {
} }
for (auto const &child : dftDependency->dependentEvents()) { for (auto const &child : dftDependency->dependentEvents()) {
uint64_t tForwardFailure = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t tForwardFailure = builder.addImmediateTransition(getFailPriority(dftDependency), 0.0,
dftDependency->name() + "_propagate_" + dftDependency->name() + "_propagate_" +
child->name()); child->name());
builder.addInputArc(forwardPlace, tForwardFailure); builder.addInputArc(forwardPlace, tForwardFailure);
@ -1011,7 +1018,7 @@ namespace storm {
u_int64_t tDontCare = addDontcareTransition(dftDependency, u_int64_t tDontCare = addDontcareTransition(dftDependency,
storm::gspn::LayoutInfo(xcenter + 3.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(1, 0,
dftDependency->name() + STR_DONTCARE); dftDependency->name() + STR_DONTCARE);
builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 4.0, ycenter)); builder.setPlaceLayoutInfo(dontCarePlace, storm::gspn::LayoutInfo(xcenter + 4.0, ycenter));
builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addInhibitionArc(dontCarePlace, tDontCare);
@ -1080,7 +1087,7 @@ namespace storm {
if (i > 0) { if (i > 0) {
builder.addOutputArc(tEnable, nextPlace); builder.addOutputArc(tEnable, nextPlace);
} }
tEnable = builder.addImmediateTransition(defaultPriority, 0.0,
tEnable = builder.addImmediateTransition(getFailPriority(dftSeq), 0.0,
dftSeq->name() + "_unblock_" + child->name()); dftSeq->name() + "_unblock_" + child->name());
builder.setTransitionLayoutInfo(tEnable, builder.setTransitionLayoutInfo(tEnable,
storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0)); storm::gspn::LayoutInfo(xcenter - 5.0 + i * 3.0, ycenter + 3.0));
@ -1136,7 +1143,7 @@ namespace storm {
DftToGspnTransformator<ValueType>::addDontcareTransition( DftToGspnTransformator<ValueType>::addDontcareTransition(
std::shared_ptr<const storm::storage::DFTElement<ValueType> > dftElement, std::shared_ptr<const storm::storage::DFTElement<ValueType> > dftElement,
storm::gspn::LayoutInfo const &layoutInfo) { storm::gspn::LayoutInfo const &layoutInfo) {
uint64_t dontcareTransition = builder.addImmediateTransition(defaultPriority, 0.0,
uint64_t dontcareTransition = builder.addImmediateTransition(dontCarePriority, 0.0,
dftElement->name() + STR_DONTCARE + dftElement->name() + STR_DONTCARE +
"_transition"); "_transition");
dontcareTransitions.emplace(dftElement->id(), dontcareTransition); dontcareTransitions.emplace(dftElement->id(), dontcareTransition);
@ -1154,9 +1161,8 @@ namespace storm {
template<typename ValueType> template<typename ValueType>
uint64_t DftToGspnTransformator<ValueType>::getFailPriority( uint64_t DftToGspnTransformator<ValueType>::getFailPriority(
std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) { std::shared_ptr<storm::storage::DFTElement<ValueType> const> dftElement) {
// Temporariliy use one priority for all
return defaultPriority;
//return mDft.maxRank() - dftElement->rank() + 2;
// Return the value given in the field
return priorities.at(dftElement->id());
} }

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

@ -227,6 +227,8 @@ namespace storm {
std::set<uint64_t> dontCareElements; std::set<uint64_t> dontCareElements;
// Map from DFT elements to their GSPN priorities // Map from DFT elements to their GSPN priorities
std::map<uint64_t, uint64_t> priorities; std::map<uint64_t, uint64_t> priorities;
// Priority for Don't Care Transitions
uint64_t dontCarePriority;
// Interface places for DFT elements // Interface places for DFT elements
std::vector<uint64_t> failedPlaces; std::vector<uint64_t> failedPlaces;

Write Preview
Loading…
Cancel
Save