From 3215af6fc00dc0f20e7e561526dc1f61d6ee950d Mon Sep 17 00:00:00 2001 From: TimQu Date: Tue, 21 Aug 2018 10:39:11 +0200 Subject: [PATCH] Implemented single- infinite- and k- server semantics for timed gspn transitions --- src/storm-gspn/builder/JaniGSPNBuilder.cpp | 26 +++++++++- .../parser/GreatSpnEditorProjectParser.cpp | 13 ++++- src/storm-gspn/storage/gspn/GSPN.cpp | 2 + src/storm-gspn/storage/gspn/GspnBuilder.cpp | 11 ++++- src/storm-gspn/storage/gspn/GspnBuilder.h | 11 ++++- .../storage/gspn/GspnJsonExporter.cpp | 11 ++++- src/storm-gspn/storage/gspn/TimedTransition.h | 47 ++++++++++++++++++- 7 files changed, 114 insertions(+), 7 deletions(-) diff --git a/src/storm-gspn/builder/JaniGSPNBuilder.cpp b/src/storm-gspn/builder/JaniGSPNBuilder.cpp index aa8c64a4f..d21ef5c21 100644 --- a/src/storm-gspn/builder/JaniGSPNBuilder.cpp +++ b/src/storm-gspn/builder/JaniGSPNBuilder.cpp @@ -3,6 +3,8 @@ #include #include "storm/logic/Formulas.h" + +#include "storm/exceptions/InvalidModelException.h" namespace storm { namespace builder { @@ -132,7 +134,7 @@ namespace storm { } for (auto const& trans : gspn.getTimedTransitions()) { storm::expressions::Expression guard = expressionManager->boolean(true); - + std::vector assignments; for (auto const& inPlaceEntry : trans.getInputPlaces()) { guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second); @@ -153,9 +155,29 @@ namespace storm { std::shared_ptr templateEdge = std::make_shared(guard); automaton.registerTemplateEdge(templateEdge); + + storm::expressions::Expression rate = expressionManager->rational(trans.getRate()); + if (trans.hasInfiniteServerSemantics() || (trans.hasKServerSemantics() && !trans.hasSingleServerSemantics())) { + STORM_LOG_THROW(trans.hasKServerSemantics() || !trans.getInputPlaces().empty(), storm::exceptions::InvalidModelException, "Unclear semantics: Found a transition with infinite-server semantics and without input place."); + storm::expressions::Expression enablingDegree; + bool firstArgumentOfMinExpression = true; + if (trans.hasKServerSemantics()) { + enablingDegree = expressionManager->integer(trans.getNumberOfServers()); + firstArgumentOfMinExpression = false; + } + for (auto const& inPlaceEntry : trans.getInputPlaces()) { + storm::expressions::Expression enablingDegreeInPlace = vars[inPlaceEntry.first]->getExpressionVariable() / expressionManager->integer(inPlaceEntry.second); // Integer division! + if (firstArgumentOfMinExpression == true) { + enablingDegree = enablingDegreeInPlace; + } else { + enablingDegree = storm::expressions::minimum(enablingDegree, enablingDegreeInPlace); + } + } + rate = rate * enablingDegree; + } templateEdge->addDestination(assignments); - storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, expressionManager->rational(trans.getRate()), templateEdge, {locId}, {expressionManager->integer(1)}); + storm::jani::Edge e(locId, storm::jani::Model::SILENT_ACTION_INDEX, rate, templateEdge, {locId}, {expressionManager->integer(1)}); automaton.addEdge(e); } diff --git a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp index f4b4418a2..17d49e6f1 100644 --- a/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp +++ b/src/storm-gspn/parser/GreatSpnEditorProjectParser.cpp @@ -297,6 +297,7 @@ namespace storm { std::string transitionName; bool immediateTransition; double rate = 1.0; // The default rate in GreatSPN. + boost::optional numServers; // traverse attributes for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) { @@ -314,6 +315,16 @@ namespace storm { } else if(name.compare("delay") == 0) { expressionParser.setAcceptDoubleLiterals(true); rate = expressionParser.parseFromString(storm::adapters::XMLtoString(attr->getNodeValue())).evaluateAsDouble(); + } else if (name.compare("nservers") == 0) { + std::string nservers = storm::adapters::XMLtoString(attr->getNodeValue()); + if (nservers == "Single") { + numServers = 1; + } else if (nservers == "Infinite") { + // Ignore this case as we assume infinite by default (similar to GreatSpn) + } else { + expressionParser.setAcceptDoubleLiterals(false); + numServers = expressionParser.parseFromString(nservers).evaluateAsInt(); + } } else if (ignoreTransitionAttribute(name)) { // ignore node } else { @@ -327,7 +338,7 @@ namespace storm { if (immediateTransition) { builder.addImmediateTransition(0, 0, transitionName); } else { - builder.addTimedTransition(0, rate, transitionName); + builder.addTimedTransition(0, rate, numServers, transitionName); } // traverse children diff --git a/src/storm-gspn/storage/gspn/GSPN.cpp b/src/storm-gspn/storage/gspn/GSPN.cpp index c622cc4fe..5278b3b30 100644 --- a/src/storm-gspn/storage/gspn/GSPN.cpp +++ b/src/storm-gspn/storage/gspn/GSPN.cpp @@ -168,6 +168,7 @@ namespace storm { for (auto& trans : this->getTimedTransitions()) { outStream << "\t" << trans.getName() << " [label=\"" << trans.getName(); outStream << "(" << trans.getRate() << ")\"];" << std::endl; + STORM_LOG_WARN_COND(trans.hasSingleServerSemantics(), "Unable to export non-trivial transition semantics"); // TODO } // print arcs @@ -555,6 +556,7 @@ namespace storm { // add timed transitions for (const auto &trans : timedTransitions) { + STORM_LOG_WARN_COND(trans.hasInfiniteServerSemantics(), "Unable to export non-trivial transition semantics"); // TODO stream << space2 << "" << std::endl; stream << space3 << "" << std::endl; stream << space4 << "" << trans.getRate() << "" << std::endl; diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.cpp b/src/storm-gspn/storage/gspn/GspnBuilder.cpp index e273768ea..6920680ed 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.cpp +++ b/src/storm-gspn/storage/gspn/GspnBuilder.cpp @@ -65,13 +65,22 @@ namespace storm { return newId; } - + uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, std::string const& name) { + return addTimedTransition(priority, rate, 1, name); + } + + uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate, boost::optional numServers, std::string const& name) { auto trans = storm::gspn::TimedTransition(); auto newId = GSPN::timedTransitionIdToTransitionId(timedTransitions.size()); trans.setName(name); trans.setPriority(priority); trans.setRate(rate); + if (numServers) { + trans.setKServerSemantics(numServers.get()); + } else { + trans.setInfiniteServerSemantics(); + } trans.setID(newId); timedTransitions.push_back(trans); diff --git a/src/storm-gspn/storage/gspn/GspnBuilder.h b/src/storm-gspn/storage/gspn/GspnBuilder.h index a9a99699f..35c5ed220 100644 --- a/src/storm-gspn/storage/gspn/GspnBuilder.h +++ b/src/storm-gspn/storage/gspn/GspnBuilder.h @@ -39,11 +39,20 @@ namespace storm { /** * Adds an timed transition to the gspn. + * The transition is assumed to have Single-Server-Semantics * @param priority The priority for the transtion. - * @param weight The weight for the transition. + * @param rate The rate for the transition. */ uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, std::string const& name = ""); + /** + * Adds an timed transition to the gspn. + * @param priority The priority for the transtion. + * @param rate The rate for the transition. + * @param numServers The number of servers this transition has (in case of K-Server semantics) or boost::none (in case of Infinite-Server-Semantics). + */ + uint_fast64_t addTimedTransition(uint_fast64_t const &priority, RateType const& rate, boost::optional numServers, std::string const& name = ""); + void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo); diff --git a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp index 4e451d094..f4e910b81 100644 --- a/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp +++ b/src/storm-gspn/storage/gspn/GspnJsonExporter.cpp @@ -160,7 +160,16 @@ namespace storm { data["name"] = transition.getName(); data["rate"] = transition.getRate(); data["priority"] = transition.getPriority(); - + if (!transition.hasSingleServerSemantics()) { + if (transition.hasInfiniteServerSemantics()) { + data["server-semantics"] = "infinite"; + } else if (transition.hasKServerSemantics()) { + data["server-semantics"] = transition.getNumberOfServers(); + } else { + STORM_LOG_WARN("Unable to export transition semantics."); + } + } + modernjson::json position; position["x"] = x * scaleFactor; position["y"] = y * scaleFactor; diff --git a/src/storm-gspn/storage/gspn/TimedTransition.h b/src/storm-gspn/storage/gspn/TimedTransition.h index d8399319d..37b5476f6 100644 --- a/src/storm-gspn/storage/gspn/TimedTransition.h +++ b/src/storm-gspn/storage/gspn/TimedTransition.h @@ -1,12 +1,18 @@ #pragma once #include "storm-gspn/storage/gspn/Transition.h" +#include "storm/exceptions/InvalidArgumentException.h" namespace storm { namespace gspn { template class TimedTransition : public storm::gspn::Transition { public: + + TimedTransition() { + setSingleServerSemantics(); + } + /*! * Sets the rate of this transition to the given value. * @@ -15,7 +21,43 @@ namespace storm { void setRate(RateType const& rate) { this->rate = rate; } - + + /*! + * Sets the semantics of this transition + */ + void setKServerSemantics(uint64_t k) { + STORM_LOG_THROW(k>0, storm::exceptions::InvalidArgumentException, "Invalid Parameter for server semantics: 0"); + nServers = k; + } + + void setSingleServerSemantics() { + nServers = 1; + } + + void setInfiniteServerSemantics() { + nServers = 0; + } + + /*! + * Retrieves the semantics of this transition + */ + bool hasKServerSemantics() const { + return nServers > 0; + } + + bool hasSingleServerSemantics() const { + return nServers == 1; + } + + bool hasInfiniteServerSemantics() const { + return nServers == 0; + } + + uint64_t getNumberOfServers() const { + STORM_LOG_ASSERT(hasKServerSemantics(), "Tried to get the number of servers of a timed transition although it does not have K-Server-Semantics."); + return nServers; + } + /*! * Retrieves the rate of this transition. * @@ -28,6 +70,9 @@ namespace storm { private: // the rate of the transition RateType rate; + + // the number of servers of this transition. 0 means infinite server semantics. + uint64_t nServers; }; } } \ No newline at end of file