BIGRAPHER(1) General Commands Manual BIGRAPHER(1)


bigrapherImplementation of Bigraphical Reactive Systems


bigrapher option

bigrapher command args


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 ( to carry out quantitative analysis. The graphical representation of bigraphs is generated by the automatic layout generator Graphviz (
Use either bigrapher command -h or bigrapher command --help for more information on a specific command.


Compute the transition system of a model.
Simulate a model.
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,, 494 - 501, 2016.
M. Sevegnani and M. Calder, Bigraphs with Sharing, Elsevier, Theoretical Computer Science, 0, 577,, 43 - 73, 2015.
Refer to for more examples and a complete reference of the big format for bigraphical models.


Michele Sevegnani <>
September 22, 2017 Darwin 16.7.0