initial import

+all: chap1 chap2
+
+chap1: chap1.pdf chap1-anim.gif
+
+chap2: chap2.pdf
+	python3 chap2-anim.py
+	mv chap2*.gif chap2/
+
+%.pdf: %.tex
+	latexmk -pdf $<
+	latexmk -pdf -c $<
+	mkdir -p $(*F)
+	convert -background white -alpha remove -density 600 $@ $(*F)/fig-%03d.png
+
+%.gif: %.py %.tex
+	python3 $<

+from t2g import *
+
+markings = {0: dict(a=3, b=0, c=0, d=0),
+            1: dict(a=1, b=1, c=0, d=0),
+            2: dict(a=1, b=0, c=1, d=0),
+            3: dict(a=1, b=0, c=0, d=2),
+            4: dict(a=2, b=0, c=0, d=1),
+            5: dict(a=0, b=1, c=0, d=1),
+            6: dict(a=0, b=0, c=1, d=1),
+            7: dict(a=0, b=0, c=0, d=3)}
+
+state = {"a": 0, "b": 0, "c": 0, "d": 0}
+
+trans = {(0,1): "t",
+         (1,2): "u",
+         (2,3): "v",
+         (3,4): "w",
+         (4,0): "w",
+         (4,5): "t",
+         (5,6): "u",
+         (6,7): "v",
+         (7,3): "w",
+         (6,2): "w",
+         (5,1): "w"}
+
+active = dict((t, "") for t in "tuvw")
+active.update((s, "") for s in range(8))
+active.update((f, "") for f in trans)
+
+load("chap1-anim.tex")
+src = 0
+
+for dst in [1, 2, 3, 4, 0, 1, 2, 3, 4, 5, 6, 7, 3, 4, 5, 1, 2, 3, 4, 5, 6, 2, 3, 4, 0] :
+    state = markings[src]
+    active[src] = "active"
+    frame(.8)
+    active[src,dst] = active[trans[src,dst]] = "active"
+    frame(.8)
+    active[src] = active[src,dst] = active[trans[src,dst]] = ""
+    src = dst
+
+gif("chap1-anim.gif")

+\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}
+
+\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{state}=[draw=blue!50!gray!50!white,
+  fill=blue!70!gray!10!white,
+  line width=2pt,
+  cloud,cloud puffs=8,
+  inner sep=-1pt]
+
+\tikzstyle{fire}=[arrows={-Straight Barb[scale=.6]},
+  shorten >=-2pt, shorten <=-1pt,
+  draw=blue!50!gray!50!white,
+  line width=2pt,
+  fill opacity=0,
+  text opacity=1,
+  line cap=round,
+  rounded corners]
+
+\tikzstyle{active}=[draw=green!50!gray!50!white,
+  fill=green!70!gray!10!white]
+
+\def\matrix #1#2#3#4{%
+  $\begin{array}{c@{\hspace{5pt}}c}
+    #1 & #2 \\
+    #3 & #4
+  \end{array}$}
+
+\begin{document}
+
+%%FRAME
+
+\begin{tikzpicture}
+  \begin{scope}[yshift=45mm,xshift=28mm,scale=1.2]
+    \node[place,tokens={{ state["a"] }}] (a) at (0,0) {};
+    \node[left] at (a.west) {$a$};
+    \node[trans,{{ active["t"] }}] (t) at (1,0) {$t$};
+    \draw[->] (a) -- node[above]{2} (t);
+    \node[place,tokens={{ state["b"] }}] (b) at (2,0) {};
+    \node[right] at (b.east) {$b$};
+    \draw[->] (t) -- (b);
+    \node[trans,{{ active["u"] }}] (u) at (2,-1) {$u$};
+    \draw[->] (b) -- (u);
+    \node[place,tokens={{ state["c"] }}] (c) at (2,-2) {};
+    \node[right] at (c.east) {$c$};
+    \draw[->] (u) -- (c);
+    \node[trans,{{ active["v"] }}] (v) at (1,-2) {$v$};
+    \draw[->] (c) -- (v);
+    \node[place,tokens={{ state["d"] }}] (d) at (0,-2) {};
+    \node[left] at (d.west) {$d$};
+    \draw[->] (v) -- node[above]{2} (d);
+    \node[trans,{{ active["w"] }}] (w) at (0,-1) {$w$};
+    \draw[->] (d) -- (w);
+    \draw[->] (w) -- (a);
+  \end{scope}
+  \begin{scope}[scale=2]
+    \node[state,{{ active[0] }}] (0) at (0,0) {\matrix 3000};
+    \node[state,{{ active[1] }}] (1) at (1,0) {\matrix 1100};
+    \draw[fire,{{ active[0,1] }}] (0) -- node[above] {$t$} (1);
+    \node[state,{{ active[2] }}] (2) at (2,0) {\matrix 1001};
+    \draw[fire,{{ active[1,2] }}] (1) -- node[above] {$u$} (2);
+    \node[state,{{ active[3] }}] (3) at (3,0) {\matrix 1020};
+    \draw[fire,{{ active[2,3] }}] (2) -- node[above] {$v$} (3);
+    \node[state,{{ active[4] }}] (4) at (4,0) {\matrix 2010};
+    \draw[fire,{{ active[3,4] }}] (3) -- node[above] {$w$} (4);
+    \draw[fire,{{ active[4,0] }}] (4) |- node[near end,above] {$w$} +(-1,.5) -| (0);
+    \node[state,{{ active[5] }}] (5) at (1,-1) {\matrix 0110};
+    \draw[fire,{{ active[4,5] }}] (4) |- node[pos=.05,right] {$t$} +(-1,-1.5) -| (5);
+    \draw[fire,{{ active[5,1] }}] (5) -- node[left] {$w$} (1);
+    \node[state,{{ active[6] }}] (6) at (2,-1) {\matrix 0011};
+    \draw[fire,{{ active[5,6] }}] (5) -- node[above] {$u$} (6);
+    \draw[fire,{{ active[6,2] }}] (6) -- node[left] {$w$} (2);
+    \node[state,{{ active[7] }}] (7) at (3,-1) {\matrix 0030};
+    \draw[fire,{{ active[7,3] }}] (7) -- node[left] {$w$} (3);
+    \draw[fire,{{ active[6,7] }}] (6) -- node[above] {$v$} (7);
+  \end{scope}
+\end{tikzpicture}
+
+%%/FRAME
+
+\end{document}

