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
(* first time we visit the node *)
NodeStatus.make
{ sat = StateSet.empty;
- todo = StateSet.diff
- (Ata.get_states auto)
- (Ata.get_starting_states auto);
+ todo = init_todo;
summary = NodeSummary.make
(node == T.first_child tree parent) (* is_left *)
(node == T.next_sibling tree parent) (* is_right *)
cache.(T.preorder tree node).NodeStatus.node.sat
in
loop (T.root tree);
- StateSet.fold
- (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
- (Ata.get_selecting_states auto) []
+ List.rev (StateSet.fold
+ (fun q acc -> (q, Hashtbl.find res_mapper q)::acc)
+ (Ata.get_selecting_states auto) [])
let prepare_run run list =
let tree = run.tree in