(** [get_form auto l q] returns a single formula for label [l] in state [q].
Takes time proportional to the number of transitions in the automaton.
*)
+val state_prerequisites : move -> t -> State.t -> StateSet.t
+(** [state_prerequisites m auto q] returns the set of all states q' such
+ that [q', _ -> phi] and [m(q)] is in phi
+*)
val print : Format.formatter -> t -> unit
(** Pretty printing of the automaton *)
*)
val union : t -> t -> t
-(** [union a a'] creates a new automaton [a''] that selects node
+(** [union a a'] creates a new automaton [a''] that selects nodes
selected by either [a] or [a']
*)
val inter : t -> t -> t
-(** [inter a a'] creates a new automaton [a''] that selects node
- selected by both [a] and [a']
+(** [inter a a'] creates a new automaton [a''] that selects nodes
+ selected both by [a] and [a']
*)
val neg : t -> t
val finalize : t -> auto
(** Finalize the automaton and return it. Clean-up unused states
(states that do not occur in any transitions and remove
- instantes of negative [move] atoms by creating fresh states
+ instances of negative [move] atoms by creating fresh states
that accept the complement of the negated state. *)
end
(** Builder facility for the automaton *)