From ec3cb1a134310c2c76d57d1c76fa128f66654921 Mon Sep 17 00:00:00 2001 From: Alexander Bork Date: Sat, 7 Jul 2018 02:40:17 +0200 Subject: [PATCH] Added alternative method to calculate priorities for better compatibility with MC4CSLTA --- src/storm-dft/api/storm-dft.cpp | 5 +- .../settings/modules/DftGspnSettings.cpp | 7 + .../settings/modules/DftGspnSettings.h | 9 +- .../DftToGspnTransformator.cpp | 137 ++++++++++++++---- .../transformations/DftToGspnTransformator.h | 11 +- 5 files changed, 136 insertions(+), 33 deletions(-) diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index d40597684..2021c3e51 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -44,8 +44,9 @@ namespace storm { // Transform to GSPN storm::transformations::dft::DftToGspnTransformator gspnTransformator(dft); - auto priorities = gspnTransformator.computePriorities(); - gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), dftGspnSettings.isMergeDCFailed()); + auto priorities = gspnTransformator.computePriorities(dftGspnSettings.isExtendPriorities()); + gspnTransformator.transform(priorities, dontCareElements, !dftGspnSettings.isDisableSmartTransformation(), + dftGspnSettings.isMergeDCFailed(), dftGspnSettings.isExtendPriorities()); std::shared_ptr gspn(gspnTransformator.obtainGSPN()); return std::make_pair(gspn, gspnTransformator.toplevelFailedPlaceId()); } diff --git a/src/storm-dft/settings/modules/DftGspnSettings.cpp b/src/storm-dft/settings/modules/DftGspnSettings.cpp index 952d127f0..88fc40d94 100644 --- a/src/storm-dft/settings/modules/DftGspnSettings.cpp +++ b/src/storm-dft/settings/modules/DftGspnSettings.cpp @@ -16,12 +16,15 @@ namespace storm { const std::string DftGspnSettings::transformToGspnOptionName = "to-gspn"; const std::string DftGspnSettings::disableSmartTransformationOptionName = "disable-smart"; const std::string DftGspnSettings::mergeDCFailedOptionName = "merge-dc-failed"; + const std::string DftGspnSettings::extendPrioritiesOptionName = "extend-priorities"; DftGspnSettings::DftGspnSettings() : ModuleSettings(moduleName) { this->addOption(storm::settings::OptionBuilder(moduleName, transformToGspnOptionName, false, "Transform DFT to GSPN.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, disableSmartTransformationOptionName, false, "Disable smart transformation.").build()); this->addOption(storm::settings::OptionBuilder(moduleName, mergeDCFailedOptionName, false, "Enable merging of Don't Care and Failed places into a combined place.").build()); + this->addOption(storm::settings::OptionBuilder(moduleName, extendPrioritiesOptionName, false, + "Enable experimental calculation of transition priorities").build()); } bool DftGspnSettings::isTransformToGspn() const { @@ -36,6 +39,10 @@ namespace storm { return this->getOption(mergeDCFailedOptionName).getHasOptionBeenSet(); } + bool DftGspnSettings::isExtendPriorities() const { + return this->getOption(extendPrioritiesOptionName).getHasOptionBeenSet(); + } + void DftGspnSettings::finalize() { } diff --git a/src/storm-dft/settings/modules/DftGspnSettings.h b/src/storm-dft/settings/modules/DftGspnSettings.h index 784438f0d..11531fdbb 100644 --- a/src/storm-dft/settings/modules/DftGspnSettings.h +++ b/src/storm-dft/settings/modules/DftGspnSettings.h @@ -38,6 +38,13 @@ namespace storm { */ bool isMergeDCFailed() const; + /*! + * Retrieves whether the experimental setting of priorities should be used + * + * @return True if the settig is enabled is enabled. + */ + bool isExtendPriorities() const; + bool check() const override; void finalize() override; @@ -50,7 +57,7 @@ namespace storm { static const std::string transformToGspnOptionName; static const std::string disableSmartTransformationOptionName; static const std::string mergeDCFailedOptionName; - + static const std::string extendPrioritiesOptionName; }; } // namespace modules diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 2d07054e9..0a85e9f62 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -19,12 +19,13 @@ namespace storm { template void DftToGspnTransformator::transform(std::map const &priorities, std::set const &dontCareElements, bool smart, - bool mergeDCFailed) { + bool mergeDCFailed, bool extendPriorities) { this->priorities = priorities; this->dontCareElements = dontCareElements; this->smart = smart; this->mergedDCFailed = mergeDCFailed; this->dontCarePriority = 1; + this->extendedPriorities = extendPriorities; builder.setGspnName("DftToGspnTransformation"); // Translate all GSPN elements @@ -35,16 +36,53 @@ namespace storm { } template - std::map DftToGspnTransformator::computePriorities() { + std::map DftToGspnTransformator::computePriorities(bool extendedPrio) { std::map priorities; - // Set priority for PDEP and FDEP according to Monolithic MA semantics - uint64_t dependency_priority = 2; - for (std::size_t i = 0; i < mDft.nrElements(); i++) { - if (mDft.getElement(i)->type() == storm::storage::DFTElementType::PDEP) - priorities[i] = dependency_priority; - else - priorities[i] = (-(mDft.getElement(i)->rank()) + mDft.maxRank()) * 2 + 5; + if (!extendedPrio) { + // Set priority for PDEP and FDEP according to Monolithic MA semantics + uint64_t dependency_priority = 2; + for (std::size_t i = 0; i < mDft.nrElements(); i++) { + if (mDft.getElement(i)->type() == storm::storage::DFTElementType::PDEP) + priorities[i] = dependency_priority; + else + priorities[i] = (-(mDft.getElement(i)->rank()) + mDft.maxRank()) * 2 + 5; + } + } else { + // make sure every element has a unique priority by working with the rank + std::map rankMap; + std::map rankCounter; + // initialize rankMap + for (std::size_t i = 0; i <= mDft.maxRank(); i++) { + rankMap[i] = 0; + rankCounter[i] = 0; + } + // Count the number of elements with each rank + for (std::size_t i = 0; i < mDft.nrElements(); i++) { + ++rankMap[mDft.getElement(i)->rank()]; + ++rankCounter[mDft.getElement(i)->rank()]; + } + + for (std::size_t i = 0; i <= mDft.maxRank(); i++) { + STORM_LOG_DEBUG("With Rank " << i << ": " << rankMap[i]); + } + uint64_t dependency_priority = mDft.nrElements() + 1; + for (std::size_t i = 0; i < mDft.nrElements(); i++) { + if (mDft.getElement(i)->type() == storm::storage::DFTElementType::PDEP) + priorities[i] = dependency_priority; + else { + // Offset saves the number of elements with higher rank than the current element + uint64_t offset = 0; + for (std::size_t j = mDft.maxRank(); j > mDft.getElement(i)->rank(); --j) { + offset += rankMap[j]; + } + // Set priority according to rank such that all elements with the same rank have a unique prio + priorities[i] = + (offset + rankCounter[mDft.getElement(i)->rank()]) * 3 + 3 + mDft.nrElements(); + rankCounter[mDft.getElement(i)->rank()]--; + } + } } + return priorities; } @@ -122,6 +160,11 @@ namespace storm { std::shared_ptr const> dftBE) { double xcenter = mDft.getElementLayoutInfo(dftBE->id()).x; double ycenter = mDft.getElementLayoutInfo(dftBE->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftBE) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t failedPlace = addFailedPlace(dftBE, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter)); @@ -164,7 +207,7 @@ namespace storm { dependencyPropagationPlaces.emplace(dftBE->id(), dependencyPropagationPlace); builder.setPlaceLayoutInfo(dependencyPropagationPlace, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 5.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftBE->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 8.0, ycenter)); @@ -172,7 +215,7 @@ namespace storm { builder.addInputArc(failedPlace, tPropagationFailed); builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, dependencyPropagationPlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftBE->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -242,6 +285,11 @@ namespace storm { std::shared_ptr const> dftAnd) { double xcenter = mDft.getElementLayoutInfo(dftAnd->id()).x; double ycenter = mDft.getElementLayoutInfo(dftAnd->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftAnd) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t failedPlace = addFailedPlace(dftAnd, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); @@ -265,7 +313,7 @@ namespace storm { uint64_t propagationPlace = builder.addPlace(1, 0, dftAnd->name() + "_prop"); builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftAnd->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); @@ -273,7 +321,7 @@ namespace storm { builder.addInputArc(failedPlace, tPropagationFailed); builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, propagationPlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftAnd->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -329,6 +377,11 @@ namespace storm { std::shared_ptr const> dftOr) { double xcenter = mDft.getElementLayoutInfo(dftOr->id()).x; double ycenter = mDft.getElementLayoutInfo(dftOr->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftOr) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t failedPlace = addFailedPlace(dftOr, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); @@ -346,7 +399,7 @@ namespace storm { uint64_t propagationPlace = builder.addPlace(1, 0, dftOr->name() + "_prop"); builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftOr->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); @@ -354,7 +407,7 @@ namespace storm { builder.addInputArc(failedPlace, tPropagationFailed); builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, propagationPlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftOr->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -423,6 +476,11 @@ namespace storm { double xcenter = mDft.getElementLayoutInfo(dftVot->id()).x; double ycenter = mDft.getElementLayoutInfo(dftVot->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftVot) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t failedPlace = addFailedPlace(dftVot, storm::gspn::LayoutInfo(xcenter, ycenter - 3.0)); @@ -469,7 +527,7 @@ namespace storm { uint64_t propagationPlace = builder.addPlace(1, 0, dftVot->name() + "_prop"); builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftVot->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); @@ -477,7 +535,7 @@ namespace storm { builder.addInputArc(failedPlace, tPropagationFailed); builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, propagationPlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftVot->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -523,6 +581,11 @@ namespace storm { //TODO Layouting double xcenter = mDft.getElementLayoutInfo(dftPand->id()).x; double ycenter = mDft.getElementLayoutInfo(dftPand->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftPand) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t failedPlace = addFailedPlace(dftPand, storm::gspn::LayoutInfo(xcenter + 3.0, ycenter - 3.0)); @@ -597,11 +660,11 @@ namespace storm { uint64_t propagationPlace = builder.addPlace(1, 0, dftPand->name() + "_prop"); builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftPand->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); - uint64_t tPropagationFailsafe = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailsafe = builder.addImmediateTransition(propagationPrio, 0.0, dftPand->name() + "_prop_failsafe"); builder.setTransitionLayoutInfo(tPropagationFailsafe, storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0)); @@ -634,7 +697,7 @@ namespace storm { storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addOutputArc(tDontCare, dontCarePlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftPand->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -658,6 +721,11 @@ namespace storm { double xcenter = mDft.getElementLayoutInfo(dftPor->id()).x; double ycenter = mDft.getElementLayoutInfo(dftPor->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftPor) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t delayPlace = 0; @@ -731,11 +799,11 @@ namespace storm { uint64_t propagationPlace = builder.addPlace(1, 0, dftPor->name() + "_prop"); builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftPor->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter + 6.0)); - uint64_t tPropagationFailsafe = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailsafe = builder.addImmediateTransition(propagationPrio, 0.0, dftPor->name() + "_prop_failsafe"); builder.setTransitionLayoutInfo(tPropagationFailsafe, storm::gspn::LayoutInfo(xcenter + 8.0, ycenter + 6.0)); @@ -768,7 +836,7 @@ namespace storm { storm::gspn::LayoutInfo(xcenter + 16.0, ycenter + 4.0)); builder.addInhibitionArc(dontCarePlace, tDontCare); builder.addOutputArc(tDontCare, dontCarePlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftPor->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -792,6 +860,11 @@ namespace storm { std::shared_ptr const> dftSpare) { double xcenter = mDft.getElementLayoutInfo(dftSpare->id()).x; double ycenter = mDft.getElementLayoutInfo(dftSpare->id()).y; + uint64_t propagationPrio = 0; + if (extendedPriorities) + propagationPrio = (getFailPriority(dftSpare) - mDft.nrElements() - 3) / 3 + 3; + else + propagationPrio = dontCarePriority; uint64_t failedPlace = addFailedPlace(dftSpare, storm::gspn::LayoutInfo(xcenter + 10.0, ycenter - 8.0)); @@ -900,7 +973,7 @@ namespace storm { dftSpare->name() + "_prop"); builder.setPlaceLayoutInfo(propagationPlace, storm::gspn::LayoutInfo(xcenter + 12.0, ycenter + 8.0)); - uint64_t tPropagationFailed = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationFailed = builder.addImmediateTransition(propagationPrio, 0.0, dftSpare->name() + "_prop_fail"); builder.setTransitionLayoutInfo(tPropagationFailed, @@ -909,7 +982,7 @@ namespace storm { builder.addInputArc(failedPlace, tPropagationFailed); builder.addOutputArc(tPropagationFailed, failedPlace); builder.addOutputArc(tPropagationFailed, propagationPlace); - uint64_t tPropagationDontCare = builder.addImmediateTransition(dontCarePriority, 0.0, + uint64_t tPropagationDontCare = builder.addImmediateTransition(propagationPrio, 0.0, dftSpare->name() + "_prop_dontCare"); builder.setTransitionLayoutInfo(tPropagationDontCare, @@ -1150,9 +1223,17 @@ namespace storm { DftToGspnTransformator::addDontcareTransition( std::shared_ptr > dftElement, storm::gspn::LayoutInfo const &layoutInfo) { - uint64_t dontcareTransition = builder.addImmediateTransition(dontCarePriority, 0.0, - dftElement->name() + STR_DONTCARE + - "_transition"); + uint64_t dontcareTransition; + if (extendedPriorities && !dftElement->isDependency()) { + uint64_t prio = (getFailPriority(dftElement) - mDft.nrElements() - 3) / 3 + 3; + dontcareTransition = builder.addImmediateTransition(prio, 0.0, + dftElement->name() + STR_DONTCARE + + "_transition"); + } else { + dontcareTransition = builder.addImmediateTransition(dontCarePriority, 0.0, + dftElement->name() + STR_DONTCARE + + "_transition"); + } dontcareTransitions.emplace(dftElement->id(), dontcareTransition); builder.setTransitionLayoutInfo(dontcareTransition, layoutInfo); return dontcareTransition; diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 1d4ff887d..0e60866fc 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -30,14 +30,19 @@ namespace storm { * @param smart Flag indicating if smart semantics should be used. * 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 extendPriorities Flag indicating if the extended priority calculation is used. */ - void transform(std::map const &priorities, std::set const &dontCareElements, bool smart = true, bool mergeDCFailed = true); + void + transform(std::map const &priorities, std::set const &dontCareElements, + bool smart = true, bool mergeDCFailed = true, bool extendPriorities = false); /*! * Compute priorities used for GSPN transformation. + * + * @param extendedPrio Flag indicating if the experimental setting of priorities should be used * @return Priority mapping. */ - std::map computePriorities(); + std::map computePriorities(bool extendedPrio); /*! * Extract Gspn by building @@ -223,6 +228,8 @@ namespace storm { bool smart; // Flag indicating if Don't Care places and Failed places should be merged. bool mergedDCFailed; + //Flag indicating if extended priorities should be used for extended GreatSPN compatibility + bool extendedPriorities; // Set of DFT elements which should have Don't Care propagation. std::set dontCareElements; // Map from DFT elements to their GSPN priorities