Tutorial for the untimed Petri net toolbox

Here, we present the functionalities of the untimed_pn toolbox, which allows to analyze and control untimed Petri nets. The first thing to do is to import the untimed_pn module from folder petritub:

from petritub.untimed_pn import *

# the following line is just to display plots inline -- you can ignore it
#%matplotlib inline

Analysis of Petri nets

In the following example we will be analyzing the Petri net shown below using various functions of the untimed_pn library for untimed Petri nets.

Petri net from exercise sheet 02. DES 2021/22, TU Berlin.

Petri nets in Python

First of all we have to create an object of the PetriNet class. To initialize a Petri net we need to pass it its initial marking, vector \(x^0\), and two matrices \(A^+\) and \(A^-\) (such that the incidence matrix is \(A = A^+ - A^-\)). These arguments have to be 2D numpy arrays.

Aplus = np.array([[0, 0, 1, 0, 0, 0],
                  [1, 0, 0, 1, 0, 0],
                  [0, 1, 0, 0, 0, 0],
                  [1, 0, 0, 1, 0, 0],
                  [0, 0, 0, 0, 1, 1]])

Aminus = np.array([[1, 0, 0, 0, 0, 0],
                   [0, 1, 1, 0, 0, 0],
                   [0, 0, 1, 1, 0, 0],
                   [0, 0, 0, 1, 1, 0],
                   [0, 0, 0, 0, 0, 1]])
x0 = np.array([[1],
               [0],
               [0],
               [0],
               [0]])

Now we can create the PetriNet object.

examplePN = PetriNet(Aplus, Aminus, x0)

Attributes of a Petri net

The incidence matrix and the initial marking vector of our Petri net are now saved as its attributes. We can easily access them and print them out.

print("Matrix A+:\n", examplePN.Aplus, "\n")
print("Matrix A-:\n", examplePN.Aminus, "\n")
print("Incidence matrix A:\n", examplePN.A, "\n")
print("Initial marking vector:\n", examplePN.x0, "\n")

Matrix A+:
 [[0. 0. 1. 0. 0. 0.]
 [1. 0. 0. 1. 0. 0.]
 [0. 1. 0. 0. 0. 0.]
 [1. 0. 0. 1. 0. 0.]
 [0. 0. 0. 0. 1. 1.]]

Matrix A-:
 [[1. 0. 0. 0. 0. 0.]
 [0. 1. 1. 0. 0. 0.]
 [0. 0. 1. 1. 0. 0.]
 [0. 0. 0. 1. 1. 0.]
 [0. 0. 0. 0. 0. 1.]]

Incidence matrix A:
 [[-1  0  1  0  0  0]
 [ 1 -1 -1  1  0  0]
 [ 0  1 -1 -1  0  0]
 [ 1  0  0  0 -1  0]
 [ 0  0  0  0  1  0]]

Initial marking vector:
 [[1.]
 [0.]
 [0.]
 [0.]
 [0.]]

Coverability tree

Next we want to draw the coverability tree of this Petri net. We call the drawCoverabilityTree() function, which computes the coverability tree and displays the resulting graph. If we also want to save the graph as a pdf file, we can pass a string as an argument to the function and it will use it as a name for that file and save it.

examplePN.drawCoverabilityTree("figures/exampleCT")

Boundedness

In this case we can see directly from the coverability tree that the Petri net is bounded as there is no \(\omega\) signifying an infinite growth. Alternatively, we can use the isBounded() method, which returns True if a Petri net is bounded and False if it is not.

examplePN.isBounded()

True

As expected – our Petri net is bounded.

Liveness

There are two functions for checking the liveness of transitions in a given Petri net. Calling printLiveDeadTransitions() will print out a list of L1-live transitions and a list of dead transitions.

examplePN.printLiveDeadTransitions()

L1-live transitions:
T1 T2 T4 T5 T6

Dead transitions:
T3

This means that all the transitions in our Petri net with the initial marking vector \(x_0\) are at least L1-live except for \(t_3\) which is dead. In the current state, the toolbox is not able to differentiate among other types of liveness (L2-liveness, L3-liveness, and liveness).

If we want to check whether a specific transition is dead, we can use the isTransitionDead() method and pass it the number of the transition as an integer argument. It will return True if the given transition is dead and False if it is at least L1-live.

examplePN.isTransitionDead(1)

False

examplePN.isTransitionDead(3)

True

Coverability