+\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}
+
+\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{state}=[draw=blue!50!gray!50!white,
+  fill=blue!70!gray!10!white,
+  line width=2pt,
+  cloud,cloud puffs=8,
+  inner sep=-1pt]
+
+\tikzstyle{fire}=[arrows={-Straight Barb[scale=.6]},
+  shorten >=-2pt, shorten <=-1pt,
+  draw=blue!50!gray!50!white,
+  line width=2pt,
+  line cap=round,
+  rounded corners]
+
+\def\matrix #1#2#3#4{%
+  $\begin{array}{c@{\hspace{5pt}}c}
+    #1 & #2 \\
+    #3 & #4
+  \end{array}$}
+
+\begin{document}
+
+% Les réseaux de Petri
+
+% Chapitre 1. Quoi ?
+% Où l'on apprend ce que sont les réseaux de Petri.
+
+%%%
+
+% Ceci est une place.
+
+\begin{tikzpicture}
+  \node[place] (p) at (0,0) {};
+\end{tikzpicture}
+
+% Une place peut contenir des jetons (ici 3).
+
+\begin{tikzpicture}
+  \node[place,tokens=3] (p) at (0,0) {};
+\end{tikzpicture}
+
+% Ceci est une transition.
+
+% Une transition ne peut pas contenir de jetons, non non.
+
+\begin{tikzpicture}
+  \node[trans] (t) at (0,0) {};
+\end{tikzpicture}
+
+% Ceci est un arc.
+
+\begin{tikzpicture}
+  \draw[->] (0,0) -- (1,0);
+\end{tikzpicture}
+
+% Un arc peut être décoré par un nombre entier (valant au moins 1).
+
+% Quand on ne met pas de nombre, c'est qu'il vaut 1.
+
+\begin{tikzpicture}
+  \draw[->] (0,0) -- node[above]{2} (1,0);
+\end{tikzpicture}
+
+% Un arc relie une place à une transition, ou l'inverse.
+
+\begin{tikzpicture}[xscale=1.2]
+  \node[place,tokens=3] (p) at (0,0) {};
+  \node[trans] (t) at (1,0) {};
+  \draw[->] (p) -- node[above]{2} (t);
+  \node[trans] (u) at (0,-1) {};
+  \node[place] (q) at (1,-1) {};
+  \draw[->] (u) -- (q);
+\end{tikzpicture}
+
+% Mais un arc ne relie jamais deux places ou deux transitions.
+% Jamais, jamais.
+
+\begin{tikzpicture}[xscale=1.2]
+  \node[place,tokens=3] (p) at (0,0) {};
+  \node[place] (q) at (1,0) {};
+  \draw[->] (p) -- node[above]{2} (q);
+  \node[trans] (t) at (0,-1) {};
+  \node[trans] (u) at (1,-1) {};
+  \draw[->] (t) -- (u);
+  \node[forbidden sign,line width=5pt,draw=red,inner sep=6mm] at (.5,-.5) {};
+\end{tikzpicture}
+
+% Ceci est un réseau de Petri que nous appellerons Carl.
+
+% Carl a une transition, deux places (l'une a trois jetons, l'autre
+% zéro), et deux arcs.
+
+\begin{tikzpicture}[xscale=1.2]
+  \node[place,tokens=3] (p) at (0,0) {};
+  \node[trans] (t) at (1,0) {};
+  \draw[->] (p) -- node[above]{2} (t);
+  \node[place] (q) at (2,0) {};
+  \draw[->] (t) -- (q);
+\end{tikzpicture}
+
+% Les transitions consomment et produisent des jetons dans les places,
+% selon ce qu'indiquent les arcs.
+
+% La transition de Carl peut consommer deux jetons dans la place de
+% gauche et en produire un dans celle de droite (le 1 n'est pas
+% indiqué puisque c'est 1 justement).
+
+% Si elle le fait, on dit qu'on tire la transition.
+
+%%%
+
+% Ici, Carl a tiré sa transition. Deux jetons ont disparu de la place
+% de gauche, et un a été ajouté dans celle de droite. Comme indiqué
+% par les arcs.
+
+\begin{tikzpicture}[xscale=1.2]
+  \node[place,tokens=1] (p) at (0,0) {};
+  \node[trans] (t) at (1,0) {};
+  \draw[->] (p) -- node[above]{2} (t);
+  \node[place,tokens=1] (q) at (2,0) {};
+  \draw[->] (t) -- (q);
+\end{tikzpicture}
+
+% Maintenant, Carl ne peut plus tirer sa transition, car elle ne peut
+% pas consommer deux jetons dans la place de gauche qui n'en contient
+% qu'un. Donc Carl est bloqué. (Pauvre Carl.)
+
+%%%
+
+% Voici un autre réseau de Petri, appelons le Adam. Comme il a
+% beaucoup de places et de transitions, on leur donne des noms: a, b,
+% c, d pour les places, et t, u, v, w pour les transitions.
+
+\begin{tikzpicture}[scale=1.2]
+  \node[place,tokens=3] (a) at (0,0) {};
+  \node[left] at (a.west) {$a$};
+  \node[trans] (t) at (1,0) {$t$};
+  \draw[->] (a) -- node[above]{2} (t);
+  \node[place] (b) at (2,0) {};
+  \node[right] at (b.east) {$b$};
+  \draw[->] (t) -- (b);
+  \node[trans] (u) at (2,-1) {$u$};
+  \draw[->] (b) -- (u);
+  \node[place] (c) at (2,-2) {};
+  \node[right] at (c.east) {$c$};
+  \draw[->] (u) -- (c);
+  \node[trans] (v) at (1,-2) {$v$};
+  \draw[->] (c) -- (v);
+  \node[place] (d) at (0,-2) {};
+  \node[left] at (d.west) {$d$};
+  \draw[->] (v) -- node[above]{2} (d);
+  \node[trans] (w) at (0,-1) {$w$};
+  \draw[->] (d) -- (w);
+  \draw[->] (w) -- (a);
+\end{tikzpicture}
+
+% Adam a trois jetons dans sa place a, et aucun ailleurs. On appelle
+% ça son marquage, c'est-à-dire le nombre de jetons dans chaque place.
+
+% On peut le dessiner dans un petit nuage bleu.
+
+\begin{tikzpicture}[scale=1.2]
+  \node[state] (s) at (1,-1) {\matrix 3000};
+  \node[place,tokens=3] (a) at (0,0) {};
+  \node[left] at (a.west) {$a$};
+  \node[trans] (t) at (1,0) {$t$};
+  \draw[->] (a) -- node[above]{2} (t);
+  \node[place] (b) at (2,0) {};
+  \node[right] at (b.east) {$b$};
+  \draw[->] (t) -- (b);
+  \node[trans] (u) at (2,-1) {$u$};
+  \draw[->] (b) -- (u);
+  \node[place] (c) at (2,-2) {};
+  \node[right] at (c.east) {$c$};
+  \draw[->] (u) -- (c);
+  \node[trans] (v) at (1,-2) {$v$};
+  \draw[->] (c) -- (v);
+  \node[place] (d) at (0,-2) {};
+  \node[left] at (d.west) {$d$};
+  \draw[->] (v) -- node[above]{2} (d);
+  \node[trans] (w) at (0,-1) {$w$};
+  \draw[->] (d) -- (w);
+  \draw[->] (w) -- (a);
+  \draw[|->,yellow,very thick,shorten >=-10pt] (a) -- (s.north west);
+  \draw[|->,yellow,very thick,shorten >=-10pt] (b) -- (s.north east);
+  \draw[|->,yellow,very thick,shorten >=-10pt] (c) -- (s.south east);
+  \draw[|->,yellow,very thick,shorten >=-10pt] (d) -- (s.south west);
+\end{tikzpicture}
+
+% Adam peut tirer sa transition t, ce qui enlèvera deux jetons dans a
+% et en ajoutera un dans b. On obtient alors ce marquage.
+
+\begin{tikzpicture}
+  \node[state] {\matrix 1100};
+\end{tikzpicture}
+
+% On peut représenter cette évolution entre deux marquages par un
+% graphe.
+
+\begin{tikzpicture}[scale=2]
+  \node[state] (0) at (0,0) {\matrix 3000};
+  \node[state] (1) at (1,0) {\matrix 1100};
+  \draw[fire] (0) -- node[above] {$t$} (1);
+\end{tikzpicture}
+
+% Et on peut prolonger ce graphe en tirant u, v, puis w.
+
+\begin{tikzpicture}[scale=2]
+  \node[state] (0) at (0,0) {\matrix 3000};
+  \node[state] (1) at (1,0) {\matrix 1100};
+  \draw[fire] (0) -- node[above] {$t$} (1);
+  \node[state] (2) at (2,0) {\matrix 1001};
+  \draw[fire] (1) -- node[above] {$u$} (2);
+  \node[state] (3) at (3,0) {\matrix 1020};
+  \draw[fire] (2) -- node[above] {$v$} (3);
+  \node[state] (4) at (4,0) {\matrix 2010};
+  \draw[fire] (3) -- node[above] {$w$} (4);
+\end{tikzpicture}
+
+% À partir du dernier marquage atteint, on peut encore tirer w, et on
+% retrouve alors le marquage départ.
+
+\begin{tikzpicture}[scale=2]
+  \node[state] (0) at (0,0) {\matrix 3000};
+  \node[state] (1) at (1,0) {\matrix 1100};
+  \draw[fire] (0) -- node[above] {$t$} (1);
+  \node[state] (2) at (2,0) {\matrix 1001};
+  \draw[fire] (1) -- node[above] {$u$} (2);
+  \node[state] (3) at (3,0) {\matrix 1020};
+  \draw[fire] (2) -- node[above] {$v$} (3);
+  \node[state] (4) at (4,0) {\matrix 2010};
+  \draw[fire] (3) -- node[above] {$w$} (4);
+  \draw[fire] (4) |- node[near end,above] {$w$} +(-1,.5) -| (0);
+\end{tikzpicture}
+
+% Mais, hop hop hop, pas si vite... Au lieu de tirer w, on aurait
+% aussi pu tirer t puisqu'il y a deux jetons dans a. Du coup, on
+% obtient un branchement dans notre graphe.
+
+\begin{tikzpicture}[scale=2]
+  \node[state] (0) at (0,0) {\matrix 3000};
+  \node[state] (1) at (1,0) {\matrix 1100};
+  \draw[fire] (0) -- node[above] {$t$} (1);
+  \node[state] (2) at (2,0) {\matrix 1001};
+  \draw[fire] (1) -- node[above] {$u$} (2);
+  \node[state] (3) at (3,0) {\matrix 1020};
+  \draw[fire] (2) -- node[above] {$v$} (3);
+  \node[state] (4) at (4,0) {\matrix 2010};
+  \draw[fire] (3) -- node[above] {$w$} (4);
+  \draw[fire] (4) |- node[near end,above] {$w$} +(-1,.5) -| (0);
+  \node[state] (5) at (1,-1) {\matrix 0110};
+  \draw[fire] (4) |- node[pos=.05,right] {$t$} +(-1,-1.5) -| (5);
+\end{tikzpicture}
+
+% On continue : à partir de chaque marquage, on tire toutes les
+% transitions possibles. Et on obtient ce qu'on appelle le graphe de
+% marquages.
+
+\begin{tikzpicture}[scale=2]
+  \node[state] (0) at (0,0) {\matrix 3000};
+  \node[state] (1) at (1,0) {\matrix 1100};
+  \draw[fire] (0) -- node[above] {$t$} (1);
+  \node[state] (2) at (2,0) {\matrix 1001};
+  \draw[fire] (1) -- node[above] {$u$} (2);
+  \node[state] (3) at (3,0) {\matrix 1020};
+  \draw[fire] (2) -- node[above] {$v$} (3);
+  \node[state] (4) at (4,0) {\matrix 2010};
+  \draw[fire] (3) -- node[above] {$w$} (4);
+  \draw[fire] (4) |- node[near end,above] {$w$} +(-1,.5) -| (0);
+  \node[state] (5) at (1,-1) {\matrix 0110};
+  \draw[fire] (4) |- node[pos=.05,right] {$t$} +(-1,-1.5) -| (5);
+  \draw[fire] (5) -- node[left] {$w$} (1);
+  \node[state] (6) at (2,-1) {\matrix 0011};
+  \draw[fire] (5) -- node[above] {$u$} (6);
+  \draw[fire] (6) -- node[left] {$w$} (2);
+  \node[state] (7) at (3,-1) {\matrix 0030};
+  \draw[fire] (7) -- node[left] {$w$} (3);
+  \draw[fire] (6) -- node[above] {$v$} (7);
+\end{tikzpicture}
+
+% Revoyons cette action au ralenti...
+
+% On remarque qu'Adam, contrairement à Carl, n'a aucun blocage.
+% (C'est un réseau épanoui.)
+
+%%%
+
+% Notre chapitre 1 est maintenant terminé.
+
+% À bientôt pour le chapitre 2: pourquoi ?
+
+\end{document}

+from t2g import *
+
+#######################
+
+load("chap2-gates.tex")
+
+state = {"low": 0, "high": 1}
+active = {"down": "", "up": ""}
+
+frame(.8)
+active["down"] = "active"
+frame(.8)
+active["down"] = ""
+state = {"low": 1, "high": 0}
+frame(.8)
+active["up"] = "active"
+frame(.8)
+
+gif("chap2-gates.gif")
+
+#######################
+
+load("chap2-track.tex")
+
+state = {"far": 1, "before": 0, "inside": 0}
+active = {"enter": "", "exit": "", "approach": ""}
+
+frame(.8)
+active["approach"] = "active"
+frame(.8)
+active["approach"] = ""
+state = {"far": 0, "before": 1, "inside": 0}
+frame(.8)
+active["enter"] = "active"
+frame(.8)
+active["enter"] = ""
+state = {"far": 0, "before": 0, "inside": 1}
+frame(.8)
+active["exit"] = "active"
+frame(.8)
+
+gif("chap2-track.gif")
+
+#######################
+
+load("chap2-draft.tex")
+
+state = {"far": 1, "before": 0, "inside": 0, "low": 0, "high": 1, "godown": 0, "goup": 0}
+active = {"enter": "", "exit": "", "approach": "", "down": "", "up": ""}
+
+frame(.8)
+active["approach"] = "active"
+frame(.8)
+active["approach"] = ""
+state = {"far": 0, "before": 1, "inside": 0, "low": 0, "high": 1, "godown": 1, "goup": 0}
+frame(.8)
+active["down"] = "active"
+frame(.8)
+active["down"] = ""
+state = {"far": 0, "before": 1, "inside": 0, "low": 1, "high": 0, "godown": 0, "goup": 0}
+frame(.8)
+active["enter"] = "active"
+frame(.8)
+active["enter"] = ""
+state = {"far": 0, "before": 0, "inside": 1, "low": 1, "high": 0, "godown": 0, "goup": 0}
+frame(.8)
+active["exit"] = "active"
+frame(.8)
+active["exit"] = ""
+state = {"far": 1, "before": 0, "inside": 0, "low": 1, "high": 0, "godown": 0, "goup": 1}
+frame(.8)
+active["up"] = "active"
+frame(.8)
+
+gif("chap2-draft.gif")
+
+#######################
+
+load("chap2-test.tex")
+
+state = {"far": 1, "before": 0, "inside": 0, "low": 0, "high": 1, "godown": 0, "goup": 0}
+active = {"enter": "", "exit": "", "approach": "", "down": "", "up": "",
+          0: "active"}
+active.update((s, "") for s in range(1,5))
+
+frame(.8)
+active["approach"] = "active"
+frame(.8)
+active["approach"] = active[0] = ""
+active[1] = "active"
+state = {"far": 0, "before": 1, "inside": 0, "low": 0, "high": 1, "godown": 1, "goup": 0}
+frame(.8)
+active["down"] = "active"
+frame(.8)
+active["down"] = active[1] = ""
+active[2] = "active"
+state = {"far": 0, "before": 1, "inside": 0, "low": 1, "high": 0, "godown": 0, "goup": 0}
+frame(.8)
+active["enter"] = "active"
+frame(.8)
+active["enter"] = active[2] = ""
+active[3] = "active"
+state = {"far": 0, "before": 0, "inside": 1, "low": 1, "high": 0, "godown": 0, "goup": 0}
+frame(.8)
+active["exit"] = "active"
+frame(.8)
+active["exit"] = active[3] = ""
+active[4] = "active"
+state = {"far": 1, "before": 0, "inside": 0, "low": 1, "high": 0, "godown": 0, "goup": 1}
+frame(.8)
+active["up"] = "active"
+frame(.8)
+
+gif("chap2-test.gif", dpi=450)

+\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}
+
+\usepackage[utf8]{inputenc}
+
+\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=-1pt]
+
+\tikzstyle{fire}=[arrows={-Straight Barb[scale=.6]},
+  shorten >=-2pt, shorten <=-1pt,
+  draw=blue!50!gray!50!white,
+  line width=2pt,
+  line cap=round,
+  rounded corners]
+
+\tikzstyle{active}=[draw=green!50!gray!50!white,
+  fill=green!70!gray!10!white]
+
+\begin{document}
+
+%%FRAME
+
+\begin{tikzpicture}[scale=1.2]
+  \node[trans,{{ active["approach"] }}] (approach) at (0,0) {};
+  \node[rotate=45] at (approach) {\tiny\textsf{approche}};
+  \node[place,tokens={{ state["before"] }}] (before) at (1,0) {};
+  \node[below] at (before.south) {\tiny\textsf{avant}};
+  \node[trans,{{ active["enter"] }}] (enter) at (2,0) {};
+  \node[rotate=45] at (enter) {\tiny\textsf{entre}};
+  \node[place,tokens={{ state["inside"] }}] (inside) at (3,0) {};
+  \node[below] at (inside.south) {\tiny\textsf{dedans}};
+  \node[trans,{{ active["exit"] }}] (exit) at (4,0) {};
+  \node[rotate=45] at (exit) {\tiny\textsf{sort}};
+  \node[place,tokens={{ state["far"] }}] (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,tokens={{ state["low"] }}] (low) at (2,1) {};
+  \node[below] at (low.south) {\tiny\textsf{bas}};
+  \node[place,tokens={{ state["high"] }}] (high) at (2,3) {};
+  \node[above] at (high.north) {\tiny\textsf{haut}};
+  \node[trans,{{ active["down"] }}] (down) at (1,2) {};
+  \node[rotate=45] at (down) {\tiny\textsf{baisse}};
+  \node[trans,{{ active["up"] }}] (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={{ state["godown"] }}] (godown) at (0,2) {};
+  \node[above] at (godown.north) {\tiny\textsf{descendre}};
+  \draw[arc] (approach) -- (godown);
+  \draw[arc] (godown) -- (down);
+  \node[place,tokens={{ state["goup"] }}] (goup) at (4,2) {};
+  \node[above] at (goup.north) {\tiny\textsf{relever}};
+  \draw[arc] (exit) -- (goup);
+  \draw[arc] (goup) -- (up);
+\end{tikzpicture}
+
+%%/FRAME
+
+\end{document}

