sig
module type COMMAND =
sig
type t
val print : Format.formatter -> t -> unit
type t_command = Internal | Input | Output
val give_type : t -> Model.COMMAND.t_command
val give_queue : t -> int
val give_message : t -> string
end
module type AUTOMATON =
sig
module Owner :
sig
type t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
end
module Location :
sig
type t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
end
module Command : COMMAND
module Transition :
sig
type t
val print : Format.formatter -> t -> unit
val owner : t -> Model.AUTOMATON.Owner.t
val is_controllable : t -> bool
val source : t -> Model.AUTOMATON.Location.t
val target : t -> Model.AUTOMATON.Location.t
val command : t -> Command.t
end
val nb_locations : int
val nb_transitions : int
val nb_owners : int
val iter_locations : (Model.AUTOMATON.Location.t -> unit) -> unit
val iter_transitions : (Model.AUTOMATON.Transition.t -> unit) -> unit
val iter_owners : (Model.AUTOMATON.Owner.t -> unit) -> unit
val fold_locations :
(Model.AUTOMATON.Location.t -> 'a -> 'a) -> 'a -> 'a
val fold_transitions :
(Model.AUTOMATON.Transition.t -> 'a -> 'a) -> 'a -> 'a
val fold_owners : (Model.AUTOMATON.Owner.t -> 'a -> 'a) -> 'a -> 'a
val iter_out_transitions :
(Model.AUTOMATON.Transition.t -> unit) ->
Model.AUTOMATON.Location.t -> unit
val iter_in_transitions :
(Model.AUTOMATON.Transition.t -> unit) ->
Model.AUTOMATON.Location.t -> unit
val fold_out_transitions :
(Model.AUTOMATON.Transition.t -> 'a -> 'a) ->
Model.AUTOMATON.Location.t -> 'a -> 'a
val fold_in_transitions :
(Model.AUTOMATON.Transition.t -> 'a -> 'a) ->
Model.AUTOMATON.Location.t -> 'a -> 'a
val print_automaton : Format.formatter -> unit -> unit
end
module type REGION =
sig
type t
val print : Format.formatter -> t -> unit
val bot : t
val top : t
val eq : t -> t -> bool
val leq : t -> t -> bool
val union : t -> t -> t
val inter : t -> t -> t
val compl : t -> t
val minus : t -> t -> t
val simplify : t -> t
val size : t -> int
val dump : Format.formatter -> t -> unit
end
module type SEMANTICS =
sig
module Region : REGION
module Command : COMMAND
val post : Region.t -> Command.t -> Region.t
val pre : Region.t -> Command.t -> Region.t
val rel : Command.t -> Region.t -> Region.t -> bool
end
module type CLOSURE =
sig module Region : REGION val clo : int -> Region.t -> Region.t end
module type SEMANTICS_CLOSURE =
sig
module Region : REGION
module Command : COMMAND
val post : Region.t -> Command.t -> Region.t
val pre : Region.t -> Command.t -> Region.t
val rel : Command.t -> Region.t -> Region.t -> bool
val clo : int -> Region.t -> Region.t
end
module type S =
sig
module Command : COMMAND
module Automaton :
sig
module Owner :
sig
type t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
end
module Location :
sig
type t
val print : Format.formatter -> t -> unit
val compare : t -> t -> int
val equal : t -> t -> bool
val hash : t -> int
end
module Command :
sig
type t = Command.t
val print : Format.formatter -> t -> unit
type t_command = Command.t_command = Internal | Input | Output
val give_type : t -> t_command
val give_queue : t -> int
val give_message : t -> string
end
module Transition :
sig
type t
val print : Format.formatter -> t -> unit
val owner : t -> Owner.t
val is_controllable : t -> bool
val source : t -> Location.t
val target : t -> Location.t
val command : t -> Command.t
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
end
module Semantics :
sig
module Region : REGION
module Command :
sig
type t = Command.t
val print : Format.formatter -> t -> unit
type t_command = Command.t_command = Internal | Input | Output
val give_type : t -> t_command
val give_queue : t -> int
val give_message : t -> string
end
val post : Region.t -> Command.t -> Region.t
val pre : Region.t -> Command.t -> Region.t
val rel : Command.t -> Region.t -> Region.t -> bool
end
module Closure :
sig
module Region :
sig
type t = Semantics.Region.t
val print : Format.formatter -> t -> unit
val bot : t
val top : t
val eq : t -> t -> bool
val leq : t -> t -> bool
val union : t -> t -> t
val inter : t -> t -> t
val compl : t -> t
val minus : t -> t -> t
val simplify : t -> t
val size : t -> int
val dump : Format.formatter -> t -> unit
end
val clo : int -> Region.t -> Region.t
end
module State :
sig
type t = Automaton.Location.t * Semantics.Region.t
val print : Format.formatter -> t -> unit
end
val nb_init : int
val nb_error : int
val iter_init : (Model.S.State.t -> unit) -> unit
val iter_error : (Model.S.State.t -> unit) -> unit
val fold_init : (Model.S.State.t -> 'a -> 'a) -> 'a -> 'a
val fold_error : (Model.S.State.t -> 'a -> 'a) -> 'a -> 'a
val print_model : Format.formatter -> unit -> unit
end
end
Loading...