- 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)