Implemented single- infinite- and k- server semantics for timed gspn transitions

src/storm-gspn/builder/JaniGSPNBuilder.cpp

@@ -3,6 +3,8 @@
 #include <memory>
 
 #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<storm::jani::Assignment> assignments;
                 for (auto const& inPlaceEntry : trans.getInputPlaces()) {
                     guard = guard && (vars[inPlaceEntry.first]->getExpressionVariable() >= inPlaceEntry.second);
@@ -153,9 +155,29 @@ namespace storm {
 
                 std::shared_ptr<storm::jani::TemplateEdge> templateEdge = std::make_shared<storm::jani::TemplateEdge>(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);
 
             }

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<uint64_t> 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

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 << "<transition id=\"" << trans.getName() << "\">" << std::endl;
                 stream << space3 << "<rate>" << std::endl;
                 stream << space4 << "<value>" << trans.getRate() << "</value>" << std::endl;

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<uint64_t> numServers, std::string const& name) {
             auto trans = storm::gspn::TimedTransition<double>();
             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);
             

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<uint64_t> numServers, std::string const& name = "");
+            
             void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo);
 
 

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;

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 <typename RateType>
         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;
         };
     }
 }