From 78d247dc5e6d5e64a4ab848702c23ce81b6fc615 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Sun, 24 Nov 2013 22:20:12 +0100 Subject: [PATCH] Implement the ranked automata evaluation to guarantee a O(|D|x|Q|) worst case complexity. The states of an automaton are given a rank (an integer) such that if rank(q) = i, then state q can be satisfied during run i at the latest. The maximum rank of a state is bounded by the number of "bi-directional" states, that is, the number of states which depends at the same time on a state upward and on another state downard. Therefore, the rank is at most |Q|. For the moment, we evaluate state [q] *only* during run i. This implies the O(|D|x|Q|) overal complexity but also means we loose a chance to discard (or accept) [q] early. A heuristic could improve that. --- src/ata.ml | 165 ++++++++++++++++++++++++++++++++++++-------------- src/ata.mli | 12 +++- src/pretty.ml | 6 +- src/run.ml | 77 +++++++++++++++-------- 4 files changed, 187 insertions(+), 73 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index 3263e46..80843e6 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -54,6 +54,17 @@ module Move = true with Exit -> false + let for_all2 p m1 m2 = + try + for i = 0 to 4 do + let v1 = m1.(i) + and v2 = m2.(i) in + if not (p (ridx i) v1 v2) then raise Exit + done; + true + with + Exit -> false + let exists p m = try iter (fun i v -> if p i v then raise Exit) m; @@ -206,6 +217,7 @@ type t = { mutable starting_states : StateSet.t; mutable selecting_states: StateSet.t; transitions: (State.t, (QNameSet.t*Formula.t) list) Hashtbl.t; + mutable ranked_states : StateSet.t array } let uid t = t.id @@ -213,7 +225,8 @@ let uid t = t.id let get_states a = a.states let get_starting_states a = a.starting_states let get_selecting_states a = a.selecting_states - +let get_states_by_rank a = a.ranked_states +let get_max_rank a = Array.length a.ranked_states - 1 let _pr_buff = Buffer.create 50 let _str_fmt = formatter_of_buffer _pr_buff @@ -229,12 +242,15 @@ let print fmt a = Number of states: %i@\n\ Starting states: %a@\n\ Selection states: %a@\n\ + Ranked states: %a@\n\ Alternating transitions:@\n" (a.id :> int) StateSet.print a.states (StateSet.cardinal a.states) StateSet.print a.starting_states - StateSet.print a.selecting_states; + StateSet.print a.selecting_states + (let r = ref 0 in Pretty.print_array ~sep:", " (fun ppf s -> + fprintf ppf "%i:%a" !r StateSet.print s; incr r)) a.ranked_states; let trs = Hashtbl.fold (fun q t acc -> List.fold_left (fun acc (s , f) -> (q,s,f)::acc) acc t) @@ -379,26 +395,99 @@ let normalize_negations auto = while not (Queue.is_empty todo) do let (q, b) as key = Queue.pop todo in - let q' = - try - Hashtbl.find memo_state key - with - Not_found -> - let nq = if b then q else - let nq = State.make () in - auto.states <- StateSet.add nq auto.states; - nq - in - Hashtbl.add memo_state key nq; nq - in - let trans = try Hashtbl.find auto.transitions q with Not_found -> [] in - let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in - Hashtbl.replace auto.transitions q' trans'; + if not (StateSet.mem q auto.starting_states) then + let q' = + try + Hashtbl.find memo_state key + with + Not_found -> + let nq = if b then q else + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; + nq + in + Hashtbl.add memo_state key nq; nq + in + let trans = try Hashtbl.find auto.transitions q with Not_found -> [] in + let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in + Hashtbl.replace auto.transitions q' trans'; done; cleanup_states auto - - +(* [compute_dependencies auto] returns a hash table storing for each + states [q] a Move.table containing the set of states on which [q] + depends (loosely). [q] depends on [q'] if there is a transition + [q, {...} -> phi], where [q'] occurs in [phi]. +*) +let compute_dependencies auto = + let edges = Hashtbl.create 17 in + StateSet.iter + (fun q -> Hashtbl.add edges q (Move.create_table StateSet.empty)) + auto.starting_states; + Hashtbl.iter (fun q trans -> + let moves = try Hashtbl.find edges q with Not_found -> + let m = Move.create_table StateSet.empty in + Hashtbl.add edges q m; + m + in + List.iter (fun (_, phi) -> + let m_phi = Formula.get_states_by_move phi in + Move.iter (fun m set -> + Move.set moves m (StateSet.union set (Move.get moves m))) + m_phi) trans) auto.transitions; + + edges + + +let compute_rank auto = + let dependencies = compute_dependencies auto in + let upward = [ `Stay ; `Parent ; `Previous_sibling ] in + let downward = [ `Stay; `First_child; `Next_sibling ] in + let swap dir = if dir == upward then downward else upward in + let is_satisfied q t = + Move.for_all (fun _ set -> StateSet.(is_empty (remove q set))) t + in + let update_dependencies dir initacc = + let rec loop acc = + let new_acc = + Hashtbl.fold (fun q deps acc -> + let to_remove = StateSet.union acc initacc in + List.iter + (fun m -> + Move.set deps m (StateSet.diff (Move.get deps m) to_remove) + ) + dir; + if is_satisfied q deps then StateSet.add q acc else acc + ) dependencies acc + in + if acc == new_acc then new_acc else loop new_acc + in + let satisfied = loop StateSet.empty in + StateSet.iter (fun q -> + Hashtbl.remove dependencies q) satisfied; + satisfied + in + let current_states = ref StateSet.empty in + let rank_list = ref [] in + let rank = ref 0 in + let current_dir = ref upward in + let detect_cycle = ref 0 in + while Hashtbl.length dependencies != 0 do + let new_sat = update_dependencies !current_dir !current_states in + if StateSet.is_empty new_sat then incr detect_cycle; + if !detect_cycle > 2 then assert false; + rank_list := (!rank, new_sat) :: !rank_list; + rank := !rank + 1; + current_dir := swap !current_dir; + current_states := StateSet.union new_sat !current_states; + done; + let by_rank = Hashtbl.create 17 in + List.iter (fun (r,s) -> + let r = r/2 in + let set = try Hashtbl.find by_rank r with Not_found -> StateSet.empty in + Hashtbl.replace by_rank r (StateSet.union s set)) !rank_list; + auto.ranked_states <- + Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i) module Builder = @@ -415,26 +504,9 @@ module Builder = starting_states = StateSet.empty; selecting_states = StateSet.empty; transitions = Hashtbl.create MED_H_SIZE; + ranked_states = [| |] } in - (* - at_exit (fun () -> - let n4 = ref 0 in - let n2 = ref 0 in - Cache.N2.iteri (fun _ _ _ b -> if b then incr n2) auto.cache2; - Cache.N4.iteri (fun _ _ _ _ _ b -> if b then incr n4) auto.cache4; - Logger.msg `STATS "automaton %i, cache2: %i entries, cache6: %i entries" - (auto.id :> int) !n2 !n4; - let c2l, c2u = Cache.N2.stats auto.cache2 in - let c4l, c4u = Cache.N4.stats auto.cache4 in - Logger.msg `STATS - "cache2: length: %i, used: %i, occupation: %f" - c2l c2u (float c2u /. float c2l); - Logger.msg `STATS - "cache4: length: %i, used: %i, occupation: %f" - c4l c4u (float c4u /. float c4l) - - ); *) auto let add_state a ?(starting=false) ?(selecting=false) q = @@ -469,6 +541,7 @@ module Builder = let finalize a = complete_transitions a; normalize_negations a; + compute_rank a; a end @@ -502,6 +575,7 @@ let rename_states mapper a = (fun l -> (List.map (fun (labels, form) -> (labels, map_form rename form)) l)) a.transitions; + ranked_states = Array.map (map_set rename) a.ranked_states } let copy a = @@ -526,16 +600,17 @@ let concat a1 a2 = (fun q -> Hashtbl.replace a1.transitions q [(QNameSet.any, link_phi)]) a2.starting_states; - { a1 with + let a = { a1 with states = StateSet.union a1.states a2.states; selecting_states = a2.selecting_states; transitions = a1.transitions; } + in compute_rank a; a let merge a1 a2 = let a1 = copy a1 in let a2 = copy a2 in - { a1 with + let a = { a1 with states = StateSet.union a1.states a2.states; selecting_states = StateSet.union a1.selecting_states a2.selecting_states; starting_states = StateSet.union a1.starting_states a2.starting_states; @@ -544,11 +619,12 @@ let merge a1 a2 = Hashtbl.iter (fun k v -> Hashtbl.add a1.transitions k v) a2.transitions in a1.transitions - } + } in + compute_rank a ; a let link a1 a2 q link_phi = - { a1 with + let a = { a1 with states = StateSet.union a1.states a2.states; selecting_states = StateSet.singleton q; starting_states = StateSet.union a1.starting_states a2.starting_states; @@ -559,6 +635,8 @@ let link a1 a2 q link_phi = Hashtbl.add a1.transitions q [(QNameSet.any, link_phi)]; a1.transitions } + in + compute_rank a; a let union a1 a2 = let a1 = copy a1 in @@ -587,7 +665,7 @@ let inter a1 a2 = let neg a = let a = copy a in let q = State.make () in - let link_phi = + let link_phi = StateSet.fold (fun q phi -> Formula.(and_ (not_(stay q)) phi)) a.selecting_states @@ -599,7 +677,6 @@ let neg a = selecting_states = StateSet.singleton q; } in - normalize_negations a; a + normalize_negations a; compute_rank a; a let diff a1 a2 = inter a1 (neg a2) - diff --git a/src/ata.mli b/src/ata.mli index 650673e..2aa27b3 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -32,6 +32,7 @@ module Move : val iter : (t -> 'a -> unit) -> 'a table -> unit val fold : (t -> 'a -> 'b -> 'b) -> 'a table -> 'b -> 'b val for_all : (t -> 'a -> bool) -> 'a table -> bool + val for_all2 : (t -> 'a -> 'b -> bool) -> 'a table -> 'b table -> bool val exists : (t -> 'a -> bool) -> 'a table -> bool end @@ -48,7 +49,7 @@ type predicate = module Atom : sig include Hcons.S with type data = predicate - include Common_sig.Printable with type t:= t + include Common_sig.Printable with type t := t end (** Module representing atoms of Boolean formulae, which are simply hashconsed [predicate]s *) @@ -112,6 +113,15 @@ val get_starting_states : t -> StateSet.t val get_selecting_states : t -> StateSet.t (** return the set of selecting states of the automaton *) +val get_states_by_rank : t -> StateSet.t array +(** return an array of states ordered by ranks. +*) + +val get_max_rank : t -> int +(** return the maximal rank of a state in the automaton, that is the + maximum number of runs needed to fuly evaluate the automaton. +*) + val get_trans : t -> QNameSet.elt -> StateSet.t -> TransList.t (** [get_trans auto l q] returns the list of transitions taken by [auto] for label [l] in state [q]. Takes time proportional to the number of diff --git a/src/pretty.ml b/src/pretty.ml index 6d1dd46..66a0225 100644 --- a/src/pretty.ml +++ b/src/pretty.ml @@ -128,11 +128,13 @@ let pp_print_list ?(sep=dummy_printer) printer fmt l = match l with [] -> () | [ e ] -> printer fmt e - | e :: es -> printer fmt e; List.iter + | e :: es -> printer fmt e; + List.iter (fun x -> sep fmt (); fprintf fmt "%a" printer x) es + let pp_print_array ?(sep=dummy_printer) printer fmt a = pp_print_list ~sep:sep printer fmt (Array.to_list a) @@ -144,5 +146,3 @@ let print_list ?(sep=" ") printer fmt l = let print_array ?(sep=" ") printer fmt a = print_list ~sep:sep printer fmt (Array.to_list a) - - diff --git a/src/run.ml b/src/run.ml index 8a9bf9e..2dd5ad5 100644 --- a/src/run.ml +++ b/src/run.ml @@ -79,10 +79,11 @@ module Make (T : Tree.S) = end type node_status = { + rank : int; sat : StateSet.t; (* States that are satisfied at the current node *) todo : StateSet.t; (* States that remain to be proven *) - (* For every node_status and automaton a: - a.states - (sat U todo) = unsat *) + (* For every node_status and automaton a, + a.states - (sat U todo) = unsat *) summary : NodeSummary.t; (* Summary of the shape of the node *) } (* Describe what is kept at each node for a run *) @@ -93,28 +94,33 @@ module Make (T : Tree.S) = type t = node_status let equal c d = c == d || + c.rank == d.rank && c.sat == d.sat && c.todo == d.todo && c.summary == d.summary let hash c = - HASHINT3((c.sat.StateSet.id :> int), + HASHINT4(c.rank, + (c.sat.StateSet.id :> int), (c.todo.StateSet.id :> int), c.summary) end ) let print ppf s = fprintf ppf - "{ sat: %a; todo: %a; summary: _ }" + "{ rank: %i; sat: %a; todo: %a; summary: _ }" + s.node.rank StateSet.print s.node.sat StateSet.print s.node.todo end let dummy_status = - NodeStatus.make { sat = StateSet.empty; - todo = StateSet.empty; - summary = NodeSummary.dummy; - } + NodeStatus.make { + rank = -1; + sat = StateSet.empty; + todo = StateSet.empty; + summary = NodeSummary.dummy; + } type run = { @@ -252,7 +258,9 @@ DEFINE AND_(t1,t2) = | `Parent | `Previous_sibling -> ps | `Stay -> ss in - if sum == dummy_status || StateSet.mem q n_sum.todo then + if sum == dummy_status + || n_sum.rank < ss.NodeStatus.node.rank + || StateSet.mem q n_sum.todo then Unknown else of_bool (b == StateSet.mem q n_sum.sat) @@ -279,13 +287,25 @@ DEFINE AND_(t1,t2) = let phi = get_form cache2 auto tag q in + let v = eval_form phi fcs nss ps old_status old_summary in +(* + Logger.msg `STATS "Evaluating for tag %a, state %a@\ncontext: %a@\nleft: %a@\nright: %a@\n\t formula %a yields %s" + QName.print tag + State.print q + NodeStatus.print old_status + NodeStatus.print fcs + NodeStatus.print nss + Ata.Formula.print phi + (match v with True -> "True" | False -> "False" | _ -> "Unknown"); +*) match v with True -> StateSet.add q a_sat, a_todo | False -> acc | Unknown -> a_sat, StateSet.add q a_todo ) old_todo (old_sat, StateSet.empty) in + (* Logger.msg `STATS ""; *) if old_sat != sat || old_todo != todo then NodeStatus.make { os_node with sat; todo } else old_status @@ -313,17 +333,18 @@ DEFINE AND_(t1,t2) = let top_down run = - let _i = run.pass in + let i = run.pass in let tree = run.tree in let auto = run.auto in let status = run.status in let cache2 = run.cache2 in let cache5 = run.cache5 in let unstable = run.unstable in - let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) in + let states_by_rank = Ata.get_states_by_rank auto in + let init_todo = states_by_rank.(i) in let rec loop node = let node_id = T.preorder tree node in - if node == T.nil || not (Bitvector.get unstable node_id) then false else begin + if node == T.nil (*|| not (Bitvector.get unstable node_id)*) then false else begin let parent = T.parent tree node in let fc = T.first_child tree node in let fc_id = T.preorder tree fc in @@ -334,17 +355,22 @@ DEFINE AND_(t1,t2) = let status0 = let c = unsafe_get_status status node_id in - if c == dummy_status then - (* first time we visit the node *) + if c.NodeStatus.node.rank < i then + (* first time we visit the node during this run *) NodeStatus.make - { sat = StateSet.empty; + { rank = i; + sat = c.NodeStatus.node.sat; todo = init_todo; - summary = NodeSummary.make - (node == T.first_child tree parent) (* is_left *) - (node == T.next_sibling tree parent) (* is_right *) - (fc != T.nil) (* has_left *) - (ns != T.nil) (* has_right *) - (T.kind tree node) (* kind *) + summary = let summary = c.NodeStatus.node.summary + in + if summary != NodeSummary.dummy then summary + else + NodeSummary.make + (node == T.first_child tree parent) (* is_left *) + (node == T.next_sibling tree parent) (* is_right *) + (fc != T.nil) (* has_left *) + (ns != T.nil) (* has_right *) + (T.kind tree node) (* kind *) } else c in @@ -469,7 +495,8 @@ DEFINE AND_(t1,t2) = let ns = T.next_sibling tree node in let status0 = NodeStatus.make - { sat = Ata.get_starting_states auto; + { rank = 0; + sat = Ata.get_starting_states auto; todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto); summary = NodeSummary.make @@ -490,10 +517,10 @@ DEFINE AND_(t1,t2) = tree_size := T.size tree; let run = make auto tree in prepare_run run nodes; - while run.redo do + for i = 0 to Ata.get_max_rank auto do top_down run done; - pass := run.pass; + pass := Ata.get_max_rank auto + 1; IFTRACE(Html.gen_trace auto (module T : Tree.S with type t = T.t) tree); run @@ -506,7 +533,7 @@ DEFINE AND_(t1,t2) = let r = compute_run auto tree nodes in get_results r - let stats () = { + let stats () = { tree_size = !tree_size; run = !pass; cache2_access = !cache2_access; -- 2.17.1