diff --git a/manual/figures/updown-automaton.fig b/manual/figures/updown-automaton.fig
new file mode 100644
index 0000000..0978eb3
--- /dev/null
+++ b/manual/figures/updown-automaton.fig
@@ -0,0 +1,25 @@
+#FIG 3.2  Produced by xfig version 3.2.5b
+Landscape
+Center
+Metric
+A4      
+100.00
+Single
+-2
+1200 2
+1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 1350 1350 315 315 1350 1350 1350 1665
+1 3 0 1 0 7 50 -1 -1 0.000 1 0.0000 3150 1350 315 315 3150 1350 3150 1665
+3 0 0 1 0 7 50 -1 -1 0.000 0 1 0 3
+	0 0 1.00 60.00 120.00
+	 1575 1125 2250 900 2925 1125
+	 0.000 1.000 0.000
+3 0 0 1 0 7 50 -1 -1 0.000 0 1 0 3
+	0 0 1.00 60.00 120.00
+	 2925 1575 2250 1800 1575 1575
+	 0.000 1.000 0.000
+4 1 0 50 -1 0 12 0.0000 6 150 525 3150 1395 Down\001
+4 0 0 50 -1 0 12 0.0000 6 195 1935 3510 1395 \\lstinline{x = last x - 1}\001
+4 1 0 50 -1 0 12 0.0000 6 195 255 1350 1395 Up\001
+4 2 0 50 -1 0 12 0.0000 6 195 1995 990 1395 \\lstinline{x = last x + 1}\001
+4 1 0 50 -1 0 12 0.0000 6 210 1815 2250 900 $\\mathtt{x} \\geq 10$\001
+4 1 0 50 -1 0 12 0.0000 6 210 1650 2250 1935 $\\mathtt{x} \\leq 0$\001
diff --git a/manual/figures/updown-automaton.pdf b/manual/figures/updown-automaton.pdf
new file mode 100644
index 0000000..2737b3d
Binary files /dev/null and b/manual/figures/updown-automaton.pdf differ
diff --git a/manual/figures/updown-automaton.tex b/manual/figures/updown-automaton.tex
new file mode 100644
index 0000000..39e7e4d
--- /dev/null
+++ b/manual/figures/updown-automaton.tex
@@ -0,0 +1,24 @@
+\begin{picture}(0,0)%
+\includegraphics{figures/updown-automaton}%
+\end{picture}%
+\setlength{\unitlength}{4144sp}%
+%
+\begingroup\makeatletter\ifx\SetFigFont\undefined%
+\gdef\SetFigFont#1#2{%
+  \fontsize{#1}{#2pt}%
+  \selectfont}%
+\fi\endgroup%
+\begin{picture}(2550,1296)(976,-1174)
+\put(3151,-556){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}Down}%
+}}}}
+\put(3511,-556){\makebox(0,0)[lb]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}\lstinline{x = last x - 1}}%
+}}}}
+\put(1351,-556){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}Up}%
+}}}}
+\put(991,-556){\makebox(0,0)[rb]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}\lstinline{x = last x + 1}}%
+}}}}
+\put(2251,-61){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}$\mathtt{x} \geq 10$}%
+}}}}
+\put(2251,-1096){\makebox(0,0)[b]{\smash{{\SetFigFont{12}{14.4}{\color[rgb]{0,0,0}$\mathtt{x} \leq 0$}%
+}}}}
+\end{picture}%
diff --git a/manual/heptagon-manual.tex b/manual/heptagon-manual.tex
index 368709f..c0e6fb4 100644
--- a/manual/heptagon-manual.tex
+++ b/manual/heptagon-manual.tex
@@ -462,8 +462,8 @@ activation instant.
 \paragraph{Example}
 \label{sec:example}
 
-The following example gives the node \texttt{updown}. This node is defined by an
-automaton composed of two states:
+The following example gives the node \texttt{updown}. This node is defined by the
+automaton given in Figure~\ref{fig:updown-automaton}, composed of two states:
 \begin{itemize}
 \item the state \texttt{Up} gives to \texttt{x} its previous value augmented of 1
 \item the state \texttt{Down} gives to \texttt{x} its previous value diminued of 1
@@ -476,6 +476,13 @@ This automaton comprises two transitions:
   equal 0.
 \end{itemize}
 
+\begin{figure}[htb]
+  \centering
+  \input{figures/updown-automaton}
+  \caption{Automaton of the \texttt{updown} node}
+  \label{fig:updown-automaton}
+\end{figure}
+
 \begin{lstlisting}
 node updown() returns (y:int)
   var last x:int = 0;
