+ (* 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);
+