From 3c87bbf00b98bcf40dab913cd334846b26cdb71d Mon Sep 17 00:00:00 2001 From: =?utf8?q?Kim=20Nguy=E1=BB=85n?= Date: Thu, 18 Apr 2013 18:14:44 +0200 Subject: [PATCH] Maintain the set of unsatisfiable states. --- src/ata.ml | 77 ++++++++++++++++++++++++++++++++++++++++++++++++++++- src/ata.mli | 15 ++++++++++- src/eval.ml | 75 ++++++++++++++++++++++++++++++++------------------- 3 files changed, 138 insertions(+), 29 deletions(-) diff --git a/src/ata.ml b/src/ata.ml index c01cd50..4d43441 100644 --- a/src/ata.ml +++ b/src/ata.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -306,6 +306,81 @@ let eval_trans auto ltrs fcs nss ps ss is_left is_right has_left has_right kind +type config = { + sat : StateSet.t; + unsat : StateSet.t; + todo : TransList.t; +} + +let eq_config c1 c2 = + c1.sat == c2.sat && c1.unsat == c2.unsat && c1.todo == c2.todo + +let simplify_atom atom pos q config = + if (pos && StateSet.mem q config.sat) + || ((not pos) && StateSet.mem q config.unsat) then SFormula.true_ + else if (pos && StateSet.mem q config.unsat) + || ((not pos) && StateSet.mem q config.sat) then SFormula.false_ + else atom + + +let eval_form2 phi fcs nss ps ss is_left is_right has_left has_right kind = + let rec loop phi = + begin match SFormula.expr phi with + Formula.True | Formula.False -> phi + | Formula.Atom a -> + let p, b, q = Atom.node a in begin + match p with + | First_child -> simplify_atom phi b q fcs + | Next_sibling -> simplify_atom phi b q nss + | Parent | Previous_sibling -> simplify_atom phi b q ps + | Stay -> simplify_atom phi b q ss + | Is_first_child -> SFormula.of_bool (b == is_left) + | Is_next_sibling -> SFormula.of_bool (b == is_right) + | Is k -> SFormula.of_bool (b == (k == kind)) + | Has_first_child -> SFormula.of_bool (b == has_left) + | Has_next_sibling -> SFormula.of_bool (b == has_right) + end + | Formula.And(phi1, phi2) -> SFormula.and_ (loop phi1) (loop phi2) + | Formula.Or (phi1, phi2) -> SFormula.or_ (loop phi1) (loop phi2) + end + in + loop phi + + + +let eval_trans2 auto fcs nss ps ss is_left is_right has_left has_right kind = + let rec loop old_config = + let { sat = old_sat; unsat = old_unsat; todo = old_todo } = old_config in + let sat, unsat, removed, kept, todo = + TransList.fold + (fun trs acc -> + let q, lab, phi = Transition.node trs in + let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in + if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else + let new_phi = + eval_form2 + phi fcs nss ps old_config + is_left is_right has_left has_right kind + in + if SFormula.is_true new_phi then + StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo + else if SFormula.is_false new_phi then + a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo + else + let new_tr = Transition.make (q, lab, new_phi) in + (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (TransList.cons new_tr a_todo)) + ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, TransList.nil) + in + (* States that have been removed from the todo list and not kept are now + unsatisfiable *) + let unsat = StateSet.union unsat (StateSet.diff removed kept) in + (* States that were found once to be satisfiable remain so *) + let unsat = StateSet.diff unsat sat in + let new_config = { sat; unsat; todo } in + if sat == old_sat && unsat == old_unsat && todo == old_todo then new_config + else loop new_config + in + loop ss (* [add_trans a q labels f] adds a transition [(q,labels) -> f] to the diff --git a/src/ata.mli b/src/ata.mli index bb94a7c..374beb2 100644 --- a/src/ata.mli +++ b/src/ata.mli @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) type predicate = @@ -86,6 +86,19 @@ val eval_trans : t -> TransList.t -> bool -> bool -> bool -> bool -> Tree.NodeKind.t -> TransList.t*StateSet.t +type config = { + sat : StateSet.t; + unsat : StateSet.t; + todo : TransList.t; +} + +val eq_config : config -> config -> bool + +val eval_trans2 : t -> config -> config -> config -> config + -> bool -> bool -> bool -> bool -> Tree.NodeKind.t + -> config + + val add_trans : t -> State.t -> QNameSet.t -> SFormula.t -> unit val print : Format.formatter -> t -> unit val complete_transitions : t -> unit diff --git a/src/eval.ml b/src/eval.ml index 5ebd1ec..8f8652e 100644 --- a/src/eval.ml +++ b/src/eval.ml @@ -14,7 +14,7 @@ (***********************************************************************) (* - Time-stamp: + Time-stamp: *) INCLUDE "utils.ml" @@ -50,12 +50,20 @@ END let fc = T.first_child tree node in let ns = T.next_sibling tree node in let tag = T.tag tree node in - let states0 = get cache tree node in - let trans0 = Ata.get_trans auto tag auto.Ata.states in + let config0 = + let c = get cache tree node in + if c == Cache.N1.dummy cache then + { c with Ata.todo = Ata.get_trans auto tag auto.Ata.states } + else c + in + let () = - TRACE(Html.trace (T.preorder tree node) _i "Pre States: %a
Pre Trans: %a
" - StateSet.print states0 (Ata.TransList.print ~sep:"
") trans0) + TRACE(Html.trace (T.preorder tree node) _i "Config0
sat: %a
unsat: %a
todo: %a
" + StateSet.print config0.Ata.sat + StateSet.print config0.Ata.unsat + (Ata.TransList.print ~sep:"
") config0.Ata.todo) in + let ps = get cache tree parent in let fcs = get cache tree fc in let nss = get cache tree ns in @@ -65,41 +73,51 @@ END and has_right = ns != T.nil and kind = T.kind tree node in - let trans1, states1 = - Ata.eval_trans auto trans0 - fcs nss ps states0 + let config1 = + Ata.eval_trans2 auto fcs nss ps config0 is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "TD States: %a
TD Trans: %a
" StateSet.print states1 (Ata.TransList.print ~sep:"
") trans1) + TRACE(Html.trace (T.preorder tree node) _i "Config1
sat: %a
unsat: %a
todo: %a
" + StateSet.print config1.Ata.sat + StateSet.print config1.Ata.unsat + (Ata.TransList.print ~sep:"
") config1.Ata.todo) in - if states1 != states0 then set cache tree node states1; + if not (Ata.eq_config config0 config1) then set cache tree node config1; let () = loop fc in let fcs1 = get cache tree fc in - let trans2, states2 = - Ata.eval_trans auto trans1 - fcs1 nss ps states1 + let config2 = + Ata.eval_trans2 auto + fcs1 nss ps config1 is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Left BU States: %a
Left BU Trans: %a
" StateSet.print states2 (Ata.TransList.print ~sep:"
") trans2) + TRACE(Html.trace (T.preorder tree node) _i "Config2
sat: %a
unsat: %a
todo: %a
" + StateSet.print config2.Ata.sat + StateSet.print config2.Ata.unsat + (Ata.TransList.print ~sep:"
") config2.Ata.todo) in - if states2 != states1 then set cache tree node states2; + + if not (Ata.eq_config config1 config2) then set cache tree node config2; let () = loop ns in - let _trans3, states3 = - Ata.eval_trans auto trans2 - fcs1 (get cache tree ns) ps states2 + let config3 = + Ata.eval_trans2 auto + fcs1 (get cache tree ns) ps config2 is_left is_right has_left has_right kind in let () = - TRACE(Html.trace (T.preorder tree node) _i "Right BU States: %a
Right BU Trans: %a
" StateSet.print states3 (Ata.TransList.print ~sep:"
") _trans3) + TRACE(Html.trace (T.preorder tree node) _i "Config3
sat: %a
unsat: %a
todo: %a
" + StateSet.print config3.Ata.sat + StateSet.print config3.Ata.unsat + (Ata.TransList.print ~sep:"
") config3.Ata.todo) in - if states3 != states2 then set cache tree node states3; - (*if states0 != states3 && (not !redo) then redo := true *) - if (not !redo) - && not (Ata.TransList.nil == _trans3) - && (states1 != states3) - && not (StateSet.intersect states3 auto.Ata.selection_states) + if not (Ata.eq_config config2 config3) then set cache tree node config3; + (* We do set the redo flat if : *) + if not ( + !redo (* already set *) + || (Ata.TransList.nil == config3.Ata.todo) (* no more transition to check *) + || (Ata.eq_config config0 config3) (* did not gain any new information *) + ) then redo := true end in @@ -113,7 +131,7 @@ END let acc0 = loop (T.next_sibling tree node) acc in let acc1 = loop (T.first_child tree node) acc0 in - if StateSet.intersect (get cache tree node) auto.Ata.selection_states then + if StateSet.intersect (get cache tree node).Ata.sat auto.Ata.selection_states then node::acc1 else acc1 @@ -121,7 +139,10 @@ END loop node [] let eval auto tree node = - let cache = Cache.N1.create StateSet.empty in + let cache = Cache.N1.create { Ata.sat = StateSet.empty; + Ata.unsat = StateSet.empty; + Ata.todo = Ata.TransList.nil } + in let redo = ref true in let iter = ref 0 in Ata.reset auto; -- 2.17.1