From 05af95627d36110724ec6a2a6439c4842a228d19 Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Wed, 14 May 2014 14:01:41 +0200 Subject: [PATCH] Change in the Ata module: - whole file indentation - compute for each set of ranked states the output states, that is the states that are needed to compute following rank - fix a bug in state_prerequisites --- src/ata.ml | 387 +++++++++++++++++++++++++++------------------------- src/ata.mli | 4 +- src/run.ml | 4 +- 3 files changed, 206 insertions(+), 189 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index 190c4c7..9ad2b12 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -23,66 +23,66 @@ type move = [ `First_child | `Stay ] module Move = - struct - type t = move - type 'a table = 'a array - let idx = function - | `First_child -> 0 - | `Next_sibling -> 1 - | `Parent -> 2 - | `Previous_sibling -> 3 - | `Stay -> 4 - let ridx = function - | 0 -> `First_child - | 1 -> `Next_sibling - | 2 -> `Parent - | 3 -> `Previous_sibling - | 4 -> `Stay - | _ -> assert false - - let create_table a = Array.make 5 a - let get m k = m.(idx k) - let set m k v = m.(idx k) <- v - let iter f m = Array.iteri (fun i v -> f (ridx i) v) m - let fold f m acc = - let acc = ref acc in - iter (fun i v -> acc := f i v !acc) m; - !acc - let for_all p m = - try - iter (fun i v -> if not (p i v) then raise Exit) m; - 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; - false - with - Exit -> true - let print ppf m = - match m with - `First_child -> fprintf ppf "%s" Pretty.down_arrow - | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow - | `Parent -> fprintf ppf "%s" Pretty.up_arrow - | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow - | `Stay -> fprintf ppf "%s" Pretty.bullet - - let print_table pr_e ppf m = - iter (fun i v -> fprintf ppf "%a: %a" print i pr_e v; - if (idx i) < 4 then fprintf ppf ", ") m - end +struct + type t = move + type 'a table = 'a array + let idx = function + | `First_child -> 0 + | `Next_sibling -> 1 + | `Parent -> 2 + | `Previous_sibling -> 3 + | `Stay -> 4 + let ridx = function + | 0 -> `First_child + | 1 -> `Next_sibling + | 2 -> `Parent + | 3 -> `Previous_sibling + | 4 -> `Stay + | _ -> assert false + + let create_table a = Array.make 5 a + let get m k = m.(idx k) + let set m k v = m.(idx k) <- v + let iter f m = Array.iteri (fun i v -> f (ridx i) v) m + let fold f m acc = + let acc = ref acc in + iter (fun i v -> acc := f i v !acc) m; + !acc + let for_all p m = + try + iter (fun i v -> if not (p i v) then raise Exit) m; + 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; + false + with + Exit -> true + let print ppf m = + match m with + `First_child -> fprintf ppf "%s" Pretty.down_arrow + | `Next_sibling -> fprintf ppf "%s" Pretty.right_arrow + | `Parent -> fprintf ppf "%s" Pretty.up_arrow + | `Previous_sibling -> fprintf ppf "%s" Pretty.left_arrow + | `Stay -> fprintf ppf "%s" Pretty.bullet + + let print_table pr_e ppf m = + iter (fun i v -> fprintf ppf "%a: %a" print i pr_e v; + if (idx i) < 4 then fprintf ppf ", ") m +end type predicate = Move of move * State.t | Is_first_child @@ -146,19 +146,19 @@ struct has_first_child let next_sibling q = - and_ - (mk_move `Next_sibling q) - has_next_sibling + and_ + (mk_move `Next_sibling q) + has_next_sibling let parent q = - and_ - (mk_move `Parent q) - is_first_child + and_ + (mk_move `Parent q) + is_first_child let previous_sibling q = - and_ - (mk_move `Previous_sibling q) - is_next_sibling + and_ + (mk_move `Previous_sibling q) + is_next_sibling let stay q = mk_move `Stay q @@ -179,38 +179,38 @@ struct end module Transition = - struct - include Hcons.Make (struct - type t = State.t * QNameSet.t * Formula.t - let equal (a, b, c) (d, e, f) = - a == d && b == e && c == f - let hash (a, b, c) = - HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) -end) - let print ppf t = - let q, l, f = t.node in - fprintf ppf "%a, %a %s %a" - State.print q - QNameSet.print l - Pretty.double_right_arrow - Formula.print f - end +struct + include Hcons.Make (struct + type t = State.t * QNameSet.t * Formula.t + let equal (a, b, c) (d, e, f) = + a == d && b == e && c == f + let hash (a, b, c) = + HASHINT4 (PRIME1, a, ((QNameSet.uid b) :> int), ((Formula.uid c) :> int)) + end) + let print ppf t = + let q, l, f = t.node in + fprintf ppf "%a, %a %s %a" + State.print q + QNameSet.print l + Pretty.double_right_arrow + Formula.print f +end module TransList : sig include Hlist.S with type elt = Transition.t val print : Format.formatter -> ?sep:string -> t -> unit end = - struct - include Hlist.Make(Transition) - let print ppf ?(sep="\n") l = - iter (fun t -> - let q, lab, f = Transition.node t in - fprintf ppf "%a, %a → %a%s" - State.print q - QNameSet.print lab - Formula.print f sep) l - end +struct + include Hlist.Make(Transition) + let print ppf ?(sep="\n") l = + iter (fun t -> + let q, lab, f = Transition.node t in + fprintf ppf "%a, %a → %a%s" + State.print q + QNameSet.print lab + Formula.print f sep) l +end @@ -220,7 +220,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 + mutable ranked_states : (StateSet.t*StateSet.t) array } let uid t = t.id @@ -252,8 +252,8 @@ let print fmt a = (StateSet.cardinal a.states) StateSet.print a.starting_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 r = ref 0 in Pretty.print_array ~sep:", " (fun ppf (s1,s2) -> + fprintf ppf "(%i:%a,%a)" !r StateSet.print s1 StateSet.print s2; 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) @@ -369,31 +369,31 @@ let normalize_negations auto = | Boolean.Atom(a, b') -> begin match a.Atom.node with | Move (m, q) -> - if b == b' then begin - (* a appears positively, either no negation or double negation *) - if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; - Formula.mk_atom (Move(m, q)) - end else begin - (* need to reverse the atom - either we have a positive state deep below a negation - or we have a negative state in a positive formula - b' = sign of the state - b = sign of the enclosing formula - *) - let not_q = - try - (* does the inverted state of q exist ? *) - Hashtbl.find memo_state (q, false) - with - Not_found -> - (* create a new state and add it to the todo queue *) - let nq = State.make () in - auto.states <- StateSet.add nq auto.states; - Hashtbl.add memo_state (q, false) nq; - Queue.add (q, false) todo; nq - in - Formula.mk_atom (Move (m,not_q)) - end + if b == b' then begin + (* a appears positively, either no negation or double negation *) + if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; + Formula.mk_atom (Move(m, q)) + end else begin + (* need to reverse the atom + either we have a positive state deep below a negation + or we have a negative state in a positive formula + b' = sign of the state + b = sign of the enclosing formula + *) + let not_q = + try + (* does the inverted state of q exist ? *) + Hashtbl.find memo_state (q, false) + with + Not_found -> + (* create a new state and add it to the todo queue *) + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; + Hashtbl.add memo_state (q, false) nq; + Queue.add (q, false) todo; nq + in + Formula.mk_atom (Move (m,not_q)) + end | _ -> if b then f else Formula.not_ f end in @@ -446,12 +446,12 @@ let compute_dependencies auto = edges let state_prerequisites dir auto q = - Hashtbl.fold (fun q' trans acc -> - List.fold_left (fun acc (_, phi) -> - let m_phi = Formula.get_states_by_move phi in - if StateSet.mem q (Move.get m_phi dir) - then StateSet.add q' acc else acc) - acc trans) auto.transitions StateSet.empty + let trans = Hashtbl.find auto.transitions q in + List.fold_left (fun acc (_, phi) -> + let m_phi = Formula.get_states_by_move phi in + let prereq = Move.get m_phi dir in + StateSet.union prereq acc) + StateSet.empty trans let compute_rank auto = let dependencies = compute_dependencies auto in @@ -502,64 +502,81 @@ let compute_rank auto = List.iter (fun (r,s) -> 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; + let rank = Hashtbl.length by_rank in auto.ranked_states <- - Array.init (Hashtbl.length by_rank) (fun i -> Hashtbl.find by_rank i) - - -module Builder = - struct - type auto = t - type t = auto - let next = Uid.make_maker () - - let make () = - let auto = - { - id = next (); - states = StateSet.empty; - starting_states = StateSet.empty; - selecting_states = StateSet.empty; - transitions = Hashtbl.create MED_H_SIZE; - ranked_states = [| |] - } + Array.init rank + (fun i -> + let set = try Hashtbl.find by_rank i with Not_found -> StateSet.empty in + let source = + if i + 1 == rank then auto.selecting_states else + let post_set = Hashtbl.find by_rank (i+1) in + let source = if i + 1 == rank then post_set else + StateSet.fold (fun q acc -> + List.fold_left (fun acc m -> + StateSet.union acc (state_prerequisites m auto q )) + acc [`First_child; `Next_sibling; `Parent; `Previous_sibling; `Stay] + ) post_set StateSet.empty + in + StateSet.inter set source in - auto + (source, set) + ) - let add_state a ?(starting=false) ?(selecting=false) q = - a.states <- StateSet.add q a.states; - if starting then a.starting_states <- StateSet.add q a.starting_states; - if selecting then a.selecting_states <- StateSet.add q a.selecting_states - let add_trans a q s f = - if not (StateSet.mem q a.states) then add_state a q; - let trs = try Hashtbl.find a.transitions q with Not_found -> [] in - let cup, ntrs = - List.fold_left (fun (acup, atrs) (labs, phi) -> - let lab1 = QNameSet.inter labs s in - let lab2 = QNameSet.diff labs s in - let tr1 = - if QNameSet.is_empty lab1 then [] - else [ (lab1, Formula.or_ phi f) ] - in - let tr2 = - if QNameSet.is_empty lab2 then [] - else [ (lab2, Formula.or_ phi f) ] - in - (QNameSet.union acup labs, tr1@ tr2 @ atrs) - ) (QNameSet.empty, []) trs - in - let rem = QNameSet.diff s cup in - let ntrs = if QNameSet.is_empty rem then ntrs - else (rem, f) :: ntrs - in - Hashtbl.replace a.transitions q ntrs +module Builder = +struct + type auto = t + type t = auto + let next = Uid.make_maker () + + let make () = + let auto = + { + id = next (); + states = StateSet.empty; + starting_states = StateSet.empty; + selecting_states = StateSet.empty; + transitions = Hashtbl.create MED_H_SIZE; + ranked_states = [| |] + } + in + auto + + let add_state a ?(starting=false) ?(selecting=false) q = + a.states <- StateSet.add q a.states; + if starting then a.starting_states <- StateSet.add q a.starting_states; + if selecting then a.selecting_states <- StateSet.add q a.selecting_states + + let add_trans a q s f = + if not (StateSet.mem q a.states) then add_state a q; + let trs = try Hashtbl.find a.transitions q with Not_found -> [] in + let cup, ntrs = + List.fold_left (fun (acup, atrs) (labs, phi) -> + let lab1 = QNameSet.inter labs s in + let lab2 = QNameSet.diff labs s in + let tr1 = + if QNameSet.is_empty lab1 then [] + else [ (lab1, Formula.or_ phi f) ] + in + let tr2 = + if QNameSet.is_empty lab2 then [] + else [ (lab2, Formula.or_ phi f) ] + in + (QNameSet.union acup labs, tr1@ tr2 @ atrs) + ) (QNameSet.empty, []) trs + in + let rem = QNameSet.diff s cup in + let ntrs = if QNameSet.is_empty rem then ntrs + else (rem, f) :: ntrs + in + Hashtbl.replace a.transitions q ntrs - let finalize a = - complete_transitions a; - normalize_negations a; - compute_rank a; - a - end + let finalize a = + complete_transitions a; + normalize_negations a; + compute_rank a; + a +end let map_set f s = @@ -575,8 +592,8 @@ let rec map_form f phi = | Boolean.Or(phi1, phi2) -> Formula.or_ (map_form f phi1) (map_form f phi2) | Boolean.And(phi1, phi2) -> Formula.and_ (map_form f phi1) (map_form f phi2) | Boolean.Atom({ Atom.node = Move(m,q); _}, b) -> - let a = Formula.mk_atom (Move (m,f q)) in - if b then a else Formula.not_ a + let a = Formula.mk_atom (Move (m,f q)) in + if b then a else Formula.not_ a | _ -> phi let rename_states mapper a = @@ -591,7 +608,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 + ranked_states = Array.map (fun (a,b) -> map_set rename a, map_set rename b) a.ranked_states } let copy a = diff --git a/src/ata.mli b/src/ata.mli index 443bb0b..815e20a 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -122,8 +122,8 @@ 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_states_by_rank : t -> (StateSet.t*StateSet.t) array +(** return an array of states (sources, states) ordered by ranks. *) val get_max_rank : t -> int diff --git a/src/run.ml b/src/run.ml index be8bbeb..167e0af 100644 --- a/src/run.ml +++ b/src/run.ml @@ -236,11 +236,11 @@ struct let tree = run.tree in let auto = run.auto in let states_by_rank = Ata.get_states_by_rank auto in - let td_todo = states_by_rank.(i) in + let td_todo = snd states_by_rank.(i) in let bu_todo = if i == Array.length states_by_rank - 1 then StateSet.empty else - states_by_rank.(i+1) + snd (states_by_rank.(i+1)) in let last_run = i >= Array.length states_by_rank - 2 in let rec loop_td_and_bu node parent parent_sat = -- 2.17.1