sig
type env = {
ph : Ph_types.ph;
ctx : Ph_types.ctx;
pl : Ph_types.process list;
bs_cache : Ph_bounce_seq.bs_cache;
concrete : Ph_glc._concrete_ph;
}
val init_env :
Ph_types.ph -> Ph_types.ctx -> Ph_types.process list -> Ph_reach.env
type refGLC = NullGLC | GLC of Ph_glc.glc
val local_reachability :
?saveGLC:Ph_reach.refGLC Pervasives.ref ->
Ph_reach.env -> PintTypes.ternary
val coop_priority_ua_glc_setup : Ph_glc.glc_setup
val coop_priority_reachability :
?saveGLC:Ph_reach.refGLC Pervasives.ref ->
Ph_reach.env -> PintTypes.ternary
val color_nodes_connected_to_trivial_sols : #Ph_glc.glc -> Ph_glc.NodeSet.t
val get_Sols :
Ph_reach.env ->
Ph_types.objective -> (Ph_types.PSet.t * PintTypes.ISet.t) list
val bot_trimmed_cwA : Ph_reach.env -> #Ph_glc.glc -> Ph_glc.glc
val top_trimmed_cwA : Ph_reach.env -> #Ph_glc.graph -> unit
val unordered_over_approx :
Ph_reach.env ->
(Ph_types.objective -> (Ph_types.PSet.t * PintTypes.ISet.t) list) ->
bool * (Ph_types.objective -> (Ph_types.PSet.t * PintTypes.ISet.t) list)
end