X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fauto%2Fata.ml;h=275d6577600c9eafa3fc4bb9245aaad908b01217;hb=249bd234500a64919cf00f4a59ab4927a068d689;hp=576941d198f0e411524d6e726d8d5f84636cd5eb;hpb=a3d6ecbcea379fa51785848a5b8b53bca4e4bdd2;p=tatoo.git diff --git a/src/auto/ata.ml b/src/auto/ata.ml index 576941d..275d657 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,21 +14,30 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" open Format open Utils -type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ] +type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon |`Is1 |`Is2 ] type state_ctx = { mutable left : StateSet.t; mutable right : StateSet.t; mutable up1 : StateSet.t; mutable up2 : StateSet.t; - mutable epsilon : StateSet.t} + mutable epsilon : StateSet.t; + mutable is_left : bool; + mutable is_root : bool} type pred_ = move * bool * State.t +let make_ctx a b c d e f g = + { left = a; right = b; up1 = c; up2 = d; epsilon = e; is_left = f; is_root = g } + +let print_ctx fmt c = fprintf fmt "{ left : %a; right : %a; up1: %a ; up2 : %a; epsilon : %a ; is_left : %b; is_root : %b }" + StateSet.print c.left StateSet.print c.right StateSet.print c.up1 StateSet.print c.up2 + StateSet.print c.epsilon + c.is_left c.is_root module Move : (Formula.PREDICATE with type data = pred_ and type ctx = state_ctx ) = struct @@ -42,8 +51,6 @@ struct type ctx = state_ctx - let make_ctx a b c d e = - { left = a; right = b; up1 = c; up2 = d; epsilon = e } include Hcons.Make(Node) let _pr_buff = Buffer.create 10 @@ -63,27 +70,40 @@ struct | `Epsilon -> Pretty.epsilon, "" | `Up1 -> Pretty.up_arrow, Pretty.subscript 1 | `Up2 -> Pretty.up_arrow, Pretty.subscript 2 + | `Is1 -> "?", Pretty.subscript 1 + | `Is2 -> "?", Pretty.subscript 2 in fprintf _str_fmt "%s%s" dir num; - State.print _str_fmt s; + if s != State.dummy then State.print _str_fmt s; let str = _flush_str_fmt () in - if b then fprintf ppf "%s" str - else Pretty.pp_overline ppf str - + fprintf ppf "%s%s" (if b then "" else Pretty.lnot) str let neg p = let l, b, s = p.node in make (l, not b, s) + exception NegativeAtom of (move*State.t) + let eval ctx p = let l, b, s = p.node in - if b then raise (NegativeAtom(l,s)); - StateSet.mem s begin - match l with - `Left -> ctx.left - | `Right -> ctx.right - | `Up1 -> ctx.up1 - | `Up2 -> ctx.up2 - | `Epsilon -> ctx.epsilon + if s == State.dummy then + let dir = + match l with + | `Is1 -> ctx.is_left + | _ -> not ctx.is_left + in + let res = dir && not ctx.is_root in + res && b || (not (b || res)) + else begin + if not b then raise (NegativeAtom(l,s)); + StateSet.mem s begin + match l with + `Left -> ctx.left + | `Right -> ctx.right + | `Up1 -> ctx.up1 + | `Up2 -> ctx.up2 + | `Epsilon -> ctx.epsilon + | _ -> StateSet.empty + end end end @@ -91,8 +111,8 @@ module SFormula = Formula.Make(Move) type t = { id : Uid.t; mutable states : StateSet.t; -(* mutable top_states : StateSet.t; - mutable bottom_states: StateSet.t; *) + mutable top_states : StateSet.t; + mutable bottom_states: StateSet.t; mutable selection_states: StateSet.t; transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; } @@ -101,13 +121,22 @@ let next = Uid.make_maker () let create () = { id = next (); states = StateSet.empty; -(* top_states = StateSet.empty; - bottom_states = StateSet.empty; *) + top_states = StateSet.empty; + bottom_states = StateSet.empty; selection_states = StateSet.empty; transitions = Hashtbl.create 17; } +let get_trans a states tag = + StateSet.fold (fun q acc0 -> + try + let trs = Hashtbl.find a.transitions q in + List.fold_left (fun acc1 (labs, phi) -> + if QNameSet.mem tag labs then (q,phi)::acc1 else acc1) acc0 trs + with Not_found -> acc0 + ) states [] + (* [add_trans a q labels f] adds a transition [(q,labels) -> f] to the automaton [a] but ensures that transitions remains pairwise disjoint @@ -146,10 +175,14 @@ let print fmt a = fprintf fmt "\nInternal UID: %i@\n\ States: %a@\n\ + Top states: %a@\n\ + Bottom states: %a@\n\ Selection states: %a@\n\ Alternating transitions:@\n" (a.id :> int) StateSet.print a.states + StateSet.print a.top_states + StateSet.print a.bottom_states StateSet.print a.selection_states; let trs = Hashtbl.fold @@ -207,7 +240,7 @@ let complete_transitions a = complementing the sub-automaton in the negative states. [TODO check the meaning of negative upward arrows] *) -let normalize_negations a = +let normalize_negations auto = let memo_state = Hashtbl.create 17 in let todo = Queue.create () in let rec flip b f = @@ -217,16 +250,18 @@ let normalize_negations a = | Formula.And(f1, f2) -> (if b then SFormula.and_ else SFormula.or_)(flip b f1) (flip b f2) | Formula.Atom(a) -> begin let l, b', q = Move.node a in - if b == b' then begin + if q == State.dummy then if b then f else SFormula.not_ f + else + 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; - SFormula.atom_ (Move.make (l, true, q)) - end else begin + if not (Hashtbl.mem memo_state (q,b)) then Queue.add (q,true) todo; + SFormula.atom_ (Move.make (l, true, 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 containing formula + b = sign of the enclosing formula *) let not_q = try @@ -236,6 +271,11 @@ let normalize_negations a = 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; +(* if not (StateSet.mem q auto.bottom_states) then + auto.bottom_states <- StateSet.add nq auto.bottom_states; + if not (StateSet.mem q auto.top_states) then + auto.top_states <- StateSet.add nq auto.top_states; *) Hashtbl.add memo_state (q, false) nq; Queue.add (q, false) todo; nq in @@ -243,7 +283,9 @@ let normalize_negations a = end end in - StateSet.iter (fun q -> Queue.add (q, true) todo) a.selection_states; + (* states that are not reachable from a selection stat are not interesting *) + StateSet.iter (fun q -> Queue.add (q, true) todo) auto.selection_states; + while not (Queue.is_empty todo) do let (q, b) as key = Queue.pop todo in let q' = @@ -251,10 +293,18 @@ let normalize_negations a = Hashtbl.find memo_state key with Not_found -> - let nq = if b then q else State.make () in + let nq = if b then q else + let nq = State.make () in + auto.states <- StateSet.add nq auto.states; +(* if not (StateSet.mem q auto.bottom_states) then + auto.bottom_states <- StateSet.add nq auto.bottom_states; + if not (StateSet.mem q auto.top_states) then + auto.top_states <- StateSet.add nq auto.top_states; *) + nq + in Hashtbl.add memo_state key nq; nq in - let trans = Hashtbl.find a.transitions q in + let trans = Hashtbl.find auto.transitions q in let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in - Hashtbl.replace a.transitions q' trans' + Hashtbl.replace auto.transitions q' trans' done