Module Bigraph.Rs_intf

module type L = sig ... end

Input signature of functor Rs.Make representing the type of computation limit (i.e. discrete or dense time).

type rs_type =
  1. | BRS
    (*

    Bigraphical Reactive Systems

    *)
  2. | PBRS
    (*

    Probabilistic Bigraphical Reactive Systems

    *)
  3. | SBRS
    (*

    Stochastic Bigraphical Reactive Systems

    *)
  4. | ABRS
    (*

    Action (Nondeterministic) Bigraphical Reactive Systems

    *)

Type for the kind of reactive system.

type stats = {
  1. time : float;
    (*

    Build time

    *)
  2. states : int;
    (*

    Number of states

    *)
  3. trans : int;
    (*

    Number of transitions

    *)
  4. occs : int;
    (*

    Number of occurrences

    *)
  5. internal : Stdlib.Hashtbl.statistics;
    (*

    Internal storage statistics from state deduplication

    *)
  6. mean_size : float;
    (*

    States mean size

    *)
  7. mean_size_match : float;
    (*

    Matches mean size

    *)
}

The type of execution and rewrite statistics.

type pred_entry = {
  1. base : Predicate.t * Big.t;
    (*

    Checked against every state.

    *)
  2. variants : (Predicate.t * Big.t) list;
    (*

    Per-value patterns, checked only where the base occurs.

    *)
}

Predicate entry for RS.bfs and RS.sim. base is checked against every state. For a plain predicate variants is empty and the base's predicate is recorded for every matching state. For a factored BRS family base is the single bracket-guarded pattern and variants holds one named concrete pattern per family member: each variant is checked only for the states where base occurs, and its predicate is what the transition system records, so the labels hold one entry per member value.

module type RS = sig ... end

Output signature of functor Rs.Make.

module type MAKER = functor (_ : Solver.M) -> functor (R : React.T) -> functor (_ : Priority.P with type r_t := R.t and type r_label := R.label) -> functor (L : L with type label := R.label) -> functor (G : Ts.S with type label := R.label) -> RS with type react = R.t and type label = R.label and type graph = G.t and type limit = L.t

Functor building a concrete implementation of a reactive system.

module type Intf = sig ... end