sig
type sort = string
type sortidx = int
type process = Ph_types.sort * Ph_types.sortidx
module PSet :
sig
type elt = process
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
end
module PMap :
sig
type key = process
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
end
module PCSet :
sig
type elt = process * process
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
end
val procs_of_ps : Ph_types.process list -> Ph_types.PSet.t
val string_of_proc : Ph_types.process -> string
val pintstring_of_proc : Ph_types.process -> string
val string_of_procs : Ph_types.PSet.t -> string
type rate = (float * int) option
val rsa_of_stochatime : PintTypes.stochatime -> Ph_types.rate
type hits =
(Ph_types.process,
(Ph_types.process * PintTypes.stochatime) * Ph_types.sortidx)
Hashtbl.t
type ph = Ph_types.process list * Ph_types.hits
type action = Hit of (Ph_types.process * Ph_types.process * int)
module ASet :
sig
type elt = action
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
end
val string_of_action : Ph_types.action -> string
val pintstring_of_action : Ph_types.action -> string
val string_of_actions : Ph_types.action list -> string
val hitter : Ph_types.action -> Ph_types.process
val target : Ph_types.action -> Ph_types.process
val bounce : Ph_types.action -> int
val bounce2 : Ph_types.action -> Ph_types.process
type state = Ph_types.sortidx PintTypes.SMap.t
val string_of_state : ?show_zero:bool -> Ph_types.state -> string
val state0 : Ph_types.process list -> Ph_types.state
val merge_states : Ph_types.state -> Ph_types.state -> Ph_types.state
val merge_state_with_ps :
Ph_types.state -> Ph_types.process list -> Ph_types.state
val state_value : Ph_types.state -> Ph_types.sort -> Ph_types.sortidx
val list_of_state : Ph_types.state -> Ph_types.process list
val procs_of_state : Ph_types.state -> Ph_types.PSet.t
val state_empty : Ph_types.state
type ctx = PintTypes.ISet.t PintTypes.SMap.t
val ctx_equal : Ph_types.ctx -> Ph_types.ctx -> bool
val ctx_empty : Ph_types.ctx
val ctx_sorts : Ph_types.ctx -> PintTypes.SSet.t
val ctx_get : Ph_types.sort -> Ph_types.ctx -> PintTypes.ISet.t
val ctx_safe_get : Ph_types.sort -> Ph_types.ctx -> PintTypes.ISet.t
val ctx_has_proc : Ph_types.process -> Ph_types.ctx -> bool
val ctx_add_proc : Ph_types.process -> Ph_types.ctx -> Ph_types.ctx
val ctx_rm_proc : Ph_types.process -> Ph_types.ctx -> Ph_types.ctx
val string_of_ctx : Ph_types.ctx -> string
val procs_of_ctx : Ph_types.ctx -> Ph_types.PSet.t
val procs_to_ctx : Ph_types.PSet.t -> Ph_types.ctx
val state_of_ctx : Ph_types.ctx -> Ph_types.state
val ctx_override_by_ctx : Ph_types.ctx -> Ph_types.ctx -> Ph_types.ctx
val ctx_override : Ph_types.ctx -> Ph_types.PSet.t -> Ph_types.ctx
val ctx_union : Ph_types.ctx -> Ph_types.ctx -> Ph_types.ctx
val ctx_union_state : Ph_types.ctx -> Ph_types.state -> Ph_types.ctx
val ctx_inter : Ph_types.ctx -> Ph_types.ctx -> Ph_types.ctx
val ctx_diff : Ph_types.ctx -> Ph_types.ctx -> Ph_types.ctx
val ctx_of_state : Ph_types.state -> Ph_types.ctx
val ph_sigma : Ph_types.ph -> Ph_types.sort list
type t_directive = {
mutable default_rate : float option;
mutable default_sa : int;
mutable sample : float;
}
val directive : Ph_types.t_directive
type objective = Ph_types.sort * Ph_types.sortidx * Ph_types.sortidx
module ObjSet :
sig
type elt = objective
type t
val empty : t
val is_empty : t -> bool
val mem : elt -> t -> bool
val add : elt -> t -> t
val singleton : elt -> t
val remove : elt -> t -> t
val union : t -> t -> t
val inter : t -> t -> t
val diff : t -> t -> t
val compare : t -> t -> int
val equal : t -> t -> bool
val subset : t -> t -> bool
val iter : (elt -> unit) -> t -> unit
val map : (elt -> elt) -> t -> t
val fold : (elt -> 'a -> 'a) -> t -> 'a -> 'a
val for_all : (elt -> bool) -> t -> bool
val exists : (elt -> bool) -> t -> bool
val filter : (elt -> bool) -> t -> t
val partition : (elt -> bool) -> t -> t * t
val cardinal : t -> int
val elements : t -> elt list
val min_elt : t -> elt
val max_elt : t -> elt
val choose : t -> elt
val split : elt -> t -> t * bool * t
val find : elt -> t -> elt
val of_list : elt list -> t
end
module ObjMap :
sig
type key = objective
type +'a t
val empty : 'a t
val is_empty : 'a t -> bool
val mem : key -> 'a t -> bool
val add : key -> 'a -> 'a t -> 'a t
val singleton : key -> 'a -> 'a t
val remove : key -> 'a t -> 'a t
val merge :
(key -> 'a option -> 'b option -> 'c option) -> 'a t -> 'b t -> 'c t
val union : (key -> 'a -> 'a -> 'a option) -> 'a t -> 'a t -> 'a t
val compare : ('a -> 'a -> int) -> 'a t -> 'a t -> int
val equal : ('a -> 'a -> bool) -> 'a t -> 'a t -> bool
val iter : (key -> 'a -> unit) -> 'a t -> unit
val fold : (key -> 'a -> 'b -> 'b) -> 'a t -> 'b -> 'b
val for_all : (key -> 'a -> bool) -> 'a t -> bool
val exists : (key -> 'a -> bool) -> 'a t -> bool
val filter : (key -> 'a -> bool) -> 'a t -> 'a t
val partition : (key -> 'a -> bool) -> 'a t -> 'a t * 'a t
val cardinal : 'a t -> int
val bindings : 'a t -> (key * 'a) list
val min_binding : 'a t -> key * 'a
val max_binding : 'a t -> key * 'a
val choose : 'a t -> key * 'a
val split : key -> 'a t -> 'a t * 'a option * 'a t
val find : key -> 'a t -> 'a
val map : ('a -> 'b) -> 'a t -> 'b t
val mapi : (key -> 'a -> 'b) -> 'a t -> 'b t
end
val string_of_obj : Ph_types.objective -> string
val obj_sort : Ph_types.objective -> Ph_types.sort
val obj_target : Ph_types.objective -> Ph_types.sortidx
val obj_bounce : Ph_types.objective -> Ph_types.sortidx
val obj_bounce_proc : Ph_types.objective -> Ph_types.process
val obj_reach : Ph_types.state -> Ph_types.process -> Ph_types.objective
type anostate = int list
type state_matching_t =
SM of (string list * Ph_types.anostate list)
| SM_Not of Ph_types.state_matching_t
| SM_And of (Ph_types.state_matching_t * Ph_types.state_matching_t)
| SM_Or of (Ph_types.state_matching_t * Ph_types.state_matching_t)
end