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: RdbgEvent.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 : RdbgEvent.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 RdbgEvent.End _ -> !rn
  in
  time aux ()