Merge branch 'gspn' into jani_gspn_support

Former-commit-id: 9cc806342a [formerly ee4578bf99]
Former-commit-id: 9ec04ac1de

examples/gspn/pnpro_test1/project01.PNPRO

@@ -0,0 +1,14 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<!-- This project file has been saved by the New GreatSPN Editor, v.100 --><project name="project01" version="121">
+  <gspn name="gspn_1_1" show-color-cmd="false" show-fluid-cmd="false">
+    <nodes>
+      <place marking="1" name="P0" x="3.0" y="2.0"/>
+      <transition name="T0" nservers-x="0.5" type="EXP" x="9.55" y="2.0"/>
+      <place name="P1" x="14.0" y="2.0"/>
+    </nodes>
+    <edges>
+      <arc head="T0" kind="INPUT" tail="P0"/>
+      <arc head="P1" kind="OUTPUT" tail="T0"/>
+    </edges>
+  </gspn>
+</project>

src/parser/GspnParser.cpp

@@ -64,9 +64,19 @@ namespace storm {
             // build gspn by traversing the DOM object
             parser->getDocument()->normalizeDocument();
             xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement();
-            // If the top-level node is not a "pnml" node, then throw an exception.
-            STORM_LOG_THROW(getName(elementRoot).compare("pnml") == 0, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n");
-            traversePnmlElement(elementRoot);
+
+            if (getName(elementRoot).compare("pnml") == 0) {
+                traversePnmlElement(elementRoot);
+            } else if (getName(elementRoot).compare("project") == 0) {
+                traverseProjectElement(elementRoot);
+            } else {
+                // If the top-level node is not a "pnml" or "" node, then throw an exception.
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n");
+            }
+
+
+
+
 
             // clean up
             delete parser;
@@ -568,6 +578,311 @@ namespace storm {
             delete tmp;
             return result;
         }
+
+        void GspnParser::traverseProjectElement(xercesc::DOMNode const* const node) {
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+                if (name.compare("version") == 0 ||
+                           name.compare("name") == 0) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment not handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (name.compare("gspn") == 0) {
+                    traverseGspnElement(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
+
+        void GspnParser::traverseGspnElement(xercesc::DOMNode const* const node) {
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+                if (name.compare("name") == 0) {
+                    gspn.setName(XMLtoString(attr->getNodeValue()));
+                } else if (name.compare("show-color-cmd") == 0 ||
+                           name.compare("show-fluid-cmd") == 0) {
+                    // ignore node
+                } else {
+                    // Found node or attribute which is at the moment not handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG(
+                        "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (name.compare("nodes") == 0) {
+                    traverseNodesElement(child);
+                } else if (name.compare("edges") == 0) {
+                    traverseEdgesElement(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
+
+        void GspnParser::traverseNodesElement(xercesc::DOMNode const* const node) {
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+                // Found node or attribute which is at the moment not handled by this parser.
+                // Notify the user and continue the parsing.
+                STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (name.compare("place") == 0) {
+                    traversePlaceElement(child);
+                } else if(name.compare("transition") == 0) {
+                    traverseTransitionElement(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
+
+        void GspnParser::traverseEdgesElement(xercesc::DOMNode const* const node) {
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+
+                // Found node or attribute which is at the moment not handled by this parser.
+                // Notify the user and continue the parsing.
+                STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (name.compare("arc") == 0) {
+                    traverseArcElement(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
+
+        void GspnParser::traversePlaceElement(xercesc::DOMNode const* const node) {
+            storm::gspn::Place place;
+            place.setID(newNode);
+            ++newNode;
+
+
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+                if (name.compare("name") == 0) {
+                    place.setName(XMLtoString(attr->getNodeValue()));
+                } else if (name.compare("marking") == 0) {
+                    place.setNumberOfInitialTokens(std::stoull(XMLtoString(attr->getNodeValue())));
+                } else if (name.compare("x") == 0 ||
+                           name.compare("y") == 0) {
+                    // ignore node
+                } else {
+                    // Found node or attribute which is at the moment not handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG(
+                            "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+
+            gspn.addPlace(place);
+        }
+
+        void GspnParser::traverseTransitionElement(xercesc::DOMNode const* const node) {
+            std::string transitionName;
+            bool immediateTransition;
+            double rate;
+
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+                if (name.compare("name") == 0) {
+                    transitionName = XMLtoString(attr->getNodeValue());
+                } else if (name.compare("type") == 0) {
+                    if (XMLtoString(attr->getNodeValue()).compare("EXP") == 0) {
+                        immediateTransition = false;
+                    } else {
+                        immediateTransition = true;
+                    }
+                } else if(name.compare("nservers-x") == 0) {
+                    rate = std::stod(XMLtoString(attr->getNodeValue()));
+                } else if (name.compare("x") == 0 ||
+                           name.compare("y") == 0) {
+                    // ignore node
+                } else {
+                    // Found node or attribute which is at the moment not handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG(
+                            "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+
+            if (immediateTransition) {
+                auto transition = storm::gspn::ImmediateTransition<double>();
+                transition.setName(transitionName);
+                gspn.addImmediateTransition(transition);
+            } else {
+                auto transition = storm::gspn::TimedTransition<double>();
+                transition.setName(transitionName);
+                transition.setRate(rate);
+                gspn.addTimedTransition(transition);
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
+
+        void GspnParser::traverseArcElement(xercesc::DOMNode const* const node) {
+            std::string head, tail, kind;
+            uint_fast64_t mult = 1;
+
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+
+                if (name.compare("head") == 0) {
+                    head = XMLtoString(attr->getNodeValue());
+                } else if (name.compare("tail") == 0) {
+                    tail = XMLtoString(attr->getNodeValue());
+                } else if (name.compare("kind") == 0) {
+                    kind = XMLtoString(attr->getNodeValue());
+                } else if (name.compare("mult") == 0) {
+                    mult = std::stoull(XMLtoString(attr->getNodeValue()));
+                } else if (name.compare("mult-x") == 0 ||
+                           name.compare("mult-y") == 0 ||
+                           name.compare("mult-k") == 0) {
+                    // ignore node
+                } else {
+                    // Found node or attribute which is at the moment not handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG(
+                            "unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+
+            if (kind.compare("INPUT") == 0) {
+                auto transition = gspn.getTransition(head);
+                if (!transition.first) {
+                    std::cout << "transition not found" << std::endl;
+                }
+                auto place = gspn.getPlace(tail);
+                if (!place.first) {
+                    std::cout << "place not found" << std::endl;
+                }
+                transition.second->setInputArcMultiplicity(place.second, mult);
+            } else if (kind.compare("INHIBITOR") == 0) {
+                auto transition = gspn.getTransition(head);
+                auto place = gspn.getPlace(tail);
+                transition.second->setInhibitionArcMultiplicity(place.second, mult);
+            } else if (kind.compare("OUTPUT") == 0) {
+                auto transition = gspn.getTransition(tail);
+                auto place = gspn.getPlace(head);
+                transition.second->setOutputArcMultiplicity(place.second, mult);
+            } else {
+                // TODO error!
+            }
+
+            // traverse children
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    // Found node or attribute which is at the moment nod handled by this parser.
+                    // Notify the user and continue the parsing.
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
+
+
+
+
+
+
+
+
     }
 }
 

src/parser/GspnParser.h

@@ -132,6 +132,18 @@ namespace storm {
             */
             static std::string XMLtoString(const XMLCh* xmlString);
 
+
+            void traverseProjectElement(xercesc::DOMNode const* const node);
+
+            void traverseGspnElement(xercesc::DOMNode const* const node);
+            void traverseNodesElement(xercesc::DOMNode const* const node);
+            void traverseEdgesElement(xercesc::DOMNode const* const node);
+
+            void traversePlaceElement(xercesc::DOMNode const* const node);
+            void traverseTransitionElement(xercesc::DOMNode const* const node);
+            void traverseArcElement(xercesc::DOMNode const* const node);
+
+
             // the constructed gspn
             storm::gspn::GSPN gspn;
 

src/storage/gspn/GSPN.cpp

@@ -40,15 +40,24 @@ namespace storm {
             return m;
         }
 
-        std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
+        std::pair<bool, storm::gspn::Place> GSPN::getPlace(uint_fast64_t const& id) const {
             for (auto& place : places) {
-                if (id.compare(place.getName()) == 0) {
+                if (id == place.getID()) {
                     return std::make_pair<bool, storm::gspn::Place const&>(true, place);
                 }
             }
             return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
         }
 
+        std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
+            for (auto& place : places) {
+                if (id.compare(place.getName())) {
+                    return std::make_pair<bool, storm::gspn::Place const&>(true, place);
+                }
+            }
+            return std::make_pair<bool, storm::gspn::Place>(false, storm::gspn::Place());
+        };
+
         std::pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const> GSPN::getTimedTransition(std::string const& id) const {
             for (auto& trans : timedTransitions) {
                 if (id.compare(trans->getName()) == 0) {
@@ -100,56 +109,43 @@ namespace storm {
 
             // print arcs
             for (auto& trans : this->getImmediateTransitions()) {
-                auto it = trans->getInputPlacesCBegin();
-                while (it != trans->getInputPlacesCEnd()) {
-                    outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" <<
-                            trans->getInputArcMultiplicity(**it);
-                    outStream << "\"];" << std::endl;
 
-                    ++it;
+                for (auto &placePtr : trans->getInputPlaces()) {
+                    outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"normal:" <<
+                            trans->getInputArcMultiplicity(*placePtr);
+                    outStream << "\"];" << std::endl;
                 }
 
-                it = trans->getInhibitionPlacesCBegin();
-                while (it != trans->getInhibitionPlacesCEnd()) {
-                    outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
-                            trans->getInhibitionArcMultiplicity(**it);
+                for (auto &placePtr : trans->getInhibitionPlaces()) {
+                    outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
+                            trans->getInhibitionArcMultiplicity(*placePtr);
                     outStream << "\"];" << std::endl;
-                    ++it;
                 }
 
-                it = trans->getOutputPlacesCBegin();
-                while (it != trans->getOutputPlacesCEnd()) {
-                    outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" <<
-                            trans->getOutputArcMultiplicity(**it);
+                for (auto &placePtr : trans->getOutputPlaces()) {
+                    outStream << "\t" << trans->getName() << " -> " << placePtr->getName() << "[label=\"" <<
+                            trans->getOutputArcMultiplicity(*placePtr);
                     outStream << "\"];" << std::endl;
-                    ++it;
                 }
             }
 
             for (auto& trans : this->getTimedTransitions()) {
-                auto it = trans->getInputPlacesCBegin();
-                while (it != trans->getInputPlacesCEnd()) {
-                    outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"normal:" <<
-                            trans->getInputArcMultiplicity(**it);
+                for (auto &placePtr : trans->getInputPlaces()) {
+                    outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"normal:" <<
+                            trans->getInputArcMultiplicity(*placePtr);
                     outStream << "\"];" << std::endl;
-                    ++it;
                 }
 
-
-                it = trans->getInhibitionPlacesCBegin();
-                while (it != trans->getInhibitionPlacesCEnd()) {
-                    outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
-                            trans->getInhibitionArcMultiplicity(**it);
+                for (auto &placePtr : trans->getInhibitionPlaces()) {
+                    outStream << "\t" << placePtr->getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
+                              trans->getInhibitionArcMultiplicity(*placePtr);
                     outStream << "\"];" << std::endl;
-                    ++it;
                 }
 
-                it = trans->getOutputPlacesCBegin();
-                while (it != trans->getOutputPlacesCEnd()) {
-                    outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" <<
-                            trans->getOutputArcMultiplicity(**it);
+                for (auto &placePtr : trans->getOutputPlaces()) {
+                    outStream << "\t" << trans->getName() << " -> " << placePtr->getName() << "[label=\"" <<
+                              trans->getOutputArcMultiplicity(*placePtr);
                     outStream << "\"];" << std::endl;
-                    ++it;
                 }
             }
 
@@ -202,26 +198,26 @@ namespace storm {
             bool result = true;
 
             for (auto const& transition : this->getImmediateTransitions()) {
-                if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() &&
-                    transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) {
+                if (transition->getInputPlaces().empty() &&
+                    transition->getInhibitionPlaces().empty()) {
                     STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n")
                     result = false;
                 }
 
-                if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) {
+                if (transition->getOutputPlaces().empty()) {
                     STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n")
                     result = false;
                 }
             }
 
             for (auto const& transition : this->getTimedTransitions()) {
-                if (transition->getInputPlacesCBegin() == transition->getInputPlacesCEnd() &&
-                    transition->getInhibitionPlacesCBegin() == transition->getInhibitionPlacesCEnd()) {
+                if (transition->getInputPlaces().empty() &&
+                    transition->getInputPlaces().empty()) {
                     STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no input or inhibition place\n")
                     result = false;
                 }
 
-                if (transition->getOutputPlacesCBegin() == transition->getOutputPlacesCEnd()) {
+                if (transition->getOutputPlaces().empty()) {
                     STORM_PRINT_AND_LOG("transition \"" + transition->getName() + "\" has no output place\n")
                     result = false;
                 }
@@ -229,82 +225,82 @@ namespace storm {
 
             //test if places exists in the gspn
             for (auto const& transition : this->getImmediateTransitions()) {
-                for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) {
+                for (auto &placePtr : transition->getInputPlaces()) {
                     bool foundPlace = false;
                     for (auto const& place : places) {
-                        if (place.getName() == (*it)->getName()) {
+                        if (place.getName() == placePtr->getName()) {
                             foundPlace = true;
                         }
                     }
                     if (!foundPlace) {
-                        STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
+                        STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
                         result = false;
                     }
                 }
 
-                for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) {
+                for (auto &placePtr : transition->getInhibitionPlaces()) {
                     bool foundPlace = false;
                     for (auto const& place : places) {
-                        if (place.getName() == (*it)->getName()) {
+                        if (place.getName() == placePtr->getName()) {
                             foundPlace = true;
                         }
                     }
                     if (!foundPlace) {
-                        STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
+                        STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
                         result = false;
                     }
                 }
 
-                for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) {
+                for (auto &placePtr : transition->getOutputPlaces()) {
                     bool foundPlace = false;
                     for (auto const& place : places) {
-                        if (place.getName() == (*it)->getName()) {
+                        if (place.getName() == placePtr->getName()) {
                             foundPlace = true;
                         }
                     }
                     if (!foundPlace) {
-                        STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
+                        STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
                         result = false;
                     }
                 }
             }
 
             for (auto const& transition : this->getTimedTransitions()) {
-                for (auto it = transition->getInputPlacesCBegin(); it != transition->getInputPlacesCEnd(); ++it) {
+                for (auto &placePtr : transition->getInputPlaces()) {
                     bool foundPlace = false;
                     for (auto const& place : places) {
-                        if (place.getName() == (*it)->getName()) {
+                        if (place.getName() == placePtr->getName()) {
                             foundPlace = true;
                         }
                     }
                     if (!foundPlace) {
-                        STORM_PRINT_AND_LOG("input place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
+                        STORM_PRINT_AND_LOG("input place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
                         result = false;
                     }
                 }
 
-                for (auto it = transition->getInhibitionPlacesCBegin(); it != transition->getInhibitionPlacesCEnd(); ++it) {
+                for (auto &placePtr : transition->getInhibitionPlaces()) {
                     bool foundPlace = false;
                     for (auto const& place : places) {
-                        if (place.getName() == (*it)->getName()) {
+                        if (place.getName() == placePtr->getName()) {
                             foundPlace = true;
                         }
                     }
                     if (!foundPlace) {
-                        STORM_PRINT_AND_LOG("inhibition place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
+                        STORM_PRINT_AND_LOG("inhibition place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
                         result = false;
                     }
                 }
 
-                for (auto it = transition->getOutputPlacesCBegin(); it != transition->getOutputPlacesCEnd(); ++it) {
+                for (auto &placePtr : transition->getOutputPlaces()) {
                     bool foundPlace = false;
                     for (auto const& place : places) {
-                        if (place.getName() == (*it)->getName()) {
+                        if (place.getName() == placePtr->getName()) {
                             foundPlace = true;
                         }
                     }
                     if (!foundPlace) {
-                        STORM_PRINT_AND_LOG("output place \"" + (*it)->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
+                        STORM_PRINT_AND_LOG("output place \"" + placePtr->getName() + "\" of transition \"" + transition->getName() + "\" was not found \n")
                         result = false;
                     }
                 }
@@ -354,54 +350,54 @@ namespace storm {
 
             stream << space2 << "<edges>" << std::endl;
             for (auto& trans : timedTransitions) {
-                for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getInputPlaces()) {
                     stream << space3 << "<arc ";
                     stream << "head=\"" << trans->getName() << "\" ";
-                    stream << "tail=\"" << (*it)->getName() << "\" ";
+                    stream << "tail=\"" << placePtr->getName() << "\" ";
                     stream << "kind=\"INPUT\" ";
-                    stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" ";
+                    stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" ";
                     stream << "/>" << std::endl;
                 }
-                for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getInhibitionPlaces()) {
                     stream << space3 << "<arc ";
                     stream << "head=\"" << trans->getName() << "\" ";
-                    stream << "tail=\"" << (*it)->getName() << "\" ";
+                    stream << "tail=\"" << placePtr->getName() << "\" ";
                     stream << "kind=\"INHIBITOR\" ";
-                    stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" ";
+                    stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" ";
                     stream << "/>" << std::endl;
                 }
-                for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getOutputPlaces()) {
                     stream << space3 << "<arc ";
-                    stream << "head=\"" << (*it)->getName() << "\" ";
+                    stream << "head=\"" << placePtr->getName() << "\" ";
                     stream << "tail=\"" << trans->getName() << "\" ";
                     stream << "kind=\"OUTPUT\" ";
-                    stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" ";
+                    stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" ";
                     stream << "/>" << std::endl;
                 }
             }
             for (auto& trans : immediateTransitions) {
-                for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getInputPlaces()) {
                     stream << space3 << "<arc ";
                     stream << "head=\"" << trans->getName() << "\" ";
-                    stream << "tail=\"" << (*it)->getName() << "\" ";
+                    stream << "tail=\"" << placePtr->getName() << "\" ";
                     stream << "kind=\"INPUT\" ";
-                    stream << "mult=\"" << trans->getInputArcMultiplicity(**it) << "\" ";
+                    stream << "mult=\"" << trans->getInputArcMultiplicity(*placePtr) << "\" ";
                     stream << "/>" << std::endl;
                 }
-                for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getInhibitionPlaces()) {
                     stream << space3 << "<arc ";
                     stream << "head=\"" << trans->getName() << "\" ";
-                    stream << "tail=\"" << (*it)->getName() << "\" ";
+                    stream << "tail=\"" << placePtr->getName() << "\" ";
                     stream << "kind=\"INHIBITOR\" ";
-                    stream << "mult=\"" << trans->getInhibitionArcMultiplicity(**it) << "\" ";
+                    stream << "mult=\"" << trans->getInhibitionArcMultiplicity(*placePtr) << "\" ";
                     stream << "/>" << std::endl;
                 }
-                for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getOutputPlaces()) {
                     stream << space3 << "<arc ";
-                    stream << "head=\"" << (*it)->getName() << "\" ";
+                    stream << "head=\"" << placePtr->getName() << "\" ";
                     stream << "tail=\"" << trans->getName() << "\" ";
                     stream << "kind=\"OUTPUT\" ";
-                    stream << "mult=\"" << trans->getOutputArcMultiplicity(**it) << "\" ";
+                    stream << "mult=\"" << trans->getOutputArcMultiplicity(*placePtr) << "\" ";
                     stream << "/>" << std::endl;
                 }
             }
@@ -456,15 +452,15 @@ namespace storm {
             // add arcs for immediate transitions
             for (const auto &trans : immediateTransitions) {
                 // add input arcs
-                for (auto it = trans->getInputPlacesCBegin(); it != trans->getInputPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getInputPlaces()) {
                     stream << space2 << "<arc ";
                     stream << "id=\"arc" << i++ << "\" ";
-                    stream << "source=\"" << (*it)->getName() << "\" ";
+                    stream << "source=\"" << placePtr->getName() << "\" ";
                     stream << "target=\"" << trans->getName() << "\" ";
                     stream << ">" << std::endl;
 
                     stream << space3 << "<inscription>" << std::endl;
-                    stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
+                    stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
                     stream << space3 << "</inscription>" << std::endl;
 
                     stream << space3 << "<type value=\"normal\" />" << std::endl;
@@ -473,15 +469,15 @@ namespace storm {
                 }
 
                 // add inhibition arcs
-                for (auto it = trans->getInhibitionPlacesCBegin(); it != trans->getInhibitionPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getInhibitionPlaces()) {
                     stream << space2 << "<arc ";
                     stream << "id=\"arc" << i++ << "\" ";
-                    stream << "source=\"" << (*it)->getName() << "\" ";
+                    stream << "source=\"" << placePtr->getName() << "\" ";
                     stream << "target=\"" << trans->getName() << "\" ";
                     stream << ">" << std::endl;
 
                     stream << space3 << "<inscription>" << std::endl;
-                    stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
+                    stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
                     stream << space3 << "</inscription>" << std::endl;
 
                     stream << space3 << "<type value=\"inhibition\" />" << std::endl;
@@ -490,15 +486,15 @@ namespace storm {
                 }
 
                 // add output arcs
-                for (auto it = trans->getOutputPlacesCBegin(); it != trans->getOutputPlacesCEnd(); ++it) {
+                for (auto &placePtr : trans->getOutputPlaces()) {
                     stream << space2 << "<arc ";
                     stream << "id=\"arc" << i++ << "\" ";
                     stream << "source=\"" << trans->getName() << "\" ";
-                    stream << "target=\"" << (*it)->getName() << "\" ";
+                    stream << "target=\"" << placePtr->getName() << "\" ";
                     stream << ">" << std::endl;
 
                     stream << space3 << "<inscription>" << std::endl;
-                    stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(**it) << "</value>" << std::endl;
+                    stream << space4 << "<value>Default," << trans->getInputArcMultiplicity(*placePtr) << "</value>" << std::endl;
                     stream << space3 << "</inscription>" << std::endl;
 
                     stream << space3 << "<type value=\"normal\" />" << std::endl;

src/storage/gspn/GSPN.h

@@ -83,8 +83,9 @@ namespace storm {
              *         If the first element is true, then the second element is the wanted place.
              *         If the first element is false, then the second element is not defined.
              */
-            std::pair<bool, storm::gspn::Place> getPlace(std::string const& id) const;
+            std::pair<bool, storm::gspn::Place> getPlace(uint_fast64_t const& id) const;
 
+            std::pair<bool, storm::gspn::Place> getPlace(std::string const& id) const;
             /*!
              * Returns the timed transition with the corresponding id.
              *

src/storage/gspn/GspnBuilder.cpp

@@ -7,37 +7,33 @@
 
 namespace storm {
     namespace gspn {
-        void GspnBuilder::addPlace(uint_fast64_t const& id, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
-            addPlace(id, "place_" + std::to_string(id), capacity, initialTokens);
-        }
-
-        void GspnBuilder::addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
+        uint_fast64_t GspnBuilder::addPlace(int_fast64_t const& capacity, uint_fast64_t const& initialTokens) {
             auto place = storm::gspn::Place();
             place.setCapacity(capacity);
-            place.setID(id);
-            place.setName(name);
+            place.setID(nextStateID);
             place.setNumberOfInitialTokens(initialTokens);
-
-            idToPlaceName.insert(std::pair<uint_fast64_t const, std::string const>(id, name));
             gspn.addPlace(place);
+            return nextStateID++;
         }
 
-        void GspnBuilder::addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority, double const& weight) {
+        uint_fast64_t GspnBuilder::addImmediateTransition(uint_fast64_t const& priority, double const& weight) {
             auto trans = storm::gspn::ImmediateTransition<double>();
-            trans.setName(std::to_string(id));
+            trans.setName(std::to_string(nextTransitionID));
             trans.setPriority(priority);
             trans.setWeight(weight);
-
+            trans.setID(nextTransitionID);
             gspn.addImmediateTransition(trans);
+            return nextTransitionID++;
         }
 
-        void GspnBuilder::addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority, double const &rate) {
+        uint_fast64_t GspnBuilder::addTimedTransition(uint_fast64_t const &priority, double const &rate) {
             auto trans = storm::gspn::TimedTransition<double>();
-            trans.setName(std::to_string(id));
+            trans.setName(std::to_string(nextTransitionID));
             trans.setPriority(priority);
             trans.setRate(rate);
-
+            trans.setID(nextTransitionID);
             gspn.addTimedTransition(trans);
+            return nextTransitionID++;
         }
 
         void GspnBuilder::addInputArc(uint_fast64_t const &from, uint_fast64_t const &to,
@@ -47,7 +43,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist.");
             }
 
-            auto placePair = gspn.getPlace(idToPlaceName.at(from));
+            auto placePair = gspn.getPlace(from);
             if (!std::get<0>(placePair)) {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist.");
             }
@@ -61,7 +57,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist.");
             }
 
-            auto placePair = gspn.getPlace(idToPlaceName.at(from));
+            auto placePair = gspn.getPlace(from);
             if (!std::get<0>(placePair)) {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist.");
             }
@@ -75,7 +71,7 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The transition with the name \"" + std::to_string(to) + "\" does not exist.");
             }
 
-            auto placePair = gspn.getPlace(idToPlaceName.at(to));
+            auto placePair = gspn.getPlace(to);
             if (!std::get<0>(placePair)) {
                 STORM_LOG_THROW(false, storm::exceptions::IllegalFunctionCallException, "The place with the id \"" + std::to_string(from) + "\" does not exist.");
             }

src/storage/gspn/GspnBuilder.h

@@ -11,15 +11,6 @@ namespace storm {
     namespace gspn {
         class GspnBuilder {
         public:
-            /**
-             * Add a place to the gspn.
-             * @param id The id must be unique for the gspn.
-             * @param capacity The capacity is the limit of tokens in the place.
-             *                 A capacity of -1 indicates an unbounded place.
-             * @param initialTokens The number of inital tokens in the place.
-             */
-            void addPlace(uint_fast64_t const& id, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
-
             /**
              * Add a place to the gspn.
              * @param id The id must be unique for the gspn.
@@ -28,7 +19,7 @@ namespace storm {
              *                 A capacity of -1 indicates an unbounded place.
              * @param initialTokens The number of inital tokens in the place.
              */
-            void addPlace(uint_fast64_t const& id, std::string const& name, int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
+            uint_fast64_t addPlace(int_fast64_t const& capacity = 1, uint_fast64_t const& initialTokens = 0);
 
             /**
              * Adds an immediate transition to the gspn.
@@ -36,7 +27,7 @@ namespace storm {
              * @param priority The priority for the transtion.
              * @param weight The weight for the transition.
              */
-            void addImmediateTransition(uint_fast64_t const& id, uint_fast64_t const& priority = 0, double const& weight = 0);
+            uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, double const& weight = 0);
 
             /**
              * Adds an timed transition to the gspn.
@@ -44,7 +35,7 @@ namespace storm {
              * @param priority The priority for the transtion.
              * @param weight The weight for the transition.
              */
-            void addTimedTransition(uint_fast64_t const &id, uint_fast64_t const &priority = 0, double const &rate = 0);
+            uint_fast64_t addTimedTransition(uint_fast64_t const &priority = 0, double const &rate = 0);
 
             /**
              * Adds an new input arc from a place to an transition.
@@ -78,8 +69,10 @@ namespace storm {
         private:
             // gspn which is returned
             storm::gspn::GSPN gspn;
-            // map from ids to names (for places)
-            std::map<uint_fast64_t const, std::string const> idToPlaceName;
+            // id for the next state which is added
+            uint_fast64_t nextStateID = 0;
+            // id for the next transition (timed or immediate) which is added
+            uint_fast64_t nextTransitionID = 0;
         };
     }
 }

src/storage/gspn/Place.cpp

@@ -30,7 +30,7 @@ namespace storm {
         }
 
         void Place::setCapacity(int_fast64_t const& capacity) {
-            STORM_LOG_THROW(capacity >= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1.");
+            STORM_LOG_THROW(capacity <= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1.");
             this->capacity = capacity;
         }
 

src/storage/gspn/Place.h

@@ -11,7 +11,9 @@ namespace storm {
         class Place {
         public:
             /*!
-             * Sets the name of this place. The name must be unique for a gspn.
+             * Sets the name of this place. The name is not used to identify a place (and therefore do not have to be unique).
+             * Some input and output formats use the name to identify a place. If you want to use the export or import
+             * features make sure that the names a unique if necessary.
              *
              * @param name The new name for the place.
              */
@@ -68,10 +70,10 @@ namespace storm {
             int_fast64_t getCapacity() const;
         private:
             // contains the number of initial tokens of this place
-            uint_fast64_t numberOfInitialTokens;
+            uint_fast64_t numberOfInitialTokens = 0;
 
             // unique id (is used to refer to a specific place in a bitvector)
-            uint_fast64_t id;
+            uint_fast64_t id = 0;
 
             // name which is used in pnml file
             std::string name;
@@ -79,7 +81,7 @@ namespace storm {
             // capacity of this place
             // -1 indicates that the capacity is not set
             // other non-negative values represents the capacity
-            int_fast64_t capacity;
+            int_fast64_t capacity = -1;
         };
     }
 }

src/storage/gspn/Transition.cpp

@@ -7,14 +7,14 @@ namespace storm {
 
         void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
             auto ptr = std::make_shared<storm::gspn::Place>(place);
-            inputMultiplicities[ptr] = multiplicity;
+            inputMultiplicities[ptr->getID()] = multiplicity;
             inputPlaces.push_back(ptr);
         }
 
         bool Transition::removeInputArc(storm::gspn::Place const& place) {
             if (existsInputArc(place)) {
                 auto ptr = std::make_shared<storm::gspn::Place>(place);
-                inputMultiplicities.erase(ptr);
+                inputMultiplicities.erase(ptr->getID());
                 inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr));
                 return true;
             } else {
@@ -24,19 +24,19 @@ namespace storm {
 
         bool Transition::existsInputArc(storm::gspn::Place const& place) const {
             auto ptr = std::make_shared<storm::gspn::Place>(place);
-            return inputMultiplicities.end() != inputMultiplicities.find(ptr);
+            return inputMultiplicities.end() != inputMultiplicities.find(ptr->getID());
         }
 
         void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
             auto ptr = std::make_shared<storm::gspn::Place>(place);
-            outputMultiplicities[ptr] = multiplicity;
+            outputMultiplicities[ptr->getID()] = multiplicity;
             outputPlaces.push_back(ptr);
         }
 
         bool Transition::removeOutputArc(storm::gspn::Place const& place) {
             if (existsOutputArc(place)) {
                 auto ptr = std::make_shared<storm::gspn::Place>(place);
-                outputMultiplicities.erase(ptr);
+                outputMultiplicities.erase(ptr->getID());
                 outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr));
                 return true;
             } else {
@@ -46,20 +46,20 @@ namespace storm {
 
         bool Transition::existsOutputArc(storm::gspn::Place const& place) const {
             auto ptr = std::make_shared<storm::gspn::Place>(place);
-            return outputMultiplicities.end() != outputMultiplicities.find(ptr);
+            return outputMultiplicities.end() != outputMultiplicities.find(ptr->getID());
         }
 
         void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place,
                                                       uint_fast64_t multiplicity) {
             auto ptr = std::make_shared<storm::gspn::Place>(place);
-            inhibitionMultiplicities[ptr] = multiplicity;
+            inhibitionMultiplicities[ptr->getID()] = multiplicity;
             inhibitionPlaces.push_back(ptr);
         }
 
         bool Transition::removeInhibitionArc(storm::gspn::Place const& place) {
             if (existsInhibitionArc(place)) {
                 auto ptr = std::make_shared<storm::gspn::Place>(place);
-                inhibitionMultiplicities.erase(ptr);
+                inhibitionMultiplicities.erase(ptr->getID());
                 inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr));
                 return true;
             } else {
@@ -69,13 +69,13 @@ namespace storm {
 
         bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const {
             auto ptr = std::make_shared<storm::gspn::Place>(place);
-            return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr);
+            return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr->getID());
         }
 
         bool Transition::isEnabled(storm::gspn::Marking const& marking) const {
             auto inputIterator = inputMultiplicities.cbegin();
             while (inputIterator != inputMultiplicities.cend()) {
-                if (marking.getNumberOfTokensAt(inputIterator->first->getID()) < inputIterator->second) {
+                if (marking.getNumberOfTokensAt(inputIterator->first) < inputIterator->second) {
                     return false;
                 }
 
@@ -84,22 +84,19 @@ namespace storm {
 
             auto inhibitionIterator = inhibitionMultiplicities.cbegin();
             while (inhibitionIterator != inhibitionMultiplicities.cend()) {
-                if (marking.getNumberOfTokensAt(inhibitionIterator->first->getID()) >= inhibitionIterator->second) {
+                if (marking.getNumberOfTokensAt(inhibitionIterator->first) >= inhibitionIterator->second) {
                     return false;
                 }
 
                 ++inhibitionIterator;
             }
 
-            auto outputIterator = outputMultiplicities.cbegin();
-            while (outputIterator != outputMultiplicities.cend()) {
-                if (outputIterator->first->getCapacity() >= 0) {
-                    if (marking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second > outputIterator->first->getCapacity()) {
+            for (auto &placePtr : getOutputPlaces()) {
+                if (placePtr->getCapacity() >= 0) {
+                    if (marking.getNumberOfTokensAt(placePtr->getID()) + getOutputArcMultiplicity(*placePtr) > placePtr->getCapacity()) {
                         return false;
                     }
                 }
-
-                ++outputIterator;
             }
 
             return true;
@@ -110,15 +107,15 @@ namespace storm {
 
             auto inputIterator = inputMultiplicities.cbegin();
             while (inputIterator != inputMultiplicities.cend()) {
-                newMarking.setNumberOfTokensAt(inputIterator->first->getID(),
-                                               newMarking.getNumberOfTokensAt(inputIterator->first->getID()) - inputIterator->second);
+                newMarking.setNumberOfTokensAt(inputIterator->first,
+                                               newMarking.getNumberOfTokensAt(inputIterator->first) - inputIterator->second);
                 ++inputIterator;
             }
 
             auto outputIterator = outputMultiplicities.cbegin();
             while (outputIterator != outputMultiplicities.cend()) {
-                newMarking.setNumberOfTokensAt(outputIterator->first->getID(),
-                                               newMarking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second);
+                newMarking.setNumberOfTokensAt(outputIterator->first,
+                                               newMarking.getNumberOfTokensAt(outputIterator->first) + outputIterator->second);
                 ++outputIterator;
             }
 
@@ -133,34 +130,22 @@ namespace storm {
             return this->name;
         }
 
-        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator  Transition::getInputPlacesCBegin() const {
-            return this->inputPlaces.cbegin();
-        }
-
-        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInputPlacesCEnd() const {
-            return this->inputPlaces.cend();
-        }
-
-        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getOutputPlacesCBegin() const {
-            return this->outputPlaces.cbegin();
-        }
-
-        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getOutputPlacesCEnd() const {
-            return this->outputPlaces.cend();
+        const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getInputPlaces() const {
+            return inputPlaces;
         }
 
-        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCBegin() const {
-            return this->inhibitionPlaces.cbegin();
+        const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getOutputPlaces() const {
+            return outputPlaces;
         }
 
-        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCEnd() const {
-            return this->inhibitionPlaces.cend();
+        const std::vector<std::shared_ptr<storm::gspn::Place>> &Transition::getInhibitionPlaces() const {
+            return inhibitionPlaces;
         }
 
         uint_fast64_t Transition::getInputArcMultiplicity(storm::gspn::Place const& place) const {
             if (existsInputArc(place)) {
                 auto ptr = std::make_shared<storm::gspn::Place>(place);
-                return inputMultiplicities.at(ptr);
+                return inputMultiplicities.at(ptr->getID());
             } else {
                 return 0;
             }
@@ -169,7 +154,7 @@ namespace storm {
         uint_fast64_t Transition::getInhibitionArcMultiplicity(storm::gspn::Place const& place) const {
             if (existsInhibitionArc(place)) {
                 auto ptr = std::make_shared<storm::gspn::Place>(place);
-                return inhibitionMultiplicities.at(ptr);
+                return inhibitionMultiplicities.at(ptr->getID());
             } else {
                 return 0;
             }
@@ -178,7 +163,7 @@ namespace storm {
         uint_fast64_t Transition::getOutputArcMultiplicity(storm::gspn::Place const& place) const {
             if (existsOutputArc(place)) {
                 auto ptr = std::make_shared<storm::gspn::Place>(place);
-                return outputMultiplicities.at(ptr);
+                return outputMultiplicities.at(ptr->getID());
             } else {
                 return 0;
             }

src/storage/gspn/Transition.h

@@ -121,46 +121,22 @@ namespace storm {
             std::string const& getName() const;
 
             /*!
-             * Returns a constant iterator to the begin of a vector which contains all input places.
-             *
-             * @return Returns iterator.
+             * Returns a list of places which are connected via a input arc.
+             * @return
              */
-            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCBegin() const;
+            const std::vector<std::shared_ptr<storm::gspn::Place>> &getInputPlaces() const;
 
             /*!
-             * Returns a constant iterator to the end of a vector which contains all input places.
-             *
-             * @return Returns iterator.
+             * Returns a list of places which are connected via a output arc.
+             * @return
              */
-            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCEnd() const;
+            const std::vector<std::shared_ptr<storm::gspn::Place>> &getOutputPlaces() const;
 
             /*!
-             * Returns a constant iterator to the begin of a vector which contains all output places.
-             *
-             * @return Returns iterator.
+             * Returns a list of places which are connected via a inhibition arc.
+             * @return
              */
-            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getOutputPlacesCBegin() const;
-
-            /*!
-             * Returns a constant iterator to the end of a vector which contains all output places.
-             *
-             * @return Returns iterator.
-             */
-            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getOutputPlacesCEnd() const;
-
-            /*!
-             * Returns a constant iterator to the begin of a vector which contains all inhibition places.
-             *
-             * @return Returns iterator.
-             */
-            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInhibitionPlacesCBegin() const;
-
-            /*!
-             * Returns a constant iterator to the end of a vector which contains all inhibition places.
-             *
-             * @return Returns iterator.
-             */
-            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInhibitionPlacesCEnd() const;
+            const std::vector<std::shared_ptr<storm::gspn::Place>> &getInhibitionPlaces() const;
 
             /*!
              * Returns the corresponding multiplicity.
@@ -199,25 +175,29 @@ namespace storm {
              * @return The priority.
              */
             uint_fast64_t getPriority() const;
+
+            void setID(uint_fast64_t const& id) {
+                this->id = id;
+            }
         private:
             /*!
              * Comparator which defines an total order on places.
              * A place is less than another place if the id is less than the id from the other place.
              */
             struct PlaceComparator {
-                bool operator()(std::shared_ptr<storm::gspn::Place> const& lhs, std::shared_ptr<storm::gspn::Place> const& rhs) const {
-                    return lhs->getID() < rhs->getID();
+                bool operator()(uint_fast64_t const& lhs, uint_fast64_t const& rhs) const {
+                    return lhs < rhs;
                 }
             };
 
-            // maps places connected to this transition with an input arc to the corresponding multiplicity
-            std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities;
+            // maps place ids connected to this transition with an input arc to the corresponding multiplicity
+            std::map<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities;
 
-            // maps places connected to this transition with an output arc to the corresponding multiplicities
-            std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities;
+            // maps place ids connected to this transition with an output arc to the corresponding multiplicities
+            std::map<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities;
 
-            // maps places connected to this transition with an inhibition arc to the corresponding multiplicity
-            std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inhibitionMultiplicities;
+            // maps place ids connected to this transition with an inhibition arc to the corresponding multiplicity
+            std::map<uint_fast64_t, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inhibitionMultiplicities;
 
             // name of the transition
             std::string name;
@@ -232,7 +212,9 @@ namespace storm {
             std::vector<std::shared_ptr<storm::gspn::Place>> inhibitionPlaces;
 
             // priority of this transition
-            uint_fast64_t priority;
+            uint_fast64_t priority = 0;
+
+            uint_fast64_t id;
         };
     }
 }

src/storm-gspn.cpp

@@ -13,71 +13,70 @@
 #include <fstream>
 #include <iostream>
 #include <string>
-// TODO clean-up includes after doing all other todos
+
 
 /*!
  * Parses the arguments to storm-gspn
  * The read data is stored in the different arguments (e.g., inputFile, formula, ...)
  *
- * @param argc number of arguments passed to storm-gspn
- * @param argv array of arguments
+ * @param begin pointer to the first argument passed to storm-gspn
+ * @param end pointer to one past the last argument passed to storm-gspn
  * @param inputFile the input file is stored in this object
  * @param formula the formula is stored in this object
  * @param outputFile the output file is stored in this object
  * @param outputType the output type is stored in this object
  * @return false if the help flag is set or the input file is missing
  */
-bool parseArguments(const int argc, const char **argv, std::string &inputFile, std::string &formula,
+bool parseArguments(const char **begin, const char **end, std::string &inputFile, std::string &formula,
                     std::string &outputFile, std::string &outputType) {
-    auto end = argv + argc;
     bool result = false;
 
-    for (auto it = argv; it != end; ++it) {
-        std::string currentArg = *it;
+    for (; begin != end; ++begin) {
+        std::string currentArg = *begin;
 
         // parse input file argument
         if (currentArg == "--input_file" || currentArg == "-i") {
-            auto next = it + 1;
-            if (next == end) {
-                return -1;
-            } else {
+            auto next = begin + 1;
+            if (next != end) {
                 inputFile = *next;
                 result = true;
+            } else {
+                return -1;
             }
-            break;
+            continue;
         }
 
         // parse formula argument
         if (currentArg == "--formula" || currentArg == "-f") {
-            auto next = it + 1;
+            auto next = begin + 1;
             if (next != end) {
-                return -1;
-            } else {
                 formula = *next;
+            } else {
+                return -1;
             }
-            break;
+            continue;
         }
 
         // parse output file argument
         if (currentArg == "--output_file" || currentArg == "-o") {
-            auto next = it + 1;
+            auto next = begin + 1;
             if (next != end) {
-                return -1;
-            } else {
                 outputFile = *next;
+            } else {
+                return -1;
             }
-            break;
+            continue;
         }
 
         // parse output file type argument
         if (currentArg == "--output_type" || currentArg == "-ot") {
-            auto next = it + 1;
+            auto next = begin + 1;
             if (next != end) {
-                return -1;
-            } else {
                 outputType = *next;
+            } else {
+                return -1;
             }
-            break;
+            continue;
         }
 
         // parse help argument
@@ -99,7 +98,7 @@ void printHelp() {
     std::cout << "-f, --formula:      formula which should be checked on the gspn" << std::endl;
     std::cout << "-o, -output_file:   file in which the gspn/markov automaton should be stored" << std::endl
               << "                    requires the option -ot to be set" << std::endl;
-    std::cout << "-ot, --output_type: possible output types are: pnml, pnpro or ma" << std::endl;
+    std::cout << "-ot, --output_type: possible output types are: pnml, pnpro, dot or ma" << std::endl;
 }
 
 void handleJani(storm::gspn::GSPN const& gspn) {
@@ -112,7 +111,7 @@ void handleJani(storm::gspn::GSPN const& gspn) {
 
 int main(const int argc, const char **argv) {
     std::string inputFile, formula, outputFile, outputType;
-    if (!parseArguments(argc, argv, inputFile, formula, outputFile, outputType)) {
+    if (!parseArguments(argv+1, argv+argc, inputFile, formula, outputFile, outputType)) {
         printHelp();
         return 1;
     }
@@ -120,41 +119,41 @@ int main(const int argc, const char **argv) {
     try {
         storm::utility::setUp();
 
-        // parse GSPN from file
+        // parse gspn from file
         auto parser = storm::parser::GspnParser();
         auto gspn = parser.parse(inputFile);
 
-        // todo ------[marker]
-        gspn.isValid();
-
+        if (!gspn.isValid()) {
+            STORM_LOG_ERROR("The gspn is not valid.");
+        }
+        
         handleJani(gspn);
-        //storm::gspn::GspnBuilder builder2;
-        //builder2.addPlace(2);
-
-        //
-        //std::ofstream file;
-        //file.open("/Users/thomas/Desktop/storm.dot");
-        //gspn.writeDotToStream(file);
-        //file.close();
-
-        //std::ofstream file;
-        //file.open("/Users/thomas/Desktop/gspn.pnpro");
-        //gspn.toPnpro(file);
-        //file.close();
-
-        std::cout << "Parsing complete!" << std::endl;
-
-
-        // Construct MA
-        //auto builder = storm::builder::ExplicitGspnModelBuilder<>();
-        //auto ma = builder.translateGspn(gspn, argv[2]);
-        //std::cout << "Markov Automaton: " << std::endl;
-        //std::cout << "number of states: " << ma.getNumberOfStates() << std::endl;
-        //std::cout << "number of transitions: " << ma.getNumberOfTransitions() << std::endl << std::endl;
-
-
-
-
+        
+        return 0;
+        
+
+        // construct ma
+        auto builder = storm::builder::ExplicitGspnModelBuilder<>();
+        auto ma = builder.translateGspn(gspn, formula);
+
+        // write gspn into output file
+        if (!outputFile.empty()) {
+            std::ofstream file;
+            file.open(outputFile);
+            if (outputType == "pnml") {
+                gspn.toPnml(file);
+            }
+            if (outputType == "pnpro") {
+                gspn.toPnpro(file);
+            }
+            if (outputType == "dot") {
+                gspn.writeDotToStream(file);
+            }
+            if (outputType == "ma") {
+                ma.writeDotToStream(file);
+            }
+            file.close();
+        }
 
         // All operations have now been performed, so we clean up everything and terminate.
         storm::utility::cleanUp();