diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 8377f2f8e..6cae21e99 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -27,8 +27,8 @@ namespace storm { return tId; } - GSPN::GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions) - : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions) + GSPN::GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions, std::vector const& partitions) + : name(name), places(places), immediateTransitions(itransitions), timedTransitions(ttransitions), partitions(partitions) { } diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h index 17448bc8b..06ee0e788 100644 --- a/src/storm-gspn/storage/gspn/GSPN.h +++ b/src/storm-gspn/storage/gspn/GSPN.h @@ -10,6 +10,7 @@ #include "storm-gspn/storage/gspn/Marking.h" #include "storm-gspn/storage/gspn/Place.h" #include "storm-gspn/storage/gspn/TimedTransition.h" +#include "storm-gspn/storage/gspn/TransitionPartition.h" namespace storm { namespace gspn { @@ -27,7 +28,8 @@ namespace storm { typedef double WeightType; - GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, std::vector> const& ttransitions); + GSPN(std::string const& name, std::vector const& places, std::vector> const& itransitions, + std::vector> const& ttransitions, std::vector const& partitions); /*! * Returns the number of places in this gspn. @@ -176,7 +178,8 @@ namespace storm { // set containing all timed transitions std::vector> timedTransitions; - + std::vector partitions; + }; } } diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index cbea96b6a..d634c00e9 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -29,8 +29,27 @@ namespace storm { auto newId = GSPN::immediateTransitionIdToTransitionId(immediateTransitions.size()); trans.setName(name); trans.setPriority(priority); - trans.setWeight(weight); trans.setID(newId); + + // ensure that the first partition is for the 'general/weighted' transitions + if(partitions.count(priority) == 0) { + TransitionPartition newPart; + newPart.priority = priority; + partitions.at(priority).push_back(newPart); + } + + if(storm::utility::isZero(weight)) { + trans.setWeight(storm::utility::one()); + TransitionPartition newPart; + newPart.priority = priority; + newPart.transitions = {newId}; + partitions.at(priority).push_back(newPart); + } else { + trans.setWeight(weight); + partitions.at(priority).front().transitions.push_back(newId); + + + } immediateTransitions.push_back(trans); return newId; @@ -131,7 +150,20 @@ namespace storm { storm::gspn::GSPN* GspnBuilder::buildGspn() const { - return new GSPN(gspnName, places, immediateTransitions, timedTransitions); + std::vector orderedPartitions; + for(auto const& priorityPartitions : partitions) { + for (auto const& partition : priorityPartitions.second) { + // sanity check + assert(partition.priority == priorityPartitions.first); + + if(partition.nrTransitions() > 0) { + orderedPartitions.push_back(partition); + } + } + + } + + return new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions); } } } diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h index 59f098a82..2f63ba719 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.h +++ b/src/storm-gspn/storage/gspn/GspnBuilder.h @@ -102,6 +102,8 @@ namespace storm { std::string gspnName = "_gspn_"; + std::map> partitions; + // set containing all immediate transitions std::vector> immediateTransitions; diff --git a/src/storm-gspn/storage/gspn/TransitionPartition.h b/src/storm-gspn/storage/gspn/TransitionPartition.h new file mode 100644 index 000000000..128a87641 --- /dev/null +++ b/src/storm-gspn/storage/gspn/TransitionPartition.h @@ -0,0 +1,18 @@ +#pragma once +#include + +namespace storm { + namespace gspn { + + struct TransitionPartition { + std::vector transitions; + uint64_t priority; + + + uint64_t nrTransitions() const { + return transitions.size(); + } + }; + + } +} \ No newline at end of file