then ()
else NodeHash.add run node (map_leaf asta)
else
- let tfnode = Tree.first_child tree tnode (* first child *)
- and tnnode = Tree.next_sibling tree tnode in (* next-sibling *)
+ let tfnode = Tree.first_child tree tnode
+ and tnnode = Tree.next_sibling tree tnode in
let fnode,nnode = (* their preorders *)
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
begin
let qf,qn = q_rec fnode,q_rec nnode in
let lab = Tree.tag tree tnode in
let list_tr,_ = Asta.transitions_lab asta lab in (* only take query. *)
- let set_node,_ = try NodeHash.find run node
- with _ -> raise Max_fail in
- let self = try NodeHash.find run node
+ let (set_node,set_nr) as self = try NodeHash.find run node
with Not_found -> raise Max_fail in
+ (* We must compute again accepting states from self transitions since
+ previous calls of tp_max may remove them *)
+ let rec comp_acc_self set flag = function
+ | [] -> set,flag
+ | (q,form) :: tl ->
+ if Formula.infer_form set qf qn form
+ then if StateSet.mem q set
+ then comp_acc_self set 0 tl
+ else comp_acc_self (StateSet.add q set) 1 tl
+ else comp_acc_self set 0 tl
+ and rec fix_point selfq_i =
+ let setq,flag = comp_acc_self selfq_i 0 list_tr in
+ if flag = 1 then set
+ else fix_point setq qf qn 0 in
+ NodeHash.replace run node (fix_point set_node, set_nr);
+
let rec result = function
| [] -> []
| (q,form) :: tl ->
- if (Formula.infer_form self qf qn form) &&
- (StateSet.mem q set_node) (* infers & trans. can start here *)
+ if (StateSet.mem q set_node) && (* infers & trans. can start here *)
+ (Formula.infer_form self qf qn form)
then form :: (result tl)
else result tl in
let list_form = result list_tr in (* tran. candidates *)
if tnnode == Tree.nil
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
+ (* indeed we delete all states from self transitions! *)
tp_max asta run tree tfnode;
tp_max asta run tree tnnode;
end;