StateSet.print asta.selec;
pp "@[<v 0># Bottom states: %a@ @]"
StateSet.print asta.bottom;
- pp "@[<v 0># Tom states: %a@ @]"
+ pp "@[<v 0># Top states: %a@ @]"
StateSet.print asta.top;
let print_list_tr fmt z=
if SetT.is_empty z
Asta.add_quer asta top_st;
Asta.init_top asta;
Asta.add_top asta top_st;
+ Asta.add_bot asta top_st; (* for trees which are leaves *)
Asta.add_tr asta (top_st, Asta.any_label, or_top) true
and trans_last (ax,test,pred) = (* a selecting state is needed *)
Asta.add_quer asta q';
Asta.add_top asta q;
Asta.add_top asta q';
- Asta.add_bot asta q;
- Asta.add_bot asta q';
+ Asta.add_bot asta q; (* q' \notin B !! *)
let Simple lab = test in
let tr_selec = (q', lab, fo_p)
and tr_q = (q, Asta.any_label, form_propa_selec q q' ax) in
# Query states: { q₁ q₂ q₈ q₉ }
# Recognizing states: { q₀ q₃ q₄ q₅ q₆ q₇ }
# Selecting states: { q₁ }
- # Bottom states: { qâ\82\81 qâ\82\82 qâ\82\88 }
- # Tom states: { q₉ }
+ # Bottom states: { qâ\82\82 qâ\82\88 qâ\82\89 }
+ # Top states: { q₉ }
# Queries transitions:
| q₁ ----F(b)---> ↓₁q₀
| q₂ ----Cof(ø)---> ↓₁q₂ ∨ ↓₂q₂ ∨ ↓₁q₁ ∨ ↓₂q₁