Cubicle 1.1.2 documentation and source : Enumerative.replay_trace_and

let replay_trace_and_expand procs system faulty =
  List.iter (fun env ->
  (* let tmp_visited = HST.create 2_000_001 in *)
  let st_inits = List.map snd (init_to_states env procs system) in
  let trc = faulty.from in
  let rec replay trc sts depth =
    if depth >= forward_depth then sts
    else match sts, trc with
      | [], _ | _, [] -> sts
      | _, ({tr_name = name}, args, _) :: trc ->
          let st_trs = find_tr_funs env name in
          let to_do =
            List.fold_left (fun acc st_tr ->
              List.fold_left (fun acc st ->
                
                eprintf ">>> : %a\n@."
                  SAtom.print (state_to_cube env st);

                try List.rev_append (st_tr.st_f st) acc
                with Not_applicable -> acc) acc sts
            ) [] st_trs in
          eprintf "%a ( %a )@." Hstring.print name Variable.print_vars args; 
          replay trc to_do (depth + 1)
  in
  let new_inits = replay trc st_inits 0 in
  List.iter (fun (st) ->
  eprintf "new_inits : %a\n@." SAtom.print (state_to_cube env st))
    new_inits;
  forward_bfs faulty procs env (List.map (fun s -> 0, s) new_inits)
 ) !global_envs