BigraphER

BigraphER (Bigraph Evaluator & Rewriting) computes the reachable transition system of a bigraphical reactive system (BRS), either exhaustively or by simulation, and exports it for probabilistic model checking in PRISM, for plotting (DOT, SVG or TikZ), or as JSON. It is built on the bigraph library, a standalone API for programmatically manipulating bigraphs, reaction rules, and BRS.

Quick start

A model is a .big file. Check it, explore it, and export a PRISM model:

$ bigrapher validate model.big
$ bigrapher full model.big
$ bigrapher full -p model.tra -r model.rews model.big
$ bigrapher sim -S 100 --seed=42 model.big

validate statically checks the model's validity, without rewriting or state-space exploration. full explores every reachable state, optionally bounded with -M N; sim performs a random walk for models too large to exhaust. The tutorial walks through the language with worked examples.

Building from source

With opam and a C/C++ toolchain:

$ git clone https://bitbucket.org/uog-bigraph/bigraph-tools.git
$ cd bigraph-tools
$ opam update
$ opam switch create .
$ eval $(opam env)
$ dune build @all
$ dune install

opam switch create . creates a local switch in the repository and automatically installs the project's dependencies, including dune, the build tool.

Use dune build --profile=release @all for an optimised build, or --profile=static for a statically linked binary. Graphviz is optional, needed only for SVG export.

Commands

Each subcommand has its own manpage, generated from the tool itself:

The BigraphER language

Emacs mode

big-mode is an Emacs major mode for .big files, with syntax highlighting, indentation, and comment support. It is part of the distribution; add the bigrapher/big-mode directory to your load-path:

(add-to-list 'load-path "~/.emacs.d/bigraph-tools/bigrapher/big-mode")
(require 'big-mode)

Requires Emacs 27.1 or later.

References