(***********************************************************************)
(*
- Time-stamp: <Last modified on 2013-04-24 18:41:35 CEST by Kim Nguyen>
+ Time-stamp: <Last modified on 2013-04-24 23:24:11 CEST by Kim Nguyen>
*)
INCLUDE "utils.ml"
let config = config.Ata.Config.node in
let oldi = config.Ata.round in
Html.trace (T.preorder tree node) i oldi
- "%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
+ "node: %i<br/>%s<br/>sat: %a<br/>unsat: %a<br/>todo: %around: %i<br/>"
+ ((T.preorder tree node):>int)
msg
StateSet.print config.Ata.sat
StateSet.print config.Ata.unsat
(Ata.TransList.print ~sep:"<br/>") config.Ata.todo oldi
-
type cache = StateSet.t Cache.N1.t
let get c t n = Cache.N1.find c (T.preorder t n)
let fc = T.first_child tree node in
let ns = T.next_sibling tree node in
let tag = T.tag tree node in
- let config0 =
+ let _, config0 =
let c = get cache tree node in
if c == Cache.N1.dummy cache then
- Ata.Config.make
+ true,Ata.Config.make
{ c.Ata.Config.node with
Ata.todo = Ata.get_trans auto tag auto.Ata.states;
summary = Ata.node_summary
TRACE(html tree node _i config0 "Entering node");
- let ps = get cache tree parent in
- let fcs = get cache tree fc in
- let nss = get cache tree ns in
+ let _, ps = get cache tree parent in
+ let old_unstable_left, fcs = get cache tree fc in
+ let old_unstable_right, nss = get cache tree ns in
let config1 = Ata.eval_trans auto fcs nss ps config0 in
TRACE(html tree node _i config1 "Updating transitions");
- if config0 != config1 then set cache tree node config1 _i;
- let unstable_left = loop fc in
- let fcs1 = get cache tree fc in
+ if config0 != config1 then set cache tree node (true,config1) _i;
+ let unstable_left = old_unstable_left && loop fc in
+ let _, fcs1 = get cache tree fc in
let config2 = Ata.eval_trans auto fcs1 nss ps config1 in
TRACE(html tree node _i config2 "Updating transitions (after first-child)");
- if config1 != config2 then set cache tree node config2 _i;
- let unstable_right = loop ns in
- let config3 = Ata.eval_trans auto fcs1 (get cache tree ns) ps config2 in
+ if config1 != config2 then set cache tree node (true, config2) _i;
+ let unstable_right = old_unstable_right && loop ns in
+ let _, nss1 = get cache tree ns in
+ let config3 = Ata.eval_trans auto fcs1 nss1 ps config2 in
TRACE(html tree node _i config3 "Updating transitions (after next-sibling)");
- if config2 != config3 then set cache tree node config3 _i;
+ if config2 != config3 then set cache tree node (true, config3) _i;
let unstable =
unstable_left
|| unstable_right
- || (config0 != config3 && Ata.(TransList.nil != config3.Config.node.todo))
+ || Ata.(TransList.nil != config3.Config.node.todo)
in
- if Ata.(unstable && not config3.Config.node.unstable_subtree) then
- Ata.(config3.Config.node.unstable_subtree <- unstable);
+ if Ata.(config3.Config.node.unstable_subtree) && not unstable then
+ Ata.(config3.Config.node.unstable_subtree <- false);
unstable
end
in
let eval auto tree node =
let cache = Cache.N1.create
- Ata.(Config.make { sat = StateSet.empty;
- unsat = StateSet.empty;
- todo = TransList.nil;
- summary = dummy_summary;
- round = ~-1;
- unstable_subtree = true;
- })
+ true , Ata.(Config.make { sat = StateSet.empty;
+ unsat = StateSet.empty;
+ todo = TransList.nil;
+ summary = dummy_summary;
+ round = ~-1
+ })
in
let redo = ref true in
let iter = ref 0 in