Test: add a rdbg/ml oracle for the async unison

test/async-unison/Makefile

-# Time-stamp: <modified the 09/10/2019 (at 22:14) by Erwan Jahier>
+# Time-stamp: <modified the 11/10/2019 (at 14:22) by Erwan Jahier>
 
 
 test: ring.cmxs ring.lut
@@ -12,12 +12,12 @@ gnuplot: ring.rif
 	gnuplot-rif $< 
 
 lurette: ring.cmxs
-	lurette -o ring.rif -l 100 \
+	lurette -o ring.rif -l 10000 \
       -sut "sasa -rif ring.dot -cd"  \
-		-oracle "lv6 ring_oracle.lus -n oracle" 
+		-oracle "lv6 -2c-exec ring_oracle.lus -n oracle" 
 
 rdbg: ring.ml
-	rdbg -o ring.rif -l 100 \
+	rdbg -o ring.rif -l 10000 \
       -env "$(sasa) -vl 1 ring.dot -cd" 
 
 rdbgl: ring.cmxs

test/async-unison/async_unison_oracle.lus

@@ -11,15 +11,15 @@ function is_stable<<const l:int>>(State : int^pn) returns (res:bool)
 var
   i,j:int;
 let
-  i = l / pn;
+  i = l/pn;
   j = l mod pn;
   res = 
      with l = 0 then true
      else is_stable<<l-1>>(State) and
-       ((i<=j) or (adjency[l / pn][l mod pn] => is_close(State[l / pn], State[l mod pn])));
+       (i<=j or (adjency[l/pn][l mod pn] => is_close(State[l/pn], State[l mod pn])));
 tel
 
-node async_unison_oracle<<const an:int; const pn:int>> (State : int^pn; Enab, Acti: bool^an^pn) 
+node async_unison_oracle (State : int^pn; Enab, Acti: bool^an^pn) 
 returns (res, Stable:bool; rn:int);
 let
   rn = count(round <<an,pn>>(Enab,Acti));

test/async-unison/async_unison_oracle.ml

+
+type sl = Data.subst list
+(* extract from an event the state variables values *)
+let (get_states: sl -> sl * sl) =
+  fun sl ->
+  let is_state_var vname = String.sub vname ((String.length vname)-2 ) 2 = "_i" in
+  List.partition (fun (n,v) -> is_state_var n) sl
+
+let (get_enab: sl -> sl * sl) =
+  fun sl ->
+  let is_state_var vname = String.sub vname 0 5= "Enab_" in
+  List.partition (fun (n,v) -> is_state_var n) sl
+
+let (get_states_enab_acti: Event.t -> sl * sl * sl) = fun e ->
+  let sl = e.data in
+  let states, sl = get_states sl in
+  let enab, acti = get_enab sl in
+  states, enab, acti
+
+open Topology 
+let (is_stable : Event.t -> bool) = fun e ->
+  let states, _, _ = get_states_enab_acti e in
+  let pidl = List.map (fun n -> n.id) p.nodes in
+  let get_val p =
+    match  List.assoc_opt (p^"_i") states with
+    | Some (I i) -> i | Some _ | None -> assert false
+  in
+  let is_close p q =
+    let pv = get_val p
+    and qv = get_val q in
+    (pv = qv) || (pv-qv-1) mod P.k = 0 || (pv-qv+1) mod P.k = 0
+  in
+  let aux pid =
+    let qidl = List.map (fun (_,qid) -> qid) (p.succ pid) in
+    List.for_all (is_close pid) qidl
+  in
+  List.for_all aux pidl
+
+let move_forward_until_stabilisation e =
+  let rec aux rn e =
+  let e = next_round e in
+  if is_stable e then (
+    let rn = rn+1 in
+    rn, e
+  ) else 
+    aux (rn+1) e
+  in
+  aux 0 e
+
+
+(* move forward until stabilisation *)
+let stab () =
+  let rn, ne = move_forward_until_stabilisation  !e in
+  e := ne;
+  Printf.printf "Stabilisation reached after %i round%s\n" rn
+    (if rn<=1 then "" else "s");
+  flush stdout;
+  d ();;
+
+
+
+let time f x =
+  let t = Sys.time() in
+  let fx = f x in
+  Printf.printf "Execution time: %fs\n" (Sys.time() -. t);
+  fx
+   
+(* Mimick  the work of  the lurette oracle  (to compare perf):  a each
+   step, compute the round number + check for stabilisation *)
+let go () =
+  let n = Algo.card() in
+  let diameter = Algo.diameter() in
+  let rn = ref 0 in
+  let was_stable = ref false in
+  let rec aux () =
+    let ne = nexti_np !e 1 in
+    e := ne;
+    if (round ne) then incr rn;
+    if is_stable ne && not !was_stable then (
+      assert (!rn < diameter * n );
+      was_stable := true
+    );
+    try aux () with Event.End _ -> !rn
+  in
+  time aux ()
+

test/async-unison/my-rdbg-tuning.ml

-../my-rdbg-tuning.ml
\ No newline at end of file

test/async-unison/my-rdbg-tuning.ml

+
+#use "../my-rdbg-tuning.ml";;
+#use "async_unison_oracle.ml";;

test/async-unison/ring_oracle.lus

@@ -40,5 +40,5 @@ let
            [Enab_p7_a1,Enab_p7_a2]];
   State = [p1_i,p2_i,p3_i,p4_i,p5_i,p6_i,p7_i];
 
-  ok,stable,rn = async_unison_oracle<<an,pn>>(State,Enab,Acti);
+  ok,stable,rn = async_unison_oracle(State,Enab,Acti);
 tel

test/coloring/Makefile

-# Time-stamp: <modified the 08/10/2019 (at 21:58) by Erwan Jahier>
+# Time-stamp: <modified the 08/10/2019 (at 22:22) by Erwan Jahier>
 
 sasa=$(DIR)/bin/sasa   -l 100
 
@@ -24,7 +24,7 @@ test100:
 
 rdbg: ring.ml
 	rdbg -o ring.rif  \
-      -env "$(sasa) --replay ring.dot -lcd" 
+      -env "$(sasa)  ring.dot -lcd" 
 
 rdbg1: ring.ml ring_oracle.lus
 	rdbg -o rdbg-ring.rif \

test/my-rdbg-tuning.ml

@@ -49,6 +49,7 @@ let nd () = n();ci();;
 let bd () = b();ci();;
 
 (**********************************************************************)
+(* Computing rounds *)
 
 (* a process can be removed from the mask if one action of p is triggered
   or if no action of p is enabled *)
@@ -101,12 +102,17 @@ let (round : Event.t -> bool) =
       )
     );
     res
-
+ 
 (* go to next and previous rounds  *)
 let next_round e = next_cond e round;;
 let nr () = e:=next_round !e; circo p dotfile !e;;
 let pr () = e:=goto_last_ckpt !e.nb; circo p dotfile !e;;
 
+(**********************************************************************)
+(* *)
+
+
+(**********************************************************************)
 (* Goto to the next oracle violation *)
 let goto_next_false_oracle e =
   next_cond e (fun e -> e.kind = Exit && e.lang = "lustre" &&