X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=blobdiff_plain;f=src%2Fata.ml;h=c045aaff0560fbb67b647163cfeb9fcc7c94322d;hp=80843e6deae7aafb8860db5a3b8bce7125968ed5;hb=fed343e8df1900043dc993ac5458c757d3ac2ee0;hpb=78d247dc5e6d5e64a4ab848702c23ce81b6fc615 diff --git a/src/ata.ml b/src/ata.ml index 80843e6..c045aaf 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -184,29 +184,28 @@ module Transition = 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)) + let hash ((a, b, c) : t) = + HASHINT4 (PRIME1, ((a) :> int), ((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 + Pretty.left_arrow Formula.print f end module TransList : sig include Hlist.S with type elt = Transition.t - val print : Format.formatter -> ?sep:string -> t -> unit + val print : ?sep:string -> Format.formatter -> t -> unit end = struct include Hlist.Make(Transition) - let print ppf ?(sep="\n") l = + let print ?(sep="\n") ppf 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 + fprintf ppf "%a%s" Transition.print t sep) l end @@ -258,28 +257,30 @@ let print fmt a = [] in let sorted_trs = List.stable_sort (fun (q1, s1, _) (q2, s2, _) -> - let c = State.compare q1 q2 in - (if c == 0 then QNameSet.compare s1 s2 else c)) + let c = State.compare q2 q1 in if c == 0 then QNameSet.compare s2 s1 else c) trs in let _ = _flush_str_fmt () in - let strs_strings, max_pre, max_all = List.fold_left (fun (accl, accp, acca) (q, s, f) -> - let s1 = State.print _str_fmt q; _flush_str_fmt () in - let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in - let s3 = Formula.print _str_fmt f; _flush_str_fmt () in - let pre = Pretty.length s1 + Pretty.length s2 in - let all = Pretty.length s3 in - ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) - ) ([], 0, 0) sorted_trs + let strs_strings, max_pre, max_all = + List.fold_left (fun (accl, accp, acca) (q, s, f) -> + let s1 = State.print _str_fmt q; _flush_str_fmt () in + let s2 = QNameSet.print _str_fmt s; _flush_str_fmt () in + let s3 = Formula.print _str_fmt f; _flush_str_fmt () in + let pre = Pretty.length s1 + Pretty.length s2 in + let all = Pretty.length s3 in + ( (q, s1, s2, s3) :: accl, max accp pre, max acca all) + ) ([], 0, 0) sorted_trs in let line = Pretty.line (max_all + max_pre + 6) in - let prev_q = ref State.dummy in + let prev_q = ref State.dummy_state in fprintf fmt "%s@\n" line; List.iter (fun (q, s1, s2, s3) -> - if !prev_q != q && !prev_q != State.dummy then fprintf fmt "%s@\n" line; + if !prev_q != q && !prev_q != State.dummy_state then fprintf fmt "%s@\n" line; prev_q := q; fprintf fmt "%s, %s" s1 s2; - fprintf fmt "%s" (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); - fprintf fmt " %s %s@\n" Pretty.right_arrow s3; + fprintf fmt "%s" + (Pretty.padding (max_pre - Pretty.length s1 - Pretty.length s2)); + fprintf fmt " %s %s@\n" Pretty.left_arrow s3; ) strs_strings; fprintf fmt "%s@\n" line @@ -357,8 +358,10 @@ let normalize_negations auto = let rec flip b f = match Formula.expr f with Boolean.True | Boolean.False -> if b then f else Formula.not_ f - | Boolean.Or(f1, f2) -> (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2) - | Boolean.And(f1, f2) -> (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2) + | Boolean.Or(f1, f2) -> + (if b then Formula.or_ else Formula.and_)(flip b f1) (flip b f2) + | Boolean.And(f1, f2) -> + (if b then Formula.and_ else Formula.or_)(flip b f1) (flip b f2) | Boolean.Atom(a, b') -> begin match a.Atom.node with | Move (m, q) -> @@ -380,7 +383,7 @@ let normalize_negations auto = with Not_found -> (* create a new state and add it to the todo queue *) - let nq = State.make () in + let nq = State.next () in auto.states <- StateSet.add nq auto.states; Hashtbl.add memo_state (q, false) nq; Queue.add (q, false) todo; nq @@ -402,7 +405,7 @@ let normalize_negations auto = with Not_found -> let nq = if b then q else - let nq = State.make () in + let nq = State.next () in auto.states <- StateSet.add nq auto.states; nq in @@ -438,14 +441,24 @@ 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 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 + let is_satisfied dir q t = + Move.for_all (fun d set -> + if List.mem d dir then + StateSet.(is_empty (remove q set)) + else StateSet.is_empty set) t in let update_dependencies dir initacc = let rec loop acc = @@ -457,7 +470,7 @@ let compute_rank auto = 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 + if is_satisfied dir q deps then StateSet.add q acc else acc ) dependencies acc in if acc == new_acc then new_acc else loop new_acc @@ -483,7 +496,6 @@ let compute_rank auto = 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 <- @@ -581,7 +593,7 @@ let rename_states mapper a = let copy a = let mapper = Hashtbl.create MED_H_SIZE in let () = - StateSet.iter (fun q -> Hashtbl.add mapper q (State.make())) a.states + StateSet.iter (fun q -> Hashtbl.add mapper q (State.next())) a.states in rename_states mapper a @@ -641,7 +653,7 @@ let link a1 a2 q link_phi = let union a1 a2 = let a1 = copy a1 in let a2 = copy a2 in - let q = State.make () in + let q = State.next () in let link_phi = StateSet.fold (fun q phi -> Formula.(or_ (stay q) phi)) @@ -653,7 +665,7 @@ let union a1 a2 = let inter a1 a2 = let a1 = copy a1 in let a2 = copy a2 in - let q = State.make () in + let q = State.next () in let link_phi = StateSet.fold (fun q phi -> Formula.(and_ (stay q) phi)) @@ -664,7 +676,7 @@ let inter a1 a2 = let neg a = let a = copy a in - let q = State.make () in + let q = State.next () in let link_phi = StateSet.fold (fun q phi -> Formula.(and_ (not_(stay q)) phi))