Untimed Petri nets toolbox

The module untimed_pn contains four classes – PetriNet, Node, CoverabilityTree and StateController.

Two have public functions (PetriNet and StateController) that can be used to analyze untimed Petri nets or to compute their state-based controller for a given specification.

Two are private (Node, CoverabilityTree) and only their attributes are documented on this page. For further information about their functions, see directly the untimed_pn module.

PetriNet

class petritub.untimed_pn.PetriNet(Aplus: ndarray, Aminus: ndarray, x0: ndarray)

Bases: object

Class that represents Petri net with the initial vector x0 and the matrices Aplus and Aminus.

Variables:

Aplus (np.ndarray) – The entries of this matrix represent the number of tokens that place p_i gains when transition t_j fires.
Aminus (np.ndarray) – The entries of this matrix represent the number of tokens that place p_i loses when transition t_j fires.
x0 (np.ndarray) – Initial marking vector.
A (np.ndarray) – Incidence matrix of the Petri net. Computed internally from matrices Aplus and Aminus.
_coverabilityTree (CoverabilityTree) – Instance of the class CoverabilityTree. If the coverability tree has not yet been calculated, the attribute has the value None.

Examples

To create an instance of the PetriNet class. Pass the matrices Aplus, Aminus and the initial marking vector (as a column vector).

>>> A_plus = np.array([[0, 1, 0, 1, 0],
...                    [0, 0, 0, 1, 0],
...                    [1, 0, 1, 0, 0],
...                    [0, 0, 1, 0, 1],
...                    [0, 0, 0, 1, 0]])
>>> A_minus = np.array([[1, 0, 0, 1, 0],
...                     [0, 0, 0, 0, 0],
...                     [0, 1, 1, 0, 0],
...                     [0, 0, 0, 1, 0],
...                     [0, 0, 0, 0, 1]])
>>> x0 = np.array([[1],
...                [0],
...                [0],
...                [0],
...                [0]])
>>> pn = PetriNet(A_plus, A_minus, x0)

closedLoop(controller: StateController) → PetriNet

Returns the Petri net representing the closed-loop system.

Computes the Petri net representing the closed-loop system formed by a PetriNet object, corresponding to the plant, and a StateController object, corresponding to the controller.

Parameters:: controller (StateController) – Controller computed using method getStateController() of the class PetriNet
Returns:: An object of the class PetriNet corresponding to the closed-loop system
Return type:: object of PetriNet

Examples

Assuming an object pn of the class PetriNet, and np.arrays Gamma and b has already been defined.

>>> controller = pn.getStateController(Gamma, b)
... cl_pn = closedLoop(pn, controller)

drawCoverabilityTree(name: str | None = None) → None

Draws the coverability tree of a Petri net.

Draws the coverability tree of a petri net as a matplotlib type plot using the networkx library. If the coverability tree has not been computed yet, it will do so automatically. Depending on the number of nodes the states will either be displayed as single column vectors or in a more compact, multiline vector form. If no parameter ist given, it will only display the coverability tree plot. If a name is given as a parameter, the plot will be saved in a PDF format.

Parameters:: name (str, optional) – Choose a name for the PDF file if you wish to save the drawn coverability tree, defaults to None and does not save the CT as a PDF if no name is given.
Returns:: This function only draws the CT and shows the plot, if parameter name is given, the resulting plot will be saved as a PDF.
Return type:: None

Examples

Assuming an object pn of the class PetriNet has already been created.

>>> pn.drawCoverabilityTree()

fire(transition_number: int) → None

Update the initial state of a Petri net by firing a transition.

Checks if it is possible to fire the given transition. If not, raises an error, otherwise, updates the initial state of the Petri net with the new marking obtained after firing the transition.

Parameters:: transition_number (int) – Number of transition to be fired, starting from 0.

Examples

Assuming an object pn of the class PetriNet has already been created, the following code simulates the firing of the first transition of pn and updates the initial state of pn accordingly (recall that Python is 0-based).

>>> pn.fire(0)

getStateController(Gamma: ndarray, b: ndarray, multipleCtrls: bool = False, trans_ouc: list[int] | None = None, trans_uouc: list[int] | None = None) → StateController

Computes the state controller of a Petri net.

Computes the state controller of a Petri net according to the given conditions and regarding the controllability and observability of all transitions. It then saves all its properties as its attributes which are reachable by the user through corresponding getter-methods.

Parameters:

