diff --git a/_oasis b/_oasis
index e68bde24bc80586eb0c88d4b5352400298b952b3..2e5d5805e3f9bbd152a1e6a3eb4ea65d0ae2dd53 100644
--- a/_oasis
+++ b/_oasis
@@ -1,6 +1,6 @@
OASISFormat: 0.4
Name: lustre-v6
-Version: 1.691
+Version: 1.692
Synopsis: The Lustre V6 Verimag compiler
Description: This package contains:
(1) lus2lic: the (current) name of the compiler (and interpreter via -exec).
diff --git a/arduino/led_puzlle/doc/puzzle.org b/arduino/led_puzlle/doc/puzzle.org
index ae307d8ea55c4f838d66d902fe493cd549736511..92f4391034f09719dc20f47866d26fbf9f33a9cd 100644
--- a/arduino/led_puzlle/doc/puzzle.org
+++ b/arduino/led_puzlle/doc/puzzle.org
@@ -8,28 +8,63 @@
#+DATE: Laboratoire Verimag -- Faites de la science !
-Du Lustre pour des jolies leds
+Du Lustre aux jolies leds
-* Introduction
+file:arduino.jpg
-Au laboratoire =Verimag=, on cherche à aider les ingénieurs
+* Introduction
+
+Au laboratoire =Verimag=, nous cherchons à aider les ingénieurs
informaticiens à _prouver automatiquement_ que leurs programmes sont
_corrects_.
-- C'est important, en particulier pour les *systèmes embarqués*.
-- Mais c'est difficile (explosion combinatoire ; $2^{64}>18*10^{15}$).
-
-Plusieurs approches :
-- *Langages* de programmation (empêcher les programmeurs de faire des erreurs)
-- *Analyse de programme*
-- Tests automatisés
-
-Nous allons embarquer des puzzles écrits en =Lustre= sur un =Arduino=
-
-file:arduino.jpg
+- La correction des programmes est cruciale, en particulier pour les
+ *systèmes embarqués*, car des vies sont souvent en jeu.
+- Mais elle est difficile à cause de *l'explosion combinatoire*. Une
+ bonne illustration de ce phénoméne est donnée par l'échiquer de
+ Sissa, comportant 1 grain de riz sur case 1, 2 grains sur la case
+ 2, 4 sur la case 3, 8 sur la case 4, etc. Un tel échiquier comporte
+ $2^{64}-1$ grains de riz, c'est à dire plus de 18\nbsp{}milliards de
+ grains, soit l'équivalent de 1000 ans de production mondiale de riz
+ 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;
+- 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.
+
+Pour illustrer tous ces axes de recherche, nous proposons une petite démonstration
+permettant de montrer
+1. quelques exemples de programmes écrit en Lustre, un langage inventé
+ 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 est donc 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.
+
+
+La propriété de sureté que l'on veut vérifier est « il est impossible
+d'allumer les 5 leds ». Pour chaque programme qu'on embarquera sur
+la carte, la question sera donc
+de savoir s'il est possible d'allumer les
+5 leds (signifiant qu'il y a un problème) en jouant sur les entrées.
+Nous montreront ensuite comment des outils peuvent automatiser la
+preuve de correction ou de non correction.
-L'objectif de ces petits puzzles programmés en Lustre est d'allumer
-toutes les lampes (led) Ã l'aide de 2 boutons : un rouge, et un bleu.
* Puzzle 1
diff --git a/arduino/led_puzlle/doc/puzzle.pdf b/arduino/led_puzlle/doc/puzzle.pdf
index 24d8a915fd70ce922530a1fed0b948259f7c5650..f0998096eba733bf4d2569df943c0d5e7b4a062a 100644
Binary files a/arduino/led_puzlle/doc/puzzle.pdf and b/arduino/led_puzlle/doc/puzzle.pdf differ
diff --git a/src/lv6version.ml b/src/lv6version.ml
index 787aeb9880431ed70a587921814828df2a25c985..3ce1895e510cb8d34144c02e4f622122ef32b086 100644
--- a/src/lv6version.ml
+++ b/src/lv6version.ml
@@ -1,7 +1,7 @@
(** Automatically generated from Makefile *)
let tool = "lus2lic"
let branch = "master"
-let commit = "691"
-let sha_1 = "4b986d0e2347825949ec0bb88100d125d46d14fd"
+let commit = "692"
+let sha_1 = "1adfcf741e7130599563f6c5667e829f5efad671"
let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")")
let maintainer = "jahier@imag.fr"
diff --git a/src/soc2c.ml b/src/soc2c.ml
index 4947ca6446f046d53b45f57c81c0131cd6a8e33d..cf62cccbf254f21507a6181a864541c74f2aeec3 100644
--- a/src/soc2c.ml
+++ b/src/soc2c.ml
@@ -1,4 +1,4 @@
-(* Time-stamp: <modified the 05/05/2017 (at 17:04) by Erwan Jahier> *)
+(* Time-stamp: <modified the 01/06/2017 (at 16:12) by Erwan Jahier> *)
(* let put (os: out_channel) (fmt:('a, unit, string, unit) format4) : 'a = *)
@@ -901,13 +901,15 @@ typedef float _float;
#define _true 1
#endif
// end of _SOC2C_PREDEF_TYPES
-" ^ (typedef_all licprg stbl main_soc )
- ^ (if needs_hfile then "#include \""^ base ^"_ext.h\"" else "")^
-"// User typedef
+// User typedef
#ifndef _"^base^"_TYPES
#define _"^base^"_TYPES\n");
output_string types_h_oc (user_typedef licprg);
- output_string types_h_oc ("#endif // enf of _"^base^"_TYPES\n");
+ output_string types_h_oc ("#endif // enf of _"^base^"_TYPES
+"
+ ^ (typedef_all licprg stbl main_soc )
+ ^ (if needs_hfile then "#include \""^ base ^"_ext.h\"" else ""));
+
try
let putc s = output_string occ s in
let puth s = output_string och s in
diff --git a/test/lus2lic.sum b/test/lus2lic.sum
index 8d5ffc32d90a3ea8a882557cdab1b79cf2109ce4..ed8918d8593bc795e2ee93691df87e61636b9ce2 100644
--- a/test/lus2lic.sum
+++ b/test/lus2lic.sum
@@ -1,5 +1,5 @@
==> lus2lic0.sum <==
-Test Run By jahier on Fri May 5 17:11:23
+Test Run By jahier on Thu Jun 1 16:16:10
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic0 tests ===
@@ -64,7 +64,7 @@ XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/lecte
XFAIL: Test bad programs (assert): test_lus2lic_no_node should_fail/assert/s.lus
==> lus2lic1.sum <==
-Test Run By jahier on Fri May 5 17:11:25
+Test Run By jahier on Thu Jun 1 16:16:11
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic1 tests ===
@@ -97,7 +97,8 @@ PASS: ./lus2lic {-2c Gyroscope.lus -n Gyroscope}
PASS: sh Gyroscope.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c Gyroscope.lus {}
PASS: ./lus2lic {-2c Gyroscope2.lus -n Gyroscope2}
-FAIL: Check that the generated C code compiles : sh Gyroscope2.sh
+PASS: sh Gyroscope2.sh
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c Gyroscope2.lus {}
PASS: ./lus2lic {-2c aa.lus -n aa}
PASS: sh aa.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c aa.lus {}
@@ -271,7 +272,8 @@ PASS: sh fresh_name.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c fresh_name.lus {}
PASS: ./lus2lic {-2c func_with_body.lus -n func_with_body}
PASS: ./lus2lic {-2c hanane.lus -n hanane}
-FAIL: Check that the generated C code compiles : sh hanane.sh
+PASS: sh hanane.sh
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c hanane.lus {}
PASS: ./lus2lic {-2c heater_control.lus -n heater_control}
PASS: sh heater_control.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c heater_control.lus {}
@@ -370,7 +372,8 @@ PASS: ./lus2lic {-2c modes3x2_v2.lus -n modes3x2_v2}
PASS: sh modes3x2_v2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c modes3x2_v2.lus {}
PASS: ./lus2lic {-2c modes3x2_v3.lus -n modes3x2_v3}
-FAIL: Check that the generated C code compiles : sh modes3x2_v3.sh
+PASS: sh modes3x2_v3.sh
+PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c modes3x2_v3.lus {}
PASS: ./lus2lic {-2c modes3x2_v4.lus -n modes3x2_v4}
PASS: ./lus2lic {-2c mouse.lus -n mouse}
PASS: sh mouse.sh
@@ -395,7 +398,7 @@ PASS: sh multipar.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
-Test Run By jahier on Fri May 5 17:12:31
+Test Run By jahier on Thu Jun 1 16:17:05
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic2 tests ===
@@ -735,7 +738,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
-Test Run By jahier on Fri May 5 17:13:41
+Test Run By jahier on Thu Jun 1 16:18:03
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic3 tests ===
@@ -1240,7 +1243,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
-Test Run By jahier on Fri May 5 17:15:38
+Test Run By jahier on Thu Jun 1 16:19:48
Native configuration is x86_64-unknown-linux-gnu
=== lus2lic4 tests ===
@@ -1732,8 +1735,8 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
=== lus2lic1 Summary ===
-# of expected passes 311
-# of unexpected failures 8
+# of expected passes 317
+# of unexpected failures 5
==> lus2lic2.sum <==
@@ -1756,15 +1759,15 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
# of expected passes 465
# of unexpected failures 6
===============================
-# Total number of failures: 26
-lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
-lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 66 seconds
-lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 70 seconds
-lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 117 seconds
-lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 63 seconds
+# Total number of failures: 23
+lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 0 seconds
+lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 53 seconds
+lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 58 seconds
+lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 105 seconds
+lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 57 seconds
* Ref time:
-0.06user 0.01system 5:17.88elapsed 0%CPU (0avgtext+0avgdata 5564maxresident)k
-0inputs+0outputs (0major+6163minor)pagefaults 0swaps
+0.04user 0.02system 4:35.78elapsed 0%CPU (0avgtext+0avgdata 5672maxresident)k
+64inputs+0outputs (0major+6088minor)pagefaults 0swaps
* Quick time (-j 4):
-0.05user 0.02system 2:08.66elapsed 0%CPU (0avgtext+0avgdata 5700maxresident)k
-160inputs+0outputs (0major+6197minor)pagefaults 0swaps
+0.04user 0.04system 2:28.15elapsed 0%CPU (0avgtext+0avgdata 5660maxresident)k
+160inputs+0outputs (0major+6123minor)pagefaults 0swaps