P/T-Nets: Place/Transition Nets | Tool Documentation

P/T-Nets are basic Petri nets, which can be represented as graphs with places and tran- sitions as two different kinds of vertices. The vertices are connected with flow relations, where places can only be connected to transitions and vice versa. Places can contain tokens and the assignment of tokens to places is called a marking.

The dynamic behaviour of a Petri net lies in the firing of transitions, which removes tokens from input places and generates new tokens in places connected via outgoing flow relations. The number of required tokens in input places for firing and generated tokens in output places are specified via constraints (number and type of transported tokens) of corresponding flow relations.

The following code sample shows how a P/T-Net consisting of two transitions and two places linearly connected by flow relations can be created.

PTNet ptnet = new PTNet();
ptnet.addPlace("p1");
ptnet.addPlace("p2");
ptnet.addTransition("t1");
ptnet.addTransition("t2");
ptnet.addFlowRelationPT("p1", "t1", 2);
ptnet.addFlowRelationTP("t1", "p2", 1);
ptnet.addFlowRelationPT("p2", "t2", 1);

As specified in the flow relation the transition requires two tokens in the place to be able to fire. For this some tokens must be added to the place by defining a marking.

PTMarking ptmarking = new PTMarking();
ptmarking.set("p1", 2);
ptnet.setInitialMarking(ptmarking);

Now the transition t1 is enabled and can be fired: if (ptnet.getTransition(“t1”).isEnabled())

    ptnet.getTransition("t1").fire();

This leads the place p1 to contain no more tokens. Instead the transition created a new token in p2, s.th. the transition t2 can be fired now.

Figure 2 shows the example P/T-Net.

Figure 2: Visualization of the P/T-Net used in the example.

We can check for validity and get some topological information of the net. A P/T-Net is valid, if its structure makes sense, e.g. flow relations don’t connect two places or vice versa. A valid P/T-Net is also sound. These properties can be verified using the corresponding property checker. They are either located in the sub-package properties in the package petrinet or in the sub-package of the respective Petri net type. The following code checks the validity and soundness of a Petri net and returns its boundedness. If the Petri net is not valid or not sound, an exception is thrown.

// Check validity (throws exception if invalid)
PTNetValidity.checkValidity(ptnet);
// Check soundness (throws exception if invalid)
PTNetSoundness.checkSoundness(ptnet, false);
BoundednessCheckResult boundedness = BoundednessCheck.getBoundedness(ptnet);
System.out.println(boundedness);
// Number of outgoing relations from the place:
System.out.println(ptnet.getPlace("p1").outDegree());
// Are there enough tokens in the input places?
System.out.println(ptnet.getTransition("t1").isEnabled());

The computation of some of the properties can be costly and tedious. Therefore some of the property checks can be executed asynchronously, by what it is not necessary anymore to wait for the programs response. For that the Observer Pattern is used. The asynchronous boundedness check can be performed by creating an appropriate listener, which is shown in the following code:

BoundednessCheck.initiateBoundednessCheck(ptnet, new
        ExecutorListener>() {

    @Override
    public void executorStarted() {}

    @Override
    public void executorStopped() {}

    @Override
    public void executorFinished(BoundednessCheckResult result) {
        System.out.println( result.getBoundedness() );
    }

    @Override
    public void executorException(Exception e) {}

    @Override
    public void progress(double progress) {}
});

The method executorStart is called when the computation of the property gets started. If the execution was successful, the method executorFinished gets called.