Gamma (numpy.ndarray) – The Gamma matrix of the inequality defining the conditions for which the controller should be computed.
b (numpy.ndarray) – The b vector of the inequality defining the conditions for which the controller should be computed. Pass it to the function as a column vector.
multipleCtrls (bool, default False) – If set to True, the function will first compute a state controller and create the respective object of the StateController class but then print out the state controller and continue computing other possible controllers and printing out the new ones found. Maximum of 5 different controllers can be computed.
trans_ouc (list[int], optional) – A list of integers corresponding to all the observable but uncontrollable transitions of the Petri net, defaults to None.
trans_uouc (list[int], optional) – A list of integers corresponding to all the unobservable and therefore also uncontrollable transitions of the Petri net, defaults to None.

Returns:

An object of the clas StateController with the properties of the controller as the objects attributes.

Return type:

object of StateController

Examples

Assuming an object pn of the class PetriNet has already been created, in which transition t2 is observable but uncontrollabe, transitions t1 and t4 are unobservable and therefore uncontrollabe and the rest of transitions is observable and controllable.

>>> Gamma = np.array([[5, 2, 0, 0],
...                   [0, 0, 0, 1],
...                   [-1, 1, 0, 0]])
>>> b = np.array([[20],
...               [1],
...               [0]])
>>> controller = pn.getStateController(Gamma, b, trans_ouc=[2]},
...                                    trans_uouc=[1, 4])

isBounded() → bool

Checks the boundedness of a Petri net.

Checks if a Petri net is bounded using its coverability tree, seeing whether there are any unbounded places containing an omega. If the coverability tree has not been computed yet, it will do so automatically.

Parameters:: None –
Returns:: True if the Petri net is bounded, False if it is not bounded.
Return type:: bool

Examples

Assuming an object pn of the class PetriNet has already been created and the Petri net pn is not bounded.

>>> print(pn.isBounded())
False

isConservative(vector: ndarray) → bool

Checks the conservation of a Petri net.

Checks if the Petri net is conservative with respect to the given vector by using its coverability tree. If the coverability tree has not been computed yet, it will do so automatically.

Parameters:: vector (numpy.ndarray) – A vector with respect to which the conservation of a Petri net should be checked. Pass it to the function as a column vector.
Returns:: True if the Petri net is conservative with respect to the chosen vector, False if it is not.
Return type:: bool

Examples

Assuming an object pn of the class PetriNet has already been created and the Petri net pn is not conservative with respect to the vector [[1], [1], [0], [0]].

>>> vector = np.array([[1],
...                    [1],
...                    [0],
...                    [0]])
>>> print(pn.isConservative(vector))
False

isStateCovered(state: ndarray) → bool

Checks the coverability of a state.

Checks if the given state state is coverable by the Petri net by using its coverability tree. If the coverability tree has not been computed yet, it will do so automatically.

Parameters:: state (numpy.ndarray) – A vector which coverability should be checked. Pass it to the function as a column vector.
Returns:: True if the vector is coverable by the Petri net, False if it is not.
Return type:: bool

Examples

Assuming an object pn of the class PetriNet has already been created and the state [[1], [1], [0], [0]] is coverable by the Petri net pn.

>>> state = np.array([[1],
...                   [1],
...                   [0],
...                   [0]])
>>> print(pn.isStateCovered(state))
True

isTransitionDead(transition: int) → bool

Checks the liveness of a transition.

Checks the liveness of a given transition in the Petri for which this function is called using its coverability tree. This function does not differentiate between the specific types of live transitions as L1-live, L3-live and live. It solely tells you whether a transition is dead or not (i.e., at least L1-live). If the coverability tree has not been computed yet, it will do so automatically.

Parameters:: transition (int) – An integer value corresponding to the transition of which the liveness should be checked.
Returns:: True if the given transition is dead, False if it is at least L1-live.
Return type:: bool

Examples

Assuming an object pn of the class PetriNet has already been created, in which transition t1 is L3-live, transition t2 is live and transition t3 is dead.

>>> print(pn.isTransitionDead(1))
True
>>> print(pn.isTransitionDead(2))
True
>>> print(pn.isTransitionDead(3))
False

printLiveDeadTransitions() → None

Prints out a list of L1-live and a list of dead transitions.

Checks the liveness of each transition in a Petri net and prints out a list of live transitions and a list of dead transitions.

Parameters:: None –
Returns:: It automatically prints the lists out.
Return type:: None

Examples

Assuming an object pn of the class PetriNet has already been created, in which transition t1 is L3-live, transition t2 is live and transition t3 is dead.

>>> pn.printLiveDeadTransitions()
L1-live transitions:
T1 T2
Dead transitions:
T3

setInitialMarking(new_x0: ndarray) → None

Sets the initial marking vector of a Petri net.

Use this function if you want to change the initial marking vector x0 of an already existing Petri net. It will set the new initial marking vector as the attribute x0 of that Petri net and reset the coverability tree.