+\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}
+
+\usepackage[utf8]{inputenc}
+
+\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=-1pt]
+
+\tikzstyle{fire}=[arrows={-Straight Barb[scale=.6]},
+  shorten >=-2pt, shorten <=-1pt,
+  draw=blue!50!gray!50!white,
+  line width=2pt,
+  line cap=round,
+  rounded corners]
+
+\tikzstyle{active}=[draw=green!50!gray!50!white,
+  fill=green!70!gray!10!white]
+
+\begin{document}
+
+%%FRAME
+
+\begin{tikzpicture}[scale=1.2]
+  \node[place,tokens={{ state["low"] }}] (low) at (0,0) {};
+  \node[below] at (low.south) {\tiny\textsf{bas}};
+  \node[place,tokens={{ state["high"] }}] (high) at (0,2) {};
+  \node[above] at (high.north) {\tiny\textsf{haut}};
+  \node[trans,{{ active["down"] }}] (down) at (-1,1) {};
+  \node[rotate=45] at (down) {\tiny\textsf{baisse}};
+  \node[trans,{{ active["up"] }}] (up) at (1,1) {};
+  \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);
+  {% if state["low"] == 1 %}
+  \node at (2.5,1) {\includegraphics[width=2cm]{../chap2/low}};
+  {% else %}  
+  \node at (2.5,1) {\includegraphics[width=2cm]{../chap2/high}};
+  {% endif %}
+\end{tikzpicture}
+
+%%/FRAME
+
+\end{document}

