Test: fix the coloring oracle

- the move_count node was wrong (missing parenthesis)
- the lemma an the theorem only holds for locally central unfait demon

lib/sasacore/sasa.ml

-(* Time-stamp: <modified the 05/07/2019 (at 16:34) by Erwan Jahier> *)
+(* Time-stamp: <modified the 11/07/2019 (at 09:02) by Erwan Jahier> *)
 
 open Register
 open Sasacore
@@ -153,14 +153,20 @@ let (get_degree:Topology.t -> int*int) =
     else
       let node_deg n = List.length (t.succ (n.Topology.id)) in
       let d_start = node_deg ((List.hd t.nodes)) in
-      List.fold_left (fun (d_min,d_max) n -> (min (node_deg n) d_min, max (node_deg n) d_max)
+      List.fold_left (fun (d_min,d_max) n ->
+          (min (node_deg n) d_min, max (node_deg n) d_max)
       ) (d_start,d_start) (List.tl t.nodes)
 
-    (* take a graph t and a boolean is_oriented and return the number of link in the graph *)
+(* take a graph t and a boolean is_oriented and return the number of
+   link in the graph *)
 let (get_nb_link: Topology.t -> bool -> int) =
   fun t is_oriented ->
-  if not is_oriented then (List.fold_left (fun acc n -> ((List.length (t.succ n.Topology.id))) + acc) (0) (t.nodes)) / 2
-    else (List.fold_left (fun acc n -> ((List.length (t.succ n.Topology.id))) + acc) (0) (t.nodes))
+    if not is_oriented then
+      (List.fold_left
+         (fun acc n -> ((List.length (t.succ n.Topology.id))) + acc) (0) (t.nodes)) / 2
+    else
+      (List.fold_left
+         (fun acc n -> ((List.length (t.succ n.Topology.id))) + acc) (0) (t.nodes))
 
 let (get_mean_degree : Topology.t -> float) = 
   fun t -> 
@@ -194,18 +200,22 @@ let bfs : (Topology.t -> string -> bool * string list) =
 let is_connected_and_cyclic : Topology.t -> bool*bool = 
   fun t -> match t.nodes with
     | [] -> (false,false)
-    | hd::_ -> let (cyclic,bfs_nodes) = (bfs t hd.Topology.id) in ((List.compare_lengths t.nodes bfs_nodes) = 0, cyclic)
+    | hd::_ ->
+      let (cyclic,bfs_nodes) = (bfs t hd.Topology.id) in
+      ((List.compare_lengths t.nodes bfs_nodes) = 0, cyclic)
 
 let rec height : string list -> Topology.t -> string -> int = 
   fun parents t n ->
     (List.fold_left (fun h (_,succ) -> 
-      if List.mem succ parents then h else max h (height (n::parents) t succ)) (-1) (t.succ n)) + 1
+         if List.mem succ parents then
+           h
+         else
+           max h (height (n::parents) t succ)) (-1) (t.succ n)) + 1
 
 let get_height : Topology.t -> string -> int = 
   fun t -> 
     height ([]) t
 
