let rec reach_star_aux ((transicoes,_,_) as maq:maquina) (final:estados) (todo:estados) (ch:simbolo)= if Sestado.is_empty todo then final else let elt = Sestado.choose todo in let new_final = Sestado.add elt final in let new_todo = (Sestado.union (Sestado.remove elt todo) (Sestado.diff (reach maq elt ch) new_final)) in reach_star_aux maq new_final new_todo ch