Module type React_intf.MAKER

Functor building a concrete implementation of basic operations on rewrite rules.

Parameters

module _ : Solver.M
module R : R

Signature

type t = R.t

The type of reaction rules.

val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val to_yojson : t -> Yojson.Safe.t
val of_yojson : Yojson.Safe.t -> t Ppx_deriving_yojson_runtime.error_or
type label = R.label

The type of reaction rule labels.

val pp_label : Ppx_deriving_runtime.Format.formatter -> label -> Ppx_deriving_runtime.unit
val show_label : label -> Ppx_deriving_runtime.string
val label_to_yojson : label -> Yojson.Safe.t
val label_of_yojson : Yojson.Safe.t -> label Ppx_deriving_yojson_runtime.error_or
type react_error
exception NOT_VALID of react_error
val name : t -> string

Returns the name of a rewrite rule.

val lhs : t -> Big.t

Return the left-hand side of a rewrite rule.

val rhs : t -> Big.t

Return the right-hand side of a rewrite rule.

val conds : t -> AppCond.t list

Return application conditions for a rewrite rule.

val l : t -> label

Return the label of a rewrite rule.

val compare_label : label -> label -> int

The comparison function for labels.

val equal : t -> t -> bool

Equality for reaction rules

val map : t -> Fun.t option

Return the instantiation map of a rewrite rule.

val make : name:string -> lhs:Big.t -> rhs:Big.t -> ?conds:AppCond.t list -> ?cond_captures:string list -> label -> Fun.t option -> t

Create a new reaction rule. cond_captures names the LHS captures a factored rule's condition patterns reference (empty for every hand-written rule); at match time those captures are grounded into the condition patterns before the containment check.

val is_valid : t -> bool

Validity check.

val is_valid_exn : t -> bool

Same as is_valid but an exception is raised instead of returning false.

  • raises NOT_VALID

    when the reaction rule is not valid.

val is_valid_err : t -> (bool, react_error) Stdlib.result

Same as is_valid_exn but returns the exception as Error e or Ok true.

val string_of_react_err : react_error -> string

Convert to string the output of the validity check.

val is_enabled : Big.t -> t -> bool

is_enabled b r checks if rewrite rule r can be applied to bigraph b.

val filter_iso : (Big.t * label * t list) list -> (Big.t * label * t list) list

Merge isomorphic occurrences into a single representative, combining labels where appropriate.

val apply : Big.t -> t list -> Big.t option

Apply a list of reaction rules in sequence. Non-enabled rules are ignored.

val fix : Big.t -> t list -> Big.t * int

fix b r_list applies the rewrite rules in list r_list to bigraph b until a fixed point b' is reached. The result is fixed point b' and the number of rewriting steps performed. Note, b is returned when no rewriting is performed.

val step : Big.t -> t list -> (Big.t * label * t list) list * int

All the possible evolutions in one step. Total number of occurrences also returned.

val random_step : Stdlib.Random.State.t -> Big.t -> t list -> (Big.t * label * t list) option * int

Random step.

val random_step_forced : Stdlib.Random.State.t -> Big.t -> t list -> t -> (Big.t * label * t list) option * int

Random step conditioned on rule firing: the successor is drawn from the rule's occurrences and the SBRS sojourn at the exit rate of the full class rules. The rule's occurrence count is returned.

val select_path : unit -> unit

Resolve all internal function refs to the chosen implementation based on solver type. Call once after rule compilation, before any matching operations. Eliminates per-step conditional branches.

val set_wildcard_threshold : int -> unit

Set the group-size threshold for wildcard structural matching. Groups with fewer than n rules use direct per-rule matching; larger groups use wildcard structural matching (one solve + partition). Default is 3. Set to 1 to force wildcard for all groups; set very high to disable wildcard entirely. Call before select_path.