diff --git a/arduino/led_puzzle/doc/header.tex b/arduino/led_puzzle/doc/header.tex
new file mode 100644
index 0000000000000000000000000000000000000000..e4056791d018a6a52fe8271f3e212ae143e5b169
--- /dev/null
+++ b/arduino/led_puzzle/doc/header.tex
@@ -0,0 +1,253 @@
+% This is "sig-alternate.tex" V2.1 April 2013
+% This file should be compiled with V2.5 of "sig-alternate.cls" May 2012
+%
+% This example file demonstrates the use of the 'sig-alternate.cls'
+% V2.5 LaTeX2e document class file. It is for those submitting
+% articles to ACM Conference Proceedings WHO DO NOT WISH TO
+% STRICTLY ADHERE TO THE SIGS (PUBS-BOARD-ENDORSED) STYLE.
+% The 'sig-alternate.cls' file will produce a similar-looking,
+% albeit, 'tighter' paper resulting in, invariably, fewer pages.
+%
+% ----------------------------------------------------------------------------------------------------------------
+% This .tex file (and associated .cls V2.5) produces:
+% 1) The Permission Statement
+% 2) The Conference (location) Info information
+% 3) The Copyright Line with ACM data
+% 4) NO page numbers
+%
+% as against the acm_proc_article-sp.cls file which
+% DOES NOT produce 1) thru' 3) above.
+%
+% Using 'sig-alternate.cls' you have control, however, from within
+% the source .tex file, over both the CopyrightYear
+% (defaulted to 200X) and the ACM Copyright Data
+% (defaulted to X-XXXXX-XX-X/XX/XX).
+% e.g.
+% \CopyrightYear{2007} will cause 2007 to appear in the copyright line.
+% \crdata{0-12345-67-8/90/12} will cause 0-12345-67-8/90/12 to appear in the copyright line.
+%
+% ---------------------------------------------------------------------------------------------------------------
+% This .tex source is an example which *does* use
+% the .bib file (from which the .bbl file % is produced).
+% REMEMBER HOWEVER: After having produced the .bbl file,
+% and prior to final submission, you *NEED* to 'insert'
+% your .bbl file into your source .tex file so as to provide
+% ONE 'self-contained' source file.
+%
+% ================= IF YOU HAVE QUESTIONS =======================
+% Questions regarding the SIGS styles, SIGS policies and
+% procedures, Conferences etc. should be sent to
+% Adrienne Griscti (griscti@acm.org)
+%
+% Technical questions _only_ to
+% Gerald Murray (murray@hq.acm.org)
+% ===============================================================
+%
+% For tracking purposes - this is V2.0 - May 2012
+
+%\documentclass{sig-alternate-05-2015}
+
+% The following \documentclass options may be useful:
+
+% preprint Remove this option only once the paper is in final form.
+% 10pt To set in 10-point type instead of 9-point.
+% 11pt To set in 11-point type instead of 9-point.
+% authoryear To obtain author/year citation style instead of numeric.
+
+\usepackage{amsmath}
+%\usepackage{fancyvrb}
+
+
+%\usepackage{makeidx} % allows for indexgeneration
+%
+%
+%\frontmatter % for the preliminaries
+%
+%\pagestyle{headings} % switches on printing of running heads
+
+
+\hypersetup{colorlinks=true,citecolor=blue,linkcolor=blue,filecolor=blue,urlcolor=blue}
+
+\usepackage{color,xcolor,myxcolor}
+\definecolor{grey}{rgb}{0.745,0.745,0.745}
+
+
+%% NEUTRALISER LA GESTION FONTES/COULEURS DE XFIG ?
+\gdef\SetFigFont#1#2#3#4#5#6{#6}
+
+
+%% DIVERS ...
+\usepackage{mathptmx}
+\usepackage{helvet}
+\usepackage{version}
+ \usepackage{ragged2e}
+
+\usepackage{listings}
+\usepackage{wrapfig}
+%\usepackage{listingsutf8}
+
+
+\lstset{
+% inputencoding=utf8/latin1,
+ captionpos=b,
+ xleftmargin=0pt,
+ xrightmargin=5pt,
+ abovecaptionskip=10pt,
+ framexleftmargin=0pt,
+ framexrightmargin=5pt,
+ framextopmargin=5pt,
+ framexbottommargin=0pt,
+ escapechar={&,<,>},
+ alsoletter={&},
+ escapechar={\&},
+ alsoletter={\&},
+ escapechar={_},
+ alsoletter={_},
+ basicstyle=\scriptsize\ttfamily,
+ keywordstyle=\color{green4},
+ keywordstyle=[2]\color{IndianRed3},
+ keywordstyle=[3]\color{blue4},
+ keywordstyle=[4]\color{DeepPink3},
+ backgroundcolor=\color{LightGray},
+ rulesepcolor=\color{LightGray},
+ stringstyle=\ttfamily\color{red!50!brown},
+ identifierstyle=,
+ numbers=none,
+% column=fixed,%% XXX keyval package clash
+ commentstyle=\color{DarkGreen}\itshape,
+ frame=shadowbox,
+ escapeinside={$$},%
+ showstringspaces=false,
+}
+\lstset{}
+
+\lstdefinelanguage{trace}{%
+ morekeywords={call,exit,fail,top},
+ morekeywords=[2]{sat,try},
+ morekeywords=[3]{},
+ morekeywords=[4]{usat},
+ sensitive=false,
+ stringstyle=\color{Orange},
+ numberstyle=\color{LightGray},
+ commentstyle=\color{DarkGreen},
+ morecomment=[s][\color{goldenrod4}]{"}{"},
+ morecomment=[s]{[}{]}
+ }
+\lstdefinelanguage{liosi}{%
+ morekeywords={input,output,sock_addr,sock_port},
+ morekeywords=[2]{int,bool,real},
+}
+\lstdefinelanguage{adacstimu}{%
+ morekeywords={DEBUT_SCENARIO, FIN_SCENARIO},
+ morekeywords=[2]{GEN_MSG, ATTENDRE, CCT},
+ morekeywords=[3]{FAUX,VRAI},
+ morekeywords=[4]{TOR,ANA,VALUE},
+ sensitive=false,
+ moredelim=[l][\ttfamily\green]{CC\ },
+ morecomment=[l]{CM},
+}
+\lstdefinelanguage{rif}{%
+ morekeywords={inputs, outputs, locals},
+ morekeywords=[2]{true,false},
+ morekeywords=[3]{},
+ morekeywords=[4]{bool,int,real},
+ sensitive=false,
+ morecomment=[l]{--},
+ morecomment=[s]{(*}{*)}
+}
+\lstdefinelanguage{lutin}{%
+ morekeywords={assert,exist,run,in,let,node,returns,include},
+ morekeywords=[2]{pre,and,or,not,if,then,else},%XXX'=>'?
+ morekeywords=[3]{exception,raise,try,loop,fby,while,raise,catch,trap,with,do},
+ morekeywords=[4]{bool,int,real},
+ sensitive=false,
+ morecomment=[l]{--},
+ morecomment=[s]{(*}{*)},
+}
+
+\lstdefinelanguage{lustre}{%
+ morekeywords={node,returns,assert,var,const,let,tel,in},
+ morekeywords=[2]{pre,current,merge,when,step,and,or,if,with,then,else,not},%XXX'=>'?
+ morekeywords=[3]{true,false},
+ morekeywords=[4]{bool,int,real},
+ sensitive=false,
+ morecomment=[l]{--},
+ morecomment=[s][\color{goldenrod4}]{<<}{>>},
+ morecomment=[s]{(*}{*)},
+}
+\lstdefinelanguage{tuareg}{%
+ morekeywords={function,fun,match,with,let,in,val,type,and,;;,'=',rec}, % try
+ morekeywords=[2]{if,then,else,ref,not,or,+,raise},%XXX'=>'?
+ morekeywords=[3]{option,list,string,unit,bool,int,float,ct,List,Hashtbl,Not\_found,Filename,Sys,Event},
+ morekeywords=[4]{rdbg},
+ morekeywords=[6]{},
+ morestring=[b]",
+ sensitive=false,
+ morecomment=[l]{--},
+ morecomment=[s]{(*}{*)},
+ escapechar={!},
+ escapeinside=''
+}
+\lstdefinelanguage{custom}{%
+ morestring=[b]",
+ sensitive=false,
+ morecomment=[l]{--},
+ morestring=[b]",
+ escapeinside={(*@}{@*)},
+showspaces=false, % show spaces adding particular underscores
+showtabs=false, % show tabs within strings adding
+captionpos=b, % sets the caption-position to bottom
+breakatwhitespace=false, % sets if automatic breaks should only happen
+commandchars=\\!|,
+}
+
+
+\lstnewenvironment{rif} {\lstset{language=rif}} {}
+\lstnewenvironment{lutin} {\lstset{language=lutin}} {}
+\lstnewenvironment{lustre} {\lstset{language=lustre}} {}
+\lstnewenvironment{tuareg} {\lstset{language=tuareg}} {}
+
+
+\newcommand{\rdbg}[0]{\textsc{rdbg}}
+\newcommand{\lurette}[0]{\textsc{Lurette}}
+\newcommand{\ocaml}[0]{\textsc{Ocaml}}
+
+\newcommand{\Otawa}[0]{\textsc{Otawa}}
+\newcommand{\OWCET}[0]{\textsc{Otawa}}
+\newcommand{\Ogensim}[0]{\textsc{Osim}}
+\newcommand{\Lustre}[0]{\textsc{Lustre}}
+\newcommand{\Lutin}[0]{\textsc{Lutin}}
+\newcommand{\Lurette}[0]{\textsc{Lurette}}
+\newcommand{\Lesar}[0]{\textsc{Lesar}}
+
+%======================== Commandes spécifiques =========================
+%\input{commandes}
+\newcommand{\blue}[1]{{\color{DarkBlue}#1}}
+\newcommand{\red}[1]{{\color{red}#1}}
+\newcommand{\green}[1]{{\color{DarkGreen}#1}}
+\newcommand{\purple}[1]{{\color{purple2}#1}}
+\newcommand{\decal}{$\hspace*{1cm}$}
+\newcommand{\transTT}[1]{\raisebox{6pt}{$\underrightarrow{~~\mbox{\tt #1}~~}$}}
+\newcommand{\transMTH}[1]{\raisebox{6pt}{$\underrightarrow{~~\mbox{$#1$}~~}$}}
+\newcommand{\hide}[1]{}
+\newcommand{\NN}{\mbox{$\mathrm{I}\!\mathrm{N}$}}
+\newcommand{\MagentaIII}[1]{{\color{magenta3} #1}}
+\newcommand{\GreenIV}[1]{{\color{green4} #1}}
+\newcommand{\RedII}[1]{{\color{red2} #1}}
+\newcommand{\BlueII}[1]{{\color{blue2} #1}}
+\newcommand{\COMM}[1]{\mbox{\blue{// #1}}}
+\newcommand{\kw}[1]{\MagentaIII{\tt #1}}
+\newcommand{\ty}[1]{\GreenIV{\tt #1}}
+\newcommand{\lop}[1]{\BlueII{\tt #1}}
+\newcommand{\prog}[1]{\mbox{\tt #1}}
+\newcommand{\TR}{\mbox{$\cal T$}}
+
+\newcommand{\miparagraph}[1]{{\smallskip \noindent\bf {#1}}}
+\newcommand{\myparagraph}[1]{{\miparagraph {#1}}.}
+
+
+\usepackage{lastpage}
+
+\usepackage{acronym}
+
+
diff --git a/arduino/led_puzzle/doc/puzzle.org b/arduino/led_puzzle/doc/puzzle.org
index 459eeb6476cd7f7155509935e7df8e06f5535887..53dd398c54281cfd54f13fc2c799d1e77cdefcd8 100644
--- a/arduino/led_puzzle/doc/puzzle.org
+++ b/arduino/led_puzzle/doc/puzzle.org
@@ -10,8 +10,6 @@
Donnons du Lustre aux leds
-file:arduino.jpg
-
* Introduction
@@ -30,32 +28,32 @@ _corrects_.
actuellement. Or un programme de 64 cases (ou bits) est un
petit programme.
-Plusieurs approches sont possibles pour faire face à cette difficulté.
Au laboratoire Verimag, les axes de recherche visant à résoudre ce type
de problèmes concernent :
-- la conception de *Langages* de programmation empêchant les
- programmeurs de faire certaines erreurs;
+- la conception de *Langages* de programmation empêchant
+ certaines erreurs de programmation ;
- l'*Analyse de programmes* : conception d'algorithmes (des
programmes aussi) qui essaient de *prouver* qu'un autre programme
est « *correct* ».
-- l'automatisation des *tests* : conception d'algorithmes qui essaient
- de prouver qu'un programme n'est *pas* correct.
+- l'automatisation des *tests* : un test qui échoue prouve qu'un programme n'est *pas* correct.
-Pour illustrer tous ces axes de recherche, nous proposons une petite démonstration
-permettant de montrer
+Pour illustrer tous ces axes de recherche, nous allons vous montrer :
1. quelques exemples de programmes écrit en Lustre, un langage inventé
- au laboratoire et conçu pour mettre en oeuvre des systèmes
+ au laboratoire et conçu pour mettre en \oeuvre des systèmes
embarqués critiques ;
2. comment un tel programme peut-être embarqué sur un système (ici,
une carte =Arduino=) ;
3. comment prouver automatiquement des propriétés sur ces programmes ;
4. comment tester automatiquement ces programmes.
-Il s'agit donc de valider un petit système, composé d'un
-programme Lustre et d'une carte =Arduino=, comportant 2 entrées,
-contrôllées par un bouton rouge et un bouton bleu, et 5 sorties,
-représentées par 5 leds.
+Il s'agit donc de valider un petit système, composé d'un programme
+Lustre et d'une carte =Arduino=, comportant 2 entrées, *contrôllées*
+par un bouton rouge et un bouton bleu, et *actionnant* 5 leds.
+
+#+BEGIN_CENTER
+\includegraphics[width=.4\linewidth]{arduino.jpg}
+#+END_CENTER
Nous proposons plusieurs programmes. Pour chacun d'entre eux, l'effet
@@ -68,84 +66,41 @@ l'état dangereux. Nous montrerons ensuite comment des outils peuvent
automatiser la réponse à ces petits puzzles.
-* Puzzle 1
-
-- Bouton bleu : permute circulairement l'allumage des (jolies) leds
-- Bouton rouge : inverse l'état de la led 5
-
-* Puzzle 2
-
-
-- Bouton bleu : permute circulairement l'allumage des (jolies) leds
-- Bouton rouge : inverse l'état des leds 2 et 4
-
-#+BEGIN_SRC lustre
-node puzzle1 (red,blue:bool) returns (led1,led2,led3,led4,led5:bool);
-let
- led1 = true -> if blue then pre(led5) else pre(led1) ;
- led2 = false -> if blue then pre(led1) else if red then not(pre(led2)) else pre(led2) ;
- led3 = false -> if blue then pre(led2) else pre(led3) ;
- led4 = false -> if blue then pre(led3) else if red then not(pre(led4)) else pre(led4) ;
- led5 = true -> if blue then pre(led4) else pre(led5) ;
-tel
-#+END_SRC
+* Puzzles
+- Puzzle 1
+ - Bouton bleu : permute circulairement l'allumage des (jolies) leds
+ - Bouton rouge : inverse l'état de la led 5 (éteint \rightarrow
+ allumé \rightarrow éteint \rightarrow etc.)
-* Puzzle 3
+- Puzzle 2
+ - Bouton bleu : idem puzzle 1
+ - Bouton rouge : inverse l'état des leds 2 et 4
-- Bouton bleu : idem
-- Bouton rouge : inverse l'état d'une led qui circule à chaque pression de boutons
-* Puzzle 4
+- Puzzle 3
+ - Bouton bleu : idem puzzle 1,2
+ - Chaque pression d'un bouton décale la led « courante » : 1\rightarrow 2\rightarrow 3\rightarrow 4\rightarrow 5\rightarrow 1.
+ - Bouton rouge : inverse l'état de la led « courante/tournante »
-- Bouton rouge : inverse l'état d'une led qui circule en montant
- (=led1=, puis =led2=, etc.) Ã chaque pression
-- Bouton bleu : permutation circulaire des leds + permutation inverse
- (en descandant) de la led courante controllée par le bouton rouge
-
-* Puzzle 5
-
-#+BEGIN_SRC lustre
-true xor false = false xor true = true
-false xor false = true xor true = false
-
-true and true = true
-true and false = false and true = false and false = false
-#+END_SRC
-
-- Bouton bleu => la led courante devient le « xor » des 2 leds autour
-- Bouton red => la led courante devient le « and » des 2 leds autour
-- la led courante est la première au début, puis la deuxième, etc.
+- Puzzle 4
+ - idem puzzle 3 + le bleu décale la led courante dans le sens
+ inverse : 5\rightarrow 4\rightarrow 3\rightarrow 2\rightarrow
+ 1\rightarrow 5
+- Puzzle 5
+ - Chaque pression d'un bouton décale la led « courante » d'un cran (1\rightarrow 2\rightarrow 3\rightarrow 4\rightarrow 5\rightarrow 1).
+ - Bouton bleu : la led courante devient le « xor » des 2 leds autour
+ - Bouton red : la led courante devient le « and » des 2 leds autour
+
# Existe-t'il une configuration initiale qui rende le problème impossible ?
-* Puzzle 6
-
-- Bouton rouge => inverse l'état de la led 1
-- Bouton bleu => allume la led suivant la première led éteinte (en
- partant de la led1)
-
-#+BEGIN_SRC lustre
-node puzzle6(red,blue:bool)
-returns (led1,led2,led3,led4,led5:bool);
-var
- -- Xi = je suis la led qui suit la plus petite led eteinte
- X2, X3, X4, X5 : bool;
-let
- X2, X3, X4, X5 = (true, F, F, F) ->
- if not(pre(led1)) then (true, F, F, F) else
- if not(pre(led2)) then (F, true, F, F) else
- if not(pre(led3)) then (F, F, true, F) else
- if not(pre(led4)) then (F, F, F, true) else (F, F, F, F);
-
- led1 = F -> if red then not(pre(led1)) else pre(led1);
- led2 = F -> if blue and X2 then not(pre(led2)) else pre(led2);
- led3 = F -> if blue and X3 then not(pre(led3)) else pre(led3);
- led4 = F -> if blue and X4 then not(pre(led4)) else pre(led4);
- led5 = F -> if blue and X5 then not(pre(led5)) else pre(led5);
-tel
-#+END_SRC
+- Puzzle 6
+ - Bouton rouge : inverse l'état de la led 1
+ - Bouton bleu : allume la led suivant la première led éteinte (en
+ partant de la led1)
+
* Puzzle : saute mouton :noexport: