Introduction to Petri Nets (4IS)
Course material (french)
TP 2
The day/life of a banana picker/planter
In this practical work we consider the model of the banana picker
( picker.net ) seen in course.
The picker is initially in the field where he
picks bananas (assumed to be in infinite quantity). He stops his
work and moves to table to eat some bananas.
At the end of the meal, he goes to the garden and throws some of the skins of eated bananas. He then goes to s\
leep.
- In question 1, the modifications proposed make allow to bound the model
and to reinitialize the picker.
-
Question 2 transforms the initial problem into a game of life: the use of verification methods allows to find a strategy allowing the picker to remain alive indefinitely.
I. Modification of the course example
- Transformations of the initial model :
- Build the the coverabillity graph to verify the net is unbounded.
- Remove the operation of throwing away the banana peels.
- Let us suppose now that we have a banana tree containing a finite
number of bananas (20 for instance).
- One can only pick a banana if the banana tree has bananas.
- After leaving the garden, the picker goes to sleep.
- After sleeping the picker returns to the field.
- To avoid starvation, a banana is put back on the banana tree after havin
g eaten it
- Analysis of the transformed model :
- Edit the modified picker Petri net and simulate it.
- Construct its coverability graph and make sure that the net is bounded.
- Construct its marking graph and make sure that there is no blocking.
II Transformation into a game of life : adding an energy notion
-
Energy management
- Picking bananas is tiring, which will use one unit of energy.
- Since the picker does not live nearby, going home to eat will take 5 units of energ
y.
- Eating bananas will give back some strength to the picker, with 2 units per banana.
- Getting up from the table will take another unit.
- Fortunately sleeping will give him rest and 9 units of energy.
- Going back to work the next day will take 9 units of energy.
- Modification of the Petri net and analysis
- Modify the Petri net obtained in the previous question
to introduce the previous constraints integrating the energy notion.
- "Observe" the influence of the initial value of the banana picker
energy on the behavior of the system : Try to found a value to obtain
a bounded net.
- We now want to fix an initial value of energy that allows to obtain a net that is both bounded, infinitely active and blocking. Find the value E0 by successive tests.
Indication 1: Note that, the problem represented here is monotonic : that means that
there is only one initial energy value (noted E0) for which the corresponding
marked Petri net is both bounded and infinitely active.
For energy values above E0, the net is unbounded.
For energy values below E0, the net is not infinitely active.
Indication 2 : Two methods may be used to check that the net
is infinitely active
- (a) Strongly related component analysis ensures infinitely a
ctive; the strongly related component analysis (SCC) is given at the end of the analysis fi
le.
- (b) Generate the graph of markings in ktz format (tab
tools - reachability analysis - ouput ktz ).
Run in a terminal the following command
selt fichier.ktz -s -f '<> dead' -S inft.scn.
The net is infinitely active when the answer is false. A counterexample is produced in
the inft.scnfile. This scenario can be directly loaded via the stepper to be simulated