+\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}
+
+\usepackage[utf8]{inputenc}
+
+\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]
+
+\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}
+
+%%FRAME
+
+\begin{tikzpicture}[scale=1.2]
+  \node[trans,{{ active["approach"] }}] (approach) at (0,0) {};
+  \node[rotate=45] at (approach) {\tiny\textsf{approche}};
+  \node[place,tokens={{ state["before"] }}] (before) at (1,0) {};
+  \node[below] at (before.south) {\tiny\textsf{avant}};
+  \node[trans,{{ active["enter"] }}] (enter) at (2,0) {};
+  \node[rotate=45] at (enter) {\tiny\textsf{entre}};
+  \node[place,tokens={{ state["inside"] }}] (inside) at (3,0) {};
+  \node[below] at (inside.south) {\tiny\textsf{dedans}};
+  \node[trans,{{ active["exit"] }}] (exit) at (4,0) {};
+  \node[rotate=45] at (exit) {\tiny\textsf{sort}};
+  \node[place,tokens={{ state["far"] }}] (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,tokens={{ state["low"] }}] (low) at (2,1) {};
+  \node[below] at (low.south) {\tiny\textsf{bas}};
+  \node[place,tokens={{ state["high"] }}] (high) at (2,3) {};
+  \node[above] at (high.north) {\tiny\textsf{haut}};
+  \node[trans,{{ active["down"] }}] (down) at (1,2) {};
+  \node[rotate=45] at (down) {\tiny\textsf{baisse}};
+  \node[trans,{{ active["up"] }}] (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={{ state["godown"] }}] (godown) at (0,2) {};
+  \node[above] at (godown.north) {\tiny\textsf{descendre}};
+  \draw[arc] (approach) -- (godown);
+  \draw[arc] (godown) -- (down);
+  \node[place,tokens={{ state["goup"] }}] (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,{{ active[0] }}] (0) at (0,0) {\matrix 1000001};
+    \node[state,{{ active[1] }}] (1) at (1,0) {\matrix 1100100};
+    \node[state,{{ active[2] }}] (2) at (2,0) {\matrix 0001100};
+    \node[state,{{ active[3] }}] (3) at (1.5,-1) {\matrix 0001010};
+    \node[state,{{ active[4] }}] (4) at (.5,-1) {\matrix 0011001};
+    \draw[fire,{{ active["approach"] }}] (0) -- node[above]{\tiny\textsf{approche}} (1);
+    \draw[fire,{{ active["down"] }}] (1) -- node[above]{\tiny\textsf{baisse}} (2);
+    \draw[fire,{{ active["enter"] }}] (2) |- node[left,pos=.1]{\tiny\textsf{entre}} (3);
+    \draw[fire,{{ active["exit"] }}] (3) -- node[above]{\tiny\textsf{sort}} (4);
+    \draw[fire,{{ active["up"] }}] (4) -| node[left,pos=.6]{\tiny\textsf{lève}} (0);
+  \end{scope}
+\end{tikzpicture}
+
+%%/FRAME
+
+\end{document}

