Big (bigraph.Bigraph.Big)

type t

The type of bigraphs.

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

val place : t -> Place.t

The place graph of a bigraph.

val link : t -> Link.t

The link graph of a bigraph.

type nodes_t = Nodes.t

The type of node collections.

val nodes : t -> nodes_t

The nodes of a bigraph.

val make : Nodes.t -> Place.t -> Link.t -> t

Build a bigraph starting from its components. Note, no validity check is performed.

type inter =

| Inter of int * Face.t
(*
Inter (i, n) creates an interface with ordinal i and name-face n.
*)

The type of interfaces.

val pp_inter : 
  Ppx_deriving_runtime.Format.formatter ->
  inter ->
  Ppx_deriving_runtime.unit

val show_inter : inter -> Ppx_deriving_runtime.string

val inter_to_yojson : inter -> Yojson.Safe.t

val inter_of_yojson : 
  Yojson.Safe.t ->
  inter Ppx_deriving_yojson_runtime.error_or

Exceptions

exception SHARING_ERROR

Raised when the composition in a sharing expression fails.

exception COMP_ERROR of inter * inter

Raised when the composition fails.

exception CTRL_ERROR of int * Face.t

Raised when a control's arity does not match a face's size. The first element is the arity, the second is the mismatching face.

exception ISO_ERROR of int * int

Raised when an isomorphism is not total. The first element is the expected domain size, the second is the actual number of mapped elements.

Functions on interfaces

val inter_equal : inter -> inter -> bool

Equality over interfaces.

val ord_of_inter : inter -> int

Compute the ordinal of an interface.

val face_of_inter : inter -> Face.t

Compute the face (i.e. name-set) of an interface.

Functions on bigraphs

val to_dot : t -> string -> string

to_dot b n computes the DOT string for bigraph b named n.

val inner : t -> inter

inner b computes the inner face of bigraph b.

val outer : t -> inter

outer b computes the outer face of bigraph b.

val apply : Iso.t -> t -> t

apply i b applies isomorphism i to bigraph b.

val eval : t -> Expr.env -> t

Evaluate control parameter expressions in the given environment.

val ground : t -> Expr.env -> string list -> t

Ground control parameter expressions that reference a name in the given list, within the given environment (see Ctrl.ground_exprs).

val placing : int list list -> int -> Face.t -> t

placing l r f computes a placing with r regions by parsing list l. The format of l is the same as the input for Place.parse_placing. The link graph is the identity over face f.

val size : t -> int

Compute the size of a bigraph as the number of nodes plus the number of edges (edges are counted with multiplicity).

Elementary bigraphs

val id : inter -> t

Identity over interface i.

val id_eps : t

The empty identity.

val merge : int -> t

Bigraph consisting of one region and n sites.

val split : int -> t

Bigraph consisting of one site and n regions.

val one : t

Elementary bigraph consisting of one region.

val zero : t

Elementary bigraph consisting of one site.

val sym : inter -> inter -> t

Symmetry on interfaces i and j.

val ion : Face.t -> Ctrl.t -> t

ion ns c computes an ion of control c. Its outer names are ns. No arity check is performed.

val ion_chk : Face.t -> Ctrl.t -> t

Same as Big.ion but with arity check.

raises CTRL_ERROR
when the set of names has size different than the arity of c.

val atom : Face.t -> Ctrl.t -> t

Same as Big.ion but without the site.

val atom_chk : Face.t -> Ctrl.t -> t

Same as Big.ion_chk but without the site.

raises CTRL_ERROR
when the set of names has size different than the arity of c.

val sub : inner:Face.t -> outer:Face.t -> t

sub inner outer computes a substitution where inner and outer are the inner and outer faces, respectively.

val closure : Face.t -> t

closure f computes the closure of interface f.

val intro : Face.t -> t

intro f computes an empty bigraph providing a fresh set of names f. This function is the dual of Big.closure.

Operations

val close : Face.t -> t -> t

close f b closes names in f of bigraph b. Names in the outer face of b but not in f are propagated by an implicit identity.

raises COMP_ERROR
if f contains names not present in the outer link face of b.

val comp : t -> t -> t

comp a b computes the composition of bigraphs a and b, $a \circ b$ using the algebraic notation.

raises COMP_ERROR
when the mediating interfaces do not match.

val comp_of_list : t list -> t

comp_of_list bs computes the composition of all the bigraphs in list bs.

raises COMP_ERROR
when the mediating interfaces do not match.

val comp_seq : start:int -> stop:int -> (int -> t) -> t

comp_seq ~start ~stop f computes the composition f(start) * ... * f(stop - 1).

raises COMP_ERROR
when the mediating interfaces do not match.

val nest : t -> t -> t

nest a b computes the bigraph resulting from nesting bigraph b in bigraph a. Names in the outer face of b that also appear in a are shared. Names in the outer face of b but not in a are propagated by an implicit identity.

