Examples, ...

.gitignore

@@ -7,3 +7,4 @@
 *.blg
 *.toc
 
+_build/*

Makefile

@@ -1,8 +1,25 @@
 TEX=report
-all: $(TEX).tex
+
+DOTFIGURES=coffeemachine.game.tex coffeemachine.strat.tex
+
+###################################################
+
+DOTFIGURES_PATH=$(patsubst %,_build/dot/%,$(DOTFIGURES))
+
+all: $(TEX).tex $(DOTFIGURES_PATH)
 	pdflatex $(TEX)
 	bibtex $(TEX)
 	pdflatex $(TEX)
 	pdflatex $(TEX)
 
+_build:
+	mkdir -p _build
+	mkdir -p _build/dot
+
+_build/dot/%.tex: dot/%.dot _build
+	cat $< | dot2tex -ftikz --codeonly > $@
+
+clean:
+	rm -rf _build
+	rm -f *.aux *.bbl *.blg *.log *.out *.pdf *.toc
 

concurgames.sty

@@ -4,6 +4,9 @@
 \usepackage[normalem]{ulem}
 \usepackage{MnSymbol}
 \usepackage{stmaryrd}
+\usepackage{tikz}
+
+\usetikzlibrary{shapes,arrows}
 
 \newcommand{\con}{\operatorname{Con}}
 \newcommand{\confl}{\raisebox{0.5em}{\uwave{\hspace{2em}}}}
@@ -20,3 +23,8 @@
 \newcommand{\strParallel}{\parallel}
 
 \newcommand{\seman}[1]{\llbracket{} #1 \rrbracket}
+
+\newcommand{\includedot}[2][]{%
+	\begin{tikzpicture}[>=latex,line join=bevel,#1]
+	\input{_build/dot/#2.tex}
+	\end{tikzpicture}}

dot/coffeemachine.game.dot

@@ -0,0 +1,7 @@
+digraph {
+0 [ label="coin (0)",color = "red"]
+1 [ label="getCoffee (1)",color = "red"]
+2 [ label="getTea (2)",color = "red"]
+3 [ label="coffee (3)",color = "green"]
+4 [ label="tea (4)",color = "green"]
+}

dot/coffeemachine.strat.dot

@@ -0,0 +1,12 @@
+digraph {
+5 [ label="coin (5)",color = "red"]
+6 [ label="getCoffee (6)",color = "red"]
+7 [ label="getTea (7)",color = "red"]
+8 [ label="coffee (8)",color = "green"]
+9 [ label="tea (9)",color = "green"]
+5 -> 9 []
+5 -> 8 []
+6 -> 8 []
+7 -> 9 []
+}
+

report.tex

@@ -8,6 +8,7 @@
 \usepackage{indentfirst}
 \usepackage{enumerate}
 \usepackage{cite}
+\usepackage{caption}
 \usepackage[left=2cm,right=2cm,top=2cm,bottom=2cm]{geometry}
 
 % Custom packages
@@ -87,6 +88,9 @@ Player or Opponent.
 	$\config(A)$ is the set of configurations of $A$.
 \end{definition}
 
+A configuration can thus be seen as a valid state of the game. $\config(A)$
+plays a major role in definitions and proofs on games and strategies.
+
 \begin{notation}
 	For $x,y \in \config(A)$, $x \forkover{e} y$ states that $y = x \cup
 	\set{e}$ (and that both are valid configurations). It is also possible to
@@ -102,17 +106,57 @@ Player or Opponent.
 	$\rho$ have been reversed.
 \end{definition}
 
+For instance, one could imagine a game modeling the user interface of a coffee
+machine: Player is the coffee machine, while Opponent is a user coming to buy a
+drink.
+
+\begin{example}[Coffee machine]
+	In this example (and all the following), a red-circled node has a negative
+	polarity, while a green-circled one has a positive polarity.
+
+	Here, the game has only event, but no edges: nothing in the rules of the
+	game constrains the program to behave in a certain way, only its
+	\emph{strategy} will do that.
+
+	\smallskip
+
+	\includedot[scale=0.9]{coffeemachine.game}
+	\captionof{figure}{Coffee machine game}
+
+	The user can insert a coin, ask for a coffee or ask for a tea. The coffee
+	machine can deliver a coffee or deliver a tea.
+\end{example}
+
 \begin{definition}[pre-strategy]
-	A \emph{pre-strategy} $\sigma: S \to \calG$ is a total map of ESPs, where
-	$\calG$ is the game on which the strategy plays, such that
+	A \emph{pre-strategy} $\sigma: S \to A$ is a total map of ESPs, where
+	$A$ is the game on which the strategy plays, such that
 	\begin{enumerate}[(i)]
-		\item $\forall x \in \config(S), \sigma(x) \in \config(\calG)$;
-		\item $\forall s,s' \in \config(S), \sigma(s) = \sigma(s') \implies
-			s = s'$ (local injectivity);
-		\item $\forall s \in S, \rho_\calG(\sigma(s)) = \rho_S(s)$
+		\item $\forall x \in \config(S), \sigma(x) \in \config(A)$;
+		\item \textit{(local injectivity)} $\forall s,s' \in \config(S),
+			\sigma(s) = \sigma(s') \implies s = s'$;
+		\item $\forall s \in S, \rho_A(\sigma(s)) = \rho_S(s)$
 	\end{enumerate}
 \end{definition}
 
+\begin{example}[Coffee machine, cont.]
+	Let's now define a possible \emph{pre-strategy} for our coffee machine
+	example.
+
+	\smallskip
+
+	\begin{centering}
+	\includedot{coffeemachine.strat}
+	\captionof{figure}{Coffee machine strategy}
+	\end{centering}
+
+	This pre-strategy makes sense: the coffee machine software waits for the
+	user to both put a coin and press ``coffee'' before delivering a coffee,
+	and same goes for tea. Though, what happens if the user inserts a coin and
+	presses \emph{both} buttons at the same time? Here, the coffee machine can
+	dispense both drinks. This behavior is surely unwanted: one should add a
+	conflict relation between coffee and tea, to ensure that only one of the
+	two drinks can be dispensed.  \end{example}
+
 \begin{definition}[strategy]
 	A \emph{strategy} is a pre-strategy $\sigma : S \to A$ that
 	``behaves well'', \ie{} that is