@@ -493,9 +500,9 @@ tel
 \end{lstlisting}
 
 \[
-\begin{streams}{14}
-\text{current state} & Up & Up & Up & Up & Up & Up & Up & Up & Up & Up & Down & Down & Down & \ldots\\\hline
-\mathtt{y} & 1 & 2 & 3 & 4 & 5 & 6 & 7 & 8 & 9 & 10 & 9 & 8 & 7 & \ldots\\\hline
+\begin{streams}{9}
+\text{current state} & Up & Up & \ldots & Up & Up & Down & Down & Down & \ldots\\\hline
+\mathtt{y} & 1 & 2 & \ldots & 9 & 10 & 9 & 8 & 7 & \ldots\\\hline
 \end{streams}
 \]
 
@@ -601,9 +608,12 @@ If the backend support parametricity (like in Java), static parameters are kept
 
 Memory allocation~\cite{Gerard:2012} avoids unnecessary array copies within the nodes automatically (it can be enable with the \texttt{-memalloc} or \texttt{-O} options). In order to avoid copies when calling nodes, the user must add \emph{location annotations}. We will give here only a short introduction, the interested reader can refer to~\cite{Gerard:2012} for more details. They express the fact that a function modifies in-place its argument. For instance, consider this node that swaps two elements in an array:
 \begin{lstlisting}
-node swap(i, j:int; t_in:float^100 at r) returns (t_out:float^100 at r)
var t_tmp:float^100 at r; 
-let
  t_tmp = [ t_in with [i] = t_in[>j<] ]; 
-  t_out = [ t_tmp with [j] = t_in[>i<] ];
tel
+node swap(i, j:int; t_in:float^100 at r) returns (t_out:float^100 at r)
+var t_tmp:float^100 at r; 
+let
+  t_tmp = [ t_in with [i] = t_in[>j<] ]; 
+  t_out = [ t_tmp with [j] = t_in[>i<] ];
+tel
 \end{lstlisting}
 The location annotations are introduced by the keyword \lstinline{at} followed by a location name. All the streams with the same location name are guaranteed to be stored together in the generated code, so the function generated for \texttt{swap} will directly modify its argument in-place. 
 
@@ -613,9 +623,11 @@ Only located variables can be given to a function that expects located arguments
 \begin{lstlisting}
 node shuffle(i_arr, j_arr : int^m; q : int) = (v : float)
 var t, t_prev : float^n at r;
-let
  init<<r>> t_prev = t_0 fby t;
+let
+  init<<r>> t_prev = t_0 fby t;
   t = fold<<m>> swap(i_arr, j_arr, t_prev); 
-  v = t[>q<];
tel
+  v = t[>q<];
+tel
 \end{lstlisting}
 
 
@@ -627,11 +639,15 @@ external fun sort(a:int^100) = (o:int^100)
 \end{lstlisting}
 The imported function should respect the calling convention given in appendix \ref{sec:app-generated-code}. See the directory \texttt{examples/extern\_C} for a complete example.
 
-\section{BZR: Contracts for controller synthesis}
+Interface files can be compiled with \texttt{heptc}, in order to obtain a
+compiled interface (\texttt{.epci} file), necessary for the subsequent use of
+the declared types and values in other Heptagon programs.
+
+\subsection{Contracts for controller synthesis}
 \label{sec:extens-with-contr}
 
 Contracts are an extension of the Heptagon language, so as to allow to perform
-discrete controller synthesis on Heptagon programs. The extended language is
+discrete controller synthesis (DCS) on Heptagon programs. The extended language is
 named BZR.
 
 We associate to each node a \emph{contract}, which is a program associated with
@@ -666,7 +682,7 @@ let
 tel
 \end{lstlisting}
 
-\section{BZR Running Example:  Multi-task System}
+\section{Example with Contracts:  Multi-task System}
 \label{sec:multi-task-system}
 
 \subsection{Delayable Tasks}
@@ -708,7 +724,7 @@ node delayable(r,c,e:bool) returns (act:bool)
 
 The Figure~\ref{fig:n-del-task} shows then a node \texttt{ntasks} where $n$
 delayable tasks have been put in parallel. The tasks are inlined so as to be
-able to perform DSC on this node, taking into account the tasks' states. Until
+able to perform DCS on this node, taking into account the tasks' states. Until
 now, the only interest of modularity is, from the programmer's point of view, to
 be able to give once the delayable task code.
 
@@ -916,7 +932,7 @@ An example of main C code for the execution of this node would be then:
 \begin{lstlisting}[language=C]
 #include "example.h"
 
