Bigraphs were invented by Robin Milner as an extension/generalization of previous process calculi (some of which he invented as well). A process calculus is a way to formally model concurrent and distributed systems, including communication/interactions/synchronizations, along with a set of algebraic laws to reason about them.
The structure of a bigraph is defined as two superimposed graphs over a single set of nodes
The place graph represents the relative location of each node (in terms of containment).
The link graph represents communication across place boundaries, ie common signals that all linked nodes share.
The "motion" of a bigraph is accomplished by reaction rules, which specify a redex
showing a bigraph to match and reactum
that shows the bigraph to replace it by.
Here is an example bigraph (showing the system in a "locked" state):
You can build complex bigraphs out of simpler bigraphs using the basic operations:
You can parse bigraphs from strings into python objects, and you can also build up bigraphs programmatically using the python API. The basic operations are available:
A = bigraph('A')
B = bigraph('B')
A.nest(B)
A.B
visualize(A)
A.B
A = bigraph('A')
B = bigraph('B')
merge = Merge([A, B])
merge
A | B
visualize(merge)
A | B
A = bigraph('A')
b = Edge('b')
A.link(b)
A{b}
visualize(A)
A{b}
The notation we have been using for bigraphs is Milner's original formalized into a language named .big
, as implemented by the Glasgow Bigraph Team. We are using their engine to run simulations, but we have our own parser for .big
files implemented as a Parsing Expression Grammar that converts strings into python bigraph objects.
To access the .big
parser, use the bigraph
function:
parsed = bigraph('A.(B | C{m, n})')
parsed
A.(B | C{m,n})
The python bigraph objects are rendered by default, which mirrors the original form we parsed.
We can also build this bigraph programmatically.
A = bigraph('A')
B = bigraph('B')
C = bigraph('C')
A, B, C
(A, B, C)
C.link('m')
C.link('n')
C
C{m,n}
merge = B.merge(C)
merge
B | C{m,n}
A.nest(merge)
A
A.(B | C{m,n})
Let's visualize this bigraph:
print(A)
visualize(A)
A.(B | C{m,n})
A.(B | C{m,n})
Controls are a way to label nodes, giving it a kind of "type" which declares:
Here is an example of a control with an arity of 2:
D1 = bigraph('ctrl D = 2')
D1.symbol, D1.arity
('D', 2)
Here is another control with named parameters:
C = bigraph('fun ctrl Compartment(volume, state) = 1')
C.symbol, C.arity, C.fun
('Compartment', 1, ('volume', 'state'))
Controls give us a more principled way to create nodes, and provide a way to structure our systems and guide reactions to target specific elements.
C1 = Node(control=C, params=(0.3, "stable"), ports=('atp',))
C2 = Node(control=C, params=(11.1111, "active"), ports=('chromosome',))
C1, C2
(Compartment(0.3,stable){atp}, Compartment(11.1111,active){chromosome})
We can even assign parameters this way
C1.assign('volume', 0.4)
Compartment(0.4,stable){atp}
The nested notation we've been using so far is succinct, but sometimes we want to represent the bigraphs in a more general way, specifically not directly nesting the nodes but instead tracking the four components of a bigraph separately:
We can do this by using the unfold()
method of the Bigraph
class to generate an instance of Bigraph
:
ABC = bigraph('A.(B | C{m,n})')
open_form = Bigraph.unfold(ABC)
open_form.get_spec()
{'controls': {'B': {'symbol': 'B', 'arity': 0, 'atomic': False, 'fun': []}, 'C': {'symbol': 'C', 'arity': 2, 'atomic': False, 'fun': []}, 'A': {'symbol': 'A', 'arity': 0, 'atomic': False, 'fun': []}}, 'nodes': {1: {'control': 'B', 'params': []}, 2: {'control': 'C', 'params': []}, 0: {'control': 'A', 'params': []}}, 'places': {0: (1, 2)}, 'links': {'m': (2,), 'n': (2,)}}
This means that if you have a dictionary with the four keys controls, nodes, places, links
you can make a nested bigraph out of it (going in reverse)
spec = {'controls': {'B': {'symbol': 'B', 'arity': 0, 'atomic': False, 'fun': []},
'C': {'symbol': 'C', 'arity': 2, 'atomic': False, 'fun': []},
'A': {'symbol': 'A', 'arity': 0, 'atomic': False, 'fun': []}},
'nodes': {1: {'control': 'B', 'params': []},
2: {'control': 'C', 'params': []},
0: {'control': 'A', 'params': []}},
'places': {0: (1, 2)},
'links': {'m': (2,), 'n': (2,)}}
from_spec = Bigraph(**spec)
from_spec.fold()
A.(B | C{m,n})
We have been talking a lot about the structure of bigraphs, but the real point is to operate dynamically, in this case through reactions
. A reaction is composed of two separate bigraphs, the redex
which matches some existing structure, and the reactum
that signifies what to modify in that structure.
To create a new reaction, we need to specify the redex bigraph and the reactum bigraph. Here is a simple reaction which takes any node with a Hello
control and nests a World
node inside it:
add_world = bigraph("""
react add_world =
Hello
-->
Hello.World
""")
add_world
react add_world = Hello --> Hello.World
Now let's apply our reaction. We need an initial bigraph, in this case the lone node with control Hello
. Then we can call react
with the add_world
reaction on it:
hello = bigraph("Hello")
result = react(add_world, hello)
visualize(hello)
visualize(result)
result
Hello.World
Beyond applying a single reaction to a single bigraph, we can also run whole systems of reactions in a series of transitions starting from an initial bigraph. In order to do this, we need to define the system
.
We can declare the system using .big
notation:
system = bigraph("""
begin brs
init hello;
rules = [
{add_world}
];
end
""")
system
begin brs init hello; rules = [ {add_world} ]; end
There are a few components to this:
begin brs
declares which type of reactive system we are creating. Other options are pbrs
and sbrs
for probabilistic and stochastic reactive systems respectively. init hello
declares the bigraph we'll use as the initial state for the system. Reactions will match against this initial state at first, and then each subsequent state as transitions are applied. rules = [....]
is the collection of rules, organized into "rule groups", each group enclosed by squirrely braces. Rule groups are a way to specify groups of alternative reactions to apply to the current bigraph state. Each group will be checked one by one in order, and if any of the rules in that group match, one of the matching rules will be selected (non-deterministically) to apply a transition to the current state, then we go back to the top of the rules
section.
rules = [
{add_world, grow_world},
{perturb_world},
{remove_world, duplicate_world, invert_world}
]
In this case, we check first whether the redex of either add_world
or grow_world
matches the current state. If one of them does, it is applied, otherwise we check the next group. If both of them match, then one is selected at randomly.
Once a rule is applied, we go back to the top and iterate through the rule groups again. If none of the rules match, the simulation ends.
Now that we have all the pieces, let's put them together into a whole system and run it!
hello_world = bigraph("""
ctrl Hello = 0;
ctrl World = 0;
react add_world =
Hello
-->
Hello.World;
big initial = Hello.1;
begin brs
init initial;
rules = [
{add_world}
];
end
""")
Here is our system:
hello_world
ctrl Hello = 0; ctrl World = 0; react add_world = Hello --> Hello.World; big initial = Hello.1; begin brs init initial; rules = [ {add_world} ]; end
Let's simulate this system now:
# a path to write the simulation results
path = "out/bigraph/hello"
# we must set a number of steps to simulate
# as this system would otherwise run forever!
steps = 5
# simulate the system
results = hello_world.simulate(path=path, steps=steps)
for transition in results:
print(transition)
Hello Hello.World Hello.World.World Hello.World.World.World Hello.World.World.World.World Hello.World.World.World.World.World Hello.World.World.World.World.World.World
Let's visualize all these transitions!
hello_world.display_transitions(path=path)