add gspn model, parser and builder

Former-commit-id: f15a6e07c3

src/builder/ExplicitGspnModelBuilder.cpp

@@ -0,0 +1,249 @@
+#include "src/builder/ExplicitGspnModelBuilder.h"
+
+#include "src/models/sparse/StandardRewardModel.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/NotImplementedException.h"
+
+namespace storm {
+    namespace builder {
+
+        template<typename ValueType>
+        storm::models::sparse::MarkovAutomaton<ValueType> ExplicitGspnModelBuilder<ValueType>::translateGspn(storm::gspn::GSPN const& gspn) {
+            // set the given gspn and compute the limits of the net
+            this->gspn = gspn;
+            computeCapacities(gspn);
+
+            // markings maps markings to their corresponding rowgroups (indices)
+            markings = storm::storage::BitVectorHashMap<uint_fast64_t>(numberOfTotalBits, 100);
+            builder = storm::storage::SparseMatrixBuilder<double>(0, 0, 0, false, true);
+
+            // add initial marking to todo list
+            auto bitvector = gspn.getInitialMarking(numberOfBits, numberOfTotalBits)->getBitVector();
+            findOrAddBitvectorToMarkings(*bitvector);
+            currentRowIndex = 0;
+
+            // vector marking markovian states (vector contains an 1 if the state is markovian)
+            storm::storage::BitVector markovianStates(0);
+
+            // vector containing the exit rates for the markovian states
+            std::vector<ValueType> exitRates;
+
+
+            while (!todo.empty()) {
+                // take next element from the todo list
+                auto currentBitvector = todo.front();
+                todo.pop_front();
+                auto currentMarking = storm::gspn::Marking(gspn.getNumberOfPlaces(), numberOfBits, *currentBitvector);
+
+                // increment list of states by one
+                markovianStates.resize(markovianStates.size() + 1, 0);
+
+                // create new row group for the current marking
+                builder.newRowGroup(markings.getValue(*currentBitvector));
+
+                std::cout << "work on: " << *currentBitvector << std::endl;
+
+                auto enabledImmediateTransitions = getEnabledImmediateTransition(currentMarking);
+                if (!enabledImmediateTransitions.empty()) {
+                    markovianStates.set(currentRowIndex, 0);
+                    exitRates.push_back(0);
+
+                    auto partitions = partitonEnabledImmediateTransitions(currentMarking, enabledImmediateTransitions);
+                    addRowForPartitions(partitions, currentMarking);
+                } else {
+
+                    auto enabledTimedTransitions = getEnabledTimedTransition(currentMarking);
+                    if (!enabledTimedTransitions.empty()) {
+                        markovianStates.set(currentRowIndex, 1);
+
+                        auto accRate = getAccumulatedRate(enabledTimedTransitions);
+                        std::cout << "\t\tacc. rate: " << accRate << std::endl;
+                        exitRates.push_back(accRate);
+
+                        addRowForTimedTransitions(enabledTimedTransitions, currentMarking, accRate);
+                    } else {
+                        markovianStates.set(currentRowIndex, 0);
+                    }
+                }
+                ++currentRowIndex;
+            }
+
+            auto matrix = builder.build();
+            const storm::models::sparse::StateLabeling labeling; // TODO
+
+            return storm::models::sparse::MarkovAutomaton<double>(matrix, labeling, markovianStates, exitRates);
+        }
+
+        template<typename ValueType>
+        void ExplicitGspnModelBuilder<ValueType>::addRowForPartitions(std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> const& partitions, storm::gspn::Marking const& currentMarking) {
+            for (auto& partition : partitions) {
+                std::cout << "\tnew partition:" << std::endl;
+                auto accWeight = getAccumulatedWeight(partition);
+                std::cout << "\t\tacc. weight: " << accWeight << std::endl;
+
+                std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> weights;
+                for (auto& trans : partition) {
+                    std::cout << "\t\ttransname: " << trans->getName() << std::endl;
+                    auto newMarking = trans->fire(currentMarking);
+                    std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl;
+
+                    findOrAddBitvectorToMarkings(*newMarking.getBitVector());
+
+                    auto it = weights.find(markings.getValue(*newMarking.getBitVector()));
+                    double currentWeight = 0;
+                    if (it != weights.end()) {
+                        currentWeight = weights.at(markings.getValue(*newMarking.getBitVector()));
+                    }
+                    currentWeight += trans->getWeight() / accWeight;
+                    weights[markings.getValue(*newMarking.getBitVector())] = currentWeight;
+                }
+
+                addValuesToBuilder(weights);
+            }
+        }
+
+        template<typename ValueType>
+        void ExplicitGspnModelBuilder<ValueType>::addRowForTimedTransitions(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate) {
+            std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> rates;
+            for (auto& trans : enabledTimedTransitions) {
+                std::cout << "\t\ttransname: " << trans->getName() << std::endl;
+                auto newMarking = trans->fire(currentMarking);
+                std::cout << "\t\t\t target marking: " << *newMarking.getBitVector() << std::endl;
+
+                findOrAddBitvectorToMarkings(*newMarking.getBitVector());
+
+                auto it = rates.find(markings.getValue(*newMarking.getBitVector()));
+                double currentWeightRate = 0;
+                if (it != rates.end()) {
+                    currentWeightRate = rates.at(markings.getValue(*newMarking.getBitVector()));
+                }
+                currentWeightRate += trans->getRate() / accRate;
+                rates[markings.getValue(*newMarking.getBitVector())] = currentWeightRate;
+
+            }
+
+            addValuesToBuilder(rates);
+        }
+
+        template<typename ValueType>
+        void ExplicitGspnModelBuilder<ValueType>::addValuesToBuilder(std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> const& values) {
+            for (auto& it : values) {
+                std::cout << "\t\tadd value \"" << it.second << "\" to " << getBitvector(it.first) << std::endl;
+                builder.addNextValue(currentRowIndex, it.first, it.second);
+            }
+        }
+
+        template<typename ValueType>
+        std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> ExplicitGspnModelBuilder<ValueType>::partitonEnabledImmediateTransitions(
+                storm::gspn::Marking const& marking,
+                std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& enabledImmediateTransitions) {
+            decltype(partitonEnabledImmediateTransitions(marking, enabledImmediateTransitions)) result;
+
+            std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> weightedTransitions;
+
+            for (auto& trans : enabledImmediateTransitions) {
+                if (trans->getWeight() == 0) {
+                    decltype(weightedTransitions) singleton;
+                    singleton.push_back(trans);
+                    result.push_back(singleton);
+                } else {
+                    weightedTransitions.push_back(trans);
+                }
+            }
+
+            if (weightedTransitions.size() != 0) {
+                result.push_back(weightedTransitions);
+            }
+
+            return result;
+        }
+
+        template<typename ValueType>
+        double ExplicitGspnModelBuilder<ValueType>::getAccumulatedWeight(std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& vector) const {
+            double result = 0;
+
+            for (auto &trans : vector) {
+                result += trans->getWeight();
+            }
+
+            return result;
+        }
+
+        template<typename ValueType>
+        void ExplicitGspnModelBuilder<ValueType>::computeCapacities(storm::gspn::GSPN const& gspn) {
+            uint_fast64_t sum = 0;
+            for (auto& place : gspn.getPlaces()) {//TODO
+                numberOfBits[place.getID()] = 1;
+                sum += numberOfBits[place.getID()];
+            }
+
+            // compute next multiple of 64
+            uint_fast64_t rem = sum % 64;
+            numberOfTotalBits = sum + 64 - rem;
+        }
+
+        template<typename ValueType>
+        std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> ExplicitGspnModelBuilder<ValueType>::getEnabledTimedTransition(
+                storm::gspn::Marking const& marking) {
+            std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>>result;
+
+            for (auto& trans_ptr : gspn.getTimedTransitions()) {
+                if (trans_ptr->isEnabled(marking)) {
+                    result.push_back(trans_ptr);
+                }
+            }
+
+            return result;
+        }
+
+        template<typename ValueType>
+        std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> ExplicitGspnModelBuilder<ValueType>::getEnabledImmediateTransition(
+                storm::gspn::Marking const& marking) {
+            std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>result;
+
+            for (auto& trans_ptr : gspn.getImmediateTransitions()) {
+                if (trans_ptr->isEnabled(marking)) {
+                    result.push_back(trans_ptr);
+                }
+            }
+
+            return result;
+        }
+
+        template<typename ValueType>
+        double ExplicitGspnModelBuilder<ValueType>::getAccumulatedRate(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& vector) {
+            double result = 0;
+            for (auto trans_ptr : vector) {
+                result += trans_ptr->getRate();
+            }
+
+            return result;
+        }
+
+        template<typename ValueType>
+        storm::storage::BitVector ExplicitGspnModelBuilder<ValueType>::getBitvector(uint_fast64_t const& index) {
+            for (auto it = markings.begin(); it != markings.end(); ++it) {
+                if (std::get<1>(*it) == index) {
+                    return std::get<0>(*it);
+                }
+            }
+            return storm::storage::BitVector();
+        }
+
+        template<typename ValueType>
+        uint_fast64_t ExplicitGspnModelBuilder<ValueType>::findOrAddBitvectorToMarkings(storm::storage::BitVector const &bitvector) {
+            auto index = markings.findOrAdd(bitvector, nextRowGroupIndex);
+
+            if (index == nextRowGroupIndex) {
+                // bitvector was not already in the map
+                ++nextRowGroupIndex;
+                // bitvector was also never in the todo list
+                todo.push_back(std::make_shared<storm::storage::BitVector>(bitvector));
+            }
+            return index;
+        }
+
+        template class ExplicitGspnModelBuilder<double>;
+    }
+}

src/builder/ExplicitGspnModelBuilder.h

@@ -1,11 +1,161 @@
-#ifndef STORM_EXPLICITGSPNMODELBUILDER_H
-#define STORM_EXPLICITGSPNMODELBUILDER_H
+#ifndef STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_
+#define STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_
 
