X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fasta.ml;h=f96cd42353bd75fdf0e51b4a996d978a9a5e5aeb;hb=5e7268fb95cdc7e56fe24f324a710550ade3d851;hp=bbbba492cf6c6c01143a31b99e7f4ed2d4e5b2a6;hpb=c1b43e1dcdb3d0960dbc50db9f226d68ad30c16e;p=tatoo.git diff --git a/src/asta.ml b/src/asta.ml index bbbba49..f96cd42 100644 --- a/src/asta.ml +++ b/src/asta.ml @@ -39,6 +39,7 @@ struct State.print st (QNameSet.to_string la) Formula.print f + end module SetT = @@ -88,6 +89,14 @@ let transitions_lab asta lab = (remove_lab (SetT.elements (SetT.filter filter asta.trans_q)), (remove_lab (SetT.elements (SetT.filter filter asta.trans_r)))) +let transitions_st_lab asta q lab = + let filter (s,l,f) = q = s && QNameSet.mem lab l in + let rec remove_st_lab = function + | [] -> [] + | (s,l,f) :: tl -> f :: (remove_st_lab tl) in + (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_q)), + (remove_st_lab (SetT.elements (SetT.filter filter asta.trans_r)))) + let empty = { quer = StateSet.empty; reco = StateSet.empty; @@ -121,6 +130,12 @@ let init_top ast = ast.top <- (StateSet.empty) let top_states ast = StateSet.elements ast.top +let top_states_s ast = ast.top + +let bot_states_s ast = ast.bottom + +let selec_states ast = ast.selec + let print fmt asta = let print_box fmt flag = let pp = Format.fprintf fmt in @@ -145,6 +160,6 @@ let print fmt asta = print_box_list asta.trans_q; Format.fprintf fmt "@[# Recognizing transitions:@ %a@]" print_box_list asta.trans_r in - Format.fprintf fmt "@[##### ASTA #####@, %a@ @]@." print_box 0 + Format.fprintf fmt "@[##### ASTA #####@. %a@ @]@." print_box 0 let to_file out asta = ()