+ let mk_update_result auto =
+ let sel_states = Ata.get_selecting_states auto in
+ let res = L.create () in
+ (fun prepend sat node ->
+ if StateSet.intersect sel_states sat then begin
+ if prepend then L.push_front node res else
+ L.push_back node res
+ end),
+ (fun () -> res)
+
+
+ let mk_update_full_result auto =
+ let dummy = L.create () in
+ let res_mapper = Cache.N1.create dummy in
+ let () =
+ StateSet.iter
+ (fun q -> Cache.N1.add res_mapper (q :> int) (L.create()))
+ (Ata.get_selecting_states auto)
+ in
+ (fun prepend sat node ->
+ StateSet.iter
+ (fun q ->
+ let res = Cache.N1.find res_mapper (q :> int) in
+ if res != dummy then begin
+ if prepend then L.push_front node res
+ else L.push_back node res
+ end
+ ) sat),
+ (fun () ->
+ StateSet.fold_right
+ (fun q acc -> (q, Cache.N1.find res_mapper (q :> int))::acc)
+ (Ata.get_selecting_states auto) [])