Module Bigraph.Place

Operations on place graphs.

type m = Sparse.t

The type of boolean matrices.

val pp_m : Ppx_deriving_runtime.Format.formatter -> m -> Ppx_deriving_runtime.unit
val show_m : m -> Ppx_deriving_runtime.string
val m_to_yojson : m -> Yojson.Safe.t
val m_of_yojson : Yojson.Safe.t -> m Ppx_deriving_yojson_runtime.error_or
type t

The type of place graphs.

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 outer : t -> int

The number of regions.

val inner : t -> int

The number of sites.

val nodes : t -> int

The number of nodes.

val rn : t -> m

The region-to-node adjacency matrix.

val rs : t -> m

The region-to-site adjacency matrix.

val nn : t -> m

The node-to-node adjacency matrix.

val ns : t -> m

The node-to-site adjacency matrix.

val edges : m -> (int * int) list

Computes the representation of a boolean matrix as a list of edges.

val size : t -> int

Compute the number of edges in the DAG.

val to_dot : t -> string * string * string * string

to_dot p returns four strings expressing place graph p in DOT format. The first two elements encode region and site shapes, the third encodes node ranks, and the fourth represents the adjacency matrix.

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

Apply an isomorphism to a place graph.

val parse_placing : int list list -> int -> t

parse_placing l r returns the placing with r regions defined by list l in which each element is a site's parent set.

val leaves : t -> IntSet.t

Compute the set of nodes with no children.

val orphans : t -> IntSet.t

Compute the set of nodes with no parents.

Elementary place graphs

val elementary_id : int -> t

elementary_id m computes a place graph in the form of an identity of m.

val id0 : t

id0 is the empty place graph.

val elementary_merge : int -> t

elementary_merge m computes an elementary place graph formed by one region containing m sites.

val elementary_split : int -> t

elementary_split m computes an elementary place graph formed by one site shared by m regions.

val zero : t

zero is the place graph formed by an orphaned site.

val one : t

one is the place graph formed by an idle region.

val elementary_sym : int -> int -> t

elementary_sym m n computes a place graph consisting of a symmetry between m and n.

val elementary_ion : t

The elementary ion: one region containing one site.

Comparison

val equal_placing : t -> t -> bool

equal_placing a b returns true if placings a and b are equal. Inputs are assumed to be valid placing. No check is performed.

val compare_placing : t -> t -> int

compare_placing a b compares placings a and b.

Operations

exception COMP_ERROR of int * int

Raised when a composition between two incompatible place graphs is attempted. The two integers are the number of sites and regions involved in the composition, respectively.

val tens : t -> t -> t

tens p0 p1 returns the tensor product of place graphs p0 and p1.

val tens_of_list : t list -> t

Same as tens but on a list of place graphs.

val comp : t -> t -> t

comp p0 p1 returns the composition of place graphs p0 and p1.

  • raises COMP_ERROR

    when mediating interfaces mismatch.

Predicates

val is_id : t -> bool

is_id p returns true if place graph p is an identity, false otherwise.

val is_plc : t -> bool

Test for the absence of nodes.

val is_ground : t -> bool

is_ground p is true if place graph p has no sites, false otherwise.

val is_mono : t -> bool

is_mono p is true if place graph p is monomorphic, false otherwise. A place graph is monomorphic if no two sites are siblings and no site is an orphan.

val is_epi : t -> bool

is_epi p is true if place graph p is epimorphic, false otherwise. A place graph is epimorphic if no region is idle and no two regions are partners.

val is_guard : t -> bool

is_guard p is true if place graph p is guarded, false otherwise. A place graph is guarded if no region has sites as children.

val deg_regions : t -> int list

Invariants

Out-degree of roots, in order.

val deg_sites : t -> int list

In-degree of sites, in order.

val deg_seq : t -> (int * int) list

In and out degrees of nodes, in non-decreasing order.

Decompositions

val decomp : target:t -> pattern:t -> Iso.t -> t * t * t * Iso.t * Iso.t

decomp t p i computes the decomposition of target t given pattern p and node isomorphism i from p to t. Pattern p is assumed epi and mono. The result tuple (c, id, d, iso_c, iso_d) is formed by context c, identity id, parameter d, and nodes in c and d expressed as rows of t. The decomposition is with respect to the minimal parameter.

exception NOT_PRIME

Raised when a place graph cannot be decomposed into prime components.

val prime_components : t -> (t * Iso.t) list

Compute the prime components (i.e. place graphs with one region) of a place graph. The original node numbering is returned in the form of an isomorphism.

val decomp_d : t -> int -> t * t * Iso.t * Iso.t

Compute the decomposition D = D' X D_id.

val trans : t -> m

Compute or retrieve the transitive closure of the nodes X nodes matrix of a place graph.

val partition_nodes : t -> IntSet.t list

Compute the set of descendants for each region.

val partition_nodes_exn : m -> t -> IntSet.t list

Compute the set of descendants for each region, given the transitive closure explicitly. Avoids recomputing it when the caller already has it.