2.2.9.3. causality/Petri.hpp¶

2.2.9.3.1. Class `causality::PetriNet`¶

class causality::PetriNet¶: Adaptation of a derivation graph into a Petri net. Importantly, if the underlying derivation graph is enlarged then syncSize() must be called before calling certain other methods on the object.

2.2.9.3.1.1. Synopsis¶

class MOD_DECL PetriNet {
    explicit PetriNet(std::shared_ptr<dg::DG> dg_);
public:
    ~PetriNet();
    std::shared_ptr<dg::DG> getDG() const;
    const lib::causality::PetriNet &getNet() const;
    void syncSize();
    std::vector<dg::DG::Vertex> getPostPlaces(dg::DG::HyperEdge e) const;
public:
    static std::shared_ptr<PetriNet> make(std::shared_ptr<dg::DG> dg_);
private:
    struct Pimpl;
    std::unique_ptr<Pimpl> p;
};

2.2.9.3.1.2. Details¶

std::shared_ptr<dg::DG> getDG() const¶

Returns: the underlying derivation graph.

void syncSize()¶: Enlarges the internal data structures to the current size of the underlying derivation graph.

std::vector<dg::DG::Vertex> getPostPlaces(dg::DG::HyperEdge e) const¶

Returns: a list of unique targets for the given hyperedge.

Requires syncSize() to have been called since the last time the underlying derivation graph has changed size.

static std::shared_ptr<PetriNet> make(std::shared_ptr<dg::DG> dg_)¶

Calls syncSize().

Returns: a new Petri net, adapting the given derivation graph.
Throws: LogicError if dg_ is null.
Throws: LogicError if neither dg_->hasActiveBuilder() nor dg_->isLocked().

2.2.9.3.2. Class `causality::PetriNetMarking`¶

class causality::PetriNetMarking¶: Representation of a marking on a Petri net. Importantly, if the underlying derivation graph is enlarged then syncSize() must be called before calling certain other methods on the object.

2.2.9.3.2.1. Synopsis¶

struct MOD_DECL PetriNetMarking {
    explicit PetriNetMarking(std::shared_ptr<PetriNet> net);
    // pre: &net->getNet() == &marking.getNet()
    explicit PetriNetMarking(std::shared_ptr<PetriNet> net, const lib::causality::PetriNetMarking &marking);
    ~PetriNetMarking();
    PetriNetMarking(PetriNetMarking&&);
    PetriNetMarking &operator=(PetriNetMarking&&);
    PetriNetMarking(const PetriNetMarking&);
    PetriNetMarking &operator=(const PetriNetMarking&);
    std::shared_ptr<PetriNet> getNet() const;
    const lib::causality::PetriNetMarking &getMarking() const;
    void syncSize();
    MOD_DECL friend std::ostream &operator<<(std::ostream &s, const PetriNetMarking &m);
    int add(dg::DG::Vertex v, int c);
    int remove(dg::DG::Vertex v, int c);
    int operator[](dg::DG::Vertex v) const;
    int getNumTokens() const;
    std::vector<dg::DG::HyperEdge> getAllEnabled() const;
    std::vector<dg::DG::Vertex> getNonZeroPlaces() const;
    std::vector<dg::DG::Vertex> getEmptyPostPlaces(dg::DG::HyperEdge e) const;
    bool isEnabled(dg::DG::HyperEdge e) const;
    void fire(dg::DG::HyperEdge e);
private:
    struct Pimpl;
    std::unique_ptr<Pimpl> p;
};

2.2.9.3.2.2. Details¶

explicit PetriNetMarking(std::shared_ptr<PetriNet> net)¶

Throws: LogicError if net is null.

std::shared_ptr<PetriNet> getNet() const¶

Returns: the underlying Petri net.

void syncSize()¶

Enlarges the internal data structures to the current size of the underlying derivation graph.

Calls getNet().syncSize().

friend std::ostream &operator<<(std::ostream &s, const PetriNetMarking &m)¶: Requires syncSize() to have been called since the last time the underlying derivation graph has changed size.

int add(dg::DG::Vertex v, int c)¶

Add c tokens on the place v.

Returns: the new total token count on v.
Throws: LogicError if !v.
Throws: LogicError if v.getDG() != getNet()->getDG().
Throws: LogicError if c < 0.

Requires syncSize() to have been called since the last time the underlying derivation graph has changed size.

int remove(dg::DG::Vertex v, int c)¶

Remove c tokens from the place v.

Returns: the new total token count on v.
Throws: LogicError if !v.
Throws: LogicError if v.getDG() != getNet()->getDG().
Throws: LogicError if c < 0.
Throws: LogicError if not enough tokens are left to remove all c.

Requires syncSize() to have been called since the last time the underlying derivation graph has changed size.

int operator[](dg::DG::Vertex v)¶

Returns: the token count for v.
Throws: LogicError if !v.
Throws: LogicError if v.getDG() != getNet()->getDG().

Requires syncSize() to have been called since the last time the underlying derivation graph has changed size.

int getNumTokens() const¶

Returns: the total number of tokens in the marking.

std::vector<dg::DG::HyperEdge> getAllEnabled() const¶

Returns: a list of all hyperedges currently enabled for firing.

std::vector<dg::DG::Vertex> getNonZeroPlaces() const¶

Returns: a list of all vertices with tokens.

std::vector<dg::DG::Vertex> getEmptyPostPlaces(dg::DG::HyperEdge e) const¶

Returns: a list of all target vertices of the given hyperedge that do not have any tokens. The list represents a set, so if vertex is a target multiple times it will only be included once.
Throws: LogicError if !e.
Throws: LogicError if e.getDG() != getNet()->getDG().

bool isEnabled(dg::DG::HyperEdge e) const¶

Returns: whether the given hyperedge is enabled for firing.
Throws: LogicError if !e.
Throws: LogicError if e.getDG() != getNet()->getDG().

void fire(dg::DG::HyperEdge e)¶

Fire the given edge.

Throws: LogicError if !e.
Throws: LogicError if e.getDG() != getNet()->getDG().
Throws: LogicError if !isEnabled(e).

2.2.9.3. causality/Petri.hpp¶

2.2.9.3.1. Class causality::PetriNet¶

2.2.9.3.1.1. Synopsis¶

2.2.9.3.1.2. Details¶

2.2.9.3.2. Class causality::PetriNetMarking¶

2.2.9.3.2.1. Synopsis¶

2.2.9.3.2.2. Details¶

2.2.9.3.1. Class `causality::PetriNet`¶

2.2.9.3.2. Class `causality::PetriNetMarking`¶