loop phi
+ let eval_trans_aux cache4 fcs nss ps ss old_config =
+ let { sat = old_sat;
+ unsat = old_unsat;
+ todo = old_todo;
+ summary = old_summary } = old_config.NodeStatus.node
+ in
+ let sat, unsat, removed, kept, todo =
+ Ata.TransList.fold
+ (fun trs acc ->
+ let q, lab, phi = Ata.Transition.node trs in
+ let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
+ if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
+ let new_phi =
+ eval_form phi fcs nss ps old_config old_summary
+ in
+ if Ata.Formula.is_true new_phi then
+ StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
+ else if Ata.Formula.is_false new_phi then
+ a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
+ else
+ let new_tr = Ata.Transition.make (q, lab, new_phi) in
+ (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
+ ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
+ in
+ (* States that have been removed from the todo list and not kept are now
+ unsatisfiable *)
+ let unsat = StateSet.union unsat (StateSet.diff removed kept) in
+ (* States that were found once to be satisfiable remain so *)
+ let unsat = StateSet.diff unsat sat in
+ let new_config = NodeStatus.make { old_config.NodeStatus.node with sat; unsat; todo; } in
+ new_config
+
let eval_trans cache4 fcs nss ps ss =
let fcsid = (fcs.NodeStatus.id :> int) in
let res = Cache.N4.find cache4 oid fcsid nssid psid in
if res != dummy_status then res
else
- let { sat = old_sat;
- unsat = old_unsat;
- todo = old_todo;
- summary = old_summary } = old_config.NodeStatus.node
+ let new_config =
+ eval_trans_aux cache4 fcs nss ps ss old_config
in
- let sat, unsat, removed, kept, todo =
- Ata.TransList.fold
- (fun trs acc ->
- let q, lab, phi = Ata.Transition.node trs in
- let a_sat, a_unsat, a_rem, a_kept, a_todo = acc in
- if StateSet.mem q a_sat || StateSet.mem q a_unsat then acc else
- let new_phi =
- eval_form phi fcs nss ps old_config old_summary
- in
- if Ata.Formula.is_true new_phi then
- StateSet.add q a_sat, a_unsat, StateSet.add q a_rem, a_kept, a_todo
- else if Ata.Formula.is_false new_phi then
- a_sat, StateSet.add q a_unsat, StateSet.add q a_rem, a_kept, a_todo
- else
- let new_tr = Ata.Transition.make (q, lab, new_phi) in
- (a_sat, a_unsat, a_rem, StateSet.add q a_kept, (Ata.TransList.cons new_tr a_todo))
- ) old_todo (old_sat, old_unsat, StateSet.empty, StateSet.empty, Ata.TransList.nil)
- in
- (* States that have been removed from the todo list and not kept are now
- unsatisfiable *)
- let unsat = StateSet.union unsat (StateSet.diff removed kept) in
- (* States that were found once to be satisfiable remain so *)
- let unsat = StateSet.diff unsat sat in
- let new_config = NodeStatus.make { old_config.NodeStatus.node with sat; unsat; todo; } in
Cache.N4.add cache4 oid fcsid nssid psid new_config;
new_config
in
let c = unsafe_get_status status node_id in
if c == dummy_status then
(* first time we visit the node *)
+ let ltrs = get_trans cache2 auto tag (Ata.get_states auto) in
NodeStatus.make
{ sat = StateSet.empty;
unsat = Ata.get_starting_states auto;
- todo = get_trans cache2 auto tag (Ata.get_states auto);
+ todo = ltrs;
summary = NodeSummary.make
(node == T.first_child tree parent) (* is_left *)
(node == T.next_sibling tree parent) (* is_right *)
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 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 ->
+ try
+ let acc = Hashtbl.find res_mapper q in
+ Hashtbl.replace res_mapper q (node::acc)
+ with
+ Not_found -> ())
+ 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) []
+
let prepare_run run list =
let tree = run.tree in
let auto = run.auto in
status.(node_id) <- status0) list
-
- let eval auto tree nodes =
+ let eval full auto tree nodes =
let run = make auto tree in
prepare_run run nodes;
while run.redo do
- top_down run;
+ top_down run
done;
- get_results run
+ if full then `Full (get_full_results run)
+ else `Normal (get_results run)
+
+
+ let full_eval auto tree nodes =
+ match eval true auto tree nodes with
+ `Full l -> l
+ | _ -> assert false
+
+ let eval auto tree nodes =
+ match eval false auto tree nodes with
+ `Normal l -> l
+ | _ -> assert false
+
end
projects / tatoo.git / blobdiff