ajout d'un fichier manque pour compiler + faire tenir la doc en 2 pages

arduino/led_puzzle/doc/header.tex

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

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: