Package org.tweetyproject.logics.petri.syntax

Class PetriNet

java.lang.Object

org.tweetyproject.logics.petri.syntax.PetriNet

All Implemented Interfaces:

Iterable<PetriNetNode>, GeneralGraph<PetriNetNode>, Graph<PetriNetNode>

public class PetriNet
extends Object
implements Graph<PetriNetNode>

A class to represent a Petri net

Author:

Benedikt Knopp, Matthias Thimm

Field Summary

Fields inherited from interface org.tweetyproject.graphs.Graph

IGNORE_SELFLOOPS, INVERT_SELFLOOPS, REMOVE_SELFLOOPS

Constructor Summary

Constructors

Constructor	Description
PetriNet()	Default

Method Summary

Modifier and Type	Method	Description
boolean	add(Edge<PetriNetNode> edge)	Return add
boolean	add(GeneralEdge<PetriNetNode> edge)	Adds the given edge to this graph.
boolean	add(PetriNetNode node)	Adds the given node to this graph.
boolean	add(Place place)	Add a place to the Petri net
boolean	add(Transition transition)	Add a transition to the Petri net
boolean	addInitialMarking(Marking initialMarking)	add a designated initial marking
boolean	areAdjacent(PetriNetNode a, PetriNetNode b)	Returns "true" iff the two nodes are connected by a directed edge from a to b or an undirected edge.
boolean	checkShortCircuit()	check if this Petri net is short-circuited
boolean	contains(Object obj)	Returns "true" when this graph contains the given node or edge.
Transition	createEmptyTransition(Marking marking)	Add a transition which is enabled at the specified marking and does not change the marking
boolean	existsDirectedPath(PetriNetNode node1, PetriNetNode node2)	Checks whether there is a (directed) path from node1 to node2.
void	fire(Transition transition)	Fire
Matrix	getAdjacencyMatrix()	Returns the adjacency matrix of this graph (the order of the nodes is the same as returned by "iterator()").
Collection<PetriNetNode>	getChildren(Node node)	Returns the set of children (node connected via an undirected edge or a directed edge where the given node is the parent) of the given node.
Graph<PetriNetNode>	getComplementGraph(int selfloops)	Returns the complement graph of this graph, i.e.
Edge<PetriNetNode>	getEdge(PetriNetNode a, PetriNetNode b)	Returns the corresponding edge (a,b) if a and b are adjacent.
Set<Edge<PetriNetNode>>	getEdges()	Returns the edges of this graph.
Set<Transition>	getEnabledTransitions()	Retrieve the transitions that are enabled in the current state (token distribution) of the net
Set<Marking>	getInitialMarkings()	Return the initialMarkings
Marking	getMarking()	Get the marking of this graph, based on the current token distribution at the places
Collection<PetriNetNode>	getNeighbors(PetriNetNode node)	Returns the set of neighbors of the given node.
Set<PetriNetNode>	getNodes()	Returns the nodes of this graph.
int	getNumberOfEdges()	Returns the number of edges in this graph.
int	getNumberOfNodes()	Returns the number of nodes in this graph.
Collection<PetriNetNode>	getParents(Node node)	Returns the set of parents (node connected via an undirected edge or a directed edge where the given node is the child) of the given node.
List<Place>	getPlaces()	Return the places
Graph<PetriNetNode>	getRestriction(Collection<PetriNetNode> nodes)	Returns a copy of this graph that contains only the specified nodes and all corresponding edges between them.
Collection<Collection<PetriNetNode>>	getStronglyConnectedComponents()	Returns the strongly connected components of this graph.
Collection<Graph<PetriNetNode>>	getSubgraphs()	Returns the set of sub graphs of this graph.
List<Transition>	getTransitions()	Return the transitions
boolean	hasSelfLoops()	Returns "true" iff the graph has a self loop (an edge from a node to itself).
boolean	isInitial(Marking marking)	Check whether the marking is an initial marking
boolean	isWeightedGraph()	Checks whether this graph only contains weighted edges.
Iterator<PetriNetNode>	iterator()
void	setEdges(Set<Edge<PetriNetNode>> edges)	Setter Edges
void	setPlaces(List<Place> places)	Setter places
void	setState(Marking marking)	Set the state (token distribution) according to the provided marking
void	setTransitions(List<Transition> transitions)	Setter transitions
void	transformToShortCircuit()	Transform the Petri net to the short-circuited version, where the final place and initial place are linked via a transition

Methods inherited from class java.lang.Object

equals, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Methods inherited from interface org.tweetyproject.graphs.Graph

toString

Methods inherited from interface java.lang.Iterable

forEach, spliterator

Constructor Details

PetriNet

public PetriNet()

Default

Method Details

add

public boolean add(PetriNetNode node)

Description copied from interface: Graph

Adds the given node to this graph.

Specified by:

add in interface Graph<PetriNetNode>

Parameters:

