- let top_down run =
- let _i = run.pass in
- let tree = run.tree in
- let auto = run.auto in
- let status = run.status in
- let cache2 = run.cache2 in
- let cache5 = run.cache5 in
- let unstable = run.unstable in
- let init_todo = StateSet.diff (Ata.get_states auto) (Ata.get_starting_states auto) in
- let rec loop node =
- let node_id = T.preorder tree node in
- if node == T.nil || not (Bitvector.get unstable node_id) then false else begin
- let parent = T.parent tree node in
- let fc = T.first_child tree node in
- let fc_id = T.preorder tree fc in
- let ns = T.next_sibling tree node in
- let ns_id = T.preorder tree ns in
- let tag = T.tag tree node in
- (* We enter the node from its parent *)
-
- let status0 =
- let c = unsafe_get_status status node_id in
- if c == dummy_status then
- (* first time we visit the node *)
- NodeStatus.make
- { sat = StateSet.empty;
- todo = init_todo;
- summary = NodeSummary.make
- (node == T.first_child tree parent) (* is_left *)
- (node == T.next_sibling tree parent) (* is_right *)
- (fc != T.nil) (* has_left *)
- (ns != T.nil) (* has_right *)
- (T.kind tree node) (* kind *)
- }
- else c
- in
- TRACE(html tree node _i status0 "Entering node");
-
- (* get the node_statuses for the first child, next sibling and parent *)
- let ps = unsafe_get_status status (T.preorder tree parent) in
- let fcs = unsafe_get_status status fc_id in
- let nss = unsafe_get_status status ns_id in
- (* evaluate the transitions with all this statuses *)
- let status1 = eval_trans auto cache2 cache5 tag fcs nss ps status0 in
- TRACE(html tree node _i status1 "Updating transitions");