, 32 tweets, 6 min read Read on Twitter
Les réseaux de Petri

Chapitre 2. Pourquoi ?
Où l'on apprend à quoi servent les réseaux de Petri.
On utilise généralement les réseaux de Petri pour faire des modèles.

Non, pas vous monsieur, laissez-nous travailler, merci.
Un modèle est une simplification d'un système dont l'étude n'est pas aisée.

Le modèle étant plus simple, on peut l'analyser plus facilement.

Les conclusions de l'analyse sur le modèle pourront être reportées sur le système.
Par exemple, en biologie, la souris est un modèle de l'humain.
On ne peut pas facilement tester de nouveaux traitements sur des humains, mais on peut plus facilement le faire sur des souris, et en tirer des conclusions quant à l'effet du traitement sur les humains.
Avec des réseaux de Petri, on peut construire des modèles de systèmes très variés : systèmes critiques, protocoles de sécurité, systèmes biologiques, écosystèmes, etc.
Trêve de bavardages, voici donc un système à étudier. C'est un système critique : son fonctionnement met en jeu des vies humaines.
C'est un système jouet (ah ah) très classique car il est assez simple.

Des trains circulent sur un voie qui croise une route.

Des barrières doivent se baisser au passage du train pour éviter une collision avec une voiture.
Une solution facile est de toujours laisser les barrières fermées.

Mais ne cédons pas à la facilité.
Voici donc un modèle des barrières.

Elles peuvent être en haut ou en bas, deux transitions se chargent de les baisser ou les lever.

C'est un modèle, on simplifie en faisant abstraction du mouvement.
Et voici un modèle de la voie et du train. On représente trois positions cruciales en faisant abstraction des autres.
Dans le modèle complet, on retrouve ces deux morceaux qui communiquent via des places permettant à la voie de demander à la barrière de se lever ou de se baisser.

Regardons le fonctionner.
On a gagné !
On dépose un brevet et on vend notre conception à la SNCF.
On va être millionnaires.

... Vraiment ?
On n'a rien oublié ?
Reprenons.

Un modèle simplifie la réalité. Ça c'est fait.

Il peut être analysé. C'est fait ou pas ?
Non bien sûr !

Ce qu'on a fait c'est exécuter sur le modèle une séquence d'actions correcte. On a donc juste prouvé que le modèle est capable d'avoir le comportement attendu. Pas qu'il n'a pas de mauvais comportements.
Pour prouver qu'il n'existe aucun comportement fautif, on va calculer le graphe de marquages en vérifiant qu'aucun marquage découvert n'a de jeton dans la place 'dedans' sans jeton dans la place 'bas'.
En effet, s'il la place 'dedans' est marquée, c'est que le train se trouve entre les barrières. Il faut alors absolument qu'elles soient fermées.
Allons-y. L'état initial peut se représenter par le nombre de jeton dans chaque place comme on l'a fait dans le chapitre 1. Et en rouge, on a les deux places à surveiller ('bas' et en haut et 'dedans' est le plus extérieur... hum...).
Notre scénario correct donne un graphe simple:
Mais lieu de tirer les transitions qui nous arrangent, essayons les toutes. On observe qu'au début, on peut juste tirer 'approche'. Et ensuite, on peut bien sûr tirer 'baisse' mais aussi 'entre'.

Catastrophe !
Mais que s'est-il passé ?

Comment cela est-il possible ?
Pour répondre, il suffit de regarder la séquence d'actions jusqu'au marquage fautif.

Le train s'est approché, a envoyé le signal de descente à la barrière, mais celle-ci n'a pas bougé avant que le train n'arrive à son niveau.
Nos barrières sont-elles trop lentes ? Faut-il les forcer à descendre tout de suite ?

Non. Ce scénario peut aussi correspondre à des barrières cassées.
Donc, si on ne peut pas forcer les barrières à descendre, il faut empêcher le train d'avancer tant que les barrières ne sont pas fermées.

Mais comment ? (Suspense...)
Mesdames, messieurs, je vous présente : le feu rouge ! Sous vos applaudissements.
On va donc ajouter un feu à notre modèle : une place 'feu' telle qu'un jeton dedans représente le feu vert, et pas de jeton le feu rouge.
Quand le train approche, il met le feu au rouge.

Il ne peut entrer entre les barrières que si le feu est vert.

C'est l'arrivée des barrières en bas qui met le feu au vert.

Voilà.
Exercice à la maison.

Dessinez le graphe de marquage de ce réseau et vérifiez que chaque état accessible vérifie la propriété de sécurité : si 'dedans' est marquée, alors 'bas' l'est aussi.
Ceci clos notre chapitre 2.

J'ai plusieurs idées de chapitre 3, n'hésitez pas à me poser des question sur ce qui vous intéresserait.
Ceci clos notre chapitre 2. J'ai plusieurs idées de chapitre 3, n'hésitez pas à me poser des question sur ce qui vous intéresserait.
Ce chapitre est placé sous licence CC BY-SA. creativecommons.org/licenses/by-sa…
Missing some Tweet in this thread?
You can try to force a refresh.

Like this thread? Get email updates or save it to PDF!

Subscribe to Franck Pommereau
Profile picture

Get real-time email alerts when new unrolls are available from this author!

This content may be removed anytime!

Twitter may remove this content at anytime, convert it as a PDF, save and print for later use!

Try unrolling a thread yourself!

how to unroll video

1) Follow Thread Reader App on Twitter so you can easily mention us!

2) Go to a Twitter thread (series of Tweets by the same owner) and mention us with a keyword "unroll" @threadreaderapp unroll

You can practice here first or read more on our help page!

Follow Us on Twitter!

Did Thread Reader help you today?

Support us! We are indie developers!


This site is made by just three indie developers on a laptop doing marketing, support and development! Read more about the story.

Become a Premium Member ($3.00/month or $30.00/year) and get exclusive features!

Become Premium

Too expensive? Make a small donation by buying us coffee ($5) or help with server cost ($10)

Donate via Paypal Become our Patreon

Thank you for your support!