We can check if a state is coverable by a Petri net with the function isStateCovered(). The vector representing the state must be a 2D \(\mathrm{m}\times 1\) numpy array, where \(\mathrm{m}\) is the number of places in the Petri net. The function will return True if that state is coverable and False if it is not. We will now evaluate the coverability of two different states.

state1 = np.array([[0],
                   [1],
                   [0],
                   [0],
                   [0]])

state2 = np.array([[1],
                   [1],
                   [0],
                   [0],
                   [0]])

examplePN.isStateCovered(state1)

True

examplePN.isStateCovered(state2)

False

As we can see, the first state is coverable by our Petri net whereas the second one is not.

Conservation

By using the isConservative() method we can check if the Petri net is conservative with respect to a given vector that we pass to the function as its argument. The vector must be a 2D \(\mathrm{m}\times 1\) numpy array. The method will return True if the Petri net is conservative with respect to that vector and False if it is not. Now we can check whether our Petri net is conservative with respect to the following two vectors.

gamma1 = np.array([[1],
                   [0],
                   [0],
                   [1],
                   [1]])

gamma2 = np.array([[0],
                   [0],
                   [1],
                   [1],
                   [0]])

examplePN.isConservative(gamma1)

True

examplePN.isConservative(gamma2)

False

As we can see the Petri net is conservative with respect to \(\gamma_1\) but is not conservative with respect to \(\gamma_2\). We remark that, at the moment, method isConservative only accepts non-negative vectors as inputs, and throws an error if a negative element exist.

New initial marking

Now we want to analyze the same Petri net but with different initial marking, as shown below.

Petri net from exercise sheet 02 with different initial marking. DES 2021/22, TU Berlin.

If we want to change the initial marking vector \(x_0\) of an already existing object of the Petri net class, we should use the setter function setInitialMarking() and pass it the new initial marking vector as an argument. The vector must be a 2D \(\mathrm{m}\times 1\) numpy array.

new_x0 = np.array([[0],
                   [1],
                   [1],
                   [0],
                   [1]])

examplePN.setInitialMarking(new_x0)

Now we can check that the attribute x0 of our Petri net object has been changed succesfully.

print("Initial marking vector:\n", examplePN.x0, "\n")

Initial marking vector:
 [[0.]
 [1.]
 [1.]
 [0.]
 [1.]]

We will now draw the coverability tree for the new initial marking and save it as “exampleCT_2.pdf” in folder figures.

examplePN.drawCoverabilityTree("figures/exampleCT_2")

We see that the coverability tree has changed quite a bit. Now we can analyze this Petri net using the same functions as with the previous initial marking and see if any other properties have changed.

examplePN.isBounded()

True

The Petri net is still bounded.

examplePN.printLiveDeadTransitions()

L1-live transitions:
T1 T2 T3 T4 T5 T6

Dead transitions:

Now there are no dead transitions meaning \(t_3\) is now at least L1-live while it was dead before.

examplePN.isStateCovered(state1)

True

examplePN.isStateCovered(state2)

False

Same as before, state1 is coverable by the Petri net but state2 is not.

examplePN.isConservative(gamma1)

False

examplePN.isConservative(gamma2)

False

Our Petri net is no longer conservative with respect to neither \(\gamma_1\) nor \(\gamma_2\).

State based control

Another important feature of the untimedPN toolbox is the computation of state based controllers for Petri nets. We will demonstrate how that can be done on a Petri net shown below.

Petri net from exercise sheet 04. DES 2021/22, TU Berlin.

Initializing the Petri net

Just like in the previous example, we have to write the \(A^+\) and \(A^-\) matrices and the initial marking vector \(x^0\) as 2D numpy arrays.

Aplus = np.array([[0, 0, 0, 0, 1],
                  [1, 1, 0, 0, 0],
                  [0, 0, 0, 0, 1],
                  [0, 0, 1, 0, 0],
                  [0, 0, 0, 1, 0]])

Aminus = np.array([[1, 1, 0, 0, 0],
                   [0, 0, 0, 1, 0],
                   [0, 0, 1, 0, 0],
                   [0, 0, 0, 1, 0],
                   [0, 0, 0, 0, 1]])

x0 = np.array([[1],
               [1],
               [2],
               [0],
               [0]])

Now we create a new object of the PetriNet class.

examplePN2 = PetriNet(Aplus, Aminus, x0)

Specifications

When designing a state based controller, we want it to guarantee that the Petri net will behave according to given specification. The objective is to restrict the number of tokens in some places. This specifications are conventionally written in the form of inequalities:

