+(* Build the maximal run *)
+let rec tp_max asta run tree tnode =
+ if (Tree.is_leaf tree tnode) (* BU_oracle has already created the map *)
+ then
+ ()
+ else
+ let node = Tree.preorder 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
+ begin
+ if tnode == Tree.root tree (* we must intersect with top states *)
+ then let setq,_ = try NodeHash.find run node
+ with _ -> raise Max_fail in
+ NodeHash.replace run node
+ ((StateSet.inter (Asta.top_states_s asta) setq),StateSet.empty)
+ else ();
+ let q_rec n =
+ try NodeHash.find run n
+ with Not_found -> map_leaf asta in
+ 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,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 =
+ () (* 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
+ | [] -> []
+ | (q,form) :: tl ->
+ 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 *)
+ (* compute states occuring in transition candidates *)
+ let rec add_st (ql,qr) = function
+ | [] -> ql,qr
+ | f :: tl -> let sqs,sql,sqr = Formula.st f in
+ let ql' = StateSet.union sql ql
+ and qr' = StateSet.union sqr qr in
+ add_st (ql',qr') tl in
+ let ql,qr = add_st (StateSet.empty, StateSet.empty) list_form in
+ let qfq,qfr = try NodeHash.find run fnode
+ with | _ -> map_leaf asta
+ and qnq,qnr = try NodeHash.find run nnode
+ with | _ -> map_leaf asta in
+ begin
+ if tfnode == Tree.nil || Tree.is_attribute tree tnode
+ then ()
+ else NodeHash.replace run fnode (StateSet.inter qfq ql,qfr);
+ 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! *)
+ tp_max asta run tree tfnode;
+ tp_max asta run tree tnnode;
+ end;
+ end
+
+let compute tree asta =
+ let flag = 2 in (* debug *)
+ let size_tree = 10000 in (* todo (Tree.size ?) *)
+ let map = NodeHash.create size_tree in
+ bu_oracle asta map tree (Tree.root tree);
+ if flag > 0 then begin
+ bu_over_max asta map tree (Tree.root tree);
+ if flag = 2
+ then
+ tp_max asta map tree (Tree.root tree)
+ else ()
+ end
+ else ();
+ map