Module Bigraph.Link

Faces

type name =
| Name of string

The type of names.

module Face : sig ... end

This module provides set operations for faces.

Ports

module Ports : sig ... end

This module implements multisets of nodes as maps.

type edg = {
i : Face.t;

Inner face

o : Face.t;

Outer face

p : Ports.t;

Set of ports

}

The type of edges.

module Lg : sig ... end

This module provides set operations for link graphs.

val parse_face : string list -> Face.t

parse_face ns computes a face starting from list of string names ns.

val string_of_face : Face.t -> string

string_of_face f computes the string representation of face f.

val pp_face : Stdlib.Format.formatter -> Face.t -> unit

Pretty printer.

val to_string : Lg.t -> string

to_string l computes the string representation of link graph l.

val pp : Stdlib.Format.formatter -> Lg.t -> unit

Pretty printer.

val of_string : string -> Lg.t

Opposite of Link.to_string.

raises Invalid_argument

if the input cannot be parsed.

val parse : links:string list -> nodes:string -> Lg.t * Nodes.t

Parse a list of strings.

val get_dot : Lg.t -> string * string * string * string

get_dot l computes a four-elements tuple encoding the dot representation of link graph l. The first two elements represent inner and outer names shape declarations. The third element represent the hyperedges shape declarations. The fourth element specifies the adjacency matrix.

val inner : Lg.t -> Face.t

inner l computes the inner face of link graph l.

val outer : Lg.t -> Face.t

outer l computes the outer face of link graph l.

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

apply i l computes a link graph obtained by applying isomorphism i to l.

val elementary_sub : inner:Face.t -> outer:Face.t -> Lg.t

elementary_sub inner outer computes a substitution consisting of a single edge in which inner and outer are the inner and outer face, respectively.

val elementary_ion : Face.t -> Lg.t

elementary_ion f computes an elementary ion with outer face f.

val elementary_id : Face.t -> Lg.t

elementary_id f computes the identity over face f, i.e. one edge for each name in f.

val id_empty : Lg.t

id_empty is the empty link graph.

exception NAMES_ALREADY_DEFINED of Face.t * Face.t

Raised when the tensor product between two incompatible link graphs cannot be performed. The first element is the set of inner common names while the second is the set of outer common names.

exception FACES_MISMATCH of Face.t * Face.t

Raised when a composition between two incompatible link graphs cannot be performed.

val tens : Lg.t -> Lg.t -> int -> Lg.t

tens a b n computes the tensor product of link graphs a and b. Argument n is the number of nodes of a.

raises NAMES_ALREADY_DEFINED

when there are shared names.

val ppar : Lg.t -> Lg.t -> int -> Lg.t

ppar a b n computes the parallel composition of link graphs a and b. n is the number of nodes of a.

val comp : Lg.t -> Lg.t -> int -> Lg.t

comp a b n computes the composition of link graphs a and b. Argument n is the number of nodes of a.

raises FACES_MISMATCH

when names in the mediating interfaces differ.

Predicates

val is_id : Lg.t -> bool

is_id l is true if link graph l is an identity, false otherwise.

val is_mono : Lg.t -> bool

is_mono l is true if link graph l is monomorphic, false otherwise. A link graph is monomorphic if every edge has at most one inner name.

val is_epi : Lg.t -> bool

is_epi l is true if link graph l is epimorphic, false otherwise. A link graph is epimorphic if no outer name is idle.

val is_ground : Lg.t -> bool

is_ground l is true if link graph l has no inner names, false otherwise.

val is_guard : Lg.t -> bool

is_guard l is true if no edges in link graph l have both inner and outer names, false otherwise.

val max_ports : Lg.t -> int

Compute the maximum number of ports in one edge of a link graph.

val cardinal_ports : Lg.t -> int list

Compute a sorted list with the cardinalities of the port sets.

val closed_edges : Lg.t -> int

Compute the number of closed edges.

val closed_edges_iso : Lg.t -> Lg.t * Iso.t

closed_edges_iso l computes the set of closed edges of link graph l. The computed isomorphism maps edge indices of the new link graph to indices of edges in l.

Decompositions

val norm : Lg.t -> Lg.t * Lg.t

Normalise link graph l as follows: l = omega o l' where omega is a linking and l' is the same as l but with all links open.

val decomp : target:Lg.t -> pattern:Lg.t -> i_e:Iso.t -> i_c:Iso.t -> i_d:Iso.t -> Fun.t -> Lg.t * Lg.t * Lg.t

decomp target pattern i_e i_c i_d f_e computes the decomposition of target given pattern, iso i_e, and isos from nodes in t to nodes of c and d, respectively. Argument f_e is a total function from links in the pattern to links in the target. Pattern p is assumed epi and mono and i_e is from edges in p to edges in t. Isos i_c and i_d are obtained by Place.decomp. The results are link graph c, d and id.

val prime_components : Lg.t -> Iso.t list -> Lg.t list

Compute the prime components of a link graph. See Place.decomp.