diff --git a/src/storm-dft/api/storm-dft.cpp b/src/storm-dft/api/storm-dft.cpp index 1e17b0c5d..f6b12a965 100644 --- a/src/storm-dft/api/storm-dft.cpp +++ b/src/storm-dft/api/storm-dft.cpp @@ -45,7 +45,8 @@ namespace storm { // Transform to GSPN storm::transformations::dft::DftToGspnTransformator<double> gspnTransformator(dft); - gspnTransformator.transform(dontCareElements, smart, mergeDCFailed); + auto priorities = gspnTransformator.computePriorities(); + gspnTransformator.transform(priorities, dontCareElements, smart, mergeDCFailed); storm::gspn::GSPN* gspn = gspnTransformator.obtainGSPN(); uint64_t toplevelFailedPlace = gspnTransformator.toplevelFailedPlaceId(); diff --git a/src/storm-dft/transformations/DftToGspnTransformator.cpp b/src/storm-dft/transformations/DftToGspnTransformator.cpp index 933ed02a7..576c261d4 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.cpp +++ b/src/storm-dft/transformations/DftToGspnTransformator.cpp @@ -17,8 +17,9 @@ namespace storm { } template<typename ValueType> - void DftToGspnTransformator<ValueType>::transform(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) { + this->priorities = priorities; this->dontCareElements = dontCareElements; this->smart = smart; this->mergedDCFailed = false;//mergeDCFailed; @@ -31,10 +32,20 @@ namespace storm { // TODO } + template<typename ValueType> + std::map<uint64_t, uint64_t> DftToGspnTransformator<ValueType>::computePriorities() { + std::map<uint64_t, uint64_t> priorities; + for (std::size_t i = 0; i < mDft.nrElements(); i++) { + // Give all elements the same priority + priorities[i] = 1; + } + return priorities; + } + + template<typename ValueType> 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()); } diff --git a/src/storm-dft/transformations/DftToGspnTransformator.h b/src/storm-dft/transformations/DftToGspnTransformator.h index 0c2d9ce55..08427d708 100644 --- a/src/storm-dft/transformations/DftToGspnTransformator.h +++ b/src/storm-dft/transformations/DftToGspnTransformator.h @@ -25,13 +25,19 @@ namespace storm { /*! * Transform the DFT to a GSPN. * + * @param priorities GSPN transition priorities to use for each DFT element. * @param dontCareElements Set of DFT elements which should have Don't Care propagation. * @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. */ - void - transform(std::set<uint64_t> const &dontCareElements, bool smart = true, bool mergeDCFailed = true); + void transform(std::map<uint64_t, uint64_t> const &priorities, std::set<uint64_t> const &dontCareElements, bool smart = true, bool mergeDCFailed = true); + + /*! + * Compute priorities used for GSPN transformation. + * @return Priority mapping. + */ + std::map<uint64_t, uint64_t> computePriorities(); /*! * Extract Gspn by building @@ -219,6 +225,8 @@ namespace storm { bool mergedDCFailed; // Set of DFT elements which should have Don't Care propagation. std::set<uint64_t> dontCareElements; + // Map from DFT elements to their GSPN priorities + std::map<uint64_t, uint64_t> priorities; // Interface places for DFT elements std::vector<uint64_t> failedPlaces;