Cubicle 1.1.2 documentation and source : Enumerative.search

let search procs init =
  TimeForward.start ();
  let procs = procs (*@ init.t_glob_proc*) in
  let env = init_tables procs init in
  let st_inits = init_to_states env procs init in
  if debug then 
    List.iter (fun (_, st) ->
      eprintf "init : %a\n@." SAtom.print (state_to_cube env st))
      st_inits;
  let env = { env with st_trs = transitions_to_func procs env init.t_trans } in
  global_envs := env :: !global_envs;
  install_sigint ();
  begin try
    forward_bfs init procs env st_inits;
    with Exit -> ()
  end ;
  finalize_search env