org.processmining.framework.models.petrinet.algorithms
Class CoverabilityGraphBuilder

java.lang.Object
  extended by org.processmining.framework.models.petrinet.algorithms.CoverabilityGraphBuilder

public class CoverabilityGraphBuilder
extends java.lang.Object

A coverability graph is a finite state space model for a Petri net. If the reachability graph is finite already, the coverability graph is identical to it. However, is the reachability graph would be infinite (which may happen if a Petri net is accumulating tokens), the coverability graph introduces so-called Omega states in order to gain a final state space.

Note that this might lead to losing some information (such as if tokens are only accumulating in uneven numbers: 1,3,5,... --> becomes Omega).

This static class provides an implementation of the algorithm in definitions 3.36, 3.37 and 3.38 of "Verification of WF-nets", H.M.W. Verbeek, Technische Universiteit Eindhoven, 2004 (ISBN 90-386-1918-9)

The coverability graph is constructed via breadth-first search.

Author:
Boudewijn van Dongen

Constructor Summary
CoverabilityGraphBuilder()
           
 
Method Summary
static StateSpace build(PetriNet net)
          Constructs the full coverability graph for a given marked net.
static StateSpace build(PetriNet net, int depth)
          Constructs the coverability graph with a potentially limited depth for a given marked net.
 
Methods inherited from class java.lang.Object
clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait
 

Constructor Detail

CoverabilityGraphBuilder

public CoverabilityGraphBuilder()
Method Detail

build

public static StateSpace build(PetriNet net)
Constructs the full coverability graph for a given marked net. If a partial state space shall be constructed only, use build(PetriNet, int) instead.
Remembers the start state (that is, the marking of the given net) in the initialState attribute.

Parameters:
net - The marked net
Returns:
The coverability graph

build

public static StateSpace build(PetriNet net,
                               int depth)
Constructs the coverability graph with a potentially limited depth for a given marked net. If the full state space shall be constructed, use build(PetriNet) instead.
Remembers the start state (that is, the marking of the given net) in the initialState attribute.

Parameters:
net - The marked net
depth - The depth until which the state space should be constructed. If it is 0, only the initial state will be contained in the constructed state space. If it is 1, the initial state and all its direct successor states are constructed. If it is 2, all direct successor states of the previously constructed states are built as well etc.
Returns:
The coverability graph