- in
- let unstable_right = loop ns in
- let nss1 = unsafe_get_status status ns_id in
- let status3 = if status2.NodeStatus.node.todo == StateSet.empty then status2 else begin
- let status3 = eval_trans auto cache2 cache5 tag fcs1 nss1 ps status2 in
- IFTRACE(html tree node _i status3 "Updating transitions (after next-sibling)");
- if status3 != status2 then status.(node_id) <- status3;
- status3
- end
- in
- let unstable_self =
- (* if either our left or right child is unstable or if we still have transitions
- pending, the current node is unstable *)
- unstable_left
- || unstable_right
- || StateSet.empty != status3.NodeStatus.node.todo
- in
- Bitvector.unsafe_set unstable node_id unstable_self;
- IFTRACE((if not unstable_self then
- Html.finalize_node
- node_id
- _i
- Ata.(StateSet.intersect status3.NodeStatus.node.sat (get_selecting_states auto))));
- unstable_self
- end
- in
- run.redo <- loop (T.root tree);
- run.pass <- run.pass + 1
-
-
- let get_results run =
- let cache = run.status in
- let auto = run.auto in
- let tree = run.tree in
- let rec loop node acc =
- if node == T.nil then acc
- else
- let acc0 = loop (T.next_sibling tree node) acc in
- let acc1 = loop (T.first_child tree node) acc0 in
-
- if Ata.(
- StateSet.intersect
- cache.(T.preorder tree node).NodeStatus.node.sat
- (get_selecting_states auto)) then node::acc1
- else acc1
- in
- loop (T.root tree) []
-
-
- let get_full_results run =
- let cache = run.status in
- let auto = run.auto in
- let tree = run.tree in
- let res_mapper = Hashtbl.create MED_H_SIZE in
- let () =
- StateSet.iter
- (fun q -> Hashtbl.add res_mapper q [])
- (Ata.get_selecting_states auto)
- in
- let dummy = [ T.nil ] in
- let res_mapper = Cache.N1.create dummy in
- let () =
- StateSet.iter
- (fun q -> Cache.N1.add res_mapper (q :> int) [])
- (Ata.get_selecting_states auto)
- in
- let rec loop node =
- if node != T.nil then
- let () = loop (T.next_sibling tree node) in
- let () = loop (T.first_child tree node) in
- StateSet.iter
- (fun q ->
- let res = Cache.N1.find res_mapper (q :> int) in
- if res != dummy then
- Cache.N1.add res_mapper (q :> int) (node::res)
- )
- cache.(T.preorder tree node).NodeStatus.node.sat