diff --git a/test/coloring/p.ml b/test/coloring/p.ml
index b5102c0e7f101400318c3638dbd62f96da5038a6..9f2ca2a1716179a6f237e96b54b92f44765118cd 100644
--- a/test/coloring/p.ml
+++ b/test/coloring/p.ml
@@ -1,5 +1,7 @@
-(* Time-stamp: <modified the 31/01/2024 (at 16:34) by Erwan Jahier> *)
-(* This is algo 3.1 in the book *)
+(* Time-stamp: <modified the 24/07/2024 (at 11:02) by Erwan Jahier> *)
+(* This is algo 3.1 in the book ``Introduction to Distributed
+ Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and
+ Petit *)
open Algo
let k = if is_directed () then
@@ -36,6 +38,10 @@ let (enable_f: int -> int neighbor list -> action list) =
fun c nl ->
if List.exists (fun n -> state n = c) nl then ["conflict"] else []
+
+(*@ nc = step c nl a
+ ensures forall n. n in nl -> (state n) <> nc /\ (0 <= c < nc -> c in colors nl)
+*)
let (step_f : int -> int neighbor list -> action -> int) =
fun _ nl _ ->
List.hd (free nl) (* Returns the smallest possible color *)
diff --git a/test/unison/unison.ml b/test/unison/unison.ml
index 4f63535b383fd4667e17cc49cf0fc5274c4580a7..3d8c125592281906f0750bd80e8bda71de71242d 100644
--- a/test/unison/unison.ml
+++ b/test/unison/unison.ml
@@ -1,4 +1,11 @@
-(* Time-stamp: <modified the 13/02/2024 (at 20:55) by Erwan Jahier> *)
+(* Time-stamp: <modified the 24/07/2024 (at 11:05) by Erwan Jahier> *)
+(* Synchronous unison.
+
+ This is algo 4.2 in the book ``Introduction to Distributed
+ Self-Stabilizing Algorithms'' By Altisen, Devismes, Dubois, and
+ Petit
+
+ nb: The daemon ougth to be synchronous. *)
open Algo
@@ -18,8 +25,15 @@ let (enable_f: 'v -> 'v neighbor list -> action list) =
fun clock nl ->
if (new_clock_value nl clock) <> clock then ["g"] else []
+
+(*@
+ function min (nl: 'v neighbor list): 'v =
+ List.fold_left (fun a b -> state a <= state b)
+*)
+(*@
+ nc = step_f c nl a
+ ensures forall q. q in nl -> nc = (state q)
+*)
let (step_f : 'v -> 'v neighbor list -> action -> 'v) =
- fun clock nl a ->
- let v = new_clock_value nl clock in
- match a with
- | _ -> v
+ fun clock nl _ ->
+ new_clock_value nl clock
diff --git a/test/wolfram-cellular-automaton/Makefile b/test/wolfram-cellular-automaton/Makefile
index 3f567b254a37db9207e25ecec32b10a47f17ef48..f4c00c75ddfeab2110244fb13aa12a6b3d17fb2c 100644
--- a/test/wolfram-cellular-automaton/Makefile
+++ b/test/wolfram-cellular-automaton/Makefile
@@ -1,4 +1,4 @@
-# Time-stamp: <modified the 03/07/2023 (at 16:22) by Erwan Jahier>
+# Time-stamp: <modified the 03/07/2024 (at 16:34) by Erwan Jahier>
DECO_PATTERN="0-:p.ml"
-include ./Makefile.dot
@@ -13,13 +13,8 @@ test: chain10.gm_test chain10.rdbg-test demo50 clean
utest:
make chain10.ugm_test || echo "chain10 ok"
-# usage: make demo50
-demo%:
- make chain$*.dot
- sasa chain$*.dot --synchronous-daemon --length $(shell echo $$(( $* / 2 ))) \
- | grep outs | cut -d ' ' -f 2-$* \
- | sed -e "s/ //g" | sed -e "s/f/ /g" | sed -e "s/t/â–²/g"
+-include ./Makefile.demo
clean: genclean
rm -f chain*
diff --git a/test/wolfram-cellular-automaton/Makefile.demo b/test/wolfram-cellular-automaton/Makefile.demo
new file mode 100644
index 0000000000000000000000000000000000000000..334483056adcecae3002fdf89c7069c77084f19e
--- /dev/null
+++ b/test/wolfram-cellular-automaton/Makefile.demo
@@ -0,0 +1,17 @@
+# usage: make demo50
+
+dem%:
+ make chain$*.dot
+ sasa chain$*.dot --synchronous-daemon --length $(shell echo $$(( $* / 2 )))
+
+
+demo%:
+ make chain$*.dot
+ sasa chain$*.dot --synchronous-daemon --length $(shell echo $$(( $* / 2 ))) \
+ | grep outs | cut -d ' ' -f 2-$* \
+ | sed -e "s/ //g" | sed -e "s/f/ /g" | sed -e "s/t/â–²/g"
+demor%:
+ make ring$*.dot
+ sasa ring$*.dot --synchronous-daemon --length $(shell echo $$(( $* ))) \
+ | grep outs | cut -d ' ' -f 2-$* \
+ | sed -e "s/ //g" | sed -e "s/f/ /g" | sed -e "s/t/â–²/g"
diff --git a/test/wolfram-cellular-automaton/p.ml b/test/wolfram-cellular-automaton/p.ml
index 5fa45cefe91413b8421fbb9c0524ba5db9b73c11..1ae9cd302125abf235dc9360d8d53280db8bcfcc 100644
--- a/test/wolfram-cellular-automaton/p.ml
+++ b/test/wolfram-cellular-automaton/p.ml
@@ -1,39 +1,45 @@
-(* Time-stamp: <modified the 10/07/2023 (at 11:36) by Erwan Jahier> *)
+(* Time-stamp: <modified the 06/07/2024 (at 17:00) by Erwan Jahier> *)
-(* Draw the Sierpinski triangle using Wolfram cellular automata
+(* Elementary Cellular Automata (Wolfram)
https://mathworld.wolfram.com/ElementaryCellularAutomaton.html
*)
-let rule_nb = 126 (* Sierpinski rule *)
-let _ = assert( 0 <= rule_nb && rule_nb <256 )
+(*
+ 126 : Sierpinski
+ 30 : Choatic
+ 110 : Turing-complete
+ *)
+let rule_nb = 126
-let rec to_bool_list n = if n = 0 then [] else (n mod 2 = 1)::(to_bool_list (n/2))
-let to_array l =
+let _ = assert( 0 <= rule_nb && rule_nb <256 ) (* array of size 8 *)
+
+(**********************************************************************************)
+let to_a8 (n: int) : bool array =
let a = Array.make 8 false in
- let ll = List.length l in
- List.iteri (fun i b -> a.(i+8-ll) <- b) l; a
+ let ref_n = ref n in
+ for i = 0 to 7 do
+ a.(i) <- !ref_n mod 2 = 1;
+ ref_n := !ref_n / 2;
+ done;
+ a
-let rule_nb_array = rule_nb |> to_bool_list |> List.rev |> to_array
+let (rule_nb_array: bool array) = to_a8 rule_nb
-(* For each rule, the next value (of x2) depends its value and the ones of its 2 neighbors *)
+(* The next value (of cell) depends its value and the ones of its 2 neighbors *)
let b2i b = if b then 1 else 0
-let next x1 x2 x3 =
- let index = 7 - ((b2i x1)*4 + (b2i x2)*2 + b2i x3) in
- (* Printf.printf "index=%d\n%!" index; *)
- rule_nb_array.(index)
+let next_i x1 cell x2 = rule_nb_array.(7 - (4*x1 + 2*cell + x2))
+let next x1 cell x2 = next_i (b2i x1) (b2i cell) (b2i x2)
+(**********************************************************************************)
+(* Initialisation: only one cell is true, in the middle *)
+let n = Algo.card()
let cpt = ref 0
-let init_state _ _ =
- cpt := (!cpt+1) mod Algo.card();
- let res = !cpt = Algo.card() / 2 in (* one cell is true, in the middle *)
- (* Printf.printf "cell(%d)=%b\n%!" !cpt res; *)
- res
-
+let init_state _ _ = cpt := (!cpt+1) mod n; !cpt = n / 2
-let enable_f x2 nl =
+let enable_f cell nl =
match List.map Algo.state nl with
- | [x1; x3] -> if next x1 x2 x3 = not x2 then ["flip"] else []
+ | [x1; x2] -> if next x1 cell x2 = cell then [] else ["flip"]
| _ -> []
let step_f x _ _ = not x