diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.h b/src/storm-gspn/builder/JaniGSPNBuilder.h index 4fcb19f16..76517a3a1 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.h +++ b/src/storm-gspn/builder/JaniGSPNBuilder.h @@ -81,53 +81,74 @@ namespace storm { } if(!ignoreWeights) { - + uint64_t lastPriority; + storm::expressions::Expression lastPriorityGuard = expressionManager->boolean(false); + storm::expressions::Expression priorityGuard = expressionManager->boolean(true); // TODO here there is something to fix if we add transition partitions. - storm::expressions::Expression guard = expressionManager->boolean(false); - std::vector weightedDestinations; - // Compute enabled weight expression. - storm::expressions::Expression totalWeight = expressionManager->rational(0.0); - for (auto const& trans : gspn.getImmediateTransitions()) { - if (trans.noWeightAttached()) { - continue; - } - storm::expressions::Expression destguard = expressionManager->boolean(true); - for (auto const& inPlaceEntry : trans.getInputPlaces()) { - destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); - } - for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { - destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); - } - totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); + for (auto const& partition : gspn.getPartitions()) { + storm::expressions::Expression guard = expressionManager->boolean(false); + std::vector weightedDestinations; - } - totalWeight = totalWeight.simplify(); - - for (auto const& trans : gspn.getImmediateTransitions()) { - if (trans.noWeightAttached()) { - continue; - } - storm::expressions::Expression destguard = expressionManager->boolean(true); - std::vector assignments; - for (auto const& inPlaceEntry : trans.getInputPlaces()) { - destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); - assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) ); + + assert(lastPriority <= partition.priority); + if (lastPriority < partition.priority) { + priorityGuard = priorityGuard && !lastPriorityGuard; + lastPriority = partition.priority; + } else { + assert(lastPriority == partition.priority); } - for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { - destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); + + // Compute enabled weight expression. + storm::expressions::Expression totalWeight = expressionManager->rational(0.0); + for (auto const& transId : partition.transitions) { + auto const& trans = gspn.getImmediateTransitions()[transId]; + if (trans.noWeightAttached()) { + continue; + } + storm::expressions::Expression destguard = expressionManager->boolean(true); + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); + } + for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { + destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); + } + totalWeight = totalWeight + storm::expressions::ite(destguard, expressionManager->rational(trans.getWeight()), expressionManager->rational(0.0)); + } - for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { - assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) ); + totalWeight = totalWeight.simplify(); + + + for (auto const& transId : partition.transitions) { + auto const& trans = gspn.getImmediateTransitions()[transId]; + if (trans.noWeightAttached()) { + continue; + } + storm::expressions::Expression destguard = expressionManager->boolean(true); + std::vector assignments; + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + destguard = destguard && (vars[inPlaceEntry.first]->getExpressionVariable() > inPlaceEntry.second); + assignments.emplace_back( *vars[inPlaceEntry.first], (vars[inPlaceEntry.first]->getExpressionVariable() - inPlaceEntry.second) ); + } + for (auto const& inhibPlaceEntry : trans.getInhibitionPlaces()) { + destguard = destguard && (vars[inhibPlaceEntry.first]->getExpressionVariable() > inhibPlaceEntry.second); + } + for (auto const& outputPlaceEntry : trans.getOutputPlaces()) { + assignments.emplace_back( *vars[outputPlaceEntry.first], (vars[outputPlaceEntry.first]->getExpressionVariable() + outputPlaceEntry.second) ); + } + destguard = destguard.simplify(); + guard = guard || destguard; + storm::jani::OrderedAssignments oa(assignments); + storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa); + weightedDestinations.push_back(dest); } - destguard = destguard.simplify(); - guard = guard || destguard; - storm::jani::OrderedAssignments oa(assignments); - storm::jani::EdgeDestination dest(locId, storm::expressions::ite(destguard, (expressionManager->rational(trans.getWeight()) / totalWeight), expressionManager->rational(0.0)), oa); - weightedDestinations.push_back(dest); + storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, (priorityGuard && guard).simplify(), weightedDestinations); + automaton.addEdge(e); + lastPriorityGuard = lastPriorityGuard || guard; } - storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, boost::none, guard.simplify(), weightedDestinations); - automaton.addEdge(e); + + + } for (auto const& trans : gspn.getTimedTransitions()) { storm::expressions::Expression guard = expressionManager->boolean(true); diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index 6cae21e99..5a7f819de 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -57,6 +57,10 @@ namespace storm { return m; } + std::vector const& GSPN::getPartitions() const { + return partitions; + } + storm::gspn::Place const* GSPN::getPlace(uint64_t id) const { if(id < places.size()) { diff --git a/src/storm-gspn/storage/gspn/GSPN.h b/src/storm-gspn/storage/gspn/GSPN.h index 06ee0e788..7086a6c1c 100644 --- a/src/storm-gspn/storage/gspn/GSPN.h +++ b/src/storm-gspn/storage/gspn/GSPN.h @@ -38,6 +38,11 @@ namespace storm { */ uint64_t getNumberOfPlaces() const; + /*! + * + */ + std::vector const& getPartitions() const; + /*! * Returns the vector of timed transitions in this gspn. * @@ -65,7 +70,6 @@ namespace storm { */ std::shared_ptr getInitialMarking(std::map& numberOfBits, uint64_t const& numberOfTotalBits) const; - /*! * Returns the place with the corresponding id. * @@ -86,6 +90,7 @@ namespace storm { * Returns the timed transition with the corresponding name. * * @param name The ID of the timed transition. + * @return A pointer to the transition, and nullptr otherwise */ storm::gspn::TimedTransition const* getTimedTransition(std::string const& name) const; diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index d634c00e9..9cb662eb7 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -162,6 +162,7 @@ namespace storm { } } + std::reverse(orderedPartitions.begin(), orderedPartitions.end()); return new GSPN(gspnName, places, immediateTransitions, timedTransitions, orderedPartitions); }