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:
To cite BigraphER, please use the most recent tool paper, from CAV 2016:
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/'opam install bigrapheropam update
opam upgrade bigrapherA Docker image can be downloaded with the following command:
sudo docker pull mseve/bigrapherThen, we can run the container by doing this:
sudo docker run -i -t mseve/bigrapher:latestFinally, 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/.
bigrapher.
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.
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:
<max-time> (this
parameter is ignored if <model-file> is
non-stochastic)
bigrapherbigrapher 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.
A complete synopsis of bigrapher and all its subcommands can
be found in the following man pages:
A .big model specifies a BRS or a stochastic BRS.
It is composed of three different logical parts:
We describe them separately via the following code snippets:
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.
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.
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:
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);
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.
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] ... endwith
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.
# 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 };
endThis example can be downloaded here.
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:
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.
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.mlIf you installed BigraphER via OPAM, simply run:
opam remove bigraphermake uninstall
ocamlfind remove bigraph