|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |
java.lang.Objectorg.processmining.framework.models.petrinet.algorithms.CoverabilityGraphBuilder
public class CoverabilityGraphBuilder
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.
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 |
---|
public CoverabilityGraphBuilder()
Method Detail |
---|
public static StateSpace build(PetriNet net)
build(PetriNet, int)
instead.
initialState
attribute.
net
- The marked net
public static StateSpace build(PetriNet net, int depth)
build(PetriNet)
instead.
initialState
attribute.
net
- The marked netdepth
- 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.
|
||||||||||
PREV CLASS NEXT CLASS | FRAMES NO FRAMES | |||||||||
SUMMARY: NESTED | FIELD | CONSTR | METHOD | DETAIL: FIELD | CONSTR | METHOD |