+#include "src/models/sparse/MarkovAutomaton.h"
+#include "src/models/sparse/StandardRewardModel.h"
+#include "src/storage/Bitvector.h"
+#include "src/storage/BitvectorHashMap.h"
+#include "src/storage/gspn/GSPN.h"
+#include "src/storage/gspn/ImmediateTransition.h"
+#include "src/storage/gspn/TimedTransition.h"
 
 namespace storm {
     namespace builder {
-        // Takes a GSPN, builds an MA.
+
+        /*!
+         * This class provides the facilities for building an markov automaton.
+         */
+        template<typename ValueType=double>
+        class ExplicitGspnModelBuilder {
+        public:
+
+            /*!
+             * Builds an MarkovAutomaton from the given GSPN.
+             *
+             * @param gspn The gspn whose semantic is covered by the MarkovAutomaton
+             * @return The resulting MarkovAutomaton
+             */
+            storm::models::sparse::MarkovAutomaton<ValueType> translateGspn(storm::gspn::GSPN const& gspn);
+        private:
+
+            /*!
+             * Add for each partition a new row in the probability matrix.
+             *
+             * @param partitions The partitioned immediate transitions.
+             * @param currentMarking The current marking which is considered at the moment.
+             */
+            void addRowForPartitions(std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> const& partitions, storm::gspn::Marking const& currentMarking);
+
+
+            /*!
+             * Add row for a markovian state.
+             *
+             * @param enabledTimedTransitions List of enabled timed transitions.
+             * @param currentMarking The current marking which is considered at the moment.
+             * @param accRate The sum of all rates of the enabled timed transisitons
+             */
+            void addRowForTimedTransitions(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& enabledTimedTransitions, storm::gspn::Marking const& currentMarking, double const& accRate);
+
+            /*!
+             * Struct for comparing unsigned integer for maps
+             */
+            struct cmpByIndex {
+                bool operator()(const uint_fast64_t &a, const uint_fast64_t &b) const {
+                    return a < b;
+                }
+            };
+
+            /*!
+             * This method insert the values from a map into the matrix
+             *
+             * @param values The values which are inserted
+             */
+            void addValuesToBuilder(std::map<uint_fast64_t , double, storm::builder::ExplicitGspnModelBuilder<ValueType>::cmpByIndex> const& values);
+
+
+            /*!
+             * This method partitions all enabled immediate transitions w.r.t. a marking.
+             * All enabled weighted immediate transitions are in one vector. Between these transitions
+             * is chosen probabilistically by the weights.
+             *
+             * All other enabled non-weighted immediate transitions are in an singleton vector.
+             * Between different vectors is chosen non-deterministically.
+             *
+             * @param marking The current marking which is considered.
+             * @param enabledImmediateTransistions A vector of enabled immediate transitions.
+             * @return The vector of vectors which is described above.
+             */
+            std::vector<std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>>> partitonEnabledImmediateTransitions(storm::gspn::Marking const& marking, std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& enabledImmediateTransitions);
+
+            /*!
+             * Computes the accumulated weight of immediate transisions which are stored in a list.
+             *
+             * @param vector List of immediate transisitions.
+             */
+            double getAccumulatedWeight(std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> const& vector) const;
+
+            /*!
+             * Compute the upper bound for the number of tokens in each place.
+             * Also computes the number of bits which are used to store a marking.
+             *
+             * @param gspn The corresponding gspn.
+             */
+            void computeCapacities(storm::gspn::GSPN const& gspn);
+
+            /*!
+             * Returns the vector of enabled timed transition.
+             *
+             * @param marking The current marking which is considered.
+             * @return The vector of enabled timed transitions.
+             */
+            std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> getEnabledTimedTransition(
+                    storm::gspn::Marking const& marking);
+
+            /*!
+             * Returns the vector of active immediate transition
+             *
+             * @param marking The current marking which is considered.
+             * @return The vector of enabled immediate transitions.
+             */
+            std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<double>>> getEnabledImmediateTransition(
+                    storm::gspn::Marking const& marking);
+
+            /*!
+             * Computes the accumulated rate of a vector of timed transitions.
+             *
+             * @param vector The vector of timed transitions.
+             * @return The accumulated rate.
+             */
+            double getAccumulatedRate(std::vector<std::shared_ptr<storm::gspn::TimedTransition<double>>> const& vector);
+
+            // is only needed for debugging purposes
+            // since markings is injective, we can determine the bitvector
+            storm::storage::BitVector getBitvector(uint_fast64_t const& index);
+
+            /*!
+             * Adds the bitvector to the marking-map.
+             * If the bitvector corresponds to a new marking the bitvector is added to the todo list.
+             *
+             * @return The rowGroup index for the bitvector.
+             */
+            uint_fast64_t findOrAddBitvectorToMarkings(storm::storage::BitVector const& bitvector);
+
+
+            // contains the number of bits which are used the store the number of tokens at each place
+            std::map<uint_fast64_t, uint_fast64_t> numberOfBits;
+
+            // contains the number of bits used to create markings
+            uint_fast64_t numberOfTotalBits;
+
+            // maps bitvectors (markings w.r.t. the capacity) to their rowgroup
+            storm::storage::BitVectorHashMap<uint_fast64_t> markings = storm::storage::BitVectorHashMap<uint_fast64_t>(64, 1);
+
+            // a list of markings for which the outgoing edges need to be computed
+            std::deque<std::shared_ptr<storm::storage::BitVector>> todo;
+
+            //the gspn which is transformed
+            storm::gspn::GSPN gspn;
+
+            // the next index for a new rowgroup
+            uint_fast64_t nextRowGroupIndex = 0;
+
+            // builder object which is used to create the probability matrix
+            storm::storage::SparseMatrixBuilder<double> builder;
+
+            // contains the current row index during the computation
+            uint_fast64_t currentRowIndex;
+        };
     }
 }
 
-#endif //STORM_EXPLICITGSPNMODELBUILDER_H
+#endif //STORM_BUILDER_EXPLICITGSPNMODELBUILDER_H_

src/parser/GspnParser.cpp

@@ -1,399 +1,478 @@
-#include <string>
-#include <bitset>
-#include <iosfwd>
-#include <memory>
 #include "src/parser/GspnParser.h"
 
-storm::gspn::GSPN storm::parser::GspnParser::parse(const std::string &filename) {
-    // initialize xerces
-    try {
-        xercesc::XMLPlatformUtils::Initialize();
-    }
-    catch (const xercesc::XMLException& toCatch) {
-        // TODO do something
-    }
+#include <xercesc/dom/DOM.hpp>
+#include <xercesc/sax/HandlerBase.hpp>
+#include <xercesc/util/PlatformUtils.hpp>
+
+#include "src/exceptions/UnexpectedException.h"
+#include "src/storage/gspn/Place.h"
+#include "src/storage/gspn/ImmediateTransition.h"
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace parser {
+        storm::gspn::GSPN const& GspnParser::parse(std::string const& filename) {
+            // initialize parser
+            newNode = 0;
+            gspn = storm::gspn::GSPN();
+
+            // initialize xercesc
+            try {
+                xercesc::XMLPlatformUtils::Initialize();
+            }
+            catch (xercesc::XMLException const& toCatch) {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to initialize xercesc\n");
+            }
 
+            auto parser = new xercesc::XercesDOMParser();
+            parser->setValidationScheme(xercesc::XercesDOMParser::Val_Always);
+            parser->setDoNamespaces(false);
+            parser->setDoSchema(false);
+            parser->setLoadExternalDTD(false);
+            parser->setIncludeIgnorableWhitespace(false);
 
+            auto errHandler = (xercesc::ErrorHandler*) new xercesc::HandlerBase();
+            parser->setErrorHandler(errHandler);
 
-    auto parser = new xercesc::XercesDOMParser();
-    parser->setValidationScheme(xercesc::XercesDOMParser::Val_Always);
-    parser->setDoNamespaces(false);
-    parser->setDoSchema(false);
-    parser->setLoadExternalDTD(false);
-    parser->setIncludeIgnorableWhitespace(false);
-    //parser->loadGrammar(source, type);
+            // parse file
+            try {
+                parser->parse(filename.c_str());
+            }
+            catch (xercesc::XMLException const& toCatch) {
+                auto message = xercesc::XMLString::transcode(toCatch.getMessage());
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, message);
+                xercesc::XMLString::release(&message);
+            }
+            catch (const xercesc::DOMException& toCatch) {
+                auto message = xercesc::XMLString::transcode(toCatch.msg);
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, message);
+                xercesc::XMLString::release(&message);
+            }
+            catch (...) {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Failed to parse pnml file.\n");
+            }
 
-    auto errHandler = (xercesc::ErrorHandler*) new xercesc::HandlerBase();
-    parser->setErrorHandler(errHandler);
+            // build gspn by traversing the DOM object
+            parser->getDocument()->normalizeDocument();
+            xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement();
+            STORM_LOG_THROW(getName(elementRoot).compare("pnml") == 0, storm::exceptions::UnexpectedException, "Failed to identify the root element.\n");
+            traversePnmlElement(elementRoot);
 
-    try {
-        parser->parse(filename.c_str());
-    }
-    catch (const xercesc::XMLException& toCatch) {
-        auto message = xercesc::XMLString::transcode(toCatch.getMessage());
-        std::cout << "Exception message is: \n"
-        << message << "\n";
-        xercesc::XMLString::release(&message);
-    }
-    catch (const xercesc::DOMException& toCatch) {
-        auto message = xercesc::XMLString::transcode(toCatch.msg);
-        std::cout << "Exception message is: \n"
-        << message << "\n";
-        xercesc::XMLString::release(&message);
-    }
-    catch (...) {
-        std::cout << "Unexpected Exception \n" ;
-    }
+            // clean up
+            delete parser;
+            delete errHandler;
+            xercesc::XMLPlatformUtils::Terminate();
 
+            return gspn;
+        }
 
-    parser->getDocument()->normalizeDocument();
-    xercesc::DOMElement* elementRoot = parser->getDocument()->getDocumentElement();
-    if (getName(elementRoot).compare("pnml") != 0) {
-        std::cout << "expected: pnml" << std::endl;
-        std::cout << "found: " << XMLtoString(elementRoot->getTagName()) << std::endl;
-        // TODO error
-    }
-    parsePNML(elementRoot);
+        void GspnParser::traversePnmlElement(xercesc::DOMElement const* const element) {
+            // traverse attributes
+            for (uint_fast64_t i = 0; i < element->getAttributes()->getLength(); ++i) {
+                auto attr = element->getAttributes()->item(i);
+                auto name = getName(attr);
 
-    delete parser;
-    delete errHandler;
+                STORM_PRINT_AND_LOG("unknown attribute (node=pnml): " + name + "\n");
+            }
 
+            // traverse children
+            for (uint_fast64_t i = 0; i < element->getChildNodes()->getLength(); ++i) {
+                auto child = element->getChildNodes()->item(i);
+                auto name = getName(child);
+
+                if (name.compare("net") == 0) {
+                    traverseNetOrPage(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=pnml): " + name + "\n");
+                }
+            }
+        }
 
-    // clean up
-    xercesc::XMLPlatformUtils::Terminate();
+        void GspnParser::traverseNetOrPage(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("id") == 0) {
+                    gspn.setName(XMLtoString(attr->getNodeValue()));
+                } else {
+                    STORM_PRINT_AND_LOG("unknown attribute (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
 
-    return gspn;
-}
+            // 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) {
+                    traversePlace(child);
+                } else if (name.compare("transition") == 0) {
+                    traverseTransition(child);
+                } else if (name.compare("arc") == 0) {
+                    traverseArc(child);
+                } else if (name.compare("page") == 0) {
+                    // Some pnml files have a child named page.
+                    // The page node has the same children like the net node (e.g., place, transition, arc)
+                    traverseNetOrPage(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=" + XMLtoString(node->getNodeName()) + "): " + name + "\n");
+                }
+            }
+        }
 
-std::string storm::parser::GspnParser::XMLtoString(const XMLCh *xmlString) {
-    char* tmp = xercesc::XMLString::transcode(xmlString);
-    auto result = std::string(tmp);
-    delete tmp;
-    return result;
-}
+        void GspnParser::traversePlace(xercesc::DOMNode const* const node) {
+            std::string placeName;
+            // the first entry is false if the corresponding information was not found in the pnml file
+            std::pair<bool, uint_fast64_t> numberOfInitialTokens(false, defaultNumberOfInitialTokens);
+            std::pair<bool, int_fast64_t> capacity(false, defaultCapacity);
+
+            // 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("id") == 0) {
+                    placeName = XMLtoString(attr->getNodeValue());
+                } else {
+                    STORM_PRINT_AND_LOG("unknown attribute (node=place): " + name + "\n");
+                }
+            }
 
