Module type Model.AUTOMATON


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