-int main(int argc, char * argv[]) \{
+int main(int argc, char * argv[]) {
   
   Example__f_m mem;
   t$_{1}$ x$_{1}$;
@@ -927,7 +943,7 @@ int main(int argc, char * argv[]) \{
   /* initialize memory instance */
   f_reset(&mem);
   
-  while(1) \{
+  while(1) {
     /* read inputs */
     scanf("...", &x$_{1}$, ..., &x$_{n}$);
 
@@ -936,8 +952,8 @@ int main(int argc, char * argv[]) \{
 
     /* write outputs */
     printf("...", ans.y$_{1}$, ..., ans.y$_{p}$);
-  \}
-\}
+  }
+}
 \end{lstlisting}
 
 The above code is nearly what is produce for the simulator with the \texttt{-s}
diff --git a/manual/macros.sty b/manual/macros.sty
index 27c5e47..ea1534c 100644
--- a/manual/macros.sty
+++ b/manual/macros.sty
@@ -50,8 +50,8 @@
 
 \lstdefinelanguage{Heptagon}
 {%
-  keywords={node,returns,let,tel,var,pre,fby,when,whenot,merge,if,then,else,or,not,at,init,map,fold,mapdold,foldi,mapi},%
-  morekeywords=[2]{automaton,state,until,unless,end,present,switch,inlined},%
+  keywords={node,returns,let,tel,var,pre,last,fby,when,whenot,merge,if,then,else,or,not,at,init,map,fold,mapdold,foldi,mapi},%
+  morekeywords=[2]{automaton,state,until,unless,end,present,switch,do,inlined},%
   morekeywords=[2]{contract,assume,enforce,with},%
   otherkeywords={->,&},%
   comment=[n]{(*}{*)},%
@@ -62,7 +62,7 @@
 %   morekeywords={link,to},%
 % }[keywords,comments]
 
-%% rËgles d'infÈrence
+%% regles d'inference
 
 \RequirePackage{mathpartir}
 
@@ -96,7 +96,7 @@
 %\newcommand{\ovfun}[1]{\xrightarrow{#1}}
 \newcommand{\ovfun}[1]{{\;-\mskip-1.5\thinmuskip\langle{#1}\rangle\!\!\!\rightarrow\;}}
 
-%% Typage --- gÈnÈral
+%% Typage --- general
 
 \DeclareMathOperator{\FV}{FV}
 \DeclareMathOperator{\FTV}{FTV}
@@ -111,7 +111,7 @@
 
 \newcommand{\mergeenv}{\uplus}
 
-%% Types de donnÈes
+%% Types de donnees
 
 \newcommand{\type}[3]{\ensuremath{#1\vdash#2:#3}}
 
@@ -194,7 +194,7 @@
 
 \newcommand{\subck}{\ensuremath{<:}}
 
-%% SÈmantique synchrone
+%% Semantique synchrone
 
 \newcommand{\clock}[1]{\ensuremath{\langle#1\rangle}}
 
@@ -264,7 +264,7 @@
 \shortcal{Y}
 \shortcal{Z}
 
-%% mots-clÈs
+%% mots-cles
 
 \newcommand{\m@thspace}{%
   \ifmmode\ \fi%
@@ -309,7 +309,7 @@
 \newcommand{\unop}[2]{\begkw{#1}{#2}}
 \newcommand{\funct}[2]{\begkw{#1}{#2}}
 
-%% Mots-clÈs Lucid Synchrone
+%% Mots-cles Lucid Synchrone
 
 \begkw{\Assume}{assume}
 \begkw{\Automaton}{automaton}
@@ -374,7 +374,7 @@
 
 \newcommand{\Nil}{\ensuremath{\mathit{nil}}}
 
-%% Mots-clÈs rÈpartition
+%% Mots-cles repartition
 
 \midkw{\At}{at}
 \begkw{\Site}{site}
@@ -408,7 +408,7 @@
   \ |\ \False \rightarrow #3
 }
 
-%% ThÈorËmes, dÈfinitions, remarques...
+%% Theoremes, definitions, remarques...
 
 \RequirePackage{amsmath}
 
@@ -429,7 +429,7 @@
 \newcommand{\noeuds}{n\oe uds\xspace}
 \newcommand{\Noeuds}{N\oe uds\xspace}
 
-%% Macros mathÈmatiques
+%% Macros mathematiques
 
 \providecommand{\tonfirst}{}
 \newcommand{\ton}[1][1]{\renewcommand{\tonfirst}{#1}\tonbis}
@@ -465,7 +465,7 @@
 
 
 
-%% Flots de donnÈes
+%% Flots de donnees
 
 \newenvironment{streams}[1]{%
   \setlength{\arraycolsep}{0.3cm}
@@ -495,7 +495,7 @@
 
 \renewenvironment{amodifier}{}{}
 
-%% BoÓte-noeud code
+%% Boite-noeud code
 
 \RequirePackage{alltt}