-void storm::parser::GspnParser::parsePNML(xercesc::DOMElement *element) {
-    for (uint64_t i = 0; i < element->getChildNodes()->getLength(); ++i) {
-        auto child = element->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("net") == 0) {
-            parseNet(child);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else {
-            std::cout << "pnml" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
-        }
-    }
-}
+            // 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("initialMarking") == 0) {
+                    numberOfInitialTokens.first = true;
+                    numberOfInitialTokens.second = traverseInitialMarking(child);
+                } else if(name.compare("capacity") == 0) {
+                    capacity.first = true;
+                    capacity.second = traverseCapacity(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else if (name.compare("name") == 0 ||
+                           name.compare("graphics") == 0) {
+                    // ignore these tags
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=place): " + name + "\n");
+                }
+            }
 
-void storm::parser::GspnParser::parseNet(xercesc::DOMNode* node) {
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("page") == 0) {
-            parsePage(child);
-        } else if (name.compare("place") == 0) {
-            parsePlace(child);
-        } else if (name.compare("transition") == 0) {
-            parseTransition(child);
-        } else if (name.compare("arc") == 0) {
-            parseArc(child);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else if (name.compare("name") == 0 ||
-                   name.compare("token") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "net" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
+            // build place and add it to the gspn
+            storm::gspn::Place place;
+            place.setName(placeName);
+            if (!numberOfInitialTokens.first) {
+                STORM_PRINT_AND_LOG("unknown numberOfInitialTokens (place=" + placeName + ")\n");
+            }
+            place.setNumberOfInitialTokens(numberOfInitialTokens.second);
+            if (!capacity.first) {
+                STORM_PRINT_AND_LOG("unknown capacity (place=" + placeName + ")\n");
+            }
+            place.setCapacity(capacity.second);
+            place.setID(newNode);
+            ++newNode;
+            gspn.addPlace(place);
         }
-    }
-}
 
-void storm::parser::GspnParser::parsePage(xercesc::DOMNode *node) {
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("place") == 0) {
-            parsePlace(child);
-        } else if (name.compare("transition") == 0) {
-            parseTransition(child);
-        } else if (name.compare("arc") == 0) {
-            parseArc(child);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else {
-            std::cout << "page" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
-        }
-    }
-}
+        void GspnParser::traverseTransition(xercesc::DOMNode const* const node) {
+            // the first entry is false if the corresponding information was not found in the pnml file
+            std::pair<bool, bool> timed(false, defaultTransitionType);
+            std::pair<bool, std::string> value(false, defaultTransitionValue);
+            std::string id;
+
+            // parse 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("id") == 0) {
+                    id = XMLtoString(attr->getNodeValue());
+                } else {
+                    STORM_PRINT_AND_LOG("unknown attribute (node=transition): " + name + "\n");
+                }
+            }
 
-void storm::parser::GspnParser::parsePlace(xercesc::DOMNode *node) {
-    uint64_t place;
-    for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
-        auto attr = node->getAttributes()->item(i);
-        auto name = getName(attr);
-        if (name.compare("id") == 0) {
-            place = addNewPlace(XMLtoString(attr->getNodeValue()));
-        } else {
-            std::cout << "place" << std::endl;
-            std::cout << "unkown attr.: " << name << std::endl;
-        }
-    }
+            // 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("rate") == 0) {
+                    value.first =true;
+                    value.second = traverseTransitionValue(child);
+                } else if (name.compare("timed") == 0) {
+                    timed.first = true;
+                    timed.second = traverseTransitionType(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else if (name.compare("graphics") == 0 ||
+                           name.compare("name") == 0 ||
+                           name.compare("orientation") == 0) {
+                    // ignore these tags
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=transition): " + name + "\n");
+                }
+            }
 
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("initialMarking") == 0) {
-            auto tokens = parseInitialMarking(child);
-            gspn.setNumberOfPlaces(gspn.getNumberOfPlaces()+1);
-            gspn.setInitialTokens(place, tokens);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else if (name.compare("name") == 0 ||
-                   name.compare("graphics") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "place" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
-        }
-    }
-}
+            // build transition and add it to the gspn
+            if (!timed.first) {
+                STORM_PRINT_AND_LOG("unknown transition type (transition=" + id + ")\n");
+            }
 
-void storm::parser::GspnParser::parseTransition(xercesc::DOMNode *node) {
-    bool timed = false;
-    std::string rate, id;
-
-    for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
-        auto attr = node->getAttributes()->item(i);
-        auto name = getName(attr);
-        if (name.compare("id") == 0) {
-            id = XMLtoString(attr->getNodeValue());
-        } else {
-            std::cout << "transition" << std::endl;
-            std::cout << "unkown attr.: " << name << std::endl;
+            if (timed.second) {
+                storm::gspn::TimedTransition<storm::gspn::GSPN::RateType> transition;
+                if (!value.first) {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown transition rate (transition=" + id + ")\n");
+                }
+                transition.setRate(std::stod(value.second));
+                transition.setName(id);
+                gspn.addTimedTransition(transition);
+            } else {
+                storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType> transition;
+                if (!value.first) {
+                    STORM_PRINT_AND_LOG("unknown transition weight (transition=" + id + ")\n");
+                }
+                transition.setWeight(std::stod(value.second));
+                transition.setName(id);
+                gspn.addImmediateTransition(transition);
+            }
         }
-    }
 
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("rate") == 0) {
-            rate = parseRate(child);
-        } else if (name.compare("timed") == 0) {
-            timed = parseTimed(child);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else if (name.compare("graphics") == 0 ||
-                   name.compare("name") == 0 ||
-                   name.compare("orientation") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "transition" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
-        }
-    }
+        void GspnParser::traverseArc(xercesc::DOMNode const* const node) {
+            // the first entry is false if the corresponding information was not found in the pnml file
+            std::pair<bool, std::string> source(false, "");
+            std::pair<bool, std::string> target(false, "");
+            std::pair<bool, std::string> type(false, defaultArcType);
+            std::pair<bool, uint_fast64_t> multiplicity(false, defaultMultiplicity);
+            std::string id;
+
+            // parse 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("source") == 0) {
+                    source.first = true;
+                    source.second = XMLtoString(attr->getNodeValue());
+                } else if (name.compare("target") == 0) {
+                    target.first = true;
+                    target.second = XMLtoString(attr->getNodeValue());
+                } else if (name.compare("id") == 0) {
+                    id = XMLtoString(attr->getNodeValue());
+                } else {
+                    STORM_PRINT_AND_LOG("unknown attribute (node=arc): " + name + "\n");
+                }
+            }
 
-    if (timed) {
-        auto transition = std::make_shared<storm::gspn::TimedTransition<storm::gspn::GSPN::RateType>>();
-        transition->setRate(std::stoull(rate));
-        gspn.addTimedTransition(transition);
-        this->stringToTransition[id] = transition;
-    } else {
-        auto transition = std::make_shared<storm::gspn::ImmediateTransition<storm::gspn::GSPN::WeightType>>();
-        transition->setWeight(std::stoull(rate));
-        gspn.addImmediateTransition(transition);
-        this->stringToTransition[id] = transition;
-    }
-}
+            // parse 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("type") == 0) {
+                    type.first = true;
+                    type.second = traverseArcType(child);
+                } else if(name.compare("inscription") == 0) {
+                    multiplicity.first = true;
+                    multiplicity.second = traverseMultiplicity(child);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else if (name.compare("graphics") == 0 ||
+                           name.compare("arcpath") == 0 ||
+                           name.compare("tagged") == 0) {
+                    // ignore these tags
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=arc): " + name + "\n");
+                }
+            }
 
-void storm::parser::GspnParser::parseArc(xercesc::DOMNode *node) {
-    std::string source, target, type;
-    uint64_t cardinality;
-
-    for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
-        auto attr = node->getAttributes()->item(i);
-        auto name = getName(attr);
-        if (name.compare("source") == 0) {
-            source = XMLtoString(attr->getNodeValue());
-        } else if (name.compare("target") == 0) {
-            target = XMLtoString(attr->getNodeValue());
-        } else if (name.compare("id") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "arc" << std::endl;
-            std::cout << "unkown attr.: " << name << std::endl;
-        }
-    }
+            // check if all necessary information where stored in the pnml file
+            if (!source.first) {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source (arc=" + id + ")\n");
+            }
+            if (!target.first) {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc target (arc=" + id + ")\n");
+            }
+            if (!multiplicity.first) {
+                STORM_PRINT_AND_LOG("unknown multiplicity (node=arc): " + id + "\n");
+            }
 
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("type") == 0) {
-            type = parseType(child);
-        } else if(name.compare("inscription") == 0) {
-            cardinality = parseCapacity(child);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else if (name.compare("graphics") == 0 ||
-                   name.compare("arcpath") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "arc" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
-        }
-    }
-    //determine if it is an outgoing or incoming arc
-    {
-        auto it1 = stringToState.find(source);
-        auto it2 = stringToTransition.find(target);
-        if (it1 != stringToState.end() && it2 != stringToTransition.end()) {
-            // incoming arc
-            if (type.compare("normal") == 0) {
-                auto transition = stringToTransition[target];
-                transition->setInputArcCardinality(stringToState[source], cardinality);
-            } else {
-                std::cout << "arc" << std::endl;
-                std::cout << "unkown type: " << type << std::endl;
+            //determine if it is an outgoing or incoming arc
+            {
+                auto place = gspn.getPlace(source.second);
+                auto trans = gspn.getTransition(target.second);
+                if (true == place.first && true == trans.first) {
+                    if (!type.first) {
+                        STORM_PRINT_AND_LOG("unknown arc type (arc=" + id + ")\n");
+                    }
+
+                    // incoming arc
+                    if (type.second.compare("normal") == 0) {
+                        trans.second->setInputArcMultiplicity(place.second, multiplicity.second);
+                    } else if (type.second.compare("inhibition") == 0) {
+                        trans.second->setInhibitionArcMultiplicity(place.second, multiplicity.second);
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unknown arc type (arc=" + id + ")\n");
+                    }
+                    return;
+                }
             }
-            return;
-        }
-    }
-    {
-        auto it1 = stringToTransition.find(source);
-        auto it2 = stringToState.find(target);
-        if (it1 != stringToTransition.end() && it2 != stringToState.end()) {
-            // outgoing arc
-            if (type.compare("normal") == 0) {
-                auto transition = stringToTransition[source];
-                transition->setOutputArcCardinality(stringToState[target], cardinality);
-            } else {
-                std::cout << "arc" << std::endl;
-                std::cout << "unkown type: " << type << std::endl;
+            {
+                auto trans = gspn.getTransition(source.second);
+                auto place = gspn.getPlace(target.second);
+                if (true == place.first && true == trans.first) {
+                    // outgoing arc
+                    trans.second->setOutputArcMultiplicity(place.second, multiplicity.second);
+                    return;
+                }
             }
-            return;
+
+            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException ,"unknown arc source or target (arc=" + id + ")\n");
         }
-    }
-    // TODO add error message
-    std::cout << "found an arc with no correpsonding transition" << std::endl;
-}
 
