partial implementation of gspns, transitions and markings

Former-commit-id: 77d76d6c89

src/storage/gspn/GSPN.h

@@ -1,13 +1,28 @@
 #ifndef STORM_GSPN_H
 #define STORM_GSPN_H
 
+#include <set>
+#include "ImmediateTransition.h"
+#include "TimedTransition.h"
+#include "Marking.h"
+
 namespace storm {
     namespace gspn {
         // Stores a GSPN
         class GSPN {
+        public:
             // Later, the rates and probabilities type should become a template, for now, let it be doubles.
-            typedef double ValueType;
+            typedef double RateType;
+            typedef double WeightType;
+        private:
+            // set containing all immediate transitions
+            std::set<storm::gspn::ImmediateTransition<WeightType>> immediateTransitions;
+
+            // set containing all timed transitions
+            std::set<storm::gspn::TimedTransition<RateType>> timedTransitions;
 
+            // initial marking
+            storm::gspn::Marking initialMarking;
         };
     }
 }

src/storage/gspn/ImmediateTransition.h

@@ -0,0 +1,35 @@
+#ifndef STORM_IMMEDIATETRANSITION_H
+#define STORM_IMMEDIATETRANSITION_H
+
+#include "src/storage/gspn/Transition.h"
+
+namespace storm {
+    namespace gspn {
+        template <typename WeightType>
+        class ImmediateTransition : public storm::gspn::Transition {
+        public:
+            /*!
+             * Sets the weight of this transition to the given value.
+             *
+             * @param weight The new weight for this transition.
+             */
+            void setWeight(WeightType weight) {
+                this->weight = weight;
+            }
+
+            /*!
+             * Retrieves the weight of this transition.
+             *
+             * @return The weight of this transition.
+             */
+            WeightType getWeight() {
+                return this->weight;
+            }
+        private:
+            // the weight of the transition
+           WeightType weight;
+        };
+    }
+}
+
+#endif //STORM_IMMEDIATETRANSITION_H

src/storage/gspn/Marking.cpp

@@ -0,0 +1,43 @@
+#include "src/storage/gspn/Marking.h"
+
+namespace storm {
+    namespace gspn {
+        Marking::Marking(uint_fast64_t numberOfPlaces, uint_fast64_t maxNumberOfTokens) {
+            this->numberOfPlaces = numberOfPlaces;
+            this->maxNumberOfTokens = maxNumberOfTokens;
+
+            this->numberOfBits = std::floor(std::log2(maxNumberOfTokens)) + 1;
+            this->marking = storm::storage::BitVector(numberOfBits * numberOfPlaces);
+        }
+
+        uint_fast64_t Marking::getNumberOfPlaces() {
+            return this->numberOfPlaces;
+        }
+
+        uint_fast64_t  Marking::getMaxNumberOfTokens() {
+            return this->maxNumberOfTokens;
+        }
+
+        void Marking::setNumberOfTokensAt(uint_fast64_t place, uint_fast64_t numberOfTokens) {
+            //check range
+            for (uint_fast64_t i = getNumberOfPlaces() * numberOfBits; i <(getNumberOfPlaces() * numberOfBits) + numberOfBits; ++i) {
+                if (numberOfTokens % 2 == 0) {
+                    marking.set(i, false);
+                } else {
+                    marking.set(i, true);
+                }
+                numberOfTokens /= 2;
+            }
+        }
+
+        uint_fast64_t Marking::getNumberOfTokensAt(uint_fast64_t place) {
+            uint_fast64_t tokens = 0;
+            for (uint_fast64_t i = getNumberOfPlaces() * numberOfBits, mult = 0; i <(getNumberOfPlaces() * numberOfBits) + numberOfBits; ++i, ++mult) {
+                if (marking.get(i)) {
+                    tokens += std::pow(2, mult);
+                }
+            }
+            return tokens;
+        }
+    }
+}

src/storage/gspn/Marking.h

