BigraphER

BigraphER (Bigraph Evaluator & Rewriting) is an implementation of Robin Milner's Bigraphical Reactive System (BRS) with an extension to bigraph with sharing. Its main features are:

BigraphER consists of:

To cite BigraphER, please use the most recent tool paper, from CAV 2016:

BigraphER: rewriting and analysis engine for bigraphs
Michele Sevegnani and Muffy Calder
in proceedings of Computer Aided Verification (CAV 2016), Lecture Notes in Computer Science, Volume 9780 Part II, pp 494-501, Springer, July 2016
[bib]

Quick install

Using OPAM

OPAM is a source-based package manager for OCaml. It supports all the major Linux distributions, macOS, BSD systems and Windows (Cygwin). Once OPAM is installed on your system, add the repository of the University of Glasgow with the following command:

opam repository add glasgow 'http://www.dcs.gla.ac.uk/~michele/dcs-opam-repository/'
Then, to install BigraphER simply run:
opam install bigrapher
OPAM will automatically download and install all the dependencies. Run the following commands regularly to keep up with the latest version of BigraphER:
opam update
opam upgrade bigrapher

From sources

To compile BigraphER form source code, you will need:

and sources of the latest version of BigraphER:

Once the archive is downloaded and extracted, you can then run the following commands:

make build && make install

Depending on your system configuration, superuser privileges may be required for command make install.

BSD systems

On *BSD systems, you need to use gmake instead of make.

Using a Docker image

A Docker image can be downloaded with the following command:

sudo docker pull mseve/bigrapher

Then, we can run the container by doing this:

sudo docker run -i -t mseve/bigrapher:latest

Finally, BigraphER can be invoked within the container with command bigrapher. Other tags can be found in the repository at https://hub.docker.com/r/mseve/bigrapher/.

Tool usage

This short tutorial covers the most common use cases to get you started with bigrapher.

Computing and exporting the transition system

bigrapher full -p <out-file> <model-file>

This command will compute the transition system of input <model-file> and export it to PRISM .tra format. Input <model-file> is expected to have .big extension. If <model-file> is a BRS (i.e. non-stochastic) all the probabilities are set to 1.

Simulating and exporting states

bigrapher sim -T <max-time> -s -t <out-file> -f svg <model-file>

This command will simulate input <model-file> and export to .svg both the resulting trace and its states. The trace is stored in <out-file>, while the states are stored in the directory containing <out-file>. The states have file names in the form of <#i>.svg, where <#i> is the state number. An example trace with five states is shown below. The bigraph for a state can be visualised by clicking on the corresponding state in the trace. Hit back button in your browser to return to the trace.

The simulation runs either until:

Validating a model

bigrapher validate -d <path> -f svg <model-file>

This command is useful to debug a model. It stores in directory <path> the graphical representation in .svg format of every bigraph and reaction rule defined in <model-file>. The transition system is not computed.

Man pages

A complete synopsis of bigrapher and all its subcommands can be found in the following man pages:

Model specification

A .big model specifies a BRS or a stochastic BRS. It is composed of three different logical parts:

  1. constant and control definitions
  2. bigraphs and reaction rules definitions
  3. reactive system definition

We describe them separately via the following code snippets:

Constant definitions

float tau = 20.3;
float t_min = 15. + tau;
int size = 132;

This code defines two float constants (tau and t_min) and one int constant (size). Note that the BigraphER language does not support implicit type conversion.

Control definitions

ctrl A = 1;
atomic ctrl M = 2;

This code defines controls A and M. They have one and two ports, respectively. The keyword atomic specifies that a node of control M may not contain other nodes.

Bigraph definitions

big a0 = A{a}.Snd.(M{a, v_a} | Ready.Fun.1);

This code defines bigraph a0. Expression A{a} denotes a node of control A with name a. Operators . and | denote nesting and merge product, respectively. Expression 1 denotes a bigraph with only one region and no nodes or sites. The graphical representation of a0 is as follows:

Reaction rule definitions

react snd =
  A{a0}.Snd.(M{a1, v} | id) | Mail
  -->
  A{a0} | Mail.(M{a1, v} | id);

This code defines reaction rule snd. Symbol --> (or alternatively ->) separates the left-hand side from the right-hand side. Expression id indicates the identity, i.e. the bigraph with one site inside one region. This reaction rule models an asynchronous send action. Intuitively, it deletes the node of control Snd inside node A and moves its content (the message of control M) inside the node of control Mail.

Probabilities and rates are specified by construct -[...]-> which accepts float expressions. Here is a simple example with a stochastic version of the previous reaction rule:

float m_size = 8464.;
react snd =
  A{a0}.Snd.(M{a1, v} | id) | Mail
  -[ 1./(m_size + (2. * .112)) ]->
  A{a0} | Mail.(M{a1, v} | id);

Instantiation maps

BigraphER also supports reaction rules with instantiation maps which allow to easily duplicate or discard parts of a bigraph when a reaction rule is applied. The code in the example below models the spawning of a new node of control A. The left-hand side and the right-hand side have three and four sites, respectively.