-std::string storm::parser::GspnParser::getName(xercesc::DOMNode *node) {
-    switch (node->getNodeType()) {
-        case xercesc::DOMNode::NodeType::ELEMENT_NODE: {
-            auto elementNode = (xercesc::DOMElement *) node;
-            return XMLtoString(elementNode->getTagName());
+        std::string GspnParser::getName(xercesc::DOMNode *node) {
+            switch (node->getNodeType()) {
+                case xercesc::DOMNode::NodeType::ELEMENT_NODE: {
+                    auto elementNode = (xercesc::DOMElement *) node;
+                    return XMLtoString(elementNode->getTagName());
+                }
+                case xercesc::DOMNode::NodeType::TEXT_NODE: {
+                    return XMLtoString(node->getNodeValue());
+                }
+                case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: {
+                    return XMLtoString(node->getNodeName());
+                }
+                default: {
+                    STORM_PRINT_AND_LOG("unknown node type \n");
+                    return "";
+                }
+            }
         }
-        case xercesc::DOMNode::NodeType::TEXT_NODE: {
-            return XMLtoString(node->getNodeValue());
+
+        uint_fast64_t GspnParser::traverseInitialMarking(xercesc::DOMNode const* const node) {
+            uint_fast64_t result = defaultNumberOfInitialTokens;
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+                if (name.compare("text") == 0) {
+                    result = std::stoull(getName(child->getFirstChild()));
+                } else if (name.compare("value") == 0) {
+                    auto value = getName(child->getFirstChild());
+                    value = value.substr(std::string("Default,").length());
+                    result = std::stoull(value);
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else if (name.compare("graphics") == 0) {
+                    // ignore these tags
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=initialMarking): " + name + "\n");
+                }
+            }
+            return result;
         }
-        case xercesc::DOMNode::NodeType::ATTRIBUTE_NODE: {
-            return XMLtoString(node->getNodeName());
+
+        int_fast64_t GspnParser::traverseCapacity(xercesc::DOMNode const* const node) {
+            int_fast64_t result= defaultCapacity;
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+                if (name.compare("value") == 0) {
+                    auto value = getName(child->getFirstChild());
+                    if (value.find("Default,") == 0) {
+                        value = value.substr(std::string("Default,").length());
+                    }
+                    result = std::stoull(value);
+                } else if (name.compare("graphics") == 0) {
+                    // ignore these nodes
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=capacity): " + name + "\n");
+                }
+            }
+            return result;
         }
-        default: {
-            std::cout << "unknown NodeType: " << node->getNodeType() << std::endl;
-            return "";
+
+        uint_fast64_t GspnParser::traverseMultiplicity(xercesc::DOMNode const* const node) {
+            uint_fast64_t result = defaultMultiplicity;
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+                if (name.compare("value") == 0) {
+                    auto value = getName(child->getFirstChild());
+                    if (value.find("Default,") == 0) {
+                        value = value.substr(std::string("Default,").length());
+                    }
+                    result = std::stoull(value);
+                } else if (name.compare("graphics") == 0) {
+                    // ignore these nodes
+                } else if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=inscription): " + name + "\n");
+                }
+            }
+            return result;
         }
-    }
-}
 
-uint64_t storm::parser::GspnParser::addNewPlace(std::string id) {
-    auto place = newNode;
-    ++newNode;
-    stringToState[id] = place;// TODO check whether the id is already in the map
-    return place;
-}
 
-uint64_t storm::parser::GspnParser::parseInitialMarking(xercesc::DOMNode *node) {
-    uint64_t result= 0;
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("text") == 0) {
-            result = std::stoull(getName(child->getFirstChild()));
-        } else if (name.compare("value") == 0) {
-            auto value = getName(child->getFirstChild());
-            value = value.substr(std::string("Default,").length());
-            result = std::stoull(value);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else if (name.compare("graphics") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "initialMarking" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
+        std::string GspnParser::traverseTransitionValue(xercesc::DOMNode const* const node) {
+            std::string result = defaultTransitionValue;
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+                if (name.compare("value") == 0) {
+                    result = getName(child->getFirstChild());
+                } else  if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=rate): " + name + "\n");
+                }
+            }
+            return result;
         }
-    }
-    return result;
-}
 
-std::string storm::parser::GspnParser::parseRate(xercesc::DOMNode *node) {
-    std::string result = "";
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("value") == 0) {
-            result = getName(child->getFirstChild());
-        } else  if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else {
-            std::cout << "rate" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
+        bool GspnParser::traverseTransitionType(xercesc::DOMNode const* const node) {
+            bool result;
+            for (uint_fast64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
+                auto child = node->getChildNodes()->item(i);
+                auto name = getName(child);
+                if (name.compare("value") == 0) {
+                    result = getName(child->getFirstChild()).compare("true") == 0 ? true : false;
+                } else  if (std::all_of(name.begin(), name.end(), isspace)) {
+                    // ignore node (contains only whitespace)
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=timed): " + name + "\n");
+                }
+            }
+            return result;
         }
-    }
-    return result;
-}
 
-bool storm::parser::GspnParser::parseTimed(xercesc::DOMNode *node) {
-    bool result;
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("value") == 0) {
-            result = getName(child->getFirstChild()).compare("true") ? true : false;
-        } else  if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else {
-            std::cout << "timed" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
+        std::string GspnParser::traverseArcType(xercesc::DOMNode const* const node) {
+            for (uint_fast64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
+                auto attr = node->getAttributes()->item(i);
+                auto name = getName(attr);
+                if (name.compare("value") == 0) {
+                    return XMLtoString(attr->getNodeValue());
+                } else {
+                    STORM_PRINT_AND_LOG("unknown child (node=type): " + name + "\n");
+                }
+            }
+            return defaultArcType;
         }
-    }
-    return result;
-}
 