@@ -0,0 +1,66 @@
+#ifndef STORM_MARKING_H
+#define STORM_MARKING_H
+
+#include <cmath>
+
+#include "src/storage/BitVector.h"
+
+namespace storm {
+    namespace gspn {
+        class Marking {
+        public:
+            /*!
+             * Creates an empty marking (at all places are 0 tokens).
+             *
+             * @param numberOfPlaces The number of places in the gspn.
+             * @param maxNumberOfTokens The maximal number of tokens in one place.
+             */
+            Marking(uint_fast64_t numberOfPlaces, uint_fast64_t maxNumberOfTokens);
+
+            /*!
+             * Retrieves the number of places for which the tokens are stored.
+             *
+             * @return The number of places.
+             */
+            uint_fast64_t getNumberOfPlaces();
+
+            /*!
+             * Retrieves the maximal number of tokens which can be stored in one place.
+             *
+             * @return The maximal number of tokens.
+             */
+            uint_fast64_t getMaxNumberOfTokens();
+
+            /*!
+             * Set the number of tokens for the given place to the given amount.
+             *
+             * @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);
+
+            /*!
+             * Get the number of tokens for the given place.
+             *
+             * @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);
+        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;
+
+            // 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;
+        };
+    }
+}
+
+
+#endif //STORM_MARKING_H

src/storage/gspn/TimedTransition.h

@@ -0,0 +1,36 @@
+#ifndef STORM_TIMEDTRANSITION_H
+#define STORM_TIMEDTRANSITION_H
+
+#include "src/storage/gspn/Transition.h"
+
+namespace storm {
+    namespace gspn {
+        template <typename RateType>
+        class TimedTransition : public storm::gspn::Transition {
+        public:
+            /*!
+             * Sets the rate of this transition to the given value.
+             *
+             * @param rate The new rate for this transition.
+             */
+            void setRate(RateType rate) {
+                this->rate = rate;
+            }
+
+            /*!
+             * Retrieves the rate of this transition.
+             *
+             * @return The rate of this transition.
+             */
+            RateType getRate() {
+                return this->rate;
+            }
+
+        private:
+            // the rate of the transition
+            RateType rate;
+        };
+    }
+}
+
+#endif //STORM_TIMEDTRANSITION_H

src/storage/gspn/Transition.cpp

@@ -0,0 +1,85 @@
+#include "src/storage/gspn/Transition.h"
+
+namespace storm {
+    namespace gspn {
+
+        void Transition::setInputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) {
+            inputMultiplicities[place] = multiplicity;
+        }
+
+        bool Transition::removeInputArc(uint_fast64_t place) {
+            if (existsInputArc(place)) {
+                inputMultiplicities.erase(place);
+                return true;
+            } else {
+                return false;
+            }
+        }
+
+        bool Transition::existsInputArc(uint_fast64_t place) {
+            return inputMultiplicities.end() != inputMultiplicities.find(place);
+        }
+
+        void Transition::setOutputArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) {
+            outputMultiplicities[place] = multiplicity;
+        }
+
+        bool Transition::removeOutputArc(uint_fast64_t place) {
+            if (existsOutputArc(place)) {
+                outputMultiplicities.erase(place);
+                return true;
+            } else {
+                return false;
+            }
+        }
+
+        bool Transition::existsOutputArc(uint_fast64_t place) {
+            return outputMultiplicities.end() != outputMultiplicities.find(place);
+        }
+
+        void Transition::setInhibitionArcCardinality(uint_fast64_t place, uint_fast64_t multiplicity) {
+            inhibitionMultiplicities[place] = multiplicity;
+        }
+
+        bool Transition::removeInhibitionArc(uint_fast64_t place) {
+            if (existsInhibitionArc(place)) {
+                inhibitionMultiplicities.erase(place);
+                return true;
+            } else {
+                return false;
+            }
+        }
+
+        bool Transition::existsInhibitionArc(uint_fast64_t place) {
+            return inhibitionMultiplicities.end() != inhibitionMultiplicities.find(place);
+        }
+
+        bool Transition::isEnabled(storm::gspn::Marking marking) {
+            auto inputIterator = inputMultiplicities.cbegin();
+            while (inputIterator != inputMultiplicities.cend()) {
+                if (marking.getNumberOfTokensAt(inputIterator->first) < inputIterator->second) {
+                    return false;
+                }
+
+                ++inputIterator;
+            }
+
+            auto inhibitionIterator = inhibitionMultiplicities.cbegin();
+            while (inhibitionIterator != inhibitionMultiplicities.cend()) {
+                if (marking.getNumberOfTokensAt(inhibitionIterator->first) >= inhibitionIterator->second) {
+                    return false;
+                }
+
+                ++inhibitionIterator;
+            }
+
+            return true;
+        }
+
+        storm::gspn::Marking Transition::fire(const storm::gspn::Marking marking) {
+            //check if transition is enabled
+
+            return gspn::Marking(0, 0);
+        }
+    }
+}

src/storage/gspn/Transition.h

@@ -0,0 +1,116 @@
+#ifndef STORM_TRANSITION_H
+#define STORM_TRANSITION_H
+
+#include <map>
+#include "Marking.h"
+
+namespace storm {
+    namespace gspn {
+        class Transition {
+        public:
+            /*!
+             * Set the multiplicity of the input arc originating from the place.
+             * If the arc already exists, the former multiplicity is overwritten.
+             * If the arc does not yet exists, it is created.
+             *
+             * @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);
+
+            /*!
+             * Removes an input arc connected to a given place.
+             *
+             * @param place The place from which the input arc is originating.
+             * @return True if the arc existed.
+             */
+            bool removeInputArc(uint_fast64_t place);
+
+            /*!
+             * Checks whether the given place is connected to this transition via an input arc.
+             *
+             * @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);
+
+            /*!
+             * Set the multiplicity of the output arc going to the place.
+             * If the arc already exists, the former multiplicity is overwritten.
+             * If the arc does not yet exists, it is created.
+             *
+             * @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);
+
+            /*!
+             * Removes an output arc connected to a given place.
+             *
+             * @param place The place from which the output arc is leading to.
+             * @return True if the arc existed.
+             */
+            bool removeOutputArc(uint_fast64_t place);
+
+            /*!
+             * Checks whether the given place is connected to this transition via an output arc.
+             *
+             * @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);
+
+            /*!
+             * Set the multiplicity of the inhibition arc originating from the place.
+             * If the arc already exists, the former multiplicity is overwritten.
+             * If the arc does not yet exists, it is created.
+             *
+             * @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);
+
+            /*!
+             * Removes an inhibition arc connected to a given place.
+             *
+             * @param place The place from which the inhibition arc is originating.
+             * @return True if the arc existed.
+             */
+            bool removeInhibitionArc(uint_fast64_t place);
+
+            /*!
+             * Checks whether the given place is connected to this transition via an inhibition arc.
+             *
+             * @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);
+
+            /*!
+             * Checks if the given marking enables the transition.
+             *
+             * @return True if the transition is enabled.
+             */
+            bool isEnabled(storm::gspn::Marking marking);
+
+            /*!
+             * Fire the transition if possible.
+             *
+             * @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);
+        private:
+            // maps places connected to this transition with an input arc to the corresponding multiplicity
+            std::map<uint_fast64_t, uint_fast64_t> inputMultiplicities;
+
+            // maps places connected to this transition with an output arc to the corresponding multiplicities
+            std::map<uint_fast64_t, uint_fast64_t> outputMultiplicities;
+
+            // maps places connected to this transition with an inhibition arc to the corresponding multiplicity
+            std::map<uint_fast64_t, uint_fast64_t> inhibitionMultiplicities;
+        };
+    }
+}
+
+#endif //STORM_TRANSITION_H