+\documentclass[multi={tikzpicture},crop=true,border=5pt]{standalone}
+
+\usepackage[utf8]{inputenc}
+
+\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=-1pt]
+
+\tikzstyle{fire}=[arrows={-Straight Barb[scale=.6]},
+  shorten >=-2pt, shorten <=-1pt,
+  draw=blue!50!gray!50!white,
+  line width=2pt,
+  line cap=round,
+  rounded corners]
+
+\tikzstyle{active}=[draw=green!50!gray!50!white,
+  fill=green!70!gray!10!white]
+
+\begin{document}
+
+%%FRAME
+
+\begin{tikzpicture}[scale=1.2]
+  \node[trans,{{ active["approach"] }}] (approach) at (0,0) {};
+  \node[rotate=45] at (approach) {\tiny\textsf{approche}};
+  \node[place,tokens={{ state["before"] }}] (before) at (1,0) {};
+  \node[below] at (before.south) {\tiny\textsf{avant}};
+  \node[trans,{{ active["enter"] }}] (enter) at (2,0) {};
+  \node[rotate=45] at (enter) {\tiny\textsf{entre}};
+  \node[place,tokens={{ state["inside"] }}] (inside) at (3,0) {};
+  \node[below] at (inside.south) {\tiny\textsf{dedans}};
+  \node[trans,{{ active["exit"] }}] (exit) at (4,0) {};
+  \node[rotate=45] at (exit) {\tiny\textsf{sort}};
+  \node[place,tokens={{ state["far"] }}] (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);
+  {% if state["far"] == 1 %}
+  \node at (5.5,-.5) {\includegraphics[width=2cm]{../chap2/far}};
+  {% elif state["before"] == 1 %}
+  \node at (5.5,-.5) {\includegraphics[width=2cm]{../chap2/close}};
+  {% else %}  
+  \node at (5.5,-.5) {\includegraphics[width=2cm]{../chap2/inside}};
+  {% endif %}
+\end{tikzpicture}
+
+%%/FRAME
+
+\end{document}

