\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}

\usepackage[utf8]{inputenc}
\usepackage{multirow}

\usepackage{verbatim}
\usepackage{tikz}
\usetikzlibrary{shapes,arrows,arrows.meta,petri}
\tikzset{
  >=latex,
  every place/.style={minimum size=6mm},
  every transition/.style={minimum size=6mm},
  token distance=6pt,
}

\tikzstyle{trans}=[transition]

\tikzstyle{arc}=[->,rounded corners]

\tikzstyle{state}=[draw=blue!50!gray!50!white,
  fill=blue!70!gray!10!white,
  line width=2pt,
  cloud,cloud puffs=8,
  inner sep=-3pt]

\tikzstyle{fire}=[arrows={-Straight Barb[scale=.6]},
  shorten >=-2pt, shorten <=-1pt,
  draw=blue!50!gray!50!white,
  fill opacity=0,text opacity=1,
  line width=2pt,
  line cap=round,
  rounded corners]

\tikzstyle{active}=[draw=green!50!gray!50!white,
  fill=green!70!gray!10!white]

\tikzstyle{failure}=[draw=red!50!gray!50!white,
  fill=red!70!gray!10!white]

\def\matrix #1#2#3#4#5#6#7{%
  {\small$\begin{array}{c@{\hspace{12pt}}c}
    \multicolumn{2}{c}{#1} \\[-6pt]
    #2 & #3 \\[-6pt]
    \multicolumn{2}{c}{\color{red}#4} \\[-6pt]
    #5 & \color{red}#6 \\[-6pt]
    \multicolumn{2}{c}{#7}
  \end{array}$}}

\begin{document}

%%
%%

\begin{comment}
Les réseaux de Petri

Chapitre 2. Pourquoi ?
Où l'on apprend à quoi servent les réseaux de Petri.
\end{comment}

\begin{comment}
On utilise généralement les réseaux de Petri pour faire des modèles.

Non, pas vous monsieur, laissez-nous travailler, merci.
\end{comment}

% model.gif

\begin{comment}
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.
\end{comment}

\begin{comment}
Par exemple, en biologie, la souris est un modèle de l'humain.
\end{comment}

% mouse.gif

\begin{comment}
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.
\end{comment}

\begin{comment}
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.
\end{comment}

\begin{comment}
Trêve de bavardages, voici donc un système à étudier. C'est un système critique : son fonctionnement met en jeu des vies humaines.
\end{comment}

% train complet

\begin{comment}
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.
\end{comment}

\begin{comment}
Une solution facile est de toujours laisser les barrières fermées.

Mais ne cédons pas à la facilité.
\end{comment}

\begin{comment}
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.
\end{comment}

% gates.gif

\begin{comment}
Et voici un modèle de la voie et du train. On représente trois positions cruciales en faisant abstraction des autres.
\end{comment}

% track.gif

\begin{comment}
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.
\end{comment}

% draft.gif

\begin{comment}
On a gagné !
On dépose un brevet et on vend notre conception à la SNCF.
On va être millionnaires.

... Vraiment ?
\end{comment}

\begin{comment}
On n'a rien oublié ?
\end{comment}

\begin{comment}
Reprenons.

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

Il peut être analysé. C'est fait ou pas ?
\end{comment}

\begin{comment}
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.
\end{comment}

\begin{comment}
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'.
\end{comment}

\begin{comment}
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.
\end{comment}

\begin{comment}
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...).
\end{comment}

\begin{tikzpicture}
  \node[state] {\matrix 1000001};
\end{tikzpicture}

\begin{comment}
Notre scénario correct donne un graphe simple:
\end{comment}

% test.gif

\begin{comment}
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 !
\end{comment}

\begin{tikzpicture}[scale=1.2]
  \node[trans] (approach) at (0,0) {};
  \node[rotate=45] at (approach) {\tiny\textsf{approche}};
  \node[place] (before) at (1,0) {};
  \node[below] at (before.south) {\tiny\textsf{avant}};
  \node[trans] (enter) at (2,0) {};
  \node[rotate=45] at (enter) {\tiny\textsf{entre}};
  \node[place,tokens=1] (inside) at (3,0) {};
  \node[below] at (inside.south) {\tiny\textsf{dedans}};
  \node[trans] (exit) at (4,0) {};
  \node[rotate=45] at (exit) {\tiny\textsf{sort}};
  \node[place] (far) at (2,-1) {};
  \node[below] at (far.south) {\tiny\textsf{loin}};
  \draw[arc] (before) -- (enter);
  \draw[arc] (enter) -- (inside);
  \draw[arc] (inside) -- (exit);
  \draw[arc] (exit) |- (far);
  \draw[arc] (far) -| (approach);
  \draw[arc] (approach) -- (before);
  %
  \node[place] (low) at (2,1) {};
  \node[below] at (low.south) {\tiny\textsf{bas}};
  \node[place,tokens=1] (high) at (2,3) {};
  \node[above] at (high.north) {\tiny\textsf{haut}};
  \node[trans] (down) at (1,2) {};
  \node[rotate=45] at (down) {\tiny\textsf{baisse}};
  \node[trans] (up) at (3,2) {};
  \node[rotate=45] at (up) {\tiny\textsf{lève}};
  \draw[arc] (high) -| (down);
  \draw[arc] (down) |- (low);
  \draw[arc] (low) -| (up);
  \draw[arc] (up) |- (high);
  %
  \node[place,tokens=1] (godown) at (0,2) {};
  \node[above] at (godown.north) {\tiny\textsf{descendre}};
  \draw[arc] (approach) -- (godown);
  \draw[arc] (godown) -- (down);
  \node[place] (goup) at (4,2) {};
  \node[above] at (goup.north) {\tiny\textsf{relever}};
  \draw[arc] (exit) -- (goup);
  \draw[arc] (goup) -- (up);
  %
  \begin{scope}[scale=2,yshift=-12mm]
    \node[state] (0) at (0,0) {\matrix 1000001};
    \node[state] (1) at (1,0) {\matrix 1100100};
    \node[state] (2) at (2,0) {\matrix 0001100};
    \node[state,failure] (5) at (1,-1) {\matrix 1100010};
    \draw[fire] (0) -- node[above]{\tiny\textsf{approche}} (1);
    \draw[fire] (1) -- node[above]{\tiny\textsf{baisse}} (2);
    \draw[fire,failure] (1) -- node[left]{\tiny\textsf{entre}} (5);
  \end{scope}
\end{tikzpicture}

\begin{comment}
Mais que s'est-il passé ?

Comment cela est-il possible ?
\end{comment}

\begin{comment}
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.
\end{comment}

\begin{comment}
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.
\end{comment}

\begin{comment}
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...)
\end{comment}

