then ()
else NodeHash.add run node (map_leaf asta)
else
- let tfnode = Tree.first_child tree tnode
+ let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
let fnode,nnode = (* their preorders *)
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
then
()
else
- let tfnode = Tree.first_child tree tnode
+ let tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
begin
bu_over_max asta run tree tfnode;
()
else
let node = Tree.preorder tree tnode
- and tfnode = Tree.first_child tree tnode
+ and tfnode = Tree.first_child_x tree tnode
and tnnode = Tree.next_sibling tree tnode in
let (fnode,nnode) =
(Tree.preorder tree tfnode, Tree.preorder tree tnnode) in
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 comp_acc_self set flag =
+ () (* given a current set of states we add
+ states from self transitions which satisfy the two conditions *)
+ (* With result (below) we have all valid transitions at step 0
+ we compute the self states which occur in it and which are not in cthe current state.
+ For each of these states we compute the transitions with the correct label and state
+ we infer each of these transitions: true -> add self states occuring in it
+ to the acc and to the current set + add left and right states as result do *)
+ (* ----> With a FIFO *)
+ and fix_point selfq_i =
+ () in
+ NodeHash.replace run node (set_node, set_nr);
let rec result = function
| [] -> []
and qnq,qnr = try NodeHash.find run nnode
with | _ -> map_leaf asta in
begin
- if tfnode == Tree.nil
+ if tfnode == Tree.nil || Tree.is_attribute tree tnode
then ()
else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
- if tnnode == Tree.nil
+ if tnnode == Tree.nil || Tree.is_attribute tree tnode
then ()
else NodeHash.replace run nnode (StateSet.inter qnq qr,qnr);
(* indeed we delete all states from self transitions! *)
NodeHash.fold
(fun key set acc ->
if not(StateSet.is_empty
- (StateSet.inter (fst set) (Asta.selec_states asta)))
+ (StateSet.inter (fst set) (Asta.selec_states asta)))
then key :: acc
else acc)
run []