+\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}

+import tempfile, os, os.path, inspect
+import jinja2
+
+class T2G (object) :
+    def __init__ (self, env, header, body, trailer) :
+        self.env = env
+        self.tpl = jinja2.Template(body)
+        self.trailer = trailer
+        self.frames = []
+        self.tmp = tempfile.TemporaryDirectory(suffix=".t2g", dir=os.getcwd())
+        self.out = open(os.path.join(self.tmp.name, "frames.tex"), "w")
+        self.out.write(header)
+    def frame (self, duration) :
+        env = self.env.copy()
+        self.out.write("\n%%%%%% FRAME %s\n%s\n"
+                       % (len(self.frames), self.tpl.render(**env)))
+        self.frames.append(duration * 100)
+    def gif (self, path, dpi=500) :
+        self.out.write("\n%%%%%% TRAILER\n\n%s\n" % self.trailer)
+        self.out.flush()
+        cwd = os.getcwd()
+        path = os.path.join(cwd, path)
+        try :
+            os.chdir(self.tmp.name)
+            os.system("latexmk -pdf -cd -f frames.tex")
+            print("extracting frames")
+            os.system("convert -background white -alpha remove -density %s"
+                      " frames.pdf frames.png" % dpi)
+            print("building GIF")
+            os.system("convert -layers OptimizeFrame -loop 0 %s %s"
+                      % (" ".join("-delay %s frames-%s.png" % (duration, frame)
+                                  for frame, duration in enumerate(self.frames)),
+                         path))
+            print("optimizing GIF")
+            os.system("gifsicle --batch --optimize=3 %s" % path)
+        finally :
+            os.chdir(cwd)
+
+__t2g__ = None
+
+def load (path) :
+    global __t2g__
+    txt = open(path).read()
+    header, txt = txt.split("%%FRAME")
+    body, trailer = txt.split("%%/FRAME")
+    stack = inspect.stack()
+    __t2g__ = T2G(stack[1].frame.f_globals, header, body, trailer)
+
+def frame (duration) :
+    global __t2g__
+    assert __t2g__, "no template loaded"
+    __t2g__.frame(duration)
+
+def gif (path, dpi=500) :
+    global __t2g__
+    assert __t2g__, "no template loaded"
+    __t2g__.gif(path, dpi)