diff --git a/Makefile.dev b/Makefile.dev index 47092834b30606db4beb2802da20388c2c35f75e..a5de23956f0d3a7baae5f9019aa4333137d0e731 100644 --- a/Makefile.dev +++ b/Makefile.dev @@ -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) diff --git a/arduino/led_puzzle/Makefile b/arduino/led_puzzle/Makefile index d3f64c7ed525cbc7f28cf964ebd169833f12398e..ec1b45bef2ac8074082d1930b42d846bce8599cf 100644 --- a/arduino/led_puzzle/Makefile +++ b/arduino/led_puzzle/Makefile @@ -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 diff --git a/arduino/led_puzzle/doc/puzzle.org b/arduino/led_puzzle/doc/puzzle.org index 52977d7b284978e73fa388d471da17ab786ae166..11e3be4f9bfbdbe97b6585c31a6c5663a45b5b99 100644 --- a/arduino/led_puzzle/doc/puzzle.org +++ b/arduino/led_puzzle/doc/puzzle.org @@ -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) diff --git a/arduino/led_puzzle/doc/puzzle.pdf b/arduino/led_puzzle/doc/puzzle.pdf index 26a8ed9b69a9f3855cc6e1e2edaa3bcf36a23590..e93f68fa5792fb86a1a9c556b36cb3299ebe438a 100644 Binary files a/arduino/led_puzzle/doc/puzzle.pdf and b/arduino/led_puzzle/doc/puzzle.pdf differ diff --git a/arduino/led_puzzle/fig/boum.png b/arduino/led_puzzle/fig/boum.png new file mode 100644 index 0000000000000000000000000000000000000000..2cd603426dceea4e423cdd8897d67e2a4f185c2c Binary files /dev/null and b/arduino/led_puzzle/fig/boum.png differ diff --git a/arduino/led_puzzle/fig/interro.png b/arduino/led_puzzle/fig/interro.png new file mode 100644 index 0000000000000000000000000000000000000000..0d88998e53f016c2c63940e099eb082a4388bfb5 Binary files /dev/null and b/arduino/led_puzzle/fig/interro.png differ diff --git a/arduino/led_puzzle/fig/led.fig b/arduino/led_puzzle/fig/led.fig new file mode 100644 index 0000000000000000000000000000000000000000..d8bbb5cb0a7fd7ca962377ec863080229c0fc24d --- /dev/null +++ b/arduino/led_puzzle/fig/led.fig @@ -0,0 +1,107 @@ +#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 diff --git a/arduino/led_puzzle/fig/tex/main.tex b/arduino/led_puzzle/fig/tex/main.tex new file mode 100644 index 0000000000000000000000000000000000000000..4763a5d7498a9aeadce559f121482b9ec503118e --- /dev/null +++ b/arduino/led_puzzle/fig/tex/main.tex @@ -0,0 +1,44 @@ +\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} + + diff --git a/arduino/led_puzzle/notes.org b/arduino/led_puzzle/notes.org index 9a71631592e2cab9c3582ea7bff20706a0a0f957..090579ecfb74672c6d05da45d63f42e0f766264d 100644 --- a/arduino/led_puzzle/notes.org +++ b/arduino/led_puzzle/notes.org @@ -1,7 +1,9 @@ * 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 diff --git a/lv6-ref-man/lv6-ref-man.pdf b/lv6-ref-man/lv6-ref-man.pdf index 0f18d36a246905c5607f856b0212ab09d0994152..4bf16d6a640b69331d7b5d529ad231a12f132394 100644 Binary files a/lv6-ref-man/lv6-ref-man.pdf and b/lv6-ref-man/lv6-ref-man.pdf differ diff --git a/test/lus2lic.sum b/test/lus2lic.sum index b2970f55824dd6aabf31933e0c68eabe6eab8440..71a68188f8aec663f234f6eb1cd219cd88d421c6 100644 --- a/test/lus2lic.sum +++ b/test/lus2lic.sum @@ -1,5 +1,5 @@ ==> 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