From df7b29ef183044b8d1046412ca0568ae5a017dde Mon Sep 17 00:00:00 2001 From: ThomasH Date: Tue, 20 Oct 2015 23:08:44 +0200 Subject: [PATCH] partial implementation of gspns, transitions and markings Former-commit-id: 77d76d6c8990e8a688479d87466592527ef185f5 --- src/storage/gspn/GSPN.h | 17 +++- src/storage/gspn/ImmediateTransition.h | 35 ++++++++ src/storage/gspn/Marking.cpp | 43 +++++++++ src/storage/gspn/Marking.h | 66 ++++++++++++++ src/storage/gspn/TimedTransition.h | 36 ++++++++ src/storage/gspn/Transition.cpp | 85 ++++++++++++++++++ src/storage/gspn/Transition.h | 116 +++++++++++++++++++++++++ 7 files changed, 397 insertions(+), 1 deletion(-) create mode 100644 src/storage/gspn/ImmediateTransition.h create mode 100644 src/storage/gspn/Marking.cpp create mode 100644 src/storage/gspn/Marking.h create mode 100644 src/storage/gspn/TimedTransition.h create mode 100644 src/storage/gspn/Transition.cpp create mode 100644 src/storage/gspn/Transition.h diff --git a/src/storage/gspn/GSPN.h b/src/storage/gspn/GSPN.h index d3dab888d..09889be8d 100644 --- a/src/storage/gspn/GSPN.h +++ b/src/storage/gspn/GSPN.h @@ -1,13 +1,28 @@ #ifndef STORM_GSPN_H #define STORM_GSPN_H +#include +#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> immediateTransitions; + + // set containing all timed transitions + std::set> timedTransitions; + // initial marking + storm::gspn::Marking initialMarking; }; } } diff --git a/src/storage/gspn/ImmediateTransition.h b/src/storage/gspn/ImmediateTransition.h new file mode 100644 index 000000000..d3c29129e --- /dev/null +++ b/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 + 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 diff --git a/src/storage/gspn/Marking.cpp b/src/storage/gspn/Marking.cpp new file mode 100644 index 000000000..1e6192e3e --- /dev/null +++ b/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; + } + } +} \ No newline at end of file diff --git a/src/storage/gspn/Marking.h b/src/storage/gspn/Marking.h new file mode 100644 index 000000000..0eda58f03 --- /dev/null +++ b/src/storage/gspn/Marking.h @@ -0,0 +1,66 @@ +#ifndef STORM_MARKING_H +#define STORM_MARKING_H + +#include + +#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 diff --git a/src/storage/gspn/TimedTransition.h b/src/storage/gspn/TimedTransition.h new file mode 100644 index 000000000..86e0b3451 --- /dev/null +++ b/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 + 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 diff --git a/src/storage/gspn/Transition.cpp b/src/storage/gspn/Transition.cpp new file mode 100644 index 000000000..7e1b6ed8f --- /dev/null +++ b/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); + } + } +} diff --git a/src/storage/gspn/Transition.h b/src/storage/gspn/Transition.h new file mode 100644 index 000000000..986c7a48a --- /dev/null +++ b/src/storage/gspn/Transition.h @@ -0,0 +1,116 @@ +#ifndef STORM_TRANSITION_H +#define STORM_TRANSITION_H + +#include +#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 inputMultiplicities; + + // maps places connected to this transition with an output arc to the corresponding multiplicities + std::map outputMultiplicities; + + // maps places connected to this transition with an inhibition arc to the corresponding multiplicity + std::map inhibitionMultiplicities; + }; + } +} + +#endif //STORM_TRANSITION_H \ No newline at end of file