Introduction to Petri Nets (4IS)
Course material (french)
TINA : TP1
TP 1 : Compositional Modelling
The objective of this lab is twofold.
-
The first objective (question 1 and 2) is to address compositional modeling. A classic resource allocation system illustrates this lab.
The global modeling is obtained by composition of 3 Rdp associated with the 3 components of the system (The client and two managers).
The two modes of communication/composition are illustrated: asynchronous communication (shared places) and synchronous communication (shared transitions).
- The second objective (question 3) is to address the verification of specific properties of the system: it is a question of showing the limits of the simulation and
to illustrate the technique of verification by observers.
I 1 client and 2 resource managers
Let us consider a resource allocation system with 1 client and 2 resource managers.
A client (Cl1) needs to own two resources (R1 , R2 ) in order to work. These resources are
remote and managed individually by two managers (G1, G2).
Exchanged messages:
The communication between client and manager is governed by the following messages:
- Req - request for access to the resource,
- Ack - authorization to access the resource
- Lib - release of the resource
Behaviour description:
-
Client C1: Cl1 requests both resources sequentially. More precisely, it first requests
resource R1 , and when it has obtained it, it requests resource R2 . It enters the
what is called the critical section when it has both resources. It then releases both
resources at the same time and returns to its initial state.
-
Manager G_j:
On receipt of a Req message sent by a client Cli, Gj exclusively
allocates the resource to Cli (i.e. sends the Ack message to Cli if the resource is
free, otherwise the request remains pending. When the Lib message is received, the
resource is released.
Questions :
- By respecting the instructions below, modeling of the system by a Petri net
- The file Cl1.net cl1.net
represents the commented behavior of client 1. It is described in a textual format.
Save it and open it with the editor nd .
You can draw it with the edit ongler. Note that several places are provided
to serve as places of communication between the client and other processes (i.e
communication by shared places).
-
Using the Petri net associated with the client as a starting point, model the
behavior of manager 1 (resp 2) in a gest1.net file (resp gest2.net).
-
The global system can be obtained by composing the 3 .net files using the tpn format
(see example dans composition.tpn ).
The Petri net resulting from the composition
will be automatically built when calling nd ( nd composition.tpn ).
In case of compilation errors use the command tina
-p composition.tpn to see the errors.
-
Simulate the global system using the stepper :
Propose a cyclic scenario allowing the client to work and return to its initial state.
Save the corresponding scenario.
- Build its marking graph.
- Make sure it is free of deadlocks.
- Make sure it is reversible (For this check there is only one single strongly connected component containing all markings).
II Composition by transition fusion
In the previous question, the communication between the components was done asynchronously: shared places represent the messages exchanged.
This question illustrates the ability to simulate asynchronous communication (using shared places) by synchronous communication (using shared transitions).
Let us consider again the resource allocation system of part A. Propose a compositional
modeling (with 3 specific components: 1 client and 2 managers) equivalent in terms of
behaviour to the one realized previously (i.e the global Petri obtained here must be identical
to the one obtained previously) but such that the communication between the three
components is done only by transitions fusion (you thus do not have any more the
possibility of using shared places).
To be done at the end of the Tps series if you have time left.
III 2 Clients and 2 resource managers
We add to the system described in the first question (part A) a second client (C2) whose
behavior is described below:
Client C2:
C2 sequentially requests both resources. More precisely, it rst requests the
resource R2 , and when it has obtained it, it requests the resource R1 . It enters the
critical section when it has both resources. It then releases both resources at the same time and returns to its initial state.
- Modelling
- Give a Petri net model of client C2 according the initial model of the client based on shared places
- Adapt the model of managers ton take into accouint two clients
- Generate by composition the global model composed of the 2 clients and the 2 resource
managers.
- Simulating
- Using the stepper, find scenarios that demonstrate the
possibility of
- Interlocking
- Starvation (i.e. an infinite (cyclic) scenario where one of the clients is always
waiting)
- Verification by observer (example)
Mutual Exclusion We consider the general problem of mutual exclusion.
For the system considered, this problem admits two instances: mutual exclusion at the client level (two clients never work at the same time) or at the resource level (a resource is allocated to at most one client).
At the client level, mutual exclution property can be expressed as follows:
Forall reachable marking m, m(Cl1_work) + m(Cl2_work) <=1
(which means that the number of tokens in the place Cl1_work
plus the number of tokens in the place Cl1_work is always less or equal to one)
Questions
- Why can't the simulation guarantee that this property is satisfied?
- How can you be sure by analyzing the graph of markings?
- To check automatically this property, add to the complete system a new Petri net
consisting in a single observation transition which will be firable if and only if this exclusion property is not satisfied (see slide 37). Generate the marking graph and verify that the observation transision is dead (never fires).