Tutorial

Building bigraphs

A bigraph has two components: a place graph that describes nesting structure, and a link graph that describes connectivity. The library provides combinators for constructing bigraphs from elementary building blocks.

Elementary bigraphs

Every bigraph is composed from these primitives:

• Big.id_eps -- the empty identity (no regions, no sites).
• Big.one -- a single idle region (1).
• Big.zero -- a single orphan site (0).
• Big.ion face ctrl -- an ion: one region containing one site, with an entity of control ctrl and outer names face.
• Big.id inter -- the identity over interface inter.
• Big.merge n -- one region containing n sites.
• Big.split n -- one site shared by n regions.
• Big.atom face ctrl -- like Big.ion but without the site.
• Big.sub ~inner ~outer -- a substitution (wiring) from inner to outer.

# Ctrl.make "A" 1;;
- : Ctrl.t = <abstr>
# Big.ion (Face.make [ "a" ]) (Ctrl.make "A" 1);;
- : Big.t = <abstr>
# Big.id_eps;;
- : Big.t = <abstr>
# Big.one;;
- : Big.t = <abstr>

Operations

The core combinators are:

• Big.nest a b -- nesting (a.b). Places b inside a.
• Big.par a b -- merge product (a \mid b). Places a and b as siblings in the same region, merging common names.
• Big.ppar a b -- parallel product (a \parallel b). Places a and b in separate regions, sharing common names.
• Big.tens a b -- tensor product (a \otimes b). Places a and b in separate regions without sharing names.
• Big.comp a b -- composition (a \circ b). Inserts b's regions into a's sites, merging common names.
• Big.share f psi g -- sharing. Places f in g using the placing psi.

We build two ions and combine them with different operations:

# let ion_a = Big.ion (Face.make [ "a" ]) (Ctrl.make "A" 1);;
val ion_a : Big.t = <abstr>
# let ion_b = Big.ion Face.empty (Ctrl.make "B" 0);;
val ion_b : Big.t = <abstr>
# Big.nest ion_a Big.one;;
- : Big.t = <abstr>
# Big.nest ion_b Big.one;;
- : Big.t = <abstr>
# Big.par (Big.nest ion_a Big.one) (Big.nest ion_b Big.one);;
- : Big.t = <abstr>
# Big.tens (Big.nest ion_a Big.one) (Big.nest ion_b Big.one);;
- : Big.t = <abstr>

Composition requires matching interfaces. The mediating interface is described by an ordinal (number of sites) and a face (set of names):

# let f = Face.make [ "x" ];;
val f : Face.t = <abstr>
# let id_f = Big.id (Big.Inter (1, f));;
val id_f : Big.t = <abstr>
# Big.comp id_f (Big.nest (Big.ion f (Ctrl.make "M" 0)) Big.one);;
- : Big.t = <abstr>

A running example

We now build a more realistic bigraph representing an actor (\mathsf{A}) ready to send a message (\mathsf{M}). The actor has a sender (\mathsf{Snd}), a receiver (\mathsf{Rcv}), and a function to execute (\mathsf{Fun}). The message carries two links: an address (a) and a value (v_a).

It is built as follows:

# open Bigraph;;
# let b =
    Big.nest
      (Big.ion (Face.make [ "a" ]) (Ctrl.make "A" 1))
      (Big.nest
         (Big.ion Face.empty (Ctrl.make "Snd" 0))
         (Big.par
            (Big.nest
               (Big.ion (Face.make [ "a"; "v_a" ]) (Ctrl.make "M" 2))
               Big.one)
            (Big.nest
               (Big.ion Face.empty (Ctrl.make "Rcv" 0))
               (Big.nest (Big.ion Face.empty (Ctrl.make "Fun" 0)) Big.one))));;
val b : Big.t = <abstr>

Inspecting bigraphs

The Big.show function prints a human-readable representation:

# print_endline (Big.show b);;
{(0, A), (1, Snd), (2, M), (3, Rcv), (4, Fun)}
1 5 0
{(0, {0}), (1, {1}), (2, {2, 3}), (4, {4})}
{({}, {a}, {(0, 1), (2, 1)}), ({}, {v_a}, {(2, 1)})}
- : unit = ()

The first line lists nodes with their controls. The second line gives the number of regions, nodes, and sites. The third line is the place graph as an adjacency list. The final line is the link graph (hyperedges and ports).

Structural predicates test properties of a bigraph:

# Big.is_ground b;;
- : bool = true
# Big.is_solid b;;
- : bool = true
# Big.is_mono b;;
- : bool = true
# Big.is_epi b;;
- : bool = true

Pattern matching

The library includes a matching engine powered by external solvers. It can check occurrence, find matches, and test isomorphism.

Solvers

Choose a solver and build the matching engine. MiniCARD is the default, supporting cardinality constraints for efficient matching:

# module S = Solver.Make_SAT (Solver.MC);;
module S : Solver.M

Target and pattern

The following state bigraph s0 contains a server with two clients and an idle entity. The clients share a link named ch:

# let s0 =
    Big.nest
      (Big.ion (Face.make [ "ch" ]) (Ctrl.make "Server" 1))
      (Big.par
         (Big.nest (Big.ion (Face.make [ "ch" ]) (Ctrl.make "Client" 1)) Big.one)
         (Big.par
            (Big.nest (Big.ion (Face.make [ "ch" ]) (Ctrl.make "Client" 1)) Big.one)
            (Big.nest (Big.ion Face.empty (Ctrl.make "Idle" 0)) Big.one)));;
val s0 : Big.t = <abstr>
# let pattern =
    Big.ion (Face.make [ "ch" ]) (Ctrl.make "Client" 1);;
val pattern : Big.t = <abstr>

Checking occurrence

Test whether a pattern occurs in a target:

# S.occurs ~target:s0 ~pattern:pattern;;
- : bool = true

Finding matches

Retrieve a single match or all matches. S.occurrence returns the first match found; S.occurrences returns all matching occurrences as a list. Since s0 contains two clients, there are two matches:

# match S.occurrence ~target:s0 ~pattern:pattern ~param_filter:S.param_filter_none with
    | Some occ -> print_endline (Solver.show_occ occ)
    | None -> print_endline "no match";;
{nodes = {(0, 2)}; edges = {}; hyper_edges = {(0, 0)}}
- : unit = ()
# List.iter (fun occ -> print_endline (Solver.show_occ occ))
    (S.occurrences ~target:s0 ~pattern:pattern ~rname:"" ~param_filter:S.param_filter_none);;
{nodes = {(0, 1)}; edges = {}; hyper_edges = {(0, 0)}}
{nodes = {(0, 2)}; edges = {}; hyper_edges = {(0, 0)}}
- : unit = ()

Each occurrence maps pattern nodes to target nodes, pattern edges to target edges, and pattern hyperedges to target hyperedges. The two matches map the pattern node to different target nodes (1 and 2 respectively).

Isomorphism

Test whether two bigraphs are isomorphic:

# S.equal s0 (Big.comp (Big.id (Big.outer s0)) s0);;
- : bool = true

Reaction rules

Reaction rules describe how bigraphs evolve. Each rule has a left-hand side (pattern), a right-hand side (result), and optionally an instantiation map and application conditions.

Defining rules

Instantiate the Brs functor with a solver, then create rules:

# module R = Brs.Make (S);;
module R : Brs_intf.MAKER with module S := Solver.Make_SAT(Solver.MC)
# let rdx =
    Big.ion (Face.make [ "ch" ]) (Ctrl.make "Client" 1);;
val rdx : Big.t = <abstr>
# let rct =
    Big.ion (Face.make [ "ch" ]) (Ctrl.make "Active" 0);;
val rct : Big.t = <abstr>
# let rule =
    R.parse_react_unsafe ~name:"activate" ~lhs:rdx ~rhs:rct
      () (Some (Fun.of_list [ (0, 0) ]));;
val rule : R.react = <abstr>

The rule activate rewrites a Client entity to an Active entity. Both are ions (one region, one site), so their outer and inner interfaces match. The Client entity has arity 1 and carries an open link ch, while Active has arity 0. The instantiation map Fun.of_list (0, 0) maps the right-hand side's single site back to the left-hand side's site, so any content nested inside the matched Client is preserved.

Checking validity

Validate a rule before use:

# R.is_valid_react rule;;
- : bool = true

Computing one step

Find all states reachable in one rewriting step:

# let (stepped, total) = R.step s0 [ rule ];;
val stepped : (Big.t * unit * R.react list) list = <abstr>
val total : int = 2
# print_endline ("reachable states: " ^ string_of_int (List.length stepped));;
reachable states: 1
- : unit = ()

There are two Client entities in s0, so the rule matches twice (total occurrences: 2). However, both matches lead to the same bigraph up to isomorphism, so only one unique state is reachable.

Apply a single rule (first match found, then stops):

