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