Skip to content

GitLab

Commit a4b2a53a authored by erwan's avatar erwan
Browse files

Some enhancements on the arduino demo doc

parent 6c036c82
Hide whitespace changes
Inline Side-by-side
Makefile.dev
View file @ a4b2a53a
......@@ -35,15 +35,9 @@ README.md: README.txt
uv:update_version
update_version:
git pull
rm -f src/lv6version.ml
make src/lv6version.ml
ifneq (,$(findstring -,$(VERSION)))
echo "won't update _oasis"
else
cp _oasis _oasis.save
cat _oasis.save | sed "s/^Version:.*/Version: $(VERSION)/" > _oasis
rm -f lib/lv6version.ml
make lib/lv6version.ml
make clean && make
endif
BRANCH=$(shell git rev-parse --abbrev-ref HEAD)
......
arduino/led_puzzle/Makefile
View file @ a4b2a53a
......@@ -7,13 +7,13 @@ $(FILE)_$(NODE)_loop:
mkdir $(FILE)_$(NODE)_loop
v6: led.lus $(FILE)_$(NODE)_loop
lus2lic -2c $(FILE).lus -n $(NODE)
lv6 -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 $* &
luciole-rif lv6 -exec -rif led.lus -n $* &
%.arduino:
cp lustre/arduino_$*.lus arduino_puzzle.lus
......@@ -21,7 +21,7 @@ v6: led.lus $(FILE)_$(NODE)_loop
%.no_sol:
cp lustre/arduino_$*.lus arduino_puzzle.lus
lus2lic -ec -o no_sol.ec led.lus -n $*_has_no_solution
lv6 -ec -o no_sol.ec led.lus -n $*_has_no_solution
ecverif no_sol.ec -diag > $*.diag ; echo >> $*.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\ //'
......@@ -29,12 +29,12 @@ v6: led.lus $(FILE)_$(NODE)_loop
%.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 !"
rdbg -lurette -l 1000 -sut "lv6 led.lus -n $*" -env "lutin env.lut -n random_env" -oracle "lv6 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 -emacs -sut "lus2lic led.lus -n $*"
rdbg -emacs -sut "lv6 led.lus -n $*"
clean:
......@@ -74,3 +74,20 @@ s6: puzzle6.simu
p6: puzzle6.no_sol
t6: puzzle6.test
TARGET=led
USR_SRCS= \
./objs/mycode_puzzle.cpp \
led_arduino_puzzle_loop.cpp \
# Thinks that can be customized
USR_CPP_FLAGS=
USR_CC_FLAGS=
USR_INCLS=-I./objs
./objs/mycode_puzzle.cpp: led.lus
cd ./objs; lv6 ../led.lus -n arduino_puzzle -2c; mv arduino_puzzle_arduino_puzzle.c arduino_puzzle_arduino_puzzle.cpp
include ArduinoMega.mk
arduino/led_puzzle/doc/puzzle.org
View file @ a4b2a53a
......@@ -84,7 +84,8 @@ par un bouton rouge et un bouton bleu, et *contrôlant* l'allumage de 5
leds.
#+BEGIN_CENTER
\includegraphics[width=.4\linewidth]{arduino.jpg}
\includegraphics[width=.4\linewidth]{arduino.jpg}
\includegraphics[width=.4\linewidth]{../fig/led.png}
#+END_CENTER
......@@ -130,7 +131,7 @@ automatiser la réponse à ces petits puzzles.
- Puzzle 6
- Bouton rouge : inverse l'état de la led 1
- Bouton bleu : allume la led suivant la première led éteinte (en
- Bouton bleu : inverse l'état la led suivant la première led éteinte (en
partant de la led1)
......
arduino/led_puzzle/fig/led.fig 0 → 100644
View file @ a4b2a53a
#FIG 3.2 Produced by xfig version 3.2.6a
Landscape
Center
Metric
A4
100.00
Single
-2
1200 2
6 7223 1823 8167 2317
1 2 0 1 0 7 110 -1 -1 0.000 1 0.0000 7695 2070 472 247 7223 2070 8167 2070
4 0 0 110 -1 18 12 0.0000 4 135 525 7425 2160 10101\001
-6
6 3623 5243 4567 5737
1 2 0 1 0 7 110 -1 -1 0.000 1 0.0000 4095 5490 472 247 3623 5243 4568 5738
4 0 0 110 -1 18 12 0.0000 4 135 525 3825 5580 11001\001
-6
6 7268 4163 8212 4657
1 2 0 1 0 7 110 -1 -1 0.000 1 0.0000 7740 4410 472 247 7268 4163 8213 4658
4 0 0 110 -1 18 12 0.0000 4 135 525 7470 4500 00010\001
-6
6 3668 4163 4612 4657
1 2 0 1 0 7 70 -1 -1 0.000 1 0.0000 4140 4410 472 247 3668 4163 4613 4658
4 0 0 70 -1 18 12 0.0000 4 135 525 3870 4500 01001\001
-6
6 1890 1530 2880 2070
1 2 0 1 0 7 95 -1 -1 0.000 1 0.0000 2385 1800 472 247 1913 1553 2858 2048
4 0 0 95 -1 18 12 0.0000 4 135 525 2115 1890 00100\001
-6
6 10170 2048 12216 4230
1 2 0 1 4 7 50 -1 -1 0.000 1 0.0000 11193 3139 1023 1091 10170 3139 12216 3139
2 5 0 1 4 -1 50 -1 20 0.000 0 0 -1 0 0 5
0 boum.png
10638 2706 11853 2706 11853 3696 10638 3696 10638 2706
4 0 4 50 -1 18 12 0.0000 4 135 525 10863 2481 11111\001
-6
6 5408 413 5932 577
1 3 0 5 1 7 120 -1 -1 0.000 1 0.0000 5490 495 45 45 5490 495 5535 495
1 3 0 5 1 7 120 -1 -1 0.000 1 0.0000 5670 495 45 45 5670 495 5715 495
1 3 0 5 1 7 120 -1 -1 0.000 1 0.0000 5850 495 45 45 5850 495 5895 495
-6
1 2 0 1 0 7 70 -1 -1 0.000 1 0.0000 5850 2070 472 247 5378 2070 6322 2070
1 2 0 1 0 7 70 -1 -1 0.000 1 0.0000 5895 4410 472 247 5423 4163 6368 4658
1 2 0 1 0 7 110 -1 -1 0.000 1 0.0000 4117 518 472 247 3645 518 4589 518
1 2 0 1 0 7 60 -1 -1 0.000 1 0.0000 4095 2025 472 247 3623 1778 4568 2273
1 2 0 3 -1 11 50 -1 20 0.000 1 0.0000 2340 3285 472 247 1868 3285 2812 3285
2 1 0 5 1 7 60 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
2655 3060 3690 2160
2 1 0 5 1 7 70 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
4590 2025 5400 2025
2 1 0 5 4 7 110 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
7245 1980 6300 1980
2 1 0 5 4 7 110 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
3870 4635 3870 5310
2 1 0 5 4 7 110 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
4410 5310 4410 4590
2 1 0 5 4 7 110 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
6345 4500 7290 4500
2 1 0 5 4 7 110 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
7290 4320 6345 4320
2 1 0 5 4 7 110 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
6300 2205 7290 2205
2 1 0 5 1 7 70 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
5805 2340 5805 4185
2 1 0 5 1 7 70 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
5445 4410 4635 4410
2 1 0 5 1 7 70 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
3690 4320 2604 3464
2 1 0 5 1 7 115 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
7380 1845 4455 675
2 1 0 5 4 7 95 -1 -1 0.000 0 0 -1 1 0 2
1 1 5.00 105.00 150.00
2475 3015 2475 2025
2 1 0 5 4 7 100 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
2115 2025 2115 3060
2 5 0 1 0 -1 50 -1 20 0.000 0 0 -1 0 0 5
0 interro.png
8505 2160 10080 2160 10080 4140 8505 4140 8505 2160
2 2 0 0 0 7 0 -1 -1 0.000 0 0 -1 0 0 5
1620 270 12330 270 12330 5985 1620 5985 1620 270
2 1 0 5 1 7 120 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
4590 495 5400 495
2 1 0 5 4 7 110 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
4320 1800 4320 720
2 1 0 5 4 7 110 -1 -1 0.000 0 0 7 1 0 2
1 1 5.00 105.00 150.00
3825 720 3825 1845
4 0 0 50 -1 18 12 0.0000 4 135 525 2070 3375 10100\001
4 0 0 70 -1 18 12 0.0000 4 135 525 5580 2160 00101\001
4 0 0 70 -1 18 12 0.0000 4 135 525 5625 4500 10010\001
4 0 0 110 -1 18 12 0.0000 4 135 525 3847 608 11010\001
4 0 0 60 -1 18 12 0.0000 4 135 525 3825 2115 01010\001
arduino/led_puzzle/fig/tex/main.tex 0 → 100644
View file @ a4b2a53a
\documentclass[nowasysym]{beamer}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{graphicx}
\usepackage{textcomp}
\usepackage{marvosym}
\input{mybeamer}
\usepackage{latexsym}
\usepackage{amssymb}
\usepackage{hyperref}
\tolerance=1000
\usepackage{color}
\title{Ce programme est-il correct ?}
\author{Verimag}
\date{Fête de la science}
\hypersetup{
pdfkeywords={},
pdfsubject={},
pdfcreator={Emacs Org-mode version 7.8.03}}
\usefonttheme{structurebold}
\begin{document}
\begin{frame}
\frametitle{Ce programme est-il correct ?}
C'est-à-dire, existe-t'il un chemin de l'état initial vers l'état
dangereux ?
\scalebox{0.5}{\input{led}}
\label{sec-1-1}
\end{frame}
\end{document}
arduino/led_puzzle/notes.org
View file @ a4b2a53a
* Préliminaire
1. installer l'utilitaire arduino (apt-get install arduino)
1. installer l'utilitaire arduino (apt-get install arduino) -> si ca
ne fonctionne pas (/dev/ttyACM0 grisé), installer une version plus
recente depuis le site d'arduino !!
2. récupérer le fichier file:/home/jahier/.arduino/preferences.txt
3. le lancer (shell:arduino)
4. ouvrir avec le fichier file:led_arduino_puzzle_loop.c
......@@ -10,14 +12,14 @@
** puzzle 1
a1 : lustre compil du puzzle1 (file:led.lus::21)
s1 : simu avec luciole
t1 : test aleatoire avec lurette
p1 : model-checking avec lesar
make a1 : lustre compil du puzzle1 (file:led.lus::21)
make s1 : simu avec luciole
make t1 : test aleatoire avec lurette
make p1 : model-checking avec lesar
nb a propos de la preuve : parité versus exploration exhaustive
file
* Idées en vrac
** Compter en binaire
......
test/lus2lic.sum
View file @ a4b2a53a
==> lus2lic0.sum <==
Test run by jahier on Wed Sep 18 11:21:58
Test run by jahier on Wed Oct 9 15:40:39
Native configuration is x86_64-pc-linux-gnu
=== lus2lic0 tests ===
......@@ -66,7 +66,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 Wed Sep 18 11:21:59
Test run by jahier on Wed Oct 9 15:40:40
Native configuration is x86_64-pc-linux-gnu
=== lus2lic1 tests ===
......@@ -409,7 +409,7 @@ PASS: sh multipar.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c multipar.lus {}
==> lus2lic2.sum <==
Test run by jahier on Wed Sep 18 11:22:23
Test run by jahier on Wed Oct 9 15:41:09
Native configuration is x86_64-pc-linux-gnu
=== lus2lic2 tests ===
......@@ -749,7 +749,7 @@ PASS: sh zzz2.sh
PASS: /home/jahier/lus2lic/test/../utils/compare_exec_and_2c zzz2.lus {}
==> lus2lic3.sum <==
Test run by jahier on Wed Sep 18 11:22:50
Test run by jahier on Wed Oct 9 15:41:40
Native configuration is x86_64-pc-linux-gnu
=== lus2lic3 tests ===
......@@ -1259,7 +1259,7 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node multipar.lus {}
==> lus2lic4.sum <==
Test run by jahier on Wed Sep 18 11:23:32
Test run by jahier on Wed Oct 9 15:42:19
Native configuration is x86_64-pc-linux-gnu
=== lus2lic4 tests ===
......@@ -1777,13 +1777,13 @@ PASS: /home/jahier/lus2lic/test/../utils/test_lus2lic_no_node zzz2.lus {}
===============================
# Total number of failures: 15
lus2lic0.log:testcase ./lus2lic.tests/test0.exp completed in 1 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 24 seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 27 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 42 seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 17 seconds
lus2lic1.log:testcase ./lus2lic.tests/test1.exp completed in 29 seconds
lus2lic2.log:testcase ./lus2lic.tests/test2.exp completed in 31 seconds
lus2lic3.log:testcase ./lus2lic.tests/test3.exp completed in 39 seconds
lus2lic4.log:testcase ./lus2lic.tests/test4.exp completed in 15 seconds
* Ref time:
60.08user 21.96system 1:51.64elapsed 73%CPU (0avgtext+0avgdata 285104maxresident)k
0inputs+141480outputs (0major+15471916minor)pagefaults 0swaps
60.67user 20.82system 1:54.22elapsed 71%CPU (0avgtext+0avgdata 283180maxresident)k
0inputs+141488outputs (0major+11037451minor)pagefaults 0swaps
* Quick time (-j 4):
68.59user 23.86system 1:08.69elapsed 134%CPU (0avgtext+0avgdata 285060maxresident)k
0inputs+140072outputs (0major+15364481minor)pagefaults 0swaps
76.76user 24.63system 1:12.82elapsed 139%CPU (0avgtext+0avgdata 283284maxresident)k
2040inputs+138392outputs (0major+10828391minor)pagefaults 0swaps
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment