( Q : PriorityNodeQueue ) : Strategy = struct

  module Fixpoint = Fixpoint.FixpointTrie
  module Approx = Approx.Selected

  let nb_remaining q post () = Q.length q, List.length !post

  let search ?(invariants=[]) ?(candidates=[]) system =
    
    let visited = ref Cubetrie.empty in
    let candidates = ref candidates in
    let q = Q.create () in
    let postponed = ref [] in

    (* Initialization *)
    Q.push_list !candidates q;
    Q.push_list system.t_unsafe q;
    List.iter (fun inv -> visited := Cubetrie.add_node inv !visited)
              (invariants @ system.t_invs);

    try
      while not (Q.is_empty q) do
        let n = Q.pop q in
        Safety.check system n;
        begin
          match Fixpoint.check n !visited with
          | Some db ->
             Stats.fixpoint n db
          | None ->
             Stats.check_limit n;
             Stats.new_node n;
             let n = begin
                 match Approx.good n with
                 | None -> n
                 | Some c ->
                    try
                      (* Replace node with its approximation *)
                      Safety.check system c;
                      candidates := c :: !candidates;
                      Stats.candidate n c;
                      c
                    with Safety.Unsafe _ -> n 
                         (* If the candidate is directly reachable, no need to
                            backtrack, just forget it. *)
               end
             in
             let ls, post = Pre.pre_image system.t_trans n in
             if delete then
               visited :=
                 Cubetrie.delete_subsumed ~cpt:Stats.cpt_delete n !visited;
             postponed := List.rev_append post !postponed;
             visited := Cubetrie.add_node n !visited;
             Q.push_list ls q;
             Stats.remaining (nb_remaining q postponed);
        end;
        
        if Q.is_empty q then
          (* When the queue is empty, pour back postponed nodes in it *)
          begin
            Q.push_list !postponed q;
            postponed := []
          end
      done;
      Safe (Cubetrie.all_vals !visited, !candidates)
    with Safety.Unsafe faulty ->
      if dot then Dot.error_trace faulty;
      Unsafe (faulty, !candidates)

end