The marking graph of a Petri net describes all reachable states (markings) in terms of a transition system. Transitions of a transition system represent the firing of Petri net transitions, transition system events denote markings. Each sequence which reaches a final state (drain) represents a complete sequence of activities in the Petri net. Figure 6 shows the marking graph of the Petri net visualized in figure 5.
Figure 6: Marking graph of the P/T-Net example from the Petri net traversal in figure 5.
To build the marking graph of a Petri net the following method can be used:
PTMarkingGraph mg = MGConstruction.buildMarkingGraph(ptnet);
To get the corresponding sequences the sequence generator can be used:
SequenceGenerationCallableGenerator generator =
new SequenceGenerationCallableGenerator(ptnet);
MGTraversalResult res = SequenceGeneration.getFiringSequences(generator);
The sequences which result in a final state can be retrieved by
res.getCompleteSequences();
The result is the same as in the traversal example in section 3:
[t2, t2, t3, t3], [t2, t3, t2, t3], [t1, t3]
All possible sequences, including those not resulting in a final state, are returned by
res.getSequences();
The corresponding sequences are
[t2, t3], [t2, t2, t3, t3], [t2, t2], [t2], [t1], [t2, t3, t2, t3], [t1, t3], [t2, t2, t3], [t2, t3, t2]
The marking graph is also used to check for the boundedness property on a Petri net. If the number of possible sequences is finite or smaller than the maximum possible value for the integer data type, the Petri net is bounded. Otherwise the Petri net is assumed to be unbounded.