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