From f6fd2fa7087654323792bc60fb16671fe5954922 Mon Sep 17 00:00:00 2001
From: Erwan Jahier <jahier@imag.fr>
Date: Mon, 8 Oct 2018 14:49:23 +0200
Subject: [PATCH] clean sligthly
---
arduino/led_puzlle/Makefile | 55 +++++++++++++++----
arduino/led_puzlle/doc/puzzle.org | 10 ++--
arduino/led_puzlle/led.lus | 16 +++---
.../{ => lustre}/arduino_puzzle1.lus | 0
.../{ => lustre}/arduino_puzzle2.lus | 0
.../{ => lustre}/arduino_puzzle3.lus | 0
.../{ => lustre}/arduino_puzzle4.lus | 0
.../{ => lustre}/arduino_puzzle5.lus | 0
.../{ => lustre}/arduino_puzzle6.lus | 0
9 files changed, 58 insertions(+), 23 deletions(-)
rename arduino/led_puzlle/{ => lustre}/arduino_puzzle1.lus (100%)
rename arduino/led_puzlle/{ => lustre}/arduino_puzzle2.lus (100%)
rename arduino/led_puzlle/{ => lustre}/arduino_puzzle3.lus (100%)
rename arduino/led_puzlle/{ => lustre}/arduino_puzzle4.lus (100%)
rename arduino/led_puzlle/{ => lustre}/arduino_puzzle5.lus (100%)
rename arduino/led_puzlle/{ => lustre}/arduino_puzzle6.lus (100%)
diff --git a/arduino/led_puzlle/Makefile b/arduino/led_puzlle/Makefile
index 27ce0155..55c4acd2 100644
--- a/arduino/led_puzlle/Makefile
+++ b/arduino/led_puzlle/Makefile
@@ -3,43 +3,74 @@
FILE=led
NODE=arduino_puzzle
+$(FILE)_$(NODE)_loop:
+ mkdir $(FILE)_$(NODE)_loop
-v6: led.lus
+v6: led.lus $(FILE)_$(NODE)_loop
lus2lic -2c $(FILE).lus -n $(NODE)
mv *.h $(FILE)_$(NODE)_loop/
mv $(FILE)_$(NODE).c $(FILE)_$(NODE)_loop/$(FILE)_$(NODE).cpp
%.simu:
+ cp lustre/arduino_$*.lus arduino_puzzle.lus
luciole-rif lus2lic -exec -rif led.lus -n $* &
%.arduino:
- cp arduino_$*.lus arduino_puzzle.lus
+ cp lustre/arduino_$*.lus arduino_puzzle.lus
make v6
%.no_sol:
+ cp lustre/arduino_$*.lus arduino_puzzle.lus
lus2lic -ec -o no_sol.ec led.lus -n $*_has_no_solution
- ecverif no_sol.ec -diag | sed 's/true//' | sed 's/not\ red//' | sed 's/not\ red\ or//' | sed 's/not\ blue\ or//' | sed 's/not\ blue//' | sed 's/\ and\ //' && cat msg
+ ecverif no_sol.ec -diag > $*.diag || echo "$*: il existe une solution ! La voici:" \
+ echo "$*: ce puzzle est insoluble"
+ cat $*.diag | sed 's/true//' | sed 's/not\ red//' | sed 's/not\ red\ or//' | sed 's/not\ blue\ or//' | sed 's/not\ blue//' | sed 's/\ and\ //'
%.test:
+ cp lustre/arduino_$*.lus arduino_puzzle.lus
rdbg -lurette -l 1000 -sut "lus2lic led.lus -n $*" -env "lutin env.lut -n random_env" -oracle "lus2lic led.lus -n $*_has_no_solution" -o $*.rif || echo "Ce puzzle a une solution !"
gnuplot-rif $*.rif -no-display
gnuplot -e 'set terminal qt size 1800,400' $*.gp
%.debug:
- rdbg -sut "lus2lic led.lus -n $*"
+ rdbg -emacs -sut "lus2lic led.lus -n $*"
clean:
- rm -f *.c *.h *.ec *.sh *.rif *ession*.ml *.gp *.log *.dro *.seed
- rm -f *.ps *.pdf *.dot *.cm* *.o
+ rm -f *.c *.h *.ec *.sh *.rif *ession*.ml *.gp *.log *.dro *.seed *.diag
+ rm -f *.ps *.pdf *.dot *.cm* *.o arduino_puzzle.lus
rm -f led_arduino_puzzle_loop/led_arduino_puzzle.cpp
rm -f led_arduino_puzzle_loop/*.h
- cd doc; make clean
+ rm -f my-rdbg-tuning.ml
+a1: puzzle1.arduino
+s1: puzzle1.simu
+p1: puzzle1.no_sol
+t1: puzzle1.test
+
+a2: puzzle2.arduino
+s2: puzzle2.simu
+p2: puzzle2.no_sol
+t2: puzzle2.test
+
+a3: puzzle3.arduino
+s3: puzzle3.simu
+p3: puzzle3.no_sol
+t3: puzzle3.test
+
+a4: puzzle4.arduino
+s4: puzzle4.simu
+p4: puzzle4.no_sol
+t4: puzzle4.test
+
+a5: puzzle5.arduino
+s5: puzzle5.simu
+p5: puzzle5.no_sol
+t5: puzzle5.test
+
+a6: puzzle6.arduino
+s6: puzzle6.simu
+p6: puzzle6.no_sol
+t6: puzzle6.test
-v4:
- lus2ec $(FILE).lus $(FILE)
- ec2c $(FILE).ec
- mv $(FILE).h $(FILE)_loop_v4/
- mv $(FILE).c $(FILE)_loop_v4/$(FILE).cpp
diff --git a/arduino/led_puzlle/doc/puzzle.org b/arduino/led_puzlle/doc/puzzle.org
index 264cebcb..47067418 100644
--- a/arduino/led_puzlle/doc/puzzle.org
+++ b/arduino/led_puzlle/doc/puzzle.org
@@ -53,7 +53,7 @@ permettant de montrer
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ôlées par un bouton rouge et un bouton bleu, et 5 sorties,
+contrôllées par un bouton rouge et un bouton bleu, et 5 sorties,
représentées par 5 leds.
@@ -96,9 +96,11 @@ tel
* Puzzle 4
-- Bouton bleu : idem
-- Bouton rouge : inverse l'état d'une led qui circule à chaque pression mais
- dans un sens différent selon la couleur du bouton pressé
+
+- 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
diff --git a/arduino/led_puzlle/led.lus b/arduino/led_puzlle/led.lus
index edb6b4c3..53e385ee 100644
--- a/arduino/led_puzlle/led.lus
+++ b/arduino/led_puzlle/led.lus
@@ -8,9 +8,9 @@ const T=true;
const Eteint=false;
const Allume=true;
--- demo : mettre Allume au debut, puis Eteint faux apres la 1ere expe
- const led1_00 = Eteint;
---const led1_00 = Allume;
+-- demo : mettre Allume au debut, puis Eteint apres la 1ere expe
+-- const led1_00 = Eteint;
+const led1_00 = Allume;
const led2_00 = Allume;
const led3_00 = Eteint;
const led4_00 = Eteint;
@@ -79,9 +79,11 @@ let
tel
----------------------------------------------------------------------------
--- blue => permutation circulaire
--- red => inverse une led qui circule a chaque pression mais
--- dans un sens different selon la couleur du bouton pressé
+-- dans ce puzzle, une
+-- red => inverse l'état d'une led qui circule en montant
+-- (led1, puis led2, etc.) Ã chaque pression
+-- blue => permutation circulaire des leds + permutation inverse
+-- (en descandant) de la led courante controllée par le bouton rouge
node puzzle4 (red,blue:bool) returns (led1,led2,led3,led4,led5:bool);
var
X1, X2, X3, X4, X5 : bool;
@@ -117,7 +119,7 @@ let
if red and X5 then not(pre(led5)) else pre(led5);
tel
----------------------------------------------------------------------------
--- phase d'init sur les 5 premieres pressions : le bleu etteint , et le rouge allume
+-- phase d'init sur les 5 premieres pressions : le bleu eteint , et le rouge allume
-- blue => la led courante devient le xor des leds autours
-- red => la led courante devient le and des leds autours
-- la led courante est le premiere au debut, puis la deuxieme, etc.
diff --git a/arduino/led_puzlle/arduino_puzzle1.lus b/arduino/led_puzlle/lustre/arduino_puzzle1.lus
similarity index 100%
rename from arduino/led_puzlle/arduino_puzzle1.lus
rename to arduino/led_puzlle/lustre/arduino_puzzle1.lus
diff --git a/arduino/led_puzlle/arduino_puzzle2.lus b/arduino/led_puzlle/lustre/arduino_puzzle2.lus
similarity index 100%
rename from arduino/led_puzlle/arduino_puzzle2.lus
rename to arduino/led_puzlle/lustre/arduino_puzzle2.lus
diff --git a/arduino/led_puzlle/arduino_puzzle3.lus b/arduino/led_puzlle/lustre/arduino_puzzle3.lus
similarity index 100%
rename from arduino/led_puzlle/arduino_puzzle3.lus
rename to arduino/led_puzlle/lustre/arduino_puzzle3.lus
diff --git a/arduino/led_puzlle/arduino_puzzle4.lus b/arduino/led_puzlle/lustre/arduino_puzzle4.lus
similarity index 100%
rename from arduino/led_puzlle/arduino_puzzle4.lus
rename to arduino/led_puzlle/lustre/arduino_puzzle4.lus
diff --git a/arduino/led_puzlle/arduino_puzzle5.lus b/arduino/led_puzlle/lustre/arduino_puzzle5.lus
similarity index 100%
rename from arduino/led_puzlle/arduino_puzzle5.lus
rename to arduino/led_puzlle/lustre/arduino_puzzle5.lus
diff --git a/arduino/led_puzlle/arduino_puzzle6.lus b/arduino/led_puzlle/lustre/arduino_puzzle6.lus
similarity index 100%
rename from arduino/led_puzlle/arduino_puzzle6.lus
rename to arduino/led_puzlle/lustre/arduino_puzzle6.lus
--
GitLab