Introduction to Petri Nets (4IS)
Course material (french)
TINA : TP1
TP0
Prise en Main de TINA
TINA paths: TINA tools are normally installed and directly available from your sessions. To test it, you can launch the nd command in a terminal (nd for "net draw").
In case that doesn't work, you can also run in a terminal the command source ~vernadat/.tinarc which will set the paths for Tina or, even better, add the contents of ~vernadat/.tinarc in your own file ~/.bashrc
I Resources Sharing
The following net models a resource sharing protocol :
two (indistinguished) processes share two resources (A and B). One of the processes first obtains A (OqpA), then obtains B (OqpAB), it works (WorkAB) then it returns (at the same time) to rest and frees (FreeAB) resources A and B. The other process proceeds in reverse order: obtaining B then from A.
Load the file interblocage.ndr
(the ndr suffix indicates that the Petri net is given in graphical format)
- Execute in the directory containing the file the command nd interblocage.ndr
- Launch the simulator step by step. (tools tab: stepper)
- Simulate the system behaviour
- Find the deadlock situation.
- Quit the simulator (file tab: return to editor)
- Build the marking graph (tools tab: reachabilty / marking graph - output verbose)
- Read the file Annotated result; . Annotations are indicated by ##
- Visualization of the marking graph (tools tab: reachabilty / marking graph - output automaton)
- Open the resulting automaton under TINA (right click - open file in nd)
- Bring up the TINA toolbar (right click in the window)
- Draw it (edit tab: draw option).
Several heuristics of placement are proposed (neato, draw, circo, ...) try them. You have to
first switch back to textual form (edit tab: textify option).
II
The day of a banana picker
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 sleep.
Load the file planteur.net
(the net suffix indicates that the Petri net is given in textual format)
- Execute the following command : nd picker.net command.
The Petri net appears but in textual form.
(the suffix net stands for textual Petri net format)
- Launch the simulator step by step. step (tools tab: stepper)
- Simulate the system behaviour
- Quit the simulator (file tab: return to editor)
- Draw the network (edit tab: draw option).
You can improve the esthetics at your way.
- Launch the simulator step by step. step (tools tab: stepper).
- Simulate the system behaviour, convince yourself that it is unbounded.
- Quit the simulator (file tab: return to editor)
- Build the network coverage graph (tools tab: reachabilty /coverabilty graph - output verbose).
- Look at the result file. Unbounded places are those that appear with a weight w.
- Draw the coverage graph (tools tab: reachabilty /coverabilty graph - output automaton). ...
III Editing the following Petri net
- Edit the Petri net in the textual form (it is advisable to use your favorite editor: emacs, vi, .......)
- Edit the Petri net directly graphically. See under FAQ (in french) the features of Net Drawd (ND)