-std::string storm::parser::GspnParser::parseType(xercesc::DOMNode *node) {
-    for (uint64_t i = 0; i < node->getAttributes()->getLength(); ++i) {
-        auto attr = node->getAttributes()->item(i);
-        auto name = getName(attr);
-        if (name.compare("value") == 0) {
-            return XMLtoString(attr->getNodeValue());
-        } else {
-            std::cout << "type" << std::endl;
-            std::cout << "unkown attr.: " << name << std::endl;
+        std::string GspnParser::XMLtoString(const XMLCh *xmlString) {
+            char* tmp = xercesc::XMLString::transcode(xmlString);
+            auto result = std::string(tmp);
+            delete tmp;
+            return result;
         }
     }
-    return "";
 }
 
-uint64_t storm::parser::GspnParser::parseCapacity(xercesc::DOMNode *node) {
-    uint64_t result= 0;
-    for (uint64_t i = 0; i < node->getChildNodes()->getLength(); ++i) {
-        auto child = node->getChildNodes()->item(i);
-        auto name = getName(child);
-        if (name.compare("value") == 0) {
-            auto value = getName(child->getFirstChild());
-            value = value.substr(std::string("Default,").length());
-            result = std::stoull(value);
-        } else if (std::all_of(name.begin(), name.end(), isspace)) {
-            // ignore node (contains only whitespace)
-        } else if (name.compare("graphics") == 0) {
-            // ignore these tags
-        } else {
-            std::cout << "capacity" << std::endl;
-            std::cout << "unkown child: " << name << std::endl;
-        }
-    }
-    return result;
-}

src/parser/GspnParser.h

@@ -1,134 +1,155 @@
-#ifndef STORM_GSPNPARSER_H
-#define STORM_GSPNPARSER_H
+#ifndef STORM_PARSER_GSPNPARSER_H_
+#define STORM_PARSER_GSPNPARSER_H_
 
-#include <iostream>
 #include <string>
+
 #include <xercesc/parsers/XercesDOMParser.hpp>
-#include <xercesc/dom/DOM.hpp>
-#include <xercesc/sax/HandlerBase.hpp>
 #include <xercesc/util/XMLString.hpp>
-#include <xercesc/util/PlatformUtils.hpp>
+
 #include "src/storage/gspn/GSPN.h"
 
 namespace storm {
     namespace parser {
-        // Parses a GSPN in xml format
+
+        /* Parses a pnml-file to a gspn.
+           IMPORTANT: The names of places, transitions and arcs must differ from each other.
+         */
         class GspnParser {
         public:
-            /*!
-             * Parses the given file into the GSPN storage class assuming it complies with the PNML.
-             *
-             * @param filename The name of the file to parse
-             * @return The resulting GSPN.
-             */
-            storm::gspn::GSPN parse(std::string const& filename);
 
             /*!
-             * Transforms the given XML String to a normal string.
+             * Parses the given file into the GSPN.
              *
-             * @param xmlString The given String in the XML format
-             * @return The corresponding standard string.
+             * @param filename The name of the file to parse.
+             * @return The resulting GSPN.
              */
-            static std::string XMLtoString(const XMLCh* xmlString);
+            storm::gspn::GSPN const& parse(std::string const& filename);
         private:
-            // maps the original name of the state to its numerical representation
-            std::map<std::string,uint64_t> stringToState;
-
-            // maps the transition id to a pointer to the transition
-            std::map<std::string,std::shared_ptr<storm::gspn::Transition>> stringToTransition;
-
-            // the constructed gspn
-            storm::gspn::GSPN gspn;
-
-            // has the new id for a new node
-            uint64_t newNode;
 
             /*!
-             * Parses the root element.
+             * Traverse the root element.
              *
-             * @param element The root element.
+             * @param element The root element of the DOM object.
              */
-            void parsePNML(xercesc::DOMElement* element);
+            void traversePnmlElement(xercesc::DOMElement const* const element);
 
             /*!
-             * Parses a net node.
+             * Traverse a net or page node.
              *
-             * @param node The net node.
+             * @param node The net or page node.
              */
-            void parseNet(xercesc::DOMNode* node);
-
-            /*!
-             * Parses a page node.
-             *
-             * @param node The page node.
-a            */
-            void parsePage(xercesc::DOMNode* node);
+            void traverseNetOrPage(xercesc::DOMNode const* const node);
 
             /*!
-             * Parses a place node.
+             * Traverse a place node.
              *
              * @param node The place node.
              */
-            void parsePlace(xercesc::DOMNode* node);
+            void traversePlace(xercesc::DOMNode const* const node);
 
             /*!
-             * Parses a transition node.
+             * Traverse a transition node.
              *
              * @param node The transition node.
              */
-            void parseTransition(xercesc::DOMNode* node);
+            void traverseTransition(xercesc::DOMNode const* const node);
 
             /*!
-             * Parses an arc node.
+             * Traverse an arc node.
              *
              * @param node The arc node.
              */
-            void parseArc(xercesc::DOMNode* node);
+            void traverseArc(xercesc::DOMNode const* const node);
 
             /*!
-             * Parses an initial marking node .
+             * Traverse an initial marking node.
              *
              * @param node the initial marking node.
-             * @return The number of tokens.
+             * @return The number of initial tokens.
              */
-            uint64_t parseInitialMarking(xercesc::DOMNode* node);
+            uint_fast64_t traverseInitialMarking(xercesc::DOMNode const* const node);
 
             /*!
-             * Adds a new entry in the mapping from string to places.
+             * Traverse a capacity node.
              *
-             * @param id The string id for the new place
-             * @return The new place.
+             * @param node The capacity node.
+             * @return The capacity for the place.
              */
-            uint64_t addNewPlace(std::string id);
+            int_fast64_t traverseCapacity(xercesc::DOMNode const* const node);
 
             /*!
-             * Gives the name of the current node.
-             * @param node Current node.
-             * @return The name.
+             * Traverse a inscription node.
+             *
+             * @param node The inscription node.
+             * @return The multiplicty for the arc.
              */
-            std::string getName(xercesc::DOMNode* node);
+            uint_fast64_t traverseMultiplicity(xercesc::DOMNode const* const node);
 
             /*!
-             * Parses a rate node.
+             * Traverse a rate node.
+             *
+             * @param node The rate node.
+             * @return The rate or weight of the transition.
              */
-            std::string parseRate(xercesc::DOMNode* node);
+            std::string traverseTransitionValue(xercesc::DOMNode const* const node);
 
             /*!
-             * Parse a timed node.
+             * Traverse a timed node.
+             *
+             * @param node The timed node.
+             * @return False if the tranisition is immediate
              */
-            bool parseTimed(xercesc::DOMNode* node);
+            bool traverseTransitionType(xercesc::DOMNode const* const node);
 
             /*!
-             * Parse a type node.
+             * Traverse a type node.
+             *
+             * @param node The type node.
+             * @return Returns a string with the arc type.
              */
-            std::string parseType(xercesc::DOMNode* node);
+            std::string traverseArcType(xercesc::DOMNode const* const node);
 
             /*!
-             * Parse a capacity node.
+             * Gives the name of the current node.
+             *
+             * @param node The node.
+             * @return The name of the node.
              */
-            uint64_t parseCapacity(xercesc::DOMNode* node);
+            std::string getName(xercesc::DOMNode* node);
+
+            /*!
+            * Transforms the given XML String to a std::string.
+            *
+            * @param xmlString The given String in the XML format
+            * @return The corresponding std::string.
+            */
+            static std::string XMLtoString(const XMLCh* xmlString);
+
+            // the constructed gspn
+            storm::gspn::GSPN gspn;
+
+            // contains the id for a new node
+            uint_fast64_t newNode = 0;
+
+            // default value for initial tokens
+            uint_fast64_t defaultNumberOfInitialTokens = 0;
+
+            // default value for capacities
+            int_fast64_t defaultCapacity = -1;
+
+            // default value for the transition type (false == immediate transition)
+            bool defaultTransitionType = false;
+
+            // default value for the transition weight or rate
+            std::string defaultTransitionValue = "1"; // TODO set to 0
+
+            // default value for the arc type
+            std::string defaultArcType = "normal";
+
+            // default multiplicity for arcs
+            uint_fast64_t defaultMultiplicity = 1;
         };
     }
 }
 
-#endif //STORM_GSPNPARSER_H
+#endif //STORM_PARSER_GSPNPARSER_H_

src/storage/gspn/GSPN.cpp

@@ -1,27 +1,168 @@
 #include "src/storage/gspn/GSPN.h"
 
-storm::gspn::GSPN::GSPN() : initialMarking(0, 0) {
-}
+namespace storm {
+    namespace gspn {
+        void GSPN::addImmediateTransition(storm::gspn::ImmediateTransition<WeightType> const& transition) {
+            this->immediateTransitions.push_back(std::make_shared<storm::gspn::ImmediateTransition<WeightType>>(transition));
+        }
 
-void storm::gspn::GSPN::setInitialTokens(uint64_t place, uint64_t token) {
-    if (initialMarking.getMaxNumberOfTokens() < token) {
-        initialMarking.setMaxNumberOfTokens(token);
-    }
-    initialMarking.setNumberOfTokensAt(place, token);
-}
+        void GSPN::addTimedTransition(storm::gspn::TimedTransition<RateType> const& transition) {
+            this->timedTransitions.push_back(std::make_shared<storm::gspn::TimedTransition<RateType>>(transition));
+        }
 
-void storm::gspn::GSPN::setNumberOfPlaces(uint64_t number) {
-    initialMarking.setNumberOfPlaces(number);
-}
+        void GSPN::addPlace(Place const& place) {
+            //TODO check whether the name or id is already used by an place
+            this->places.push_back(place);
+        }
 
-uint64_t storm::gspn::GSPN::getNumberOfPlaces() {
-    return initialMarking.getNumberOfPlaces();
-}
+        uint_fast64_t GSPN::getNumberOfPlaces() const {
+            return places.size();
+        }
 
-void storm::gspn::GSPN::addImmediateTransition(std::shared_ptr<storm::gspn::ImmediateTransition<WeightType>> transition) {
-    this->immediateTransitions.push_back(transition);
-}
+        std::vector<std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>>> const& GSPN::getTimedTransitions() const {
+            return this->timedTransitions;
+        }
+
+        std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>>> const& GSPN::getImmediateTransitions() const {
+            return this->immediateTransitions;
+        }
+
+        std::vector<storm::gspn::Place> const& GSPN::getPlaces() const {
+            return places;
+        }
+
+        std::shared_ptr<storm::gspn::Marking> GSPN::getInitialMarking(std::map<uint_fast64_t, uint_fast64_t>& numberOfBits, uint_fast64_t const& numberOfTotalBits) const {
+            auto m = std::make_shared<storm::gspn::Marking>(getNumberOfPlaces(), numberOfBits, numberOfTotalBits);
+            for (auto& place : getPlaces()) {
+                m->setNumberOfTokensAt(place.getID(), place.getNumberOfInitialTokens());
+            }
+            return m;
+        }
+
+        std::pair<bool, storm::gspn::Place> GSPN::getPlace(std::string const& id) const {
+            for (auto& place : places) {
+                if (id.compare(place.getName()) == 0) {
+                    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) {
+                    return std::make_pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const>(true, static_cast<std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const>(trans));
+                }
+            }
+            return std::make_pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const>(false, nullptr);
+        }
+
+        std::pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const> GSPN::getImmediateTransition(std::string id) const {
+            for (auto& trans : immediateTransitions) {
+                if (id.compare(trans->getName()) == 0) {
+                    return std::make_pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(true, static_cast<std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(trans));
+                }
+            }
+            return std::make_pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const>(false, nullptr);
+        }
+
+        std::pair<bool, std::shared_ptr<storm::gspn::Transition> const> GSPN::getTransition(std::string const& id) const {
+            auto trans = getTimedTransition(id);
+            if (trans.first == true) {
+                return trans;
+            }
+
+            return getImmediateTransition(id);
+        }
+
+        void GSPN::writeDotToStream(std::ostream& outStream) {
+            outStream << "digraph " << this->getName() << " {" << std::endl;
+
+            // print places with initial marking (not printed is the capacity)
+            outStream << "\t" << "node [shape=ellipse]" << std::endl;
+            for (auto& place : this->getPlaces()) {
+                outStream << "\t" << place.getName() << " [label=\"" << place.getName() << "(" << place.getNumberOfInitialTokens();
+                outStream << ")\"];" << std::endl;
+            }
 
-void storm::gspn::GSPN::addTimedTransition(std::shared_ptr<storm::gspn::TimedTransition<RateType>> transition) {
-    this->timedTransitions.push_back(transition);
+            // print transitions with weight/rate
+            outStream << "\t" << "node [shape=box]" << std::endl;
+            for (auto& trans : this->getImmediateTransitions()) {
+                outStream << "\t" << trans->getName() << " [label=\"" << trans->getName();
+                outStream << "(immediate:" << trans->getWeight() << ")\"];" << std::endl;
+            }
+
+            for (auto& trans : this->getTimedTransitions()) {
+                outStream << "\t" << trans->getName() << " [label=\"" << trans->getName();
+                outStream << "(timed:" << trans->getRate() << ")\"];" << std::endl;
+            }
+
+            // 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;
+                }
+
+                it = trans->getInhibitionPlacesCBegin();
+                while (it != trans->getInhibitionPlacesCEnd()) {
+                    outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
+                            trans->getInhibitionArcMultiplicity(**it);
+                    outStream << "\"];" << std::endl;
+                    ++it;
+                }
+
+                it = trans->getOutputPlacesCBegin();
+                while (it != trans->getOutputPlacesCEnd()) {
+                    outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" <<
+                            trans->getOutputArcMultiplicity(**it);
+                    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);
+                    outStream << "\"];" << std::endl;
+                    ++it;
+                }
+
+
+                it = trans->getInhibitionPlacesCBegin();
+                while (it != trans->getInhibitionPlacesCEnd()) {
+                    outStream << "\t" << (**it).getName() << " -> " << trans->getName() << "[label=\"inhibition:" <<
+                            trans->getInhibitionArcMultiplicity(**it);
+                    outStream << "\"];" << std::endl;
+                    ++it;
+                }
+
+                it = trans->getOutputPlacesCBegin();
+                while (it != trans->getOutputPlacesCEnd()) {
+                    outStream << "\t" << trans->getName() << " -> " << (**it).getName() << "[label=\"" <<
+                            trans->getOutputArcMultiplicity(**it);
+                    outStream << "\"];" << std::endl;
+                    ++it;
+                }
+            }
+
+            outStream << "}" << std::endl;
+        }
+
+        void GSPN::setName(std::string const& name) {
+            this->name = name;
+        }
+
+        std::string const& GSPN::getName() const {
+            return this->name;
+        }
+    }
 }
+
+

src/storage/gspn/GSPN.h

@@ -1,10 +1,13 @@
-#ifndef STORM_GSPN_H
-#define STORM_GSPN_H
+#ifndef STORM_STORAGE_GSPN_GSPN_H
+#define STORM_STORAGE_GSPN_GSPN_H
 
+#include <stdint.h>
 #include <vector>
+
 #include "src/storage/gspn/ImmediateTransition.h"
-#include "src/storage/gspn/TimedTransition.h"
 #include "src/storage/gspn/Marking.h"