\begin{comment}
Mesdames, messieurs, je vous présente : le feu rouge ! Sous vos applaudissements.
\end{comment}

% feu-rouge.jpg

\begin{comment}
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.
\end{comment}

\begin{comment}
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à.
\end{comment}

\begin{tikzpicture}[scale=1.2]
  \node[trans] (approach) at (0,0) {};
  \node[rotate=45] at (approach) {\tiny\textsf{approche}};
  \node[place] (before) at (1,0) {};
  \node[below] at (before.south) {\tiny\textsf{avant}};
  \node[trans] (enter) at (2,0) {};
  \node[rotate=45] at (enter) {\tiny\textsf{entre}};
  \node[place] (inside) at (3,0) {};
  \node[below] at (inside.south) {\tiny\textsf{dedans}};
  \node[trans] (exit) at (4,0) {};
  \node[rotate=45] at (exit) {\tiny\textsf{sort}};
  \node[place,tokens=1] (far) at (2,-1) {};
  \node[below] at (far.south) {\tiny\textsf{loin}};
  \draw[arc] (before) -- (enter);
  \draw[arc] (enter) -- (inside);
  \draw[arc] (inside) -- (exit);
  \draw[arc] (exit) |- (far);
  \draw[arc] (far) -| (approach);
  \draw[arc] (approach) -- (before);
  %
  \node[place] (low) at (2,1) {};
  \node[below] at (low.south) {\tiny\textsf{bas}};
  \node[place,tokens=1] (high) at (2,3) {};
  \node[above] at (high.north) {\tiny\textsf{haut}};
  \node[trans] (down) at (1,2) {};
  \node[rotate=45] at (down) {\tiny\textsf{baisse}};
  \node[trans] (up) at (3,2) {};
  \node[rotate=45] at (up) {\tiny\textsf{lève}};
  \draw[arc] (high) -| (down);
  \draw[arc] (down) |- (low);
  \draw[arc] (low) -| (up);
  \draw[arc] (up) |- (high);
  %
  \node[place] (godown) at (0,2) {};
  \node[above] at (godown.north) {\tiny\textsf{descendre}};
  \draw[arc] (approach) -- (godown);
  \draw[arc] (godown) -- (down);
  \node[place] (goup) at (4,2) {};
  \node[above] at (goup.north) {\tiny\textsf{relever}};
  \draw[arc] (exit) -- (goup);
  \draw[arc] (goup) -- (up);
  %
  \node[place,tokens=1] (green) at (.5,1) {};
  \node[above] at (green.130) {\tiny\textsf{feu}};
  \draw[arc] (green) -- (approach);
  \draw[arc] (down) -- (green);
  \draw[<->] (green) -- (enter);
\end{tikzpicture}

\begin{comment}
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.
\end{comment}

\begin{comment}
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.
\end{comment}

%%
%%

\end{document}