GSPN.h

Go to the documentation of this file.

#pragma once
 
#include <stdint.h>
#include <iostream>
#include <memory>
#include <unordered_map>
#include <vector>
 
#include "storm/storage/expressions/ExpressionManager.h"
 
#include "storm-gspn/storage/gspn/ImmediateTransition.h"
#include "storm-gspn/storage/gspn/Marking.h"
#include "storm-gspn/storage/gspn/Place.h"
#include "storm-gspn/storage/gspn/PlacementInfo.h"
#include "storm-gspn/storage/gspn/TimedTransition.h"
#include "storm-gspn/storage/gspn/TransitionPartition.h"
 
namespace storm {
namespace gspn {
// Stores a GSPN
class GSPN {
   public:
    static uint64_t timedTransitionIdToTransitionId(uint64_t);
    static uint64_t immediateTransitionIdToTransitionId(uint64_t);
    static uint64_t transitionIdToTimedTransitionId(uint64_t);
    static uint64_t transitionIdToImmediateTransitionId(uint64_t);
 
    // Later, the rates and probabilities type should become a template, for now, let it be doubles.
    typedef double RateType;
    typedef double WeightType;
 
    GSPN(std::string const& name, std::vector<Place> const& places, std::vector<ImmediateTransition<WeightType>> const& itransitions,
         std::vector<TimedTransition<RateType>> const& ttransitions, std::vector<TransitionPartition> const& partitions,
         std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager,
         std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution =
             std::map<storm::expressions::Variable, storm::expressions::Expression>());
 
    uint64_t getNumberOfPlaces() const;
 
    uint64_t getNumberOfImmediateTransitions() const;
 
    uint64_t getNumberOfTimedTransitions() const;
 
    std::vector<TransitionPartition> const& getPartitions() const;
 
    std::vector<TimedTransition<GSPN::RateType>> const& getTimedTransitions() const;
 
    std::vector<ImmediateTransition<GSPN::WeightType>> const& getImmediateTransitions() const;
 
    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<uint64_t, uint64_t>& numberOfBits, uint64_t const& numberOfTotalBits) const;
 
    storm::gspn::Place const* getPlace(uint64_t id) const;
 
    storm::gspn::Place const* getPlace(std::string const& name) const;
 
    storm::gspn::TimedTransition<GSPN::RateType> const* getTimedTransition(std::string const& name) const;
 
    storm::gspn::ImmediateTransition<GSPN::WeightType> const* getImmediateTransition(std::string const& name) const;
 
    storm::gspn::Transition const* getTransition(std::string const& name) const;
 
    void writeDotToStream(std::ostream& outStream) const;
 
    void setName(std::string const& name);
 
    std::string const& getName() const;
 
    std::shared_ptr<storm::expressions::ExpressionManager> const& getExpressionManager() const;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> const& getConstantsSubstitution() const;
 
    void setCapacities(std::unordered_map<std::string, uint64_t> const& mapping);
 
    void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layout) const;
    void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layout) const;
    void setPlaceLayoutInfo(std::map<uint64_t, LayoutInfo> const& placeLayout) const;
    void setTransitionLayoutInfo(std::map<uint64_t, LayoutInfo> const& transitionLayout) const;
 
    std::map<uint64_t, LayoutInfo> const& getPlaceLayoutInfos() const;
 
    std::map<uint64_t, LayoutInfo> const& getTransitionLayoutInfos() const;
 
    bool isValid() const;
    // TODO doc
    void toPnpro(std::ostream& stream) const;
    // TODO doc
    void toPnml(std::ostream& stream) const;
 
    void toJson(std::ostream& stream) const;
 
    void writeStatsToStream(std::ostream& stream) const;
 
   private:
    storm::gspn::Place* getPlace(uint64_t id);
    storm::gspn::Place* getPlace(std::string const& name);
 
    bool testPlaces() const;
 
    bool testTransitions() const;
 
    // name of the gspn
    std::string name;
 
    // set containing all places
    std::vector<storm::gspn::Place> places;
 
    // set containing all immediate transitions
    std::vector<storm::gspn::ImmediateTransition<WeightType>> immediateTransitions;
 
    // set containing all timed transitions
    std::vector<storm::gspn::TimedTransition<RateType>> timedTransitions;
 
    std::vector<storm::gspn::TransitionPartition> partitions;
 
    std::shared_ptr<storm::expressions::ExpressionManager> exprManager;
 
    std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution;
 
    // Layout information
    mutable std::map<uint64_t, LayoutInfo> placeLayout;
    mutable std::map<uint64_t, LayoutInfo> transitionLayout;
};
}  // namespace gspn
}  // namespace storm