From 902bbf3612fbad7cad16d5492b52317c83191fcd Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Fri, 8 Feb 2013 18:44:11 +0100 Subject: [PATCH] Add functions to normalize an automaton: (1) Ensures that adding transitions leaves them pairwise disjoint (2) Add a function to complete an automaton with dummy states (3) Add a normalization function that replaces negative atoms with a positive state recognizing the complement --- src/auto/ata.ml | 153 ++++++++++++++++++++++++++++++++++--------- src/auto/formula.ml | 5 +- src/auto/formula.mli | 4 +- 3 files changed, 126 insertions(+), 36 deletions(-) diff --git a/src/auto/ata.ml b/src/auto/ata.ml index 5001ebc..ca641b4 100644 --- a/src/auto/ata.ml +++ b/src/auto/ata.ml @@ -14,23 +14,23 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) +INCLUDE "utils.ml" open Format open Utils type move = [ `Left | `Right | `Up1 | `Up2 | `Epsilon ] -type state_ctx = { left : StateSet.t; - right : StateSet.t; - up1 : StateSet.t; - up2 : StateSet.t; - epsilon : StateSet.t} -type ctx_ = { mutable positive : state_ctx; - mutable negative : state_ctx } +type state_ctx = { mutable left : StateSet.t; + mutable right : StateSet.t; + mutable up1 : StateSet.t; + mutable up2 : StateSet.t; + mutable epsilon : StateSet.t} + type pred_ = move * bool * State.t -module Move : (Formula.PREDICATE with type data = pred_ and type ctx = ctx_ ) = +module Move : (Formula.PREDICATE with type data = pred_ and type ctx = state_ctx ) = struct module Node = @@ -40,11 +40,12 @@ struct let hash n = Hashtbl.hash n end - type ctx = ctx_ + 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) + include Hcons.Make(Node) let print ppf a = let _ = flush_str_formatter() in @@ -68,22 +69,22 @@ struct 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 - let nctx = if b then ctx.positive else ctx.negative in + if b then raise (NegativeAtom(l,s)); StateSet.mem s begin match l with - `Left -> nctx.left - | `Right -> nctx.right - | `Up1 -> nctx.up1 - | `Up2 -> nctx.up2 - | `Epsilon -> nctx.epsilon + `Left -> ctx.left + | `Right -> ctx.right + | `Up1 -> ctx.up1 + | `Up2 -> ctx.up2 + | `Epsilon -> ctx.epsilon end end module SFormula = Formula.Make(Move) -type t = { +type 'a t = { id : Uid.t; mutable states : StateSet.t; mutable top_states : StateSet.t; @@ -92,8 +93,6 @@ type t = { transitions: (State.t, (QNameSet.t*SFormula.t) list) Hashtbl.t; } - - let next = Uid.make_maker () let create () = { id = next (); @@ -104,18 +103,30 @@ let create () = { id = next (); transitions = Hashtbl.create 17; } + +(* + [add_trans a q labels f] adds a transition [(q,labels) -> f] to the + automaton [a] but ensures that transitions remains pairwise disjoint +*) + let add_trans a q s f = let trs = try Hashtbl.find a.transitions q with Not_found -> [] in - let rem, ntrs = - List.fold_left (fun (rem, atrs) ((labs, phi) as tr) -> - let nlabs = QNameSet.inter labs rem in - if QNameSet.is_empty nlabs then - (rem, tr :: atrs) - else - let nrem = QNameSet.diff rem labs in - nrem, (nlabs, SFormula.or_ phi f)::atrs - ) (s, []) trs + 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, SFormula.or_ phi f) ] + in + let tr2 = + if QNameSet.is_empty lab2 then [] + else [ (lab2, SFormula.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 @@ -160,3 +171,85 @@ let print fmt a = fprintf fmt "%s, %s" s1 s2; fprintf fmt "%s" (Pretty.padding (maxs - String.length s1 - String.length s2 - 2)); fprintf fmt "%s %s@\n" Pretty.right_arrow s3) strs_strings + +(* + [complete transitions a] ensures that for each state q + and each symbols s in the alphabet, a transition q, s exists. + (adding q, s -> F when necessary). +*) + +let complete_transitions a = + StateSet.iter (fun q -> + let qtrans = Hashtbl.find a.transitions q in + let rem = + List.fold_left (fun rem (labels, _) -> + QNameSet.diff rem labels) QNameSet.any qtrans + in + let nqtrans = + if QNameSet.is_empty rem then qtrans + else + (rem, SFormula.false_) :: qtrans + in + Hashtbl.replace a.transitions q nqtrans + ) a.states + +(* [normalize_negations a] removes negative atoms in the formula + complementing the sub-automaton in the negative states. + [TODO check the meaning of negative upward arrows] +*) +let normalize_negations a = + let memo_state = Hashtbl.create 17 in + let todo = Queue.create () in + let rec flip b f = + match SFormula.expr f with + Formula.True | Formula.False -> if b then f else SFormula.not_ f + | Formula.Or(f1, f2) -> (if b then SFormula.or_ else SFormula.and_)(flip b f1) (flip b f2) + | 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 + (* 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 + (* 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 + *) + 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 + Hashtbl.add memo_state (q, false) nq; + Queue.add (q, false) todo; nq + in + SFormula.atom_ (Move.make (l, true, not_q)) + end + end + in + StateSet.iter (fun q -> Queue.add (q, true) todo) a.top_states; + 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 State.make () in + Hashtbl.add memo_state key nq; nq + in + let trans = Hashtbl.find a.transitions q in + let trans' = List.map (fun (lab, f) -> lab, flip b f) trans in + Hashtbl.replace a.transitions q' trans' + done; + Hashtbl.iter (fun (q, b) q' -> + if not (b || StateSet.mem q a.bottom_states) then + a.bottom_states <- StateSet.add q' a.bottom_states + ) memo_state + diff --git a/src/auto/formula.ml b/src/auto/formula.ml index 70407cf..27bd19a 100644 --- a/src/auto/formula.ml +++ b/src/auto/formula.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -26,9 +26,6 @@ open Utils (** Implementation of hashconsed Boolean formulae *) -type move = [ `Left | `Right | `Epsilon | `Up1 | `Up2 ] - -(** Direction for automata predicates *) *) module type PREDICATE = sig diff --git a/src/auto/formula.mli b/src/auto/formula.mli index 3cf240d..a537b2c 100644 --- a/src/auto/formula.mli +++ b/src/auto/formula.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) module type PREDICATE = @@ -53,7 +53,7 @@ sig (** Equality over formulae *) val expr : t -> (t,P.t) expr - (** Equality over formulae *) + (** Return a view of the formulae *) val compare : t -> t -> int (** Comparison of formulae *) -- 2.17.1