mseve/bigrapher repository overview

⁠Bigraph-Tools

Authors: Michele Sevegnani⁠, Blair Archibald⁠

This repository contains a collection of tools for writing and anlysing Bigraph models. It contains:

1. bigraph - a library to programmaticaly manipulate bigraphs, reaction rules and Bigraphical Reactive Systems (BRS). It supports both bigraphs and bigraphs with sharing, probabilistic and stochastic reaction rules, rule priorities, rules with instantiation maps, parameterised controls, simulation, exhaustive state space exploration, export to probabilistic model checker PRISM⁠, and predicate checking. It is based on an efficient matching engine based on SAT.

2. bigrapher - BigraphER is a command-line tool to compute the transition system of a BRS and export it to the stochastic model checker PRISM⁠ or to graphical form.

3. big_json - Big_json is a codec to encode and decode bigraphical structures such as bigraphs and reaction rules to the JSON⁠ data format. The library provides a JSON interface to the matching engine of the bigraph library. This is also exposed by the big_match command line tool.

4. minisat - Minisat provides bindings to the MiniSAT⁠ SAT solver.

5. minicard - Minicard provides bindings to the MiniCARD⁠ cardinality solver.

⁠Building the Tools

The tools can be built using dune (min version 2) as follows:

dune build --profile=release

To install the tools to a local opam repository you can use:

dune install --profile=release

⁠References

• Robin Milner. The space and motion of communicating agents. Cambridge University Press (2009).⁠
• Michele Sevegnani and Muffy Calder. Bigraphs with sharing. Theoretical Computer Science 577 (2015): 43-73.⁠
• Michele Sevegnani and Muffy Calder. BigraphER: rewriting and analysis engine for bigraphs. Proceedings of Computer Aided Verification (CAV 2016), Lecture Notes in Computer Science 9780 (2016): 494-501.⁠
• T. Bray Ed. The JavaScript Object Notation (JSON) Data Interchange Format. (2014)⁠
• OPAM: OCaml package manager⁠
• PRISM: probabilistic model checker⁠
• MiniSAT: a minimalistic and high-performance SAT solver⁠
• MiniCARD cardinality solver⁠

⁠Copyright and license

Copyright 2012-2020 Glasgow Bigraph Team

All rights reserved. Tools distributed under the terms of the Simplified BSD License that can be found in the LICENSE file⁠.