diff --git a/arduino/led_puzlle/Makefile b/arduino/led_puzlle/Makefile index 1f55edb1fa265924e8d79289585f4f8b814379cb..38ead00639e04077dd97f5aab7cb4e51f867e261 100644 --- a/arduino/led_puzlle/Makefile +++ b/arduino/led_puzlle/Makefile @@ -19,6 +19,10 @@ v6: led.lus lus2lic -ec -o no_sol.ec led.lus -n $*_has_no_solution ecverif no_sol.ec -diag | sed 's/not\ red//' | sed 's/not\ blue//' | sed 's/\ and\ //' || cat msg + +%.test: + rdbg -lurette -sut "lus2lic led.lus -n $*" + clean: rm -f *.c *.h *.ec *.sh *.rif rdbg-session.ml *.gp *.log *.dro rm led_arduino_puzzle_loop/led_arduino_puzzle.cpp diff --git a/arduino/led_puzlle/arduino_puzzle.lus b/arduino/led_puzlle/arduino_puzzle.lus index 51e89416949d575397d25dbfa9f8c923bdcfa04f..579fbe1440e98a75a00aef8693b510b257931b34 100644 --- a/arduino/led_puzlle/arduino_puzzle.lus +++ b/arduino/led_puzlle/arduino_puzzle.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle6(pulse(red), pulse(blue)); + led1,led2,led3,led4,led5=puzzle1(edge(red), edge(blue)); tel diff --git a/arduino/led_puzlle/arduino_puzzle1.lus b/arduino/led_puzlle/arduino_puzzle1.lus index 579fbe1440e98a75a00aef8693b510b257931b34..bedbf6705d3ada45a28c4c2fefb4d149c35c072a 100644 --- a/arduino/led_puzlle/arduino_puzzle1.lus +++ b/arduino/led_puzlle/arduino_puzzle1.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle1(edge(red), edge(blue)); + led1,led2,led3,led4,led5=puzzle1(fedge(red), fedge(blue)); tel diff --git a/arduino/led_puzlle/arduino_puzzle2.lus b/arduino/led_puzlle/arduino_puzzle2.lus index 70c232a8a71061843ab08440a8428bc97b731039..6148105c53910c92b15cb12593cf86deaae7eec4 100644 --- a/arduino/led_puzlle/arduino_puzzle2.lus +++ b/arduino/led_puzlle/arduino_puzzle2.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle2(edge(red), edge(blue)); + led1,led2,led3,led4,led5=puzzle2(fedge(red), fedge(blue)); tel diff --git a/arduino/led_puzlle/arduino_puzzle3.lus b/arduino/led_puzlle/arduino_puzzle3.lus index f7429d22efb96ed282fe28c461dd904806fd4e37..4a9002cd59167f8b0c04cd7262e6a217e083135a 100644 --- a/arduino/led_puzlle/arduino_puzzle3.lus +++ b/arduino/led_puzlle/arduino_puzzle3.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle3(edge(red), edge(blue)); + led1,led2,led3,led4,led5=puzzle3(fedge(red), fedge(blue)); tel diff --git a/arduino/led_puzlle/arduino_puzzle4.lus b/arduino/led_puzlle/arduino_puzzle4.lus index f604a54abff5a946f43941879d9b550a5928cd6a..c21a9412d362b01641a2fee2116b8c57c188a7c2 100644 --- a/arduino/led_puzlle/arduino_puzzle4.lus +++ b/arduino/led_puzlle/arduino_puzzle4.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle4(edge(red), edge(blue)); + led1,led2,led3,led4,led5=puzzle4(fedge(red), fedge(blue)); tel diff --git a/arduino/led_puzlle/arduino_puzzle5.lus b/arduino/led_puzlle/arduino_puzzle5.lus index b7bd3e2bbcc3cba00819661dc38ef8fa2e964f60..05fcc53ec950c4e3271fb610ec3eaab1007cb774 100644 --- a/arduino/led_puzlle/arduino_puzzle5.lus +++ b/arduino/led_puzlle/arduino_puzzle5.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle5(edge(red), edge(blue)); + led1,led2,led3,led4,led5=puzzle5(fedge(red), fedge(blue)); tel diff --git a/arduino/led_puzlle/arduino_puzzle6.lus b/arduino/led_puzlle/arduino_puzzle6.lus index eebf8c8767bc75b4e180ccd5092a23d564ed7364..95b7dd9cb1f43af90f34b768935bcee9bcb9d59b 100644 --- a/arduino/led_puzlle/arduino_puzzle6.lus +++ b/arduino/led_puzlle/arduino_puzzle6.lus @@ -1,4 +1,4 @@ node arduino_puzzle(red,blue:bool) returns (led1,led2,led3,led4,led5:bool); let - led1,led2,led3,led4,led5=puzzle6(edge(red), edge(blue)); + led1,led2,led3,led4,led5=puzzle6(fedge(red), fedge(blue)); tel diff --git a/arduino/led_puzlle/led.lus b/arduino/led_puzlle/led.lus index 2093055e96567de2ce4f9a48e151508f000b4690..3d05c8d0bdeb3f18f39baa038e0b59a81b7d1a2b 100644 --- a/arduino/led_puzlle/led.lus +++ b/arduino/led_puzlle/led.lus @@ -8,7 +8,8 @@ const T=true; const Eteint=false; const Allume=true; -const led1_0 = Allume; -- demo : a mettre Vrai au debut, puis a faux apres la 1ere expe +-- const led1_0 = Allume; -- demo : a mettre Vrai au debut, puis a faux apres la 1ere expe +const led1_0 = Eteint; const led2_0 = Allume; const led3_0 = Eteint; const led4_0 = Eteint; @@ -185,7 +186,8 @@ node puzzle_has_no_solution << var led1,led2,led3,led4,led5:bool; let - assert(red xor blue); +-- assert(not(blue and red)); -- just to ease the replay of counter-examples +-- assert(blue xor red); -- just to ease the replay of counter-examples led1,led2,led3,led4,led5=puzzle(red,blue); no_sol = not (led1 and led2 and led3 and led4 and led5); tel @@ -198,9 +200,9 @@ node puzzle5_has_no_solution = puzzle_has_no_solution <<puzzle5>> node puzzle6_has_no_solution = puzzle_has_no_solution <<puzzle6>> -node edge(s:bool) returns (res:bool); +node fedge(s:bool) returns (res:bool); let - res= false -> not pre(s) and s; + res = false -> pre(s) and not s; tel - + diff --git a/src/lv6version.ml b/src/lv6version.ml index e514b9975961bacd2adecd9a34816c67176f4664..ef36a5a17aeeeb0cbae4ba4049fe1c2a4d20f99e 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 = "682" -let sha_1 = "91120cfbec86724f356d936c3c991c01922002e7" +let commit = "683" +let sha_1 = "c6fc6f718951de807ba2f8d855b9473952d8331c" let str = (branch ^ "." ^ commit ^ " (" ^ sha_1 ^ ")") let maintainer = "jahier@imag.fr"