-
 let (make : bool -> string array -> 'v t) =
   fun dynlink argv ->
     let args = 
@@ -299,7 +309,7 @@ let (make : bool -> string array -> 'v t) =
           (String.concat " "
              (List.map
                 (fun (vn,vt) -> Printf.sprintf "\"%s\":%s" vn vt) inputs_decl));
-
+        flush stdout;
         Printf.printf "#outputs %s\n" (env_rif_decl args pl);
         flush stdout
       ) else (

src/sasaMain.ml

@@ -88,6 +88,8 @@ let () =
   | Silent i ->
     let str = if args.rif then "#" else "" in
     Printf.eprintf "\n%sThis algo is silent after %i steps\n" str i ;
+    flush stderr;
+    flush stdout;
     print_string "\n#quit\n"; 
     flush stderr;
     flush stdout

test/Makefile.inc

-# Time-stamp: <modified the 08/07/2019 (at 17:10) by Erwan Jahier>
+# Time-stamp: <modified the 11/07/2019 (at 09:00) by Erwan Jahier>
 
 DIR=../../_build/install/default
 
-sasa=$(DIR)/bin/sasa -seed 42  -l 100
+sasa=$(DIR)/bin/sasa  -l 100
 
 LIB=-package algo
 

test/coloring/Makefile

-# Time-stamp: <modified the 08/07/2019 (at 17:03) by Erwan Jahier>
+# Time-stamp: <modified the 10/07/2019 (at 17:44) by Erwan Jahier>
 
+sasa=$(DIR)/bin/sasa   -l 100
 
 test: p.cmxs ring.lut lurette
 	$(sasa) -l 200 ring.dot
@@ -13,9 +14,17 @@ gnuplot: ring.rif
 	gnuplot-rif $< 
 
 
+lurette:cmxs ring_oracle.lus
+	lurette  \
+      -sut "sasa ring.dot -rif -lcd " \
+		-oracle "lv6 ring_oracle.lus -n oracle "
+
+test100:
+	for i in $$(seq 100); do make lurette && make clean; done
+
 rdbg: p.cma p.cmxs  ring.lut 
 	rdbg -o ring.rif  \
-      -env "$(sasa) g.dot -dd" 
+      -env "$(sasa) g.dot -lcd" 
 
 
 rdbg2: p.cma  ring.lut 
@@ -23,15 +32,6 @@ rdbg2: p.cma  ring.lut
       -env "$(sasa) ring.dot -custd -rif" \
       -sut-nd "lutin ring.lut -n distributed"
 
-rdbg3: p.cma  g.lut 
-	rdbg -o ring.rif  \
-      -env "$(sasa) g.dot -custd"  \
-      -sut-nd "lutin g.lut -n distributed"
 
-lurette:cmxs ring.lut ring_oracle.lus
-	lurette   \
-      -env "$(sasa) ring.dot -custd " \
-      -sut "lutin ring.lut -n distributed" \
-		-oracle "lv6 ring_oracle.lus -n oracle "
 
 -include ../Makefile.inc

test/coloring/coloring_oracle.lus

@@ -2,18 +2,23 @@ include "../lustre/oracle_utils.lus"
 
 
 -----------------------------------------------------------------------------
-
+-- Lemma 3.14 The execution e terminates after at most n-1 moves 
+-- (under a Locally Central demon).
 node lemma_3_14<<const an:int; const pn: int>> (Enab, Acti: bool^an^pn) returns (res:bool);
 var 
   MoveNb:int;
+  Silent:bool;
 let
   MoveNb =  move_count(Acti);
-  res =  MoveNb <= pn-1;
+  Silent = silent<<an,pn>>(Enab);
+  res = Silent => (MoveNb) <= pn-1;
 tel
 
 -----------------------------------------------------------------------------
-
-node theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn) returns (res:bool);
+-- Theorem 3.17 The stabilization time of Color is at most one round
+-- (under a Locally Central demon).
+node theorem_3_17<<const an:int; const pn:int>> (Enab, Acti: bool^an^pn)
+returns (res:bool);
 var
   Round:bool;
   RoundNb:int;
@@ -29,3 +34,4 @@ returns (res:bool);
 let
   res = lemma_3_14<<an,pn>>(Enab,Acti) and theorem_3_17<<an,pn>>(Enab,Acti);
 tel
+

test/coloring/ring_oracle.lus

@@ -33,3 +33,4 @@ let
 
   ok = coloring_oracle<<an,pn>>(Enab,Acti);
 tel
+

test/lustre/oracle_utils.lus

@@ -16,7 +16,7 @@ tel
 -----------------------------------------------------------------------------
 node move_count (tab_acti:bool^an^pn) returns (nb_act:int);
 let
-  nb_act = 0 -> pre(nb_act) + (red<<count_true_acc<<an>>,pn>>(0,tab_acti));    
+  nb_act = (0 -> pre(nb_act)) + (red<<count_true_acc<<an>>,pn>>(0,tab_acti));    
 tel
 
 

test/lustre/utils.lus

@@ -25,6 +25,7 @@ let
   Z=red<<add_one_if_true, n>>(Acc,Y);
 tel
 
+node test_count_true_acc = count_true_acc <<1>>
 -----------------------------------------------------------------------------
 node map_and<<const n:int>> (X,Y:bool^n) returns (Z:bool^n);
 let

test/my-rdbg-tuning.ml

@@ -106,7 +106,9 @@ let pr () = e:=goto_last_ckpt !e.nb; circo p dotfile !e;;
 (* checkpoint at rounds! *)
 let _ = check_ref := round;;
 
-
+let next_match str e =
+  next_cond e (fun e -> Str.string_match (Str.regexp_string str) e.name 0)
+let nm str = e:=next_match str !e;;
 
 let _ =  ci (); Sys.command (Printf.sprintf "zathura sasa-%s.pdf&" dotfile)