sig
  type react
  type p_class = P_class of Brs.react list | P_rclass of Brs.react list
  type graph
  type occ = Big.bg
  type limit = int
  val typ : Rs.t
  val string_of_react : Brs.react -> string
  val parse_react_unsafe :
    lhs:Big.bg -> rhs:Big.bg -> Fun.t option -> Brs.react
  val parse_react :
    lhs:Big.bg -> rhs:Big.bg -> Fun.t option -> Brs.react option
  val lhs_of_react : Brs.react -> Big.bg
  val rhs_of_react : Brs.react -> Big.bg
  val string_of_limit : Brs.limit -> string
  val is_valid_react : Brs.react -> bool
  type react_error
  exception NOT_VALID of Brs.react_error
  val is_valid_react_exn : Brs.react -> bool
  val string_of_react_err : Brs.react_error -> string
  val is_valid_priority : Brs.p_class -> bool
  val is_valid_priority_list : Brs.p_class list -> bool
  val cardinal : Brs.p_class list -> int
  val apply : Big.bg -> Brs.react list -> Big.bg option
  val step : Big.bg -> Brs.react list -> Brs.occ list * int
  val random_step : Big.bg -> Brs.react list -> Brs.occ option * int
  val fix : Big.bg -> Brs.react list -> Big.bg * int
  val rewrite : Big.bg -> Brs.p_class list -> Big.bg * int
  exception MAX of Brs.graph * Stats.t
  val bfs :
    s0:Big.bg ->
    priorities:Brs.p_class list ->
    predicates:(string * Big.bg) list ->
    max:int -> iter_f:(int -> Big.bg -> unit) -> Brs.graph * Stats.t
  exception DEADLOCK of Brs.graph * Stats.t * int
  exception LIMIT of Brs.graph * Stats.t
  val sim :
    s0:Big.bg ->
    priorities:Brs.p_class list ->
    predicates:(string * Big.bg) list ->
    init_size:int ->
    stop:Brs.limit -> iter_f:(int -> Big.bg -> unit) -> Brs.graph * Stats.t
  val to_prism : Brs.graph -> string
  val to_dot : Brs.graph -> name:string -> string
  val to_lab : Brs.graph -> string
  val iter_states : f:(int -> Big.bg -> unit) -> Brs.graph -> unit
  val write_dot : Brs.graph -> name:string -> path:string -> int
  val write_lab : Brs.graph -> name:string -> path:string -> int
  val write_prism : Brs.graph -> name:string -> path:string -> int
  val write_svg : Brs.graph -> name:string -> path:string -> int
  val write_json : Brs.graph -> name:string -> path:string -> int
end