From: Lucca Hirschi Date: Thu, 12 Jul 2012 09:40:34 +0000 (+0200) Subject: Add `Self direction in Formula + compute fixed point in Run. X-Git-Tag: Core+FS_tested~7 X-Git-Url: http://git.nguyen.vg/gitweb/?p=tatoo.git;a=commitdiff_plain;h=0223b78baf156e7b8de86e334a4648fb2c3819e8 Add `Self direction in Formula + compute fixed point in Run. --- diff --git a/src/formula.ml b/src/formula.ml index 8369571..2d9893c 100644 --- a/src/formula.ml +++ b/src/formula.ml @@ -15,7 +15,7 @@ INCLUDE "utils.ml" open Format -type move = [ `Left | `Right ] +type move = [ `Left | `Right | `Self ] type 'hcons expr = | False | True | Or of 'hcons * 'hcons @@ -73,30 +73,30 @@ let prio f = | Or _ -> 1 (* Begin Lucca Hirschi *) -let rec eval_form ss f = match expr f with +let rec eval_form (q,qf,qn) f = match expr f with | False -> false | True -> true - | And(f1,f2) -> eval_form ss f1 && eval_form ss f2 - | Or(f1,f2) -> eval_form ss f1 || eval_form ss f2 + | And(f1,f2) -> eval_form (q,qf,qn) f1 && eval_form (q,qf,qn) f2 + | Or(f1,f2) -> eval_form (q,qf,qn) f1 || eval_form (q,qf,qn) f2 | Atom(dir, b, s) -> - let set = match dir with |`Left -> fst ss | `Right -> snd ss in + let set = match dir with + |`Left -> qf | `Right -> qn | `Self -> q in if b then StateSet.mem s set else not (StateSet.mem s set) -let rec infer_form ssq ssr f = match expr f with +let rec infer_form sq sqf sqn f = match expr f with | False -> false | True -> true - | And(f1,f2) -> infer_form ssq ssr f1 && infer_form ssq ssr f2 - | Or(f1,f2) -> infer_form ssq ssr f1 || infer_form ssq ssr f2 + | And(f1,f2) -> infer_form sq sqf sqn f1 && infer_form sq sqf sqn f2 + | Or(f1,f2) -> infer_form sq sqf sqn f1 || infer_form sq sqf sqn f2 | Atom(dir, b, s) -> let setq, setr = match dir with - |`Left -> fst ssq, fst ssr - | `Right -> snd ssq, snd ssr in + | `Left -> sqf | `Right -> sqn | `Self -> sq in (* WG: WE SUPPOSE THAT Q^r and Q^q are disjoint ! *) let mem = StateSet.mem s setq || StateSet.mem s setr in if b then mem else not mem (* End *) - + let rec print ?(parent=false) ppf f = if parent then fprintf ppf "("; let _ = match expr f with @@ -117,6 +117,7 @@ let rec print ?(parent=false) ppf f = match dir with | `Left -> Pretty.down_arrow, Pretty.subscript 1 | `Right -> Pretty.down_arrow, Pretty.subscript 2 + | `Self -> Pretty.down_arrow, Pretty.subscript 0 in fprintf fmt "%s%s" a_str d_str; State.print fmt s; @@ -147,6 +148,7 @@ let atom_ d p s = let ss = match d with | `Left -> si, StateSet.empty | `Right -> StateSet.empty, si + | `Self -> si, StateSet.empty (* TODO WHAT? *) in fst (cons (Atom(d,p,s)) (Atom(d,not p,s)) ss ss 1 1) let not_ f = f.Node.node.neg diff --git a/src/formula.mli b/src/formula.mli index 69bdb78..9ecf30a 100644 --- a/src/formula.mli +++ b/src/formula.mli @@ -15,7 +15,7 @@ (** Implementation of hashconsed Boolean formulae *) -type move = [ `Left |`Right ] +type move = [ `Left |`Right | `Self ] (** Direction for automata predicates *) type 'hcons expr = @@ -52,11 +52,11 @@ val compare : t -> t -> int val size : t -> int (** Syntactic size of the formula *) -val eval_form : (StateSet.t * StateSet.t) -> t -> bool -(** [eval_form (sf,sn) F] evaluates the formula [F] on [(sf,sn)] *) +val eval_form : (StateSet.t * StateSet.t * StateSet.t) -> t -> bool +(** [eval_form (s,sf,sn) F] evaluates the formula [F] on [(s,sf,sn)] *) -val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool -(** [eval_form S1 S2 F] infers S1; S2 |- F *) +val infer_form : (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> (StateSet.t * StateSet.t) -> t -> bool +(** [eval_form S Sf Sn F] infers S; (S1,S2) |- F *) val print : Format.formatter -> t -> unit (** Pretty printer *) diff --git a/src/run.ml b/src/run.ml index 482a749..2e0cf95 100644 --- a/src/run.ml +++ b/src/run.ml @@ -25,7 +25,7 @@ module NodeHash = Hashtbl.Make (Node) type t = (StateSet.t*StateSet.t) NodeHash.t (** Map from nodes to query and recognizing states *) -(* Note that we do not consider the nil nodes *) +(* Note that we do not consider nil nodes *) exception Oracle_fail exception Over_max_fail @@ -56,16 +56,22 @@ let rec bu_oracle asta run tree tnode = let (_,qfr),(_,qnr) = q_rec fnode,q_rec nnode (* computed in rec call *) and lab = Tree.tag tree tnode in let _,list_tr = Asta.transitions_lab asta lab in (* only reco. tran.*) - let rec result set = function - | [] -> set + let rec result set flag = function (* add states which satisfy a transition *) + | [] -> set,flag | (q,form) :: tl -> - if Formula.eval_form (qfr,qnr) form (* evaluates the formula *) - then result (StateSet.add q set) tl - else result set tl in - let result_set = result StateSet.empty list_tr in - NodeHash.add run node (StateSet.empty, result_set) + if Formula.eval_form (set,qfr,qnr) form (* evaluates the formula*) + then + if StateSet.mem q set + then result set 0 tl + else result (StateSet.add q set) 1 tl + else result set 0 tl in + let rec fix_point set_i = (* compute the fixed point of states of node *) + let set,flag = result set_i 0 list_tr in + if flag = 0 then set + else fix_point set in + NodeHash.add run node (StateSet.empty, fix_point StateSet.empty) end - + (* Build the over-approx. of the maximal run *) let rec bu_over_max asta run tree tnode = if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *) @@ -83,18 +89,25 @@ let rec bu_over_max asta run tree tnode = let q_rec n = try NodeHash.find run n with Not_found -> map_leaf asta in - let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in + let qf,qn = q_rec fnode,q_rec nnode in let lab = Tree.tag tree tnode in - let list_tr,_ = Asta.transitions_lab asta lab in (* only take query st. *) - let rec result set = function - | [] -> set - | (q,form) :: tl -> - if Formula.infer_form (qfq,qnq) (qfr,qnr) form (* infers the formula*) - then result (StateSet.add q set) tl - else result set tl in - let _,resultr = try NodeHash.find run node + let list_tr,_ = Asta.transitions_lab asta lab (* only take query st. *) + and _,resultr = try NodeHash.find run node with _ -> raise Over_max_fail in - let result_set = result StateSet.empty list_tr in + let rec result set flag = function + | [] -> set,flag + | (q,form) :: tl -> + if Formula.infer_form (set,resultr) qf qn form (* infers the formula*) + then if StateSet.mem q set + then result set 0 tl + else result (StateSet.add q set) 1 tl + else result set 0 tl in + let rec fix_point set_i = + let set,flag = result set_i 0 list_tr in + if flag = 0 + then set + else fix_point set in + let result_set = fix_point StateSet.empty in (* we keep the old recognizing states set *) NodeHash.replace run node (result_set, resultr) end @@ -121,15 +134,17 @@ let rec tp_max asta run tree tnode = let q_rec n = try NodeHash.find run n with Not_found -> map_leaf asta in - let (qfq,qfr),(qnq,qnr) = q_rec fnode,q_rec nnode in + let qf,qn = q_rec fnode,q_rec nnode in let lab = Tree.tag tree tnode in let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *) let set_node,_ = try NodeHash.find run node with _ -> raise Max_fail in + let self = try NodeHash.find run node + with Not_found -> raise Max_fail in let rec result = function | [] -> [] | (q,form) :: tl -> - if (Formula.infer_form (qfq,qnq) (qfr,qnr) form) && + if (Formula.infer_form self qf qn form) && (StateSet.mem q set_node) (* infers & trans. can start here *) then form :: (result tl) else result tl in