module type AUTOMATON = sig
.. end
The AUTOMATON signature specifies the syntactic representation of models.
We consider models that are finite-state control-flow automata whose
Transitions are labeled with commands. The syntax of commands is left
unspecified as an abstract type. Instead of accessors to outbound and
inbound transitions as lists, which would potentially enforce conversions
to lists, we provide iterators over outbound and inbound transitions.
module Owner: sig
.. end
module Location: sig
.. end
module Command: Model.COMMAND
module Transition: sig
.. end
val nb_locations : int
val nb_transitions : int
val nb_owners : int
val iter_locations : (Location.t -> unit) -> unit
val iter_transitions : (Transition.t -> unit) -> unit
val iter_owners : (Owner.t -> unit) -> unit
val fold_locations : (Location.t -> 'a -> 'a) -> 'a -> 'a
val fold_transitions : (Transition.t -> 'a -> 'a) -> 'a -> 'a
val fold_owners : (Owner.t -> 'a -> 'a) -> 'a -> 'a
val iter_out_transitions : (Transition.t -> unit) -> Location.t -> unit
val iter_in_transitions : (Transition.t -> unit) -> Location.t -> unit
val fold_out_transitions : (Transition.t -> 'a -> 'a) ->
Location.t -> 'a -> 'a
val fold_in_transitions : (Transition.t -> 'a -> 'a) ->
Location.t -> 'a -> 'a
val print_automaton : Format.formatter -> unit -> unit