+ let (self_q,self_r) = 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 result_q self_q queue = function (* for initializing the queue *)
+ | [] -> self_q,queue
+ | (q,form) :: tl ->
+ if (StateSet.mem q self_q)
+ then begin
+ let q_cand,_,_ = Formula.st form in
+ StateSet.iter (fun x -> Queue.push x queue) q_cand;
+ result_q (StateSet.add q self_q) queue tl;
+ end
+ else result_q self_q queue tl
+ and result_st_q self_q queue flag = function (*for computing the fixed p*)
+ | [] -> flag,queue
+ | form :: tl ->
+ if Formula.infer_form (self_q,self_r) qf qn form
+ then begin
+ let q_cand,_,_ = Formula.st form in
+ StateSet.iter (fun x -> Queue.push x queue) q_cand;
+ result_st_q self_q queue 1 tl;
+ end
+ else result_st_q self_q queue flag tl in
+ let rec comp_acc_self self_q_i queue = (* compute the fixed point *)
+ if Queue.is_empty queue
+ then self_q_i
+ else
+ let q = Queue.pop queue in
+ let list_q,_ = Asta.transitions_st_lab asta q lab in
+ let flag,queue = result_st_q self_q_i queue 0 list_q in
+ let self_q = if flag = 1 then StateSet.add q self_q_i else self_q_i in
+ comp_acc_self self_q queue in
+
+ let self,queue_init = result_q self_q (Queue.create()) list_tr in
+ let self_q = comp_acc_self self_q queue_init in
+ NodeHash.replace run node (self_q,self_r);
+ (* From now, the correct set of states is mapped to node! *)