node - some node.

Returns:

"true" iff the edge has been added successfully.

add

public boolean add(Place place)

Add a place to the Petri net

Parameters:

place - the place

Returns:

true iff adding the place was successful

add

public boolean add(Transition transition)

Add a transition to the Petri net

Parameters:

transition - the transition

Returns:

true iff adding the transition was successful

add

public boolean add(Edge<PetriNetNode> edge)

Return add

Parameters:

edge - add

Returns:

add

getNodes

public Set<PetriNetNode> getNodes()

Description copied from interface: Graph

Returns the nodes of this graph.

Specified by:

getNodes in interface GeneralGraph<PetriNetNode>

Specified by:

getNodes in interface Graph<PetriNetNode>

Returns:

the nodes of this graph.

getNumberOfNodes

public int getNumberOfNodes()

Description copied from interface: Graph

Returns the number of nodes in this graph.

Specified by:

getNumberOfNodes in interface Graph<PetriNetNode>

Returns:

the number of nodes in this graph.

getNumberOfEdges

public int getNumberOfEdges()

Description copied from interface: Graph

Returns the number of edges in this graph.

Specified by:

getNumberOfEdges in interface Graph<PetriNetNode>

Returns:

the number of edges in this graph.

areAdjacent

public boolean areAdjacent(PetriNetNode a,
 PetriNetNode b)

Description copied from interface: Graph

Returns "true" iff the two nodes are connected by a directed edge from a to b or an undirected edge.

Specified by:

areAdjacent in interface Graph<PetriNetNode>

Parameters:

a - some node

b - some node

Returns:

"true" iff the two nodes are connected by a directed edge from a to b or an undirected edge.

getEdge

public Edge<PetriNetNode> getEdge(PetriNetNode a,
 PetriNetNode b)

Description copied from interface: Graph

Returns the corresponding edge (a,b) if a and b are adjacent. Otherwise it returns null.

Specified by:

getEdge in interface Graph<PetriNetNode>

Parameters:

a - some node

b - some node

Returns:

the edge (a,b) or null.

getEdges

public Set<Edge<PetriNetNode>> getEdges()

Description copied from interface: Graph

Returns the edges of this graph.

Specified by:

getEdges in interface GeneralGraph<PetriNetNode>

Specified by:

getEdges in interface Graph<PetriNetNode>

Returns:

the edges of this graph.

getPlaces

public List<Place> getPlaces()

Return the places

Returns:

the places

getTransitions

public List<Transition> getTransitions()

Return the transitions

Returns:

the transitions

setPlaces

public void setPlaces(List<Place> places)

Setter places

Parameters:

places - the places to set

getInitialMarkings

public Set<Marking> getInitialMarkings()

Return the initialMarkings

Returns:

the initialMarkings

iterator

public Iterator<PetriNetNode> iterator()

Specified by:

iterator in interface Graph<PetriNetNode>

Specified by:

iterator in interface Iterable<PetriNetNode>

contains

public boolean contains(Object obj)

Description copied from interface: Graph

Returns "true" when this graph contains the given node or edge.

Specified by:

contains in interface Graph<PetriNetNode>

Parameters:

obj - an object

Returns:

"true" if this graph contains the given node or edge.

getChildren

public Collection<PetriNetNode> getChildren(Node node)

Description copied from interface: Graph

Returns the set of children (node connected via an undirected edge or a directed edge where the given node is the parent) of the given node.

Specified by:

getChildren in interface Graph<PetriNetNode>

Parameters:

node - some node (must be in the graph).

Returns:

the set of children of the given node.

getParents

public Collection<PetriNetNode> getParents(Node node)

Description copied from interface: Graph

Returns the set of parents (node connected via an undirected edge or a directed edge where the given node is the child) of the given node.

Specified by:

getParents in interface Graph<PetriNetNode>

Parameters:

node - some node (must be in the graph).

Returns:

the set of parents of the given node.

existsDirectedPath

public boolean existsDirectedPath(PetriNetNode node1,
 PetriNetNode node2)

Description copied from interface: Graph

Checks whether there is a (directed) path from node1 to node2.

Specified by:

existsDirectedPath in interface Graph<PetriNetNode>

Parameters:

node1 - some node.

node2 - some node.

Returns:

"true" if there is a directed path from node1 to node2.

getNeighbors

public Collection<PetriNetNode> getNeighbors(PetriNetNode node)

Description copied from interface: Graph

Returns the set of neighbors of the given node.

Specified by:

getNeighbors in interface Graph<PetriNetNode>

Parameters:

node - some node (must be in the graph).

Returns:

the set of neighbors of the given node.

getAdjacencyMatrix

public Matrix getAdjacencyMatrix()

Description copied from interface: Graph

Returns the adjacency matrix of this graph (the order of the nodes is the same as returned by "iterator()").

Specified by:

getAdjacencyMatrix in interface Graph<PetriNetNode>

