X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fasta.ml;h=f96cd42353bd75fdf0e51b4a996d978a9a5e5aeb;hb=5e7268fb95cdc7e56fe24f324a710550ade3d851;hp=19fe29fc4baedb9a2b0333d9ad112ebc75a9c4ff;hpb=43df500d1441955e3bc932be2e76318f759f7295;p=tatoo.git diff --git a/src/asta.ml b/src/asta.ml index 19fe29f..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 = @@ -74,12 +75,28 @@ let transition asta st lab = let transitions asta st = let filter (s,l,f) = State.compare s st = 0 in - let rec remove_states l = match l with + let rec remove_states = function | [] -> [] - | (a,s,l) :: tl -> (s,l) :: (remove_states tl) in + | (s,l,f) :: tl -> (l,f) :: (remove_states tl) in (remove_states (SetT.elements (SetT.filter filter asta.trans_q)), (remove_states (SetT.elements (SetT.filter filter asta.trans_r)))) +let transitions_lab asta lab = + let filter (s,l,f) = QNameSet.mem lab l in + let rec remove_lab = function + | [] -> [] + | (s,l,f) :: tl -> (s,f) :: (remove_lab tl) in + (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; @@ -113,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 @@ -137,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 = ()