+#include "src/storage/gspn/Place.h"
+#include "src/storage/gspn/TimedTransition.h"
 
 namespace storm {
     namespace gspn {
@@ -16,24 +19,119 @@ namespace storm {
             typedef double WeightType;
 
             /*!
-             * The empty constructor creates an GSPN without transition and places
+             * Adds an immediate transition to the gspn.
+             *
+             * @param transition The transition which is added to the gspn.
+             */
+            void addImmediateTransition(ImmediateTransition<WeightType> const& transition);
+
+            /*!
+             * Adds a timed transition to the gspn.
+             *
+             * @param transition The transition which is added to the gspn.
+             */
+            void addTimedTransition(TimedTransition<RateType> const& transition);
+
+            /*!
+             * Adds a place to the gspn.
+             *
+             * @param place The place which is added to the gspn.
+             */
+            void addPlace(Place const& place);
+
+            /*!
+             * Returns the number of places in this gspn.
+             *
+             * @return The number of places.
+             */
+            uint_fast64_t getNumberOfPlaces() const;
+
+            /*!
+             * Returns the vector of timed transitions in this gspn.
+             *
+             * @return The vector of timed transitions.
+             */
+            std::vector<std::shared_ptr<TimedTransition<GSPN::RateType>>> const& getTimedTransitions() const;
+
+            /*!
+             * Returns the vector of immediate transitions in this gspn.
+             *
+             * @return The vector of immediate tansitions.
+             */
+            std::vector<std::shared_ptr<ImmediateTransition<GSPN::WeightType>>> const& getImmediateTransitions() const;
+
+            /*!
+             * Returns the places of this gspn
+             */
+            std::vector<storm::gspn::Place> const& getPlaces() const;
+
+            /*
+             * Computes the initial marking of the gspn.
+             *
+             * @param map The Map determines the number of bits for each place.
+             * @return The initial Marking
+             */
+            std::shared_ptr<storm::gspn::Marking> getInitialMarking(std::map<uint_fast64_t, uint_fast64_t>& numberOfBits, uint_fast64_t const& numberOfTotalBits) const;
+
+            /*!
+             * Returns the place with the corresponding id.
+             *
+             * @param id The ID of the place.
+             * @return The first element is true if the place was found.
+             *         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;
+
+            /*!
+             * Returns the timed transition with the corresponding id.
+             *
+             * @param id The ID of the timed transition.
+             * @return The first element is true if the transition was found.
+             *         If the first element is true, then the second element is the wanted transition.
+             *         If the first element is false, then the second element is the nullptr.
+             */
+            std::pair<bool, std::shared_ptr<storm::gspn::TimedTransition<GSPN::RateType>> const> getTimedTransition(std::string const& id) const;
+
+            /*!
+             * Returns the immediate transition with the corresponding id.
+             *
+             * @param id The ID of the timed transition.
+             * @return The first element is true if the transition was found.
+             *         If the first element is true, then the second element is the wanted transition.
+             *         If the first element is false, then the second element is the nullptr.
              */
-            GSPN();
+            std::pair<bool, std::shared_ptr<storm::gspn::ImmediateTransition<GSPN::WeightType>> const> getImmediateTransition(std::string id) const;
 
             /*!
-             * Set the number of tokens for a given place.
+             * Returns the transition with the corresponding id.
              *
-             * @param place
-             * @param token
+             * @param id The ID of the transition.
+             * @return Pointer to the corresponding transition or nullptr if the place does not exists.
              */
-            void setInitialTokens(uint64_t place, uint64_t token);
+            //            std::shared_ptr<storm::gspn::Transition> getTransition(std::string const& id) const;
+            std::pair<bool, std::shared_ptr<storm::gspn::Transition> const> getTransition(std::string const& id) const;
 
-            void setNumberOfPlaces(uint64_t number);
+            /*!
+             * Write the gspn in a dot(graphviz) configuration.
+             *
+             * @param outStream The stream to which the output is written to.
+             */
+            void writeDotToStream(std::ostream& outStream);
 
-            uint64_t getNumberOfPlaces();
+            /*!
+             * Set the name of the gspn to the given name.
+             *
+             * @param name The new name.
+             */
+            void setName(std::string const& name);
 
-            void addImmediateTransition(std::shared_ptr<ImmediateTransition<WeightType>> transition);
-            void addTimedTransition(std::shared_ptr<TimedTransition<RateType>> transition);
+            /*!
+             * Returns the name of the gspn.
+             *
+             * @return The name.
+             */
+            std::string const& getName() const;
         private:
             // set containing all immediate transitions
             std::vector<std::shared_ptr<storm::gspn::ImmediateTransition<WeightType>>> immediateTransitions;
@@ -41,10 +139,13 @@ namespace storm {
             // set containing all timed transitions
             std::vector<std::shared_ptr<storm::gspn::TimedTransition<RateType>>> timedTransitions;
 
-            // initial marking
-            storm::gspn::Marking initialMarking;
+            // set containing all places
+            std::vector<storm::gspn::Place> places;
+
+            // name of the gspn
+            std::string name;
         };
     }
 }
 
-#endif //STORM_GSPN_H
+#endif //STORM_STORAGE_GSPN_GSPN_H

src/storage/gspn/ImmediateTransition.h

@@ -1,5 +1,5 @@
-#ifndef STORM_IMMEDIATETRANSITION_H
-#define STORM_IMMEDIATETRANSITION_H
+#ifndef STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_
+#define STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_
 
 #include "src/storage/gspn/Transition.h"
 
@@ -13,7 +13,7 @@ namespace storm {
              *
              * @param weight The new weight for this transition.
              */
-            void setWeight(WeightType weight) {
+            void setWeight(WeightType const& weight) {
                 this->weight = weight;
             }
 
@@ -22,7 +22,7 @@ namespace storm {
              *
              * @return The weight of this transition.
              */
-            WeightType getWeight() {
+            WeightType getWeight() const {
                 return this->weight;
             }
         private:
@@ -32,4 +32,4 @@ namespace storm {
     }
 }
 
-#endif //STORM_IMMEDIATETRANSITION_H
+#endif //STORM_STORAGE_GSPN_IMMEDIATETRANSITION_H_

src/storage/gspn/Marking.cpp

@@ -1,110 +1,59 @@
+#include <stdint.h>
 #include "src/storage/gspn/Marking.h"
 
 namespace storm {
     namespace gspn {
-        Marking::Marking(uint_fast64_t numberOfPlaces, uint_fast64_t maxNumberOfTokens) {
+        Marking::Marking(uint_fast64_t const& numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, uint_fast64_t const& numberOfTotalBits) {
             this->numberOfPlaces = numberOfPlaces;
-            this->maxNumberOfTokens = maxNumberOfTokens;
-
-            this->numberOfBits = calculateNumberOfBits(maxNumberOfTokens);
-            this->marking = storm::storage::BitVector(numberOfBits * numberOfPlaces);
+            this->numberOfBits = numberOfBits;
+            this->marking = storm::storage::BitVector(numberOfTotalBits);
         }
 
-        uint_fast64_t Marking::getNumberOfPlaces() {
-            return this->numberOfPlaces;
+        Marking::Marking(uint_fast64_t const& numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, storm::storage::BitVector const& bitvector) {
+            this->numberOfPlaces = numberOfPlaces;
+            this->numberOfBits = numberOfBits;
+            this->marking = bitvector;
         }
 
-        uint_fast64_t  Marking::getMaxNumberOfTokens() {
-            return this->maxNumberOfTokens;
+        uint_fast64_t Marking::getNumberOfPlaces() const {
+            return this->numberOfPlaces;
         }
 
-        void Marking::setNumberOfTokensAt(uint_fast64_t place, uint_fast64_t numberOfTokens) {
-            // TODO check range (place < getNumberOfPlaces(), numberOfTokens < getMaxNumberOfTokens())
-            for (uint_fast64_t i = place * numberOfBits; i <(place * numberOfBits) + numberOfBits; ++i) {
-                if (numberOfTokens % 2 == 0) {
-                    marking.set(i, false);
-                } else {
-                    marking.set(i, true);
-                }
-                numberOfTokens /= 2;
+        void Marking::setNumberOfTokensAt(uint_fast64_t const& place, uint_fast64_t const& numberOfTokens) {
+            uint_fast64_t index = 0;
+            for (uint_fast64_t i=0; i < place; ++i) {
+                index += numberOfBits[i];
             }
+            marking.setFromInt(index, numberOfBits[place], numberOfTokens);
         }
 
-        uint_fast64_t Marking::getNumberOfTokensAt(uint_fast64_t place) {
-            uint_fast64_t tokens = 0;
-            for (uint_fast64_t i = place * numberOfBits, mult = 0; i < (place * numberOfBits) + numberOfBits; ++i, ++mult) {
-                if (marking.get(i)) {
-                    tokens += std::pow(2, mult);
-                }
+        uint_fast64_t Marking::getNumberOfTokensAt(uint_fast64_t const& place) const {
+            uint_fast64_t index = 0;
+            for (uint_fast64_t i=0; i < place; ++i) {
+                index += numberOfBits.at(i);
             }
-            return tokens;
+            return marking.getAsInt(index, numberOfBits.at(place));
         }
 
-        bool Marking::setNumberOfPlaces(uint_fast64_t numberOfPlaces) {
-            if (numberOfPlaces == this->numberOfPlaces) {
-                return true;
-            }
-            if (numberOfPlaces > this->numberOfPlaces) {
-                marking.resize(numberOfPlaces * numberOfBits);
-                this->numberOfPlaces = numberOfPlaces;
-                return true;
-            } else {
-                auto diff = this->numberOfPlaces - numberOfPlaces;
-                for (uint64_t i = 0; i < diff; ++i) {
-                    if (getNumberOfTokensAt(numberOfPlaces-1-i) != 0) {
-                        // TODO error
-                        return false;
-                    }
-                }
-                marking.resize(numberOfPlaces * numberOfBits);
-                this->numberOfPlaces = numberOfPlaces;
-                return true;
-            }
+        std::shared_ptr<storm::storage::BitVector> Marking::getBitVector() const {
+            auto result = std::make_shared<storm::storage::BitVector>();
+            *result = storm::storage::BitVector(marking);
+            return result;
         }
 
-        bool Marking::setMaxNumberOfTokens(uint_fast64_t maxNumberOfTokens) {
-            for (uint64_t i = 0; i < getNumberOfPlaces(); ++i) {
-                if (getNumberOfTokensAt(i) > maxNumberOfTokens) {
-                    return false;
-                }
+        bool Marking::operator==(const Marking& other) const {
+            if (getNumberOfPlaces() != other.getNumberOfPlaces()) {
+                return false;
             }
-
-            if (maxNumberOfTokens == getMaxNumberOfTokens()) {
-                return true;
+            if (&numberOfBits == &other.numberOfBits) {
+                return marking == other.marking;
             }
-
-            uint_fast64_t newNumberOfBits = calculateNumberOfBits(maxNumberOfTokens);
-            if (maxNumberOfTokens < getMaxNumberOfTokens()) {
-                for (uint_fast64_t i = 0; i < getNumberOfPlaces(); ++i) {
-                    for (uint_fast64_t j = 0; j < numberOfBits; ++j) {
-                        marking.set(i*newNumberOfBits + j , marking.get(i*numberOfBits + j));
-                    }
-                }
-                marking.resize(getNumberOfPlaces() * newNumberOfBits);
-            } else {
-                marking.resize(getNumberOfPlaces() * newNumberOfBits);
-                for (int_fast64_t i = getNumberOfPlaces()-1; i >= 0; --i) {
-                    for (int_fast64_t j = numberOfBits-1; j >= 0; --j) {
-                        for (uint_fast64_t diff = 0; diff < newNumberOfBits-numberOfBits; ++diff) {
-                            marking.set(i*newNumberOfBits+j+diff+1, 0);
-                        }
-                        marking.set(i*newNumberOfBits+j, marking.get(i*numberOfBits+j));
-                    }
+            for (uint_fast64_t i=0; i < getNumberOfPlaces(); ++i) {
+                if (getNumberOfTokensAt(i) != other.getNumberOfTokensAt(i)) {
+                    return false;
                 }
             }
-            numberOfBits = newNumberOfBits;
             return true;
         }
-
-        void Marking::incNumberOfPlaces() {
-            setNumberOfPlaces(getNumberOfPlaces()+1);
-        }
-
-        uint_fast64_t Marking::calculateNumberOfBits(uint_fast64_t maxNumber) {
-            if (maxNumber == 0) {
-                return 1;
-            }
-            return std::floor(std::log2(maxNumber)) + 1;
-        }
     }
 }

src/storage/gspn/Marking.h

@@ -1,35 +1,39 @@
-#ifndef STORM_MARKING_H
-#define STORM_MARKING_H
+#ifndef STORM_STORAGE_GSPN_MARKING_H_
+#define STORM_STORAGE_GSPN_MARKING_H_
 
 #include <cmath>
-
+#include <map>
 #include "src/storage/BitVector.h"
 
 namespace storm {
     namespace gspn {
         class Marking {
         public:
+
             /*!
-             * Creates an empty marking (at all places are 0 tokens).
+             * Creates an empty marking (at all places contain 0 tokens).
              *
-             * @param numberOfPlaces The number of places in the gspn.
-             * @param maxNumberOfTokens The maximal number of tokens in one place.
+             * @param numberOfPlaces The number of places of the gspn.
+             * @param numberOfBits The number of bits used to store the number of tokens for each place
+             * @param numberOfTotalBits The length of the internal bitvector
              */
-            Marking(uint_fast64_t numberOfPlaces, uint_fast64_t maxNumberOfTokens);
+            Marking(uint_fast64_t const& numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, uint_fast64_t const& numberOfTotalBits);
 
             /*!
-             * Retrieves the number of places for which the tokens are stored.
+             * Create the marking described by the bitvector.
              *
-             * @return The number of places.
+             * @param numberOfPlaces The number of places of the gspn.
+             * @param numberOfBits The number of bits used to store the number of tokens for each place
+             * @param bitvector The bitvector encoding the marking.
              */
-            uint_fast64_t getNumberOfPlaces();
+            Marking(uint_fast64_t const&numberOfPlaces, std::map<uint_fast64_t, uint_fast64_t> const& numberOfBits, storm::storage::BitVector const& bitvector);
 
             /*!
-             * Retrieves the maximal number of tokens which can be stored in one place.
+             * Retrieves the number of places for which the tokens are stored.
              *
-             * @return The maximal number of tokens.
+             * @return The number of places.
              */
-            uint_fast64_t getMaxNumberOfTokens();
+            uint_fast64_t getNumberOfPlaces() const;
 
             /*!
              * Set the number of tokens for the given place to the given amount.
@@ -37,7 +41,7 @@ namespace storm {
              * @param place Place must be a valid place for which the number of tokens is changed.
              * @param numberOfTokens The new number of tokens at the place.
              */
-            void setNumberOfTokensAt(uint_fast64_t place, uint_fast64_t numberOfTokens);
+            void setNumberOfTokensAt(uint_fast64_t const& place, uint_fast64_t const& numberOfTokens);
 
             /*!
              * Get the number of tokens for the given place.
@@ -45,51 +49,31 @@ namespace storm {
              * @param place The place from which the tokens are counted.
              * @return The number of tokens at the place.
              */
-            uint_fast64_t getNumberOfTokensAt(uint_fast64_t place);
+            uint_fast64_t getNumberOfTokensAt(uint_fast64_t const& place) const;
 
             /*!
-             * Reset the number of places.
-             * If the new number of places is larger than the old one, the new places start with 0 tokens.
-             * If the new number of places is smaller than the old one, the places which are going to be
-             * erased must not contain any tokens.
+             * Returns a copy of the bitvector
              *
-             * @param numberOfPlaces The new number of places.
-             * @return Return True if the change is made.
+             * @return The bitvector which encodes the marking
              */
-            bool setNumberOfPlaces(uint_fast64_t numberOfPlaces);
+            std::shared_ptr<storm::storage::BitVector> getBitVector() const;
 
             /*!
-             * Increases the number of places by one.
+             * Overload equality operator
              */
-            void incNumberOfPlaces();
-
-            /*!
-             *
-             */
-            bool setMaxNumberOfTokens(uint_fast64_t maxNumberOfTokens);
+            bool operator==(const Marking& other) const;
         private:
             // the maximal number of places in the gspn
             uint_fast64_t numberOfPlaces;
 
-            // the maximal number of tokens in one place
-            uint_fast64_t maxNumberOfTokens;
+            // number of bits for each place
+            std::map<uint_fast64_t, uint_fast64_t> numberOfBits;
 
             // contains the information of the marking
             storm::storage::BitVector marking;
-
-            // number of bits which are needed to store the tokens for one place
-            uint_fast64_t numberOfBits;
-
-            /*!
-             * Calculates the number of bits needed to store at least the given number.
-             *
-             * @param maxNumber The maximal value which can be stored
-             * @return The number of bits needed.
-             */
-            uint_fast64_t calculateNumberOfBits(uint_fast64_t maxNumber);
         };
     }
 }
 
 
-#endif //STORM_MARKING_H
+#endif //STORM_STORAGE_GSPN_MARKING_H_

src/storage/gspn/Place.cpp

@@ -0,0 +1,41 @@
+#include "Place.h"
+
+#include "src/exceptions/IllegalArgumentValueException.h"
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace gspn {
+        void Place::setName(std::string const& name) {
+            this->name = name;
+        }
+
+        std::string Place::getName() const {
+            return this->name;
+        }
+
+        void Place::setID(uint_fast64_t const& id) {
+            this->id = id;
+        }
+
+        uint_fast64_t Place::getID() const {
+            return this->id;
+        }
+
+        void Place::setNumberOfInitialTokens(uint_fast64_t const& tokens) {
+            this->numberOfInitialTokens = tokens;
+        }
+
+        uint_fast64_t Place::getNumberOfInitialTokens() const {
+            return this->numberOfInitialTokens;
+        }
+
+        void Place::setCapacity(int_fast64_t const& capacity) {
+            STORM_LOG_THROW(capacity >= -1, storm::exceptions::IllegalArgumentValueException, "The capacity cannot be less than -1.");
+            this->capacity = capacity;
+        }
+
+        int_fast64_t Place::getCapacity() const {
+            return this->capacity;
+        }
+    }
+}

src/storage/gspn/Place.h

@@ -0,0 +1,87 @@
+#ifndef STORM_STORAGE_GSPN_PLACE_H_
+#define STORM_STORAGE_GSPN_PLACE_H_
+
+#include <string>
+
+namespace storm {
+    namespace gspn {
+        /*!
+         * This class provides methods to store and retrieve data for a place in a gspn.
+         */
+        class Place {
+        public:
+            /*!
+             * Sets the name of this place. The name must be unique for a gspn.
+             *
+             * @param name The new name for the place.
+             */
+            void setName(std::string const& name);
+
+            /*!
+             * Returns the name of this place.
+             *
+             * @return The name of this place.
+             */
+            std::string getName() const;
+
+            /*!
+             * Sets the id of this place. The id must be unique for a gspn.
+             *
+             * @param id The new id of this place.
+             */
+            void setID(uint_fast64_t const& id);
+
+            /*!
+             * Returns the id of this place.
+             *
+             * @return The id of this place.
+             */
+            uint_fast64_t getID() const;
+
+            /*!
+             * Sets the number of initial tokens of this place.
+             *
+             * @param tokens The number of initial tokens.
+             */
+            void setNumberOfInitialTokens(uint_fast64_t const& tokens);
+
+            /*!
+             * Returns the number of initial tokens of this place.
+             *
+             * @return The number of initial tokens of this place.
+             */
+            uint_fast64_t getNumberOfInitialTokens() const;
+
+            /*!
+             * Sets the capacity of tokens of this place.
+             *
+             * @param capacity The capacity of this place. A non-negative number represents the capacity.
+             *                 The value -1 indicates that the capacity is not set.
+             */
+            void setCapacity(int_fast64_t const& capacity);
+
+            /*!
+             * Returns the capacity of tokens of this place.
+             *
+             * @return The capacity of the place. The value -1 indicates that the capacity is not set.
+             */
+            int_fast64_t getCapacity() const;
+        private:
+            // contains the number of initial tokens of this place
+            uint_fast64_t numberOfInitialTokens;
+
+            // unique id (is used to refer to a specific place in a bitvector)
+            uint_fast64_t id;
+
+            // name which is used in pnml file
+            std::string name;
+
+            // capacity of this place
+            // -1 indicates that the capacity is not set
+            // other non-negative values represents the capacity
+            int_fast64_t capacity;
+        };
+    }
+}
+
+#endif //STORM_STORAGE_GSPN_PLACE_H_

src/storage/gspn/TimedTransition.h

@@ -1,5 +1,5 @@
-#ifndef STORM_TIMEDTRANSITION_H
-#define STORM_TIMEDTRANSITION_H
+#ifndef STORM_STORAGE_GSPN_TIMEDTRANSITION_H_
+#define STORM_STORAGE_GSPN_TIMEDTRANSITION_H_
 
 #include "src/storage/gspn/Transition.h"
 
@@ -13,7 +13,7 @@ namespace storm {
              *
              * @param rate The new rate for this transition.
              */
-            void setRate(RateType rate) {
+            void setRate(RateType const& rate) {
                 this->rate = rate;
             }
 
@@ -22,7 +22,7 @@ namespace storm {
              *
              * @return The rate of this transition.
              */
-            RateType getRate() {
+            RateType getRate() const {
                 return this->rate;
             }
 
@@ -33,4 +33,4 @@ namespace storm {
     }
 }
 
-#endif //STORM_TIMEDTRANSITION_H
+#endif //STORM_STORAGE_GSPN_TIMEDTRANSITION_H_

src/storage/gspn/Transition.cpp

@@ -1,63 +1,81 @@
 #include "src/storage/gspn/Transition.h"
 
+#include "src/utility/macros.h"
+
 namespace storm {
     namespace gspn {
 
-        void Transition::setInputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) {
-            inputMultiplicities[place] = multiplicity;
+        void Transition::setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
+            auto ptr = std::make_shared<storm::gspn::Place>(place);
+            inputMultiplicities[ptr] = multiplicity;
+            inputPlaces.push_back(ptr);
         }
 
-        bool Transition::removeInputArc(uint_fast64_t place) {
+        bool Transition::removeInputArc(storm::gspn::Place const& place) {
             if (existsInputArc(place)) {
-                inputMultiplicities.erase(place);
+                auto ptr = std::make_shared<storm::gspn::Place>(place);
+                inputMultiplicities.erase(ptr);
+                inputPlaces.erase(std::find(inputPlaces.begin(), inputPlaces.end(), ptr));
                 return true;
             } else {
                 return false;
             }
         }
 
-        bool Transition::existsInputArc(uint_fast64_t place) {
-            return inputMultiplicities.end() != inputMultiplicities.find(place);
+        bool Transition::existsInputArc(storm::gspn::Place const& place) const {
+            auto ptr = std::make_shared<storm::gspn::Place>(place);
+            return inputMultiplicities.end() != inputMultiplicities.find(ptr);
         }
 
-        void Transition::setOutputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) {
-            outputMultiplicities[place] = multiplicity;
+        void Transition::setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity) {
+            auto ptr = std::make_shared<storm::gspn::Place>(place);
+            outputMultiplicities[ptr] = multiplicity;
+            outputPlaces.push_back(ptr);
         }
 
-        bool Transition::removeOutputArc(uint_fast64_t place) {
+        bool Transition::removeOutputArc(storm::gspn::Place const& place) {
             if (existsOutputArc(place)) {
-                outputMultiplicities.erase(place);
+                auto ptr = std::make_shared<storm::gspn::Place>(place);
+                outputMultiplicities.erase(ptr);
+                outputPlaces.erase(std::find(outputPlaces.begin(), outputPlaces.end(), ptr));
                 return true;
             } else {
                 return false;
             }
         }
 
-        bool Transition::existsOutputArc(uint_fast64_t place) {
-            return outputMultiplicities.end() != outputMultiplicities.find(place);
+        bool Transition::existsOutputArc(storm::gspn::Place const& place) const {
+            auto ptr = std::make_shared<storm::gspn::Place>(place);
+            return outputMultiplicities.end() != outputMultiplicities.find(ptr);
         }
 
-        void Transition::setInhibitionArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) {
-            inhibitionMultiplicities[place] = multiplicity;
+        void Transition::setInhibitionArcMultiplicity(storm::gspn::Place const& place,
+                                                      uint_fast64_t multiplicity) {
+            auto ptr = std::make_shared<storm::gspn::Place>(place);
+            inhibitionMultiplicities[ptr] = multiplicity;
+            inhibitionPlaces.push_back(ptr);
         }
 
-        bool Transition::removeInhibitionArc(uint_fast64_t place) {
+        bool Transition::removeInhibitionArc(storm::gspn::Place const& place) {
             if (existsInhibitionArc(place)) {
-                inhibitionMultiplicities.erase(place);
+                auto ptr = std::make_shared<storm::gspn::Place>(place);
+                inhibitionMultiplicities.erase(ptr);
+                inhibitionPlaces.erase(std::find(inhibitionPlaces.begin(), inhibitionPlaces.end(), ptr));
                 return true;
             } else {
                 return false;
             }
         }
 
-        bool Transition::existsInhibitionArc(uint_fast64_t place) {
-            return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(place);
+        bool Transition::existsInhibitionArc(storm::gspn::Place const& place) const {
+            auto ptr = std::make_shared<storm::gspn::Place>(place);
+            return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(ptr);
         }
 
-        bool Transition::isEnabled(storm::gspn::Marking marking) {
+        bool Transition::isEnabled(storm::gspn::Marking const& marking) const {
             auto inputIterator = inputMultiplicities.cbegin();
             while (inputIterator != inputMultiplicities.cend()) {
-                if (marking.getNumberOfTokensAt(inputIterator->first) < inputIterator->second) {
+                if (marking.getNumberOfTokensAt(inputIterator->first->getID()) < inputIterator->second) {
                     return false;
                 }
 
@@ -66,20 +84,104 @@ namespace storm {
 
             auto inhibitionIterator = inhibitionMultiplicities.cbegin();
             while (inhibitionIterator != inhibitionMultiplicities.cend()) {
-                if (marking.getNumberOfTokensAt(inhibitionIterator->first) >= inhibitionIterator->second) {
+                if (marking.getNumberOfTokensAt(inhibitionIterator->first->getID()) >= 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()) {
+                        return false;
+                    }
+                }
+
+                ++outputIterator;
+            }
+
             return true;
         }
 
-        storm::gspn::Marking Transition::fire(const storm::gspn::Marking marking) {
-            //check if transition is enabled
+        storm::gspn::Marking Transition::fire(storm::gspn::Marking const& marking) const {
+            storm::gspn::Marking newMarking(marking);
+
+            auto inputIterator = inputMultiplicities.cbegin();
+            while (inputIterator != inputMultiplicities.cend()) {
+                newMarking.setNumberOfTokensAt(inputIterator->first->getID(),
+                                               newMarking.getNumberOfTokensAt(inputIterator->first->getID()) - inputIterator->second);
+                ++inputIterator;
+            }
+
+            auto outputIterator = outputMultiplicities.cbegin();
+            while (outputIterator != outputMultiplicities.cend()) {
+                newMarking.setNumberOfTokensAt(outputIterator->first->getID(),
+                                               newMarking.getNumberOfTokensAt(outputIterator->first->getID()) + outputIterator->second);
+                ++outputIterator;
+            }
+
+            return newMarking;
+        }
+
+        void Transition::setName(std::string const& name) {
+            this->name = name;
+        }
+
+        std::string const& Transition::getName() const {
+            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();
+        }
 
-            return gspn::Marking(0, 0);
+        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();
+        }
+
+        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCBegin() const {
+            return this->inhibitionPlaces.cbegin();
+        }
+
+        std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator Transition::getInhibitionPlacesCEnd() const {
+            return this->inhibitionPlaces.cend();
+        }
+
+        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);
+            } else {
+                return 0;
+            }
+        }
+
+        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);
+            } else {
+                return 0;
+            }
+        }
+
+        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);
+            } else {
+                return 0;
+            }
         }
     }
 }

src/storage/gspn/Transition.h

@@ -1,11 +1,16 @@
-#ifndef STORM_TRANSITION_H
-#define STORM_TRANSITION_H
+#ifndef STORM_STORAGE_GSPN_TRANSITION_H_
+#define STORM_STORAGE_GSPN_TRANSITION_H_
 
 #include <map>
-#include "Marking.h"
+#include <vector>
+#include "src/storage/gspn/Marking.h"
+#include "src/storage/gspn/Place.h"
 
 namespace storm {
     namespace gspn {
+        /*!
+         * This class represents a transition in a gspn.
+         */
         class Transition {
         public:
             /*!
@@ -16,7 +21,7 @@ namespace storm {
              * @param place The place connected by an input arc.
              * @param multiplicity The multiplicity of the specified arc.
              */
-            void setInputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity);
+            void setInputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity);
 
             /*!
              * Removes an input arc connected to a given place.
@@ -24,7 +29,7 @@ namespace storm {
              * @param place The place from which the input arc is originating.
              * @return True if the arc existed.
              */
-            bool removeInputArc(uint_fast64_t place);
+            bool removeInputArc(storm::gspn::Place const& place);
 
             /*!
              * Checks whether the given place is connected to this transition via an input arc.
@@ -32,7 +37,7 @@ namespace storm {
              * @param place The place which is going to be checked.
              * @return True if the place is connected via an input arc.
              */
-            bool existsInputArc(uint_fast64_t place);
+            bool existsInputArc(storm::gspn::Place const& place) const;
 
             /*!
              * Set the multiplicity of the output arc going to the place.
@@ -42,7 +47,7 @@ namespace storm {
              * @param place The place connected by an output arc.
              * @param multiplicity The multiplicity of the specified arc.
              */
-            void setOutputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity);
+            void setOutputArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity);
 
             /*!
              * Removes an output arc connected to a given place.
@@ -50,7 +55,7 @@ namespace storm {
              * @param place The place from which the output arc is leading to.
              * @return True if the arc existed.
              */
-            bool removeOutputArc(uint_fast64_t place);
+            bool removeOutputArc(storm::gspn::Place const& place);
 
             /*!
              * Checks whether the given place is connected to this transition via an output arc.
@@ -58,7 +63,7 @@ namespace storm {
              * @param place The place which is going to be checked.
              * @return True if the place is connected via an output arc.
              */
-            bool existsOutputArc(uint_fast64_t place);
+            bool existsOutputArc(storm::gspn::Place const& place) const;
 
             /*!
              * Set the multiplicity of the inhibition arc originating from the place.
@@ -68,7 +73,7 @@ namespace storm {
              * @param place The place connected by an inhibition arc.
              * @param multiplicity The multiplicity of the specified arc.
              */
-            void setInhibitionArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity);
+            void setInhibitionArcMultiplicity(storm::gspn::Place const& place, uint_fast64_t multiplicity);
 
             /*!
              * Removes an inhibition arc connected to a given place.
@@ -76,7 +81,7 @@ namespace storm {
              * @param place The place from which the inhibition arc is originating.
              * @return True if the arc existed.
              */
-            bool removeInhibitionArc(uint_fast64_t place);
+            bool removeInhibitionArc(storm::gspn::Place const& place);
 
             /*!
              * Checks whether the given place is connected to this transition via an inhibition arc.
@@ -84,14 +89,14 @@ namespace storm {
              * @param place The place which is going to be checked.
              * @return True if the place is connected via an inhibition arc.
              */
-            bool existsInhibitionArc(uint_fast64_t place);
+            bool existsInhibitionArc(storm::gspn::Place const& place) const;
 
             /*!
              * Checks if the given marking enables the transition.
              *
              * @return True if the transition is enabled.
              */
-            bool isEnabled(storm::gspn::Marking marking);
+            bool isEnabled(storm::gspn::Marking const& marking) const;
 
             /*!
              * Fire the transition if possible.
@@ -99,18 +104,120 @@ namespace storm {
              * @param marking The current marking before the transition is fired.
              * @return The marking after the transition was fired.
              */
-            storm::gspn::Marking fire(const storm::gspn::Marking marking);
+            storm::gspn::Marking fire(storm::gspn::Marking const& marking) const;
+
+            /*!
+             * Set the name of the transition.
+             *
+             * @param name New name of the transition.
+             */
+            void setName(std::string const& name);
+
+            /*!
+             * Returns the name of the transition.
+             *
+             * @return The name of the transition.
+             */
+            std::string const& getName() const;
+
+            /*!
+             * Returns a constant iterator to the begin of a vector which contains all input places.
+             *
+             * @return Returns iterator.
+             */
+            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCBegin() const;
+
+            /*!
+             * Returns a constant iterator to the end of a vector which contains all input places.
+             *
+             * @return Returns iterator.
+             */
+            std::vector<std::shared_ptr<storm::gspn::Place>>::const_iterator getInputPlacesCEnd() const;
+
+            /*!
+             * Returns a constant iterator to the begin of a vector which contains all output places.
+             *
+             * @return Returns iterator.
+             */
+            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;
+
+            /*!
+             * Returns the corresponding multiplicity.
+             *
+             * @param place connected to this transition by an input arc
+             * @return cardinality or 0 if the arc does not exists
+             */
+            uint_fast64_t getInputArcMultiplicity(storm::gspn::Place const& place) const;
+
+            /*!
+             * Returns the corresponding multiplicity.
+             *
+             * @param place connected to this transition by an inhibition arc
+             * @return cardinality or 0 if the arc does not exists
+             */
+            uint_fast64_t getInhibitionArcMultiplicity(storm::gspn::Place const& place) const;
+
+            /*!
+             * Returns the corresponding multiplicity.
+             *
+             * @param place connected to this transition by an output arc
+             * @return cardinality or 0 if the arc does not exists
+             */
+            uint_fast64_t getOutputArcMultiplicity(storm::gspn::Place const& place) const;
         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();
+                }
+            };
+
             // maps places connected to this transition with an input arc to the corresponding multiplicity
-            std::map<uint_fast64_t, uint_fast64_t> inputMultiplicities;
+            std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inputMultiplicities;
 
             // maps places connected to this transition with an output arc to the corresponding multiplicities
-            std::map<uint_fast64_t, uint_fast64_t> outputMultiplicities;
+            std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> outputMultiplicities;
 
             // maps places connected to this transition with an inhibition arc to the corresponding multiplicity
-            std::map<uint_fast64_t, uint_fast64_t> inhibitionMultiplicities;
+            std::map<std::shared_ptr<storm::gspn::Place>, uint_fast64_t, storm::gspn::Transition::PlaceComparator> inhibitionMultiplicities;
+
+            // name of the transition
+            std::string name;
+
+            // list of all places connected to this transition via an input arc
+            std::vector<std::shared_ptr<storm::gspn::Place>> inputPlaces;
+
+            // list of all places connected to this transition via an output arc
+            std::vector<std::shared_ptr<storm::gspn::Place>> outputPlaces;
+
+            // list of all places connected to this transition via an inhibition arc
+            std::vector<std::shared_ptr<storm::gspn::Place>> inhibitionPlaces;
         };
     }
 }
 
-#endif //STORM_TRANSITION_H
+#endif //STORM_STORAGE_GSPN_TRANSITION_H_