raises COMP_ERROR
if composition cannot be performed.

val nest_of_list : t list -> t

nest_of_list bs computes the nesting of all the bigraphs in list bs.

raises COMP_ERROR
when the mediating interfaces do not match.

val par : t -> t -> t

par a b computes the merge product of bigraphs a and b, $a \mid b$ using the algebraic notation.

val par_of_list : t list -> t

par_of_list bs computes the merge product of all the bigraphs in list bs.

val par_seq : start:int -> stop:int -> (int -> t) -> t

par_seq ~start ~stop f computes the merge product f(start) | ... | f(stop - 1).

val ppar : t -> t -> t

ppar a b computes the parallel product of bigraphs a and b, $a \parallel b$ using the algebraic notation.

val ppar_of_list : t list -> t

ppar_of_list bs computes the parallel product of all the bigraphs in list bs.

val ppar_seq : start:int -> stop:int -> (int -> t) -> t

ppar_seq ~start ~stop f computes the parallel product f(start) || ... || f(stop - 1).

val rename : inner:Face.t -> outer:Face.t -> t -> t

rename ~inner ~outer b renames names in inner to names in outer. Outer names in b not in inner are propagated by an implicit identity.

raises COMP_ERROR
if inner contains names not present in the outer link face of b.

raises Link.NAMES_ALREADY_DEFINED
if outer shares names with the propagated names (i.e., names in the outer face of b but not in inner). For example, renaming inner={a,b} to outer={x} on a bigraph with outer names {a,b,c,x} fails because x is both a rename target and a propagated name.

val share : t -> t -> t -> t

share f psi g computes the bigraphs obtained by sharing bigraph f in bigraph g by using placing psi.

raises SHARING_ERROR
if psi is not a placing.

raises COMP_ERROR
if one composition cannot be performed.

val tens : t -> t -> t

tens a b computes the tensor product of bigraphs a and b, $a \otimes b$ using the algebraic notation.

raises Link.NAMES_ALREADY_DEFINED
when a and b have shared names.

val tens_of_list : t list -> t

tens_of_list bs computes the tensor product of all the bigraphs in list bs.

raises Link.NAMES_ALREADY_DEFINED
when two addends have shared names.

val tens_seq : start:int -> stop:int -> (int -> t) -> t

tens_seq ~start ~stop f computes the tensor product f(start) + ... + f(stop - 1).

raises Link.NAMES_ALREADY_DEFINED
when two addends have shared names.

Predicates

val is_id : t -> bool

is_id b returns true if bigraph b is an identity, false otherwise.

val is_plc : t -> bool

is_plc b returns true if bigraph b is a placing, false otherwise.

val is_wir : t -> bool

is_wir b returns true if bigraph b is a wiring, false otherwise.

val is_epi : t -> bool

is_epi b returns true if bigraph b is epimorphic, false otherwise. A bigraph is epimorphic if both its place graph and link graph are epimorphic. See Place.is_epi and Link.is_epi.

val is_mono : t -> bool

is_mono b returns true if bigraph b is monomorphic, false otherwise. A bigraph is monomorphic if both its place graph and link graph are monomorphic. See Place.is_mono and Link.is_mono.

val is_guard : t -> bool

is_guard b returns true if bigraph b is guarded, false otherwise. A bigraph is guarded if both its place graph and link graph are guarded. See Place.is_guard and Link.is_guard.

val is_solid : t -> bool

is_solid b returns true if bigraph b is solid, false otherwise. A bigraph is solid if it is epimorphic, monomorphic, and guarded. See Big.is_epi, Big.is_mono, and Big.is_guard.

val is_ground : t -> bool

is_ground b returns true if bigraph b is ground, false otherwise. A bigraph is ground if its place graph and link graph are both ground. See Place.is_ground and Link.is_ground.

Decompositions

val decomp : 
  target:t ->
  pattern:t ->
  i_n:Iso.t ->
  i_e:Iso.t ->
  Fun.t ->
  t * t * t

decomp t p i_n i_e f_e computes the decomposition of target t given pattern p, node isomorphism i_n and edge isomorphism i_e. The isomorphism are from p to t. The elements in the result are the context, the parameter and the identity of the decomposition. Argument f_e is a total function from links in the pattern to links in the target.

val rewrite : 
  (Iso.t * Iso.t * Fun.t) ->
  s:t ->
  r0:t ->
  r1:t ->
  ?decomp':(t * t * t) ->
  Fun.t option ->
  t

rewrite o ~s ~r0 ~r1 eta computes a bigraph obtained by replacing the occurrence of ~r0 (specified by occurrence o) in ~s with eta ~r1, where eta is a valid (no check performed) instantiation map.

When ?decomp' is provided, it is used as the precomputed decomposition (context, parameter, identity), avoiding recomputation.

raises Place.NOT_PRIME
when b is not prime decomposable.