GspnBuilder.h

Go to the documentation of this file.

#pragma once
 
#include <map>
#include <string>
#include <vector>
 
#include "GSPN.h"
 
namespace storm {
namespace gspn {
class GspnBuilder {
   public:
    typedef double RateType;
    typedef double WeightType;
 
    void setGspnName(std::string const& name);
 
    uint_fast64_t addPlace(boost::optional<uint64_t> const& capacity = 1, uint_fast64_t const& initialTokens = 0, std::string const& name = "");
 
    void setPlaceLayoutInfo(uint64_t placeId, LayoutInfo const& layoutInfo);
 
    uint_fast64_t addImmediateTransition(uint_fast64_t const& priority = 0, WeightType const& weight = 0, std::string const& name = "");
 
    uint_fast64_t addTimedTransition(uint_fast64_t const& priority, RateType const& rate, std::string const& name = "");
 
    uint_fast64_t addTimedTransition(uint_fast64_t const& priority, RateType const& rate, boost::optional<uint64_t> const& numServers,
                                     std::string const& name = "");
 
    void setTransitionLayoutInfo(uint64_t transitionId, LayoutInfo const& layoutInfo);
 
    void addInputArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity = 1);
 
    void addInputArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1);
    void addInhibitionArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity = 1);
 
    void addInhibitionArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1);
 
    void addOutputArc(uint_fast64_t const& from, uint_fast64_t const& to, uint_fast64_t const& multiplicity = 1);
 
    void addOutputArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1);
 
    void addNormalArc(std::string const& from, std::string const& to, uint64_t multiplicity = 1);
 
    storm::gspn::GSPN* buildGspn(std::shared_ptr<storm::expressions::ExpressionManager> const& exprManager = nullptr,
                                 std::map<storm::expressions::Variable, storm::expressions::Expression> const& constantsSubstitution =
                                     std::map<storm::expressions::Variable, storm::expressions::Expression>()) const;
 
   private:
    bool isImmediateTransitionId(uint64_t) const;
    bool isTimedTransitionId(uint64_t) const;
    Transition& getTransition(uint64_t);
 
    std::map<std::string, uint64_t> placeNames;
    std::map<std::string, uint64_t> transitionNames;
 
    std::string gspnName = "_gspn_";
 
    std::map<uint64_t, std::vector<storm::gspn::TransitionPartition>> partitions;
 
    // set containing all immediate transitions
    std::vector<storm::gspn::ImmediateTransition<WeightType>> immediateTransitions;
 
    // set containing all timed transitions
    std::vector<storm::gspn::TimedTransition<RateType>> timedTransitions;
 
    // set containing all places
    std::vector<storm::gspn::Place> places;
 
    std::map<uint64_t, LayoutInfo> placeLayout;
    std::map<uint64_t, LayoutInfo> transitionLayout;
};
}  // namespace gspn
}  // namespace storm