Returns:

the adjacency matrix of this graph

getComplementGraph

public Graph<PetriNetNode> getComplementGraph(int selfloops)

Description copied from interface: Graph

Returns the complement graph of this graph, i.e. the graph on the same set of vertices as this graph that connects two vertices v and w with an edge if and only if v and w are not connected in this graph.

Specified by:

getComplementGraph in interface Graph<PetriNetNode>

Parameters:

selfloops - Indicates how to deal with selfloops:
IGNORE_SELFLOOPS - ignore self loops (don't add and don't remove)
INVERT_SELFLOOPS - deal with self loops like ordinary edges (add if not present and remove if present)
REMOVE_SELFLOOPS - simple remove self loops, but don't add new ones.

Returns:

the complement graph of this graph.

getStronglyConnectedComponents

public Collection<Collection<PetriNetNode>> getStronglyConnectedComponents()

Description copied from interface: Graph

Returns the strongly connected components of this graph. A set of nodes is strongly connected, if there is a path from each node to each other. A set of nodes is called strongly connected component if it is strongly connected and maximal with respect to set inclusion.

Specified by:

getStronglyConnectedComponents in interface Graph<PetriNetNode>

Returns:

the strongly connected components of this graph.

getSubgraphs

public Collection<Graph<PetriNetNode>> getSubgraphs()

Description copied from interface: Graph

Returns the set of sub graphs of this graph.

Specified by:

getSubgraphs in interface Graph<PetriNetNode>

Returns:

the set of sub graphs of this graph.

getRestriction

public Graph<PetriNetNode> getRestriction(Collection<PetriNetNode> nodes)

Description copied from interface: GeneralGraph

Returns a copy of this graph that contains only the specified nodes and all corresponding edges between them.

This method generates a subgraph (or restricted graph) from the current graph by including only the given nodes and the edges that connect them. The returned graph is a new instance and does not modify the original graph.

Specified by:

getRestriction in interface GeneralGraph<PetriNetNode>

Parameters:

nodes - a collection of nodes to be included in the restricted graph.

Returns:

a `GeneralGraph` object representing the restricted graph.

hasSelfLoops

public boolean hasSelfLoops()

Description copied from interface: Graph

Returns "true" iff the graph has a self loop (an edge from a node to itself).

Specified by:

hasSelfLoops in interface Graph<PetriNetNode>

Returns:

"true" iff the graph has a self loop (an edge from a node to itself).

isWeightedGraph

public boolean isWeightedGraph()

Description copied from interface: Graph

Checks whether this graph only contains weighted edges.

Specified by:

isWeightedGraph in interface Graph<PetriNetNode>

Returns:

"true" if all edges are weighted in this graph.

fire

public void fire(Transition transition)

Fire

Parameters:

transition - fire

getMarking

public Marking getMarking()

Get the marking of this graph, based on the current token distribution at the places

Returns:

the current marking

getEnabledTransitions

public Set<Transition> getEnabledTransitions()

Retrieve the transitions that are enabled in the current state (token distribution) of the net

Returns:

the enabled transitions

addInitialMarking

public boolean addInitialMarking(Marking initialMarking)

add a designated initial marking

Parameters:

initialMarking - the initial marking

Returns:

true iff adding the marking was successful

isInitial

public boolean isInitial(Marking marking)

Check whether the marking is an initial marking

Parameters:

marking - the marking

Returns:

true iff the marking is initial

setState

public void setState(Marking marking)

Set the state (token distribution) according to the provided marking

Parameters:

marking - the marking

add

public boolean add(GeneralEdge<PetriNetNode> edge)

Description copied from interface: Graph

Adds the given edge to this graph. If at least one of the nodes the given edge connects is not in the graph, an illegal argument exception is thrown.

Specified by:

add in interface Graph<PetriNetNode>

Parameters:

edge - some edge.

Returns:

"true" iff the edge has been added successfully.

createEmptyTransition

public Transition createEmptyTransition(Marking marking)

Add a transition which is enabled at the specified marking and does not change the marking

Parameters:

marking - the marking

Returns:

a empty transition

transformToShortCircuit

public void transformToShortCircuit()
                             throws IllegalStateException

Transform the Petri net to the short-circuited version, where the final place and initial place are linked via a transition

Throws:

IllegalStateException - if the transformation is not possible due to violations of syntactical requirements

setEdges

public void setEdges(Set<Edge<PetriNetNode>> edges)

Setter Edges

Parameters:

edges - the arks (edges)

setTransitions

public void setTransitions(List<Transition> transitions)

Setter transitions

Parameters:

transitions - the transitions

checkShortCircuit

public boolean checkShortCircuit()
                          throws IllegalStateException

check if this Petri net is short-circuited

Returns:

true if this Petri net is short-circuited

Throws:

IllegalStateException - if the number of initial and final places in this net is not equal to 1