react new =
  A{a0}.(New.(A'{a1} | id) | id)
  -->
  A{a0}.(id | id) | A{a1}.(id | id)
  @ [1, 2, 0, 2];

Instantiation map [1, 2, 0, 2] (from the right-hand side to the left-hand side) specifies that:

Note that, some sites in the left-hand side may not be mapped by any sites in the right-hand side, thus the part of the bigraph corresponding to that site is discarded when the reaction rule is applied. Also, several sites on the right-hand side my be mapped to the same site in the left-hand side, thus that part is duplicated.

Reactive system definition

begin brs
  init s0;
  rules = [ {snd, ready, lambda, new} ];
  preds = { phi };
end

A valid .big file always contains a reactive system definition:

begin [brs|pbrs|sbrs] ... end

with keywords brs, pbrs, sbrs indicating a BRS, a probabilistic BRS, and a stochastic BRS, respectively. Keyword init specifies the initial state of the system. In the example, this is bigraph s0. Construct rules = [...] defines a list of priority classes in descending order of priority. A priority class is specified by construct {...}. It may contain only reaction rules identifiers. Finally, construct preds = {...} defines a set of predicates (bigraphs) that are checked (matched) against every new state.

Full example

A simplified model of the bigraphical encoding of Actors described in [pdf] is given below:
# Signature
ctrl A = 1;
ctrl A' = 1;	  
ctrl Mail = 0;
atomic ctrl M = 2;
ctrl Snd = 0;
ctrl Ready = 0;
ctrl New = 0;
ctrl Fun = 0;

# Reaction rules
react snd =
  A{a0}.Snd.(M{a1, v} | id) | Mail
  -->
  A{a0} | Mail.(M{a1, v} | id);

react ready =
  A{a}.Ready | Mail.(M{a, v} | id)
  -->
  A{a} | Mail | {v};

react lambda = A{a}.Fun --> A{a};

react new =
  A{a0}.(New.(A'{a1} | id) | id)
  -->
  A{a0}.(id | id) | A{a1}.(id | id)
  @ [1, 2, 0, 2];
	
# Initial state
big a0 = A{a}.Snd.(M{a, v_a} | Ready.Fun.1);

big a1 = A{b}.Snd.M{a, v_b};

big s0 = a0 | a1 | Mail.1;

# Predicate
big phi = Mail.(M{a, v} | id);

# Reactive system
begin brs
  init s0;
  rules = [ {snd, ready, lambda, new} ];
  preds = { phi };
end

This example can be downloaded here.

Bigraphs with sharing

ctrl S = 1;            # Signal range
atomic ctrl M = 1;     # Mobile station

big n_0 =
  share (M{a_A} || M{a_B} || M{a_C})
  by ([{0, 1}, {0, 1, 2}, {1, 2}], 3)
  in (id{a_A, a_B, a_C} | S{a_A} | S{a_B} | S{a_C});

This code defines bigraph n_0 which represents a wireless network topology showing the hidden node problem. The full bigraphical model is described in [pdf]. Sharing is introduced by ternary operator share ... by ... in .... The first argument specifies the entities to be shared. In this case, the three mobile stations of control M. Operator || denotes parallel composition. The second argument specifies where mobile stations are placed. For example, {0, 1} says that station M{a_A} is shared by the first and the second signals (counting from left to right). The third argument specifies the entities containing the shared entities. In this case, the three signals of control S. The graphical representation of n_0 is as follows:

Functional definitions

OCaml library

APIs

A complete reference to the library is available here.

We describe the features of the bigraph library with a simple example. The OCaml function below specifies bigraph a0 defined here and prints out its textual representation:

let () =
  let a0 =
    Big.nest
      (Big.ion (Link.parse_face ["a"]) (Ctrl.C ("A", 1)))
      (Big.nest
	 (Big.ion (Link.Face.empty) (Ctrl.C ("Snd", 0)))
	 (Big.par
	    (Big.nest
	       (Big.ion (Link.parse_face ["a"; "v_a"]) (Ctrl.C ("M", 2)))
	       Big.one)
	    (Big.nest
	       (Big.ion (Link.Face.empty) (Ctrl.C ("Ready", 0)))
	       (Big.nest
		  (Big.ion (Link.Face.empty) (Ctrl.C ("Fun",0)))
		  Big.one)))) in
  print_endline ("bigraph a0:\n" ^ (Big.to_string a0))

Source file example.ml containing the code above can be downloaded here. Nesting and merge product operations are implemented by functions Big.nest and Big.par, respectively. Nodes can be added to a bigraph by calling function Big.ion which admits two arguments: the first is an interface while the second is a control. Bigraph 1 corresponds to value Big.one. A string representation of a bigraph is computed by function Big.to_string.

Compiling

Source file example.ml can be compiled to byte-code with the following command:

ocamlfind ocamlc -o example.byte -package bigraph -linkpkg example.ml

Here we use ocamlfind to automatically pass to ocamlc all the flags required to link our program with library bigraph. The execution of program example.byte prints out a textual description of a0:

$ ./example.byte 
bigraph a0:
{(0, A:1),(1, Snd:0),(2, M:2),(3, Ready:0),(4, Fun:0)}
1 5 0
10000
01000
00110
00000
00001
00000
({}, {a}, {(0, 0), (2, 0)})
({}, {v_a}, {(2, 1)})

The compilation to native-code is performed as follows:

ocamlfind opt -o example.asm -package bigraph -linkpkg example.ml

Uninstalling BigraphER

If you installed BigraphER via OPAM, simply run:

opam remove bigrapher
If you built BigraphER from sources then run:
make uninstall
ocamlfind remove bigraph