Parameters:: new_x0 (np.ndarray) – New initial marking vector.
Return type:: None

Examples

Assuming an object pn of the class PetriNet has already been created.

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

Node

final class petritub.untimed_pn.Node(state: ndarray, depth: int)

Bases: object

PRIVATE: Represents a node in a coverability tree. An instance has a state vector and additional information that is needed for coverability tree computation.

Variables:

_id (int) – Unique instance id.
_state (np.ndarray) – Numpy vector that represents marking.
_depth (int) – Depth of the node in the coverability tree, starting with 0 from the initial vector.
_duplicate (bool) – Tells if there exists a duplicate in the coverability tree.
_deadlock (bool) – Tells if the node is a deadlock.
_parent (Node | None) – Reference to the parent node. Set to “None” for the initial node.
_children (list[tuple[int, Node]]) – List of children nodes. Every child is tuple with following structure: (transition number to the child, child reference). If there are no children than the attribute is an empty list.
_trans_par (list[int]) – List of all parent transitions. A tree has only one parent per definition but identical children be created after firing different transitions. In this case, only one node will be created and multiple transitions will be stored. The list is empty for the initial node.

CoverabilityTree

final class petritub.untimed_pn.CoverabilityTree(initial_node: Node)

Bases: object

PRIVATE: Used to compute the coverability tree of a Petri Net.

Variables:

_initial_node (Node) – Initial markings of a Petri Net.
_unexplored (list[Node]) – List of all nodes yet to be explored.
_explored (list[Node]) – List of all explored nodes.
_fired_transitions (set[int]) – Set of all fired transition in the coverability tree.

StateController

final class petritub.untimed_pn.StateController(Gamma: ndarray, b: ndarray, A: ndarray, x0: ndarray, multipleCtrls: bool, trans_ouc: list[int] | None = None, trans_uouc: list[int] | None = None)

Bases: object

PRIVATE: Used to compute the StateController for a Petri Net.

Variables:

_Gamma (numpy.ndarray) – The Gamma matrix of the inequality defining the conditions for which the controller should be computed.
_b (numpy.ndarray) – The b vector of the inequality defining the conditions for which the controller should be computed. Pass it to the function as a column vector.
_A (np.ndarray) – Incidence matrix of a Petri Net.
_x0 (np.ndarray) – Initial marking vector of a Petri Net.
_trans_ouc (list[int] | None) – List of observable but uncontrollable transitions.
_trans_uouc (list[int] | None) – List of unobservable and uncontrollable transitions.

getA_c() → ndarray

Returns the computed matrix A_c.

If a state controller has already been computed using the .getStateController() function, this function will return matrix A_c in the form of a numpy ndarray. In case the state controlled could not have been obtained, it will throw an error.

Parameters:: None –
Returns:: The incidence matrix relative to the controller places.
Return type:: numpy.array

Examples

Assuming an object pn of the class PetriNet has already been created and its state controller has been computed and saved as controller.

>>> print(controller.getA_c())
[[ 0 -1  0  1  0  0  0  0  0]
 [ 0  0  0  0 -1  0  0  0  1]
 [ 0  0  0  0 -1  0  0  0  1]]

getx_c() → ndarray

Returns the computed initial marking of the controller places.

If a state controller has already been computed using the .getStateController() function, this function will return vector x_c in the form of a numpy ndarray. This vector represent the initial marking of the controller places. In case the state controlled could not have been obtained, it will throw an error.

Parameters:: None –
Returns:: The initial marking of the controller places.
Return type:: numpy.array

Examples

Assuming an object pn of the class PetriNet has already been created and its state controller has been computed and saved as controller.

>>> print(controller.getxc())
[[3]
 [3]
 [2]]

toString() → str

Returns the computed state controller in a string format.

If a state controller has already been computed using the .getStateController() function, this function will return the result in a string format as matrix. Furthermore, the string will also tell the user whether the state controller was ideally enforceable. In case the state controlled could not have been obtained, it will return a message saying the controller has no solution.

Parameters:: None –
Returns:: A state controller as a matrix in a string format and information about the ideal enforceability or a message saying the state controller has no solution.
Return type:: str

Examples

Assuming an object pn of the class PetriNet has already been created and its state controller has been computed and saved as controller.

>>> print(controller.toString())
State Controller (non-ideal case):
- Initial marking of the controller places:
[[3]
 [3]
 [2]]
- Controller matrix:
[[ 0 -1  0  1  0  0  0  0  0]
 [ 0  0  0  0 -1  0  0  0  1]
 [ 0  0  0  0 -1  0  0  0  1]]