Module Place

module Place: sig .. end
This module provides operations on place graphs.
Author(s): Michele Sevegnani

type bmatrix 
The type of boolean matrices.
type pg = {
   r : int; (*
Number of regions
*)
   n : int; (*
Number of nodes
*)
   s : int; (*
Number of sites
*)
   rn : bmatrix; (*
Boolean adjacency matrix regions X nodes
*)
   rs : bmatrix; (*
Boolean adjacency matrix regions X sites
*)
   nn : bmatrix; (*
Boolean adjacency matrix nodes X nodes
*)
   ns : bmatrix; (*
Boolean adjacency matrix nodes X sites
*)
}
The type of place graphs.
val to_string : pg -> string
to_string p returns a string representation of place graph p.
val json_of_place : pg -> string
Return a JSON representation of a place graph. Example:

"place_graph": {
       "regions": 2,
       "nodes": 3,
       "sites": 1,
       "dag": [
         {
           "source": 1,
           "target": 2
         },
         {
           "source": 0,
           "target": 2
         }
       ]
     }

val json_of_place_f : pg -> Base.JSON.json_node
val edges : pg -> int
Compute the number of edges in the DAG.
val parse : regions:int -> nodes:int -> sites:int -> string list -> pg
parse r n s lines computes a place graph with r regions, n nodes and s sites. Each element in lines is a string in the same format of the output of Place.to_string.
Raises Invalid_argument if the arguments do not specify a valid place graph.
val get_dot : pg -> string * string * string * string
get_dot p returns three strings expressing place graph p in dot format. The first two elements encode regions and sites shapes, the third encodes the node ranks and the fourth represents the adjacency matrix.
val apply : Iso.t -> pg -> pg
Apply an isomorphism
val parse_placing : int list list -> int -> pg
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 : pg -> IntSet.t
Compute the set of nodes with no children.
val orphans : pg -> IntSet.t
Compute the set of nodes with no parents.

Elementary place graphs


val elementary_id : int -> pg
elementary_id m computes a place graph in the form of an identity of m.
val id0 : pg
id0 is the empty place graph.
val elementary_merge : int -> pg
elementary_merge m computes an elementary place graph formed by one region containing m sites.
val elementary_split : int -> pg
elementary_split m computes an elementary place graph formed by one site shared by m regions.
val zero : pg
zero is the place graph formed by an orphaned site.
val one : pg
one is the place graph formed by an idle region.
val elementary_sym : int -> int -> pg
elementary_sym m n computes an place graph consisting of a symmetry between m and n.
val elementary_ion : pg
An ion.

Comparison


val equal_placing : pg -> pg -> 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 : pg -> pg -> int
compare_placing a b compares placings a and b.
val equal_bmatrix : bmatrix -> bmatrix -> bool
Equality for Place.bmatrix.
val compare_bmatrix : bmatrix -> bmatrix -> int
Comparison for Place.bmatrix.
val entries_bmatrix : bmatrix -> int
Return the number of edges in a Place.bmatrix.

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 : pg -> pg -> pg
tens p0 p1 returns the tensor product of place graphs p0 and p1.
val tens_of_list : pg list -> pg
Same as Place.tens but on a list of place graphs.
val comp : pg -> pg -> pg
comp p0 p1 returns the composition of place graphs p0 and p1.
Raises COMP_ERROR when mediating interfaces mismatch.

Predicates


val is_id : pg -> bool
is_id p returns true if place graph p is an identity, false otherwise.
val is_plc : pg -> bool
Test for the absence of nodes.
val is_ground : pg -> bool
is_ground p is true if place graph p has no sites, false otherwise.
val is_mono : pg -> 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 : pg -> bool
is_epi p is true if place graph p is epimorphic, false otherwise. A place graph is epimorphic if no root is idle and no two roots are partners.
val is_guard : pg -> 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.

Decompositions


val decomp : target:pg ->
pattern:pg -> Iso.t -> pg * pg * pg * 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.
exception NOT_PRIME
Raised when a place graph cannot be decomposed into prime components. The first element is a set of shared nodes and the second a set of shared sites.
val prime_components : pg -> (pg * 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.
Raises NOT_PRIME when some region is shared
val decomp_d : pg -> int -> pg * pg * Iso.t * Iso.t
Compute the decomposition D = D' X D_id.
Raises NOT_PRIME when some region is shared

Matching constraints


exception NOT_TOTAL
Raised when a node in the pattern cannot be matched to any node in the target.
val match_list : target:pg ->
pattern:pg ->
n_t:Nodes.t ->
n_p:Nodes.t ->
(Cnf.clause * Cnf.b_clause list) list * Cnf.clause list * IntSet.t
match_list t p n_t n_p computes constraints to match edges in pattern p with compatible edges in target t. n_t and n_p are the node sets of t and p, respectively.
Raises NOT_TOTAL when there are nodes in the pattern that cannot be matched.
val match_leaves : target:pg ->
pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t
match_leaves t p n_t n_p computes constraints to match the leaves (i.e. nodes without children) in p with those in t. n_t and n_p are defined as in Place.match_list.
Raises NOT_TOTAL when there are leaves in the pattern that cannot be matched.
val match_orphans : target:pg ->
pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t
Dual of Place.match_leaves.
Raises NOT_TOTAL when there are orphans in the pattern that cannot be matched.
val match_regions : target:pg ->
pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t
Compute constraints to match regions. Arguments are as in Place.match_list. Only controls and degrees are checked.
val match_sites : target:pg ->
pattern:pg -> n_t:Nodes.t -> n_p:Nodes.t -> Cnf.clause list * IntSet.t
Dual of Place.match_regions.
val match_trans : target:pg -> pattern:pg -> Cnf.clause list
Compute constraints to block matches between unconnected pairs of nodes with sites and nodes with regions.
val check_match : target:pg -> pattern:pg -> bmatrix -> Iso.t -> bool
check_match t p trans iso checks if iso from p to t is a valid match.
val match_region_nodes : pg -> pg -> Nodes.t -> Nodes.t -> Cnf.clause list * IntSet.t
Compute constraints for equality: regions must have children with the same controls.
val match_nodes_sites : pg -> pg -> Nodes.t -> Nodes.t -> Cnf.clause list * IntSet.t
Dual of Place.match_region_nodes.
val match_list_eq : pg ->
pg ->
Nodes.t ->
Nodes.t -> (Cnf.clause * Cnf.b_clause list) list * Cnf.clause list * IntSet.t
Compute constraints for equality. Similar to Place.match_list.
val deg_regions : pg -> int list
Compute the outer degree of the regions of a place graph.
val deg_sites : pg -> int list
Compute the inner degree of the sites of a place graph.
val trans : pg -> bmatrix
Compute the transitive closure of the nodes X nodes matrix of a place graph.