bigrapher —
Implementation of Bigraphical Reactive
Systems
BigraphER (Bigraph Evaluator & Rewriting) is an implementation of
Bigraphical Reactive Systems (BRS) that supports bigraphs with sharing,
stochastic and probabilistic reaction rules, rule priorities and BiLog
predicate checking. The bigraph matching engine is based on a SAT encoding of
the subgraph isomorphism problem. A BRS and its labelling function can be
exported to text files in
tra and
csl format, respectively, and used in stochastic
model checker PRISM
(
http://www.prismmodelchecker.org)
to carry out quantitative analysis. The graphical representation of bigraphs
is generated by the automatic layout generator Graphviz
(
http://www.graphviz.org).
Use either
bigrapher
command -h or
bigrapher
command
--help for more
information on a specific command.
-
-
- full
- Compute the transition system of a model.
-
-
- sim
- Simulate a model.
-
-
- validate
- Parse a model and check its validity.
-
-
- -C,
--config
- Print a summary of your configuration.
-
-
- -h,
--help
- Display the list of options.
-
-
- -V,
--version
- Show version information.
bigrapher-full(1),
bigrapher-sim(1),
bigrapher-validate(1)
The following references provide more in-depth details on bigraphs and the
implementation of the BigraphER tool:
R. Milner,
The Space and Motion of Communicating Agents,
Cambridge University Press,
2009.
M. Sevegnani and
M. Calder, BigraphER: Rewriting and
Analysis Engine for Bigraphs, Computer Aided
Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada,
July 17-23, 2016, Proceedings, Part II, Springer
International Publishing,
http://doi.org/10.1007/978-3-319-41540-6_27,
494 - 501, 2016.
M. Sevegnani and
M. Calder, Bigraphs with
Sharing, Elsevier, Theoretical
Computer Science, 0,
577,
http://doi.org/10.1016/j.tcs.2015.02.011,
43 - 73, 2015.
Refer to
http://www.dcs.gla.ac.uk/~michele/bigrapher.html
for more examples and a complete reference of the
big format for bigraphical models.
Michele Sevegnani
<
michele.sevegnani@glasgow.ac.uk>