# R.apply s0 [ rule ];;
- : Big.t option = Some <abstr>

Reduce to a fixed point (for reducing priority classes):

# R.fix s0 [ rule ];;
- : Big.t * int = ((...), 2)

The result is the fixed-point bigraph and the number of rewriting steps. Both clients were activated, requiring two steps.

Reactive systems

The library supports four kinds of reactive system, each built by instantiating a functor with a solver:

• Brs -- standard bigraphical reactive systems.
• Pbrs -- probabilistic reactive systems (weighted rules).
• Sbrs -- stochastic reactive systems (rate-annotated rules).
• Abrs -- action reactive systems (MDP semantics).

Computing a transition system

Build a system and explore its state space with breadth-first search:

# let pc = R.P_class [ rule ];;
# let (ts, stats) =
    try R.bfs ~s0:s0 ~priorities:[pc] ~predicates:[]
          ~max:50 (fun _ _ -> ())
    with R.MAX (g, s) -> (g, s);;

The search returns the transition system graph and statistics (build time, number of states, transitions, occurrences).

Probabilistic rules

Probabilistic rules carry a weight. Weights are normalised at runtime:

# module WP = Pbrs.Make (S);;
# let wr =
    WP.parse_react_unsafe ~name:"tick" ~lhs:rdx ~rhs:rct
      7.0
      (Some (Fun.of_list [ (0, 0) ]));;

If two enabled rules have weights 7 and 3, the transition probabilities are 0.7 and 0.3 respectively.

Stochastic rules

Stochastic rules carry a continuous rate:

# module WS = Sbrs.Make (S);;
# let sr =
    WS.parse_react_unsafe ~name:"decay" ~lhs:rdx ~rhs:rct
      1.0
      (Some (Fun.of_list [ (0, 0) ]));;

The exit rate of a state is the sum of the rates of all enabled occurrences.

JSON serialisation

All types derive JSON encoders and decoders. Here we serialise the actor bigraph b and parse it back:

# print_endline (Big.to_yojson b |> Yojson.Safe.pretty_to_string);;
{
  "place_graph": {
    "num_regions": 1,
    "num_nodes": 5,
    "num_sites": 0,
    "rn": { "r": 1, "c": 5, "r_major": [ [ 0, [ 0 ] ] ] },
    "rs": { "r": 1, "c": 0, "r_major": [] },
    "nn": {
      "r": 5,
      "c": 5,
      "r_major": [ [ 0, [ 1 ] ], [ 1, [ 2, 3 ] ], [ 3, [ 4 ] ] ]
    },
    "ns": { "r": 5, "c": 0, "r_major": [] }
  },
  "link_graph": [
    { "inner": [], "outer": [ "a" ], "ports": [ [ 0, 1 ], [ 2, 1 ] ] },
    { "inner": [], "outer": [ "v_a" ], "ports": [ [ 2, 1 ] ] }
  ],
  "nodes": [
    [ 0, { "ctrl_name": "A", "ctrl_params": [], "ctrl_arity": 1 } ],
    [ 1, { "ctrl_name": "Snd", "ctrl_params": [], "ctrl_arity": 0 } ],
    [ 2, { "ctrl_name": "M", "ctrl_params": [], "ctrl_arity": 2 } ],
    [ 3, { "ctrl_name": "Rcv", "ctrl_params": [], "ctrl_arity": 0 } ],
    [ 4, { "ctrl_name": "Fun", "ctrl_params": [], "ctrl_arity": 0 } ]
  ]
}
- : unit = ()

Graphical output

Graphviz

Generate a DOT file and render it with Graphviz. The figures above were produced this way:

# let oc = open_out "b.dot";;
# Big.to_dot b "b" |> output_string oc;;
# close_out oc;;

$ dot -Tsvg b.dot > b.svg

TikZ

Generate TikZ output for LaTeX documents. Tikz.big_to_tikz produces a standalone LaTeX document that can be compiled with pdflatex to obtain vector graphics matching the Graphviz figures above.

Interactive use

Start a toplevel session from the repository root:

$ dune utop .

Then load the library and install pretty-printers:

# #use "./bigraph/toplevel/bigtop.ml";;

This opens the Bigraph module and configures the toplevel to print bigraphs, reaction rules, and other types in a readable format.

Compiling

Add bigraph to the libraries stanza of your dune file:

(executable
 (name example)
 (libraries bigraph))

Then build and run:

$ dune build path/to/example.exe
$ dune exec path/to/example.exe