X-Git-Url: http://git.nguyen.vg/gitweb/?a=blobdiff_plain;f=src%2Fasta.mli;h=76ebdb17247b48ae9e3a0f597f52c4628a78420e;hb=6b4b9309e0f49f9a87d97ea87829aa74614dedb7;hp=a0d589f691988f48c931d4b61c18249b574e1367;hpb=e80e269c313952b4d427fa6a5a9729ea15e43f39;p=tatoo.git diff --git a/src/asta.mli b/src/asta.mli index a0d589f..76ebdb1 100644 --- a/src/asta.mli +++ b/src/asta.mli @@ -34,8 +34,9 @@ type t val transition : t -> state -> label -> formula (** Give the formula which must hold for a current state and label *) -val transitions : t -> state -> (label*formula) list -(** Give the list of labels and formulae from transitions for a given state *) +val transitions : t -> state -> ((label*formula) list)*((label*formula) list) +(** Give the list of labels and formulae from queries and recognizing + transitions for a given state *) val empty : t (** The empty automaton *) @@ -46,14 +47,17 @@ val any_label : label val new_state : unit -> state (** Give a new state (different from all others states) *) -val add_tr : t -> transition -> unit -(** Add a transition to an asta *) +val add_tr : t -> transition -> bool -> unit +(** Add a query transition (recognizing transition if flag=false) to an asta *) val add_reco : t -> state -> unit (** Add a state to the recognizing states of an asta *) +val add_quer : t -> state -> unit +(** Add a state to the query states of an asta *) + val add_selec : t -> state -> unit -(** Add a state to the recognizing states of an asta *) +(** Add a state to the selecting states of an asta *) val add_bot : t -> state -> unit (** Add a state to the bottom states of an asta *) @@ -61,11 +65,14 @@ val add_bot : t -> state -> unit val add_top : t -> state -> unit (** Add a state to the top states of an asta *) +val init_top : t -> unit +(** Remove all top states *) + val top_states : t -> state list (** Give the list of top states of an ASTA *) val print : Format.formatter -> t -> unit -(** Describe the automaton as text *) +(** Pretty printer *) val to_file : out_channel -> t -> unit (** Outputs the description of the automaton on the given out_channel *)