mutable entry_points : (Tag.t*Ptset.t) list;
mutable contains : string option;
mutable univ_states : Ata.state list;
mutable entry_points : (Tag.t*Ptset.t) list;
mutable contains : string option;
mutable univ_states : Ata.state list;
let s = Ptset.union anc_st (Ptset.from_list [])
in if has_backward then Ptset.add config.st_from_root s else s
in { Ata.id = Oo.id (object end);
let s = Ptset.union anc_st (Ptset.from_list [])
in if has_backward then Ptset.add config.st_from_root s else s
in { Ata.id = Oo.id (object end);
Ata.init = Ptset.singleton config.st_root;
Ata.final = Ptset.union anc_st config.final_state;
Ata.universal = Ptset.add a_dst (Ptset.from_list config.univ_states);
Ata.phi = phi;
Ata.init = Ptset.singleton config.st_root;
Ata.final = Ptset.union anc_st config.final_state;
Ata.universal = Ptset.add a_dst (Ptset.from_list config.univ_states);
Ata.phi = phi;