\[\Gamma \cdot \mathrm{x(k)} \leq \mathrm{b}.\]

For this example let us say we want to ensure that the number of tokens in place \(p_5\) never exceeds 1. We can write this specification as follows:

\[\underbrace{\begin{bmatrix} 0 & 0 & 0 & 0 & 1\end{bmatrix}}_{\Gamma} \cdot \mathrm{x(k)} \leq \underbrace{1}_{\mathrm{b}}.\]

To use the matrices \(\Gamma\) and \(\mathrm{b}\) in our library they have to be written as 2D numpy arrays where \(\mathrm{b}\) is a column vector and therefore has the shape \(\mathrm{m}\times 1\).

Gamma = np.array([[0, 0, 0, 0, 1]])

b = np.array([[1]])

Controllable transitions

To be able to design a state controller we always need to know which transitions of the Petri net are controllable, which are uncontrollable but still observable and which are unobservable (and therefore also uncontrollable). Let us first assume that all of the transitions are controllable. This means we only need only \(\Gamma\) and \(\mathrm{b}\) to get the state based controller.

Computing the state based controller

The untimed_pn toolbox has a separate class for the state controllers. When we want to get a state based controller for a given Petri net, we call the function getStateController() for that PetriNet object with the correct arguments and it will create a new object of the class StateController. The incidence matrix, initial marking vector and other properties of the controller will be saved as attributes of that object. Now we create a controller for our Petri net with the given specification.

controller = examplePN2.getStateController(Gamma, b)

We can use the toString() method on a StateController object to print out the controller.

print(controller.toString())

State Controller (ideal case):
- Initial marking of the controller places:
[[1]]
- Controller matrix:
[[ 0  0  0 -1  1]]

This tells us that the specification was ideally enforceable and gives the initial marking vector \(x^0_c = \begin{bmatrix} 1 \end{bmatrix}\) and the controller matrix \(A_c = \begin{bmatrix} 0 & 0 & 0 & -1 & 1 \end{bmatrix}\).

Petri net from exercise sheet 04 with a controller. DES 2021/22, TU Berlin.

Uncontrollable and unobservable transitions

If there are any uncontrollable and/or unobservable transitions, we have to create lists with the numbers of these transitions, one for the uncontrollable but observable transitions and one for the uncontrollable and unobservable transitions. Now let us suppose that the transition \(t_4\) is observable but uncontrollable. We create a new state based controller using the same getStateController() function but now we add a list called trans_ouc as an additional argument. If there were any unobservable transitions, we would also add a list called trans_uouc with these transitions as an argument.

controllerUC = examplePN2.getStateController(Gamma, b, trans_ouc=[4])

Just like before we can use the toString method to print out the information about the new controller.

print(controllerUC.toString())

State Controller (non-ideal case):
- Initial marking of the controller places:
[[0]]
- Controller matrix:
[[-1 -1  0  0  1]]

We see that in this case the specification was not ideally enforceable and the initial marking vector as well as the controller matrix have changed. The initial marking vector is now \(x^0_c = \begin{bmatrix} 0 \end{bmatrix}\) and the new controller matrix is \(A_c = \begin{bmatrix} -1 & -1 & 0 & 0 & 1 \end{bmatrix}\).

Petri net from exercise sheet 04 with a controller. DES 2021/22, TU Berlin.

Multiple state controllers

In the non-ideal case, sometimes one specification can be enforced by different, equally restrictive, state based controllers. If we set the argument multipleCtrls of the getStateController() function to True, the algorithm computing the controller will save the properties of the first computed controller as the attributes of the StateController object (so that we can access and use that controller later) but it will then try to find other possible controllers and directly print them out, including the first one.

controllerUC = examplePN2.getStateController(Gamma, b, multipleCtrls = True, trans_ouc=[4])

Option 1:
 State Controller (non-ideal case):
- Initial marking of the controller places:
[[0]]
- Controller matrix:
[[-1 -1  0  0  1]]

Option 2:
 State Controller (non-ideal case):
- Initial marking of the controller places:
[[1]]
- Controller matrix:
[[ 0  0 -1  0  1]]

As we can see the algorithm found another controller with the initial marking vector \(x^0_c = \begin{bmatrix} 1 \end{bmatrix}\) and the controller matrix \(A_c = \begin{bmatrix} 0 & 0 & -1 & 0 & 1 \end{bmatrix}\).