diff --git a/lib/sasacore/sasa.ml b/lib/sasacore/sasa.ml
index d656ffb5fba957e4be4e5c3d56f50df2084d3586..0202d5fdce0a8962a636e19eba8e3d85848760dd 100644
--- a/lib/sasacore/sasa.ml
+++ b/lib/sasacore/sasa.ml
@@ -1,4 +1,4 @@
-(* 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 (
diff --git a/src/sasaMain.ml b/src/sasaMain.ml
index 370584b84c99d7326493972cf69c267b9e048ca3..5d5b1a8e58f4a0e07d969fdb4cbb9a264958d7a5 100644
--- a/src/sasaMain.ml
+++ b/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
diff --git a/test/Makefile.inc b/test/Makefile.inc
index 06aff70275d6d5e473b95de497319c92301eaa78..8e3abd2189f5fb0ca31e40dbe551df35cc91f533 100644
--- a/test/Makefile.inc
+++ b/test/Makefile.inc
@@ -1,8 +1,8 @@
-# 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
diff --git a/test/coloring/Makefile b/test/coloring/Makefile
index 5417f0176f92acea4b5da0520a12a0d74360dba6..ad1da7ad0e857b499a914fb1553ac6aa0e5084bc 100644
--- a/test/coloring/Makefile
+++ b/test/coloring/Makefile
@@ -1,5 +1,6 @@
-# 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
diff --git a/test/coloring/coloring_oracle.lus b/test/coloring/coloring_oracle.lus
index 467302257313aa23abdf359e025fe916049cb34f..458fca7d5678d172c8dd826344ce9c092e6579ea 100644
--- a/test/coloring/coloring_oracle.lus
+++ b/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
+
diff --git a/test/coloring/ring_oracle.lus b/test/coloring/ring_oracle.lus
index 687acb0ca71f394f1b4b3cd1c484cebddd63ec36..c05483b07eb67dd7c1fb410f8f071f2f0d8100fd 100644
--- a/test/coloring/ring_oracle.lus
+++ b/test/coloring/ring_oracle.lus
@@ -33,3 +33,4 @@ let
ok = coloring_oracle<<an,pn>>(Enab,Acti);
tel
+
diff --git a/test/lustre/oracle_utils.lus b/test/lustre/oracle_utils.lus
index d07c2da133aaa4a0bae984fa8ec6e5f2135b969d..20eee78ebf5f1b199bb6efbe913c92b2f692f360 100644
--- a/test/lustre/oracle_utils.lus
+++ b/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
diff --git a/test/lustre/utils.lus b/test/lustre/utils.lus
index 8032b57df5053f24a84c00203da2b69275b3fb25..824aaf1e3dee84496a6bd9d7390f34731456d826 100644
--- a/test/lustre/utils.lus
+++ b/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
diff --git a/test/my-rdbg-tuning.ml b/test/my-rdbg-tuning.ml
index f909968538316ce6a74fcfb856ad72cfee778e7b..d9ab26b7d4180cddae031570add147f8a98f100a 100644
--- a/test/my-rdbg-tuning.ml
+++ b/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)