BigraphER accepts model files in a concrete syntax that describes bigraphs, reaction rules, and reactive system variants. The examples in this section are checked automatically as part of the test suite.
The notation and modelling conventions follow:
For background on the implementation of BigraphER, see:
This tutorial covers model structure, bigraph expressions, reaction rules, reactive system variants, and advanced features.
BigraphER provides five commands: validate to check models, format to reformat them, full to compute transition systems, sim to run simulations, and interactive to step through a model by hand. For a complete option reference, see the Commands reference. This tutorial focuses on modelling concepts and common workflows.
A model consists of a non-empty declaration section followed by a reactive system block.
ctrl A = 0;
big b = A.1;
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet examples/minimal.big
OKIn the example above, ctrl A = 0; declares a control of arity zero: entities with control A do not allow links. The binding big b = A.1; declares a bigraph b containing a single A entity with no nested content.
The reactive system block starts with begin brs, gives the initial bigraph with init b;, and declares an empty rule set with rules = [];.
Declarations introduce parameters, controls, bigraphs, and reaction rules. The following model uses integer, float, string, control, atomic control, and bigraph declarations.
int n = 3;
float rate = 0.5;
string label = "x";
ctrl A = 0;
atomic ctrl B = 1;
big b = A.1 | B{x};
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet --warn-family=none examples/declarations.big
OKThe keywords int, float, and string define named parameters, used later when instantiating parameterised controls, bigraphs, and reaction rules.
The declaration ctrl A = 0; introduces a control A of arity zero.
The declaration atomic ctrl B = 1; introduces an atomic control B of arity one. Entities with atomic controls may have links but do not allow nesting below them.
The binding big b = A.1 | B{x}; defines a bigraph with A and B as siblings in the same region. The notation {x} indicates that B has an open link named x. Nesting is denoted by .; the symbol 1 is the empty bigraph, so A.1 means A contains no nested content.
Warnings are enabled by default in validate and disabled by default in full and sim; a few of the examples use --warn-family=none to keep the output focused. In practice, you should run bigrapher validate --warnings model.big to check your models for issues. The Warnings section covers this topic.
This model demonstrates tensor product, composition, merge product, parallel product, and shared names.
ctrl A = 1;
ctrl B = 1;
ctrl C = 1;
ctrl D = 1;
ctrl P = 0;
ctrl Q = 0;
big t = P.1 + Q.1;
big c = id(2) * t;
big p = A{x}.1 | B{x}.1;
big pp = C{y}.1 || D{y}.1;
# Use all bigraphs in the initial state
big init_state = p | pp | c;
begin brs
init init_state;
rules = [];
end$ bigrapher validate --quiet examples/bigraphs.big
OKThe tensor product + juxtaposes two bigraphs side by side. In P.1 + Q.1, the two entities are placed in separate regions.
Bigraph composition * inserts one bigraph into the sites of another. In id(2) * t, t's regions fill id(2)'s sites. Common names are merged when present.
The merge product | places entities as siblings in the same region. In A{x}.1 | B{x}.1, A and B are siblings. Since both use the name x, their links are merged into a single hyperedge.
The parallel product || shares common names across two terms while keeping them in separate regions. In C{y}.1 || D{y}.1, the name y is shared, giving a single hyperedge, but C and D occupy different regions.
The number in a control declaration ctrl A = n; specifies how many ports the control has -- connection points for links. A control with arity n can participate in up to n distinct links.
ctrl Hub = 3;
ctrl Spoke = 1;
# Three independent spokes, each connected to a different port of the hub.
big net = Hub{x,y,z}.1 | Spoke{x}.1 | Spoke{y}.1 | Spoke{z}.1;
begin brs
init net;
rules = [];
end$ bigrapher validate --quiet examples/ports.big
OKThe control Hub has arity 3, meaning each Hub entity has three ports. In Hub{x,y,z}, the three ports connect to three different links x, y and z. Each Spoke has arity 1 and contributes one port to its single link. Altogether the link graph connects four entities through three independent links.
Ports are tracked as a multiset, not a set, so multiplicities matter for matching. When a reaction rule pattern expects an entity with control A connected to x and y (two ports), the matching engine checks that the entity in the target bigraph has at least two ports linked to x and y respectively. A pattern A{x} matches any A that has at least one port on x; extra ports on x are left in the matched context.
Bigraph expressions can be combined using these operators. They have the following precedence, from strongest to weakest:
* + | and ||
The operators | and || have the same precedence and associate to the left. For example, the expression
A | B + C * D || E
is parsed as
(A | (B + (C * D))) || E
Parentheses can be used to override this convention.
Reaction rules describe how a bigraph can evolve. A rule has a left-hand side, an arrow -->, and a right-hand side. Reaction rules are introduced with the keyword react.
This example also shows comments, name closure, new names, and instantiation maps. Comments start with # and continue to the end of the line.
ctrl A = 1;
ctrl B = 0;
atomic ctrl C = 0;
ctrl D = 1;
big open = A{x};
big closed = /x D{x} | {x};
big gone = B.1 | {x};
react close = open --> closed;
react remove = open --> gone @[];
# Initial state
big s0 = open * C;
begin brs
init s0;
rules = [ {close, remove} ];
end$ bigrapher validate --quiet examples/reactions.big
OKThe bigraph open is an A-entity connected to the open name x.
The bigraph closed uses closure and new-name creation. The closure /x binds more tightly than merge product |, so it applies only to D{x}. The bound x inside the closure and the open x introduced by {x} are not merged by |.
The bigraph gone introduces B and keeps the open name x. The suffix .1 means B contains the empty bigraph.
The rule close rewrites a match of open into closed.
The rule remove rewrites open into gone with an instantiation map @[...] appended to the right-hand side. An instantiation map determines, for each site in the right-hand side, which site in the left-hand side it maps to. Here the map is empty @[], meaning the content matched by the site in the left-hand side is discarded.
The initial state s0 composes open with C. Since open has a site, the composition places C inside the A-entity.
The reactive system block sets init s0; and places close and remove in the same priority class with rules = [{close, remove}];.
Reaction rules can have conditions. A condition restricts when a rule is applicable by checking for a predicate bigraph in either the matched context or the matched parameter.
ctrl Room = 0;
atomic ctrl Person = 0;
atomic ctrl Alarm = 0;
atomic ctrl Safe = 0;
atomic ctrl Done = 0;
react evacuate =
Person --> Done
if Alarm in ctx;
react stay =
Person --> Safe
if !Alarm in ctx;
react clear =
Room.Person --> Room.Done
if Person in param;
big s0 =
Room.Person | Alarm;
begin brs
init s0;
rules = [ {evacuate, stay, clear} ];
end$ bigrapher validate --quiet examples/conditions.big
OKThe condition Alarm in ctx checks for an Alarm entity in the matched context. The rule evacuate applies only when an alarm exists outside the matched Person.
Negated conditions use the ! prefix. The rule stay applies only when Alarm is absent from the context.
The condition Person in param checks the matched parameter rather than the context. The rule clear matches a Room containing a parameter and requires that parameter to contain a Person.
This model extends the brs block with multiple rule classes, an instantaneous class, predicates with rewards, and an instantiation map that duplicates a matched site.
ctrl A = 1;
ctrl B = 0;
atomic ctrl C = 0;
ctrl D = 1;
big open = A{x};
big duplicated = D{x}.(id | id);
big closed = /x D{x} | {x};
big gone = B.1 | {x};
big has_d = D{x};
big has_b = B.1;
react duplicate = open --> duplicated @[0,0];
react close = open --> closed;
react remove = open --> gone @[];
# Initial state
big s0 = open * C;
begin brs
init s0;
rules = [ {duplicate, close}, (remove) ];
preds = { has_d[10], has_b[1] };
end$ bigrapher validate --quiet examples/brs.big
OKThe keyword brs selects an ordinary Bigraphical Reactive System, enclosed between begin brs and end.
The duplicate rule has two sites on the right-hand side, written as id | id. Its instantiation map @[0,0] maps both right-hand-side sites to site 0 on the left-hand side. The content matched inside A is duplicated.
The rules declaration organises rules into priority classes. Classes are listed from higher to lower priority. In this example, {duplicate, close} has higher priority than (remove). Rules in a lower-priority class are considered only when no rule in any higher-priority class is applicable.
After an ordinary rule is applied, rule selection starts again from the highest-priority class. It does not continue with the next class. During simulation, if several rules in the selected class are applicable, one rule is chosen at random for the next step -- see Simulation. During full transition system computation, all applicable rules in the selected class are applied, producing the corresponding outgoing transitions.
A class written with parentheses, such as (remove), is an instantaneous or reducing class. Rules in an instantaneous class are applied until no rule in the class is applicable. These applications do not appear as ordinary transitions in the generated transition system. The class must be exhausted before ordinary rewriting continues.
Instantaneous classes should be terminating and confluent.
BigraphER does not currently check this condition. It is the modeller's responsibility.
The preds declaration lists predicates to be checked over states. In this example, has_d has reward 10 and has_b has reward 1. For each reachable state, BigraphER checks which predicates hold and sums their rewards to produce the state reward for that state. Predicates with rewards are available in all model types, not just BRS. Rewards must be non-negative integers. The rewards are exported in PRISM .rews format.
Priorities and instantaneous classes affect the generated transition system, as described in Full exploration.
The variants pbrs, sbrs, and abrs all use annotated reaction arrows -[e]->, with weights for pbrs and abrs, and rates for sbrs.
Probabilistic reactive systems (begin pbrs) use weights on reaction arrows. BigraphER normalises the weights of all enabled rule occurrences from each state so outgoing probabilities sum to 1.
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
big a = A.1;
big b = B.1;
big c = C.1;
react to_b = a -[7]-> b;
react to_c = a -[3]-> c;
begin pbrs
init a;
rules = [ {to_b, to_c} ];
end$ bigrapher validate --quiet examples/pbrs.big
OKIn this example, to_b and to_c each have one enabled occurrence, with weights 7 and 3. The transition to b has probability 7 / (7 + 3), and the transition to c has probability 3 / (7 + 3).
Priority classes, instantaneous classes, and predicates work identically to brs. The normalisation of weights applies within the selected priority class: if a state enables rules from a higher-priority class, only those rules' weights are normalised and the lower-priority classes are not considered.
ctrl Token = 0;
ctrl Success = 0;
ctrl Failure = 0;
ctrl Done = 0;
big token = Token.1;
big success = Success.1;
big failure = Failure.1;
big done = Done.1;
big has_success = Success.1;
big has_failure = Failure.1;
# First class: try the operation (weighted choice)
react try_ok = token -[7]-> success;
react try_fail = token -[3]-> failure;
# Second class: recover from failure
react recover = failure -[4]-> token;
react give_up = failure -[1]-> done;
# Instantaneous: success is absorbed into done
react absorb = success -[1]-> done;
begin pbrs
init token;
rules = [ {try_ok, try_fail}, {recover, give_up}, (absorb) ];
preds = { has_success[10], has_failure[1] };
end$ bigrapher validate --quiet examples/pbrs-rich.big
OKIn this example, the first priority class {try_ok, try_fail} offers a weighted choice from the token state. The second class {recover, give_up} governs transitions from the failure state. The instantaneous class (absorb) silently rewrites success to done before any ordinary transition is recorded.
From token, try_ok (weight 7) and try_fail (weight 3) are the only enabled occurrences. The transition to success has probability 7 / (7 + 3) = 0.7, but success is immediately absorbed by absorb into done. The transition to failure has probability 0.3.
From failure, recover (weight 4) leads back to token with probability 4 / (4 + 1) = 0.8, and give_up (weight 1) leads to done with probability 0.2.
The predicates has_success and has_failure assign state rewards. Because success is always absorbed instantly, has_success is never observed in any reachable state.
Stochastic reactive systems (begin sbrs) use rates on reaction arrows. Rates are not normalised; they contribute to the exit rate of each state.
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
big a = A.1;
big b = B.1;
big c = C.1;
react to_b = a -[1.0]-> b;
react to_c = a -[2.0]-> c;
begin sbrs
init a;
rules = [ {to_b, to_c} ];
end$ bigrapher validate --quiet examples/sbrs.big
OKIn this example, to_b and to_c each have one enabled occurrence, with rates 1.0 and 2.0. The exit rate of the state is 1.0 + 2.0. More generally, the exit rate is the sum of the rates of all enabled rule occurrences in the state. If a rule with rate r has n distinct occurrences, those occurrences contribute n \times r to the exit rate.
The exit rate determines the exponential waiting time before the next reaction. The probability that a particular enabled occurrence is chosen is its rate divided by the exit rate. If several occurrences lead to the same successor state, their rates are added to obtain the transition rate to that successor.
Priority classes and predicates work identically to brs. The exit rate is computed over the enabled occurrences in the selected priority class only. Instantaneous classes are not supported for sbrs.
ctrl Token = 0;
ctrl Success = 0;
ctrl Failure = 0;
ctrl Done = 0;
big token = Token.1;
big success = Success.1;
big failure = Failure.1;
big done = Done.1;
big has_success = Success.1;
big has_failure = Failure.1;
# First class: try the operation (rate-based choice)
react try_ok = token -[0.7]-> success;
react try_fail = token -[0.3]-> failure;
# Second class: recover from failure or complete
react recover = failure -[0.4]-> token;
react give_up = failure -[0.1]-> done;
react complete = success -[0.5]-> done;
begin sbrs
init token;
rules = [ {try_ok, try_fail}, {recover, give_up, complete} ];
preds = { has_success[10], has_failure[1] };
end$ bigrapher validate --quiet examples/sbrs-rich.big
OKIn this model, the first priority class {try_ok, try_fail} governs the initial token state. The exit rate from token is 0.7 + 0.3 = 1.0. The transition to success occurs with probability 0.7 / 1.0 = 0.7, and to failure with probability 0.3.
From failure, the second class {recover, give_up, complete} enables recover (rate 0.4) and give_up (rate 0.1). The exit rate is 0.5, and recover is chosen with probability 0.4 / 0.5 = 0.8.
From success, only complete is enabled (rate 0.5), so the exit rate is 0.5 and the transition to done is deterministic.
The predicates has_success and has_failure assign state rewards, computed in the same way as for BRS and PBRS.
Action reactive systems (abrs) use weights like pbrs, plus an actions declaration that groups rules into named actions with optional rewards. The resulting transition systems are Markov decision processes.
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
big a = A.1;
big b = B.1;
big c = C.1;
react to_b = a -[7]-> b;
react to_c = a -[3]-> c;
react stay = a -[1]-> a;
begin abrs
init a;
rules = [ {to_b, to_c, stay} ];
actions = [ choose[2] = {to_b, to_c}, wait[0] = {stay} ];
end$ bigrapher validate --quiet --warn-family=none examples/abrs.big
OKThe entry choose[2] = {to_b, to_c} defines an action choose containing the rules to_b and to_c, with reward 2. The entry wait[0] = {stay} defines a second action wait, with reward 0.
Normalisation is local to each enabled action. If choose is selected, the enabled rules to_b and to_c each have one occurrence, with weights 7 and 3. The transition to b has probability 7 / (7 + 3), and the transition to c has probability 3 / (7 + 3).
In general, the normalisation is over enabled rule occurrences within the selected action. If a rule with weight w has n distinct occurrences, those occurrences contribute total weight n \times w within that action.
If both choose and wait are enabled, the model contains an explicit non-deterministic choice between these actions. Within the selected action, the next successor is chosen probabilistically according to the normalised weights.
Multiple priority classes are commonly used in abrs models. Each ordinary class is called a source class. Source classes are independent: rules in different source classes produce transitions independently and do not compete within a single action selection. This models systems where several agents act concurrently.
Instantaneous classes and predicates work identically to brs. Every rule, including those in instantaneous classes, must belong to some action in the actions declaration.
ctrl Token = 0;
ctrl Result = 0;
ctrl Empty = 0;
# Source patterns
big has_token = Token.1;
big has_result = Result.1;
# Source class 1: produce a token or do nothing
react produce = Empty.1 -[1]-> Token.1;
react idle = Empty.1 -[1]-> Empty.1;
# Source class 2: consume the token
react succeed = Token.1 -[8]-> Result.1;
react fail = Token.1 -[2]-> Empty.1;
# Instantaneous: result decays back to empty
react decay = Result.1 -[1]-> Empty.1;
big s0 = Empty.1;
begin abrs
init s0;
rules = [ {produce, idle}, {succeed, fail}, (decay) ];
actions = [
act[1] = {produce, succeed, decay},
pass[0] = {idle, fail}
];
preds = { has_token[1], has_result[5] };
end$ bigrapher validate --quiet --warn-family=none examples/abrs-rich.big
OKThis model has two source classes. The first {produce, idle} governs transitions from the Empty state. The second {succeed, fail} governs transitions from the Token state. The instantaneous class (decay) silently rewrites Result to Empty.
The actions span both source classes: act (reward 1) contains produce, succeed, and decay, while pass (reward 0) contains idle and fail.
In the Empty state, source class 1 enables both produce and idle. If act is selected, produce fires (weight 1) and the state becomes Token. If pass is selected, idle fires (weight 1) and the state remains Empty.
In the Token state, source class 2 enables succeed and fail. If act is selected, succeed fires (weight 8) producing Result, which is instantly decayed to Empty. If pass is selected, fail fires (weight 2) and the state becomes Empty directly.
The predicates has_token and has_result assign state rewards. Note that has_result is never observed because Result is always instantaneously decayed.
ABRS models carry a single global reward structure with two components.
.rews format.actions declaration is ABRS-only. Each action is assigned a single non-negative integer reward. When a transition results from taking that action, the reward is paid once regardless of how many rule occurrences fired. Action rewards are exported in PRISM .trew format.BigraphER enforces the following constraints for ABRS models:
To explore a model's behaviour, BigraphER either computes the full transition system (Full exploration) or runs a random simulation (Simulation).
The full subcommand explores all reachable states and transitions:
Key options:
-M N sets the maximum state index: states are indexed from 0, so the transition system holds at most N + 1 states (default 1000).-t FILE and -f FORMAT export the transition system in dot, json, svg, txt, or tikz format.--metrics-json FILE writes run and matching metrics in JSON format, including the total solver time solver_time_ms (reported under all three backends) and the BRS family factoring statistics; see the manpage for the field list.For the complete option list, see the full manpage.
The matching engine supports three backends, selected by --solver:
MCARD (default) -- Optimised solver with built-in support for counting constraints. Generally the fastest choice.MSAT -- Standard SAT-based solver. Useful for comparison with MCARD.GBS -- Graph-based solver that uses subgraph isomorphism. May outperform the SAT-based solvers on models with large but structurally simple bigraphs.$ bigrapher full --solver=GBS model.bigFor most models, the default MCARD solver provides the best performance.
For stochastic model checking, BigraphER can export the transition system in PRISM format:
-p FILE exports the transition relation in .tra format.-r FILE exports state rewards in .rews format.-R FILE exports transition rewards in .trew format (for abrs models).-l FILE exports the labelling function in .csl format.$ bigrapher full -p model.tra -r model.rews model.bigFor abrs models, the .tra file encodes an MDP with choice indices per source state. Transition rewards from action rewards are exported via -R.
The sim subcommand performs a random walk through the state space rather than exploring all reachable states:
$ bigrapher sim --simulation-steps=100 model.bigThis is useful for large models where full exploration is infeasible, or for quick sanity checks. The simulation limit is controlled by different flags depending on the model type:
--simulation-steps (or -S) to set the simulation limit; the simulation stops once the step count exceeds it.--simulation-time (or -T) to set the simulation limit; the simulation stops once the accumulated time exceeds it.The simulated transition system is exported with the same options as full: -t FILE sets the destination file and -f FORMAT the format (dot, json, svg, txt, or tikz).
At each step, BigraphER finds all enabled rule occurrences, rewrites each to produce candidate successor states, merges occurrences that lead to the same successor, and samples one transition. The sampling strategy depends on the model type:
1 / |A|, where |A| is the number of enabled actions (actions whose total transition weight is zero are disabled and not considered). Within the chosen action, transitions are sampled proportionally to their probabilities, as in PBRS.This uniform action scheduler is a standard heuristic for MDP simulation (consistent with PRISM's default).
Simulation uses a pseudo-random number generator. By default, the seed is initialised from the system time, producing different traces on each run. To obtain reproducible results, use --seed:
$ bigrapher sim -S 100 --seed=42 model.bigThe same seed always produces the same trace. The seed controls both action selection (for abrs models) and transition sampling.
Additional simulation options:
-i FILE uses the JSON bigraph in FILE as the initial state instead of the one declared in the model.The interactive subcommand steps a model one rewrite at a time, showing the enabled rules and predicate match status at each state. It suits small models, teaching, and debugging rules by hand.
In a terminal, the session displays the current state and reads commands at a prompt. A rule name fires that rule; slash commands control the session:
$ bigrapher interactive --seed 42 examples/brs.big
Type: BRS
Bindings: 14
Rules: 3
Starting interactive session ...
Seed: 42
-------------------------------------------------------------------------------
State 0:
Matching predicates (none of 2):
Enabled rules:
close (1 occurrence)
duplicate (1 occurrence)
Type a rule name, /quit to quit or /help for all commands.
[0]> duplicate
Applied "duplicate" (state 0 -> 1)
-------------------------------------------------------------------------------
State 1:
Matching predicates (1 of 2):
has_d
No rules enabled (deadlock)
[1]> /quit
Exiting interactive mode.Each step samples one occurrence with the same selection policy as sim (Simulation). When a rule fires in more than one way, the step is annotated with the number of possible rewritings. The session prints its seed at start-up; pass it back with --seed to replay the same sequence of steps.
The available commands (also listed by /help):
/step name, fires the named rule, sampling one occurrence. In an SBRS model a named step is the path conditioned on the rule firing: the sojourn is drawn at the exit rate of the full class, as in a sampled step. /step alone samples one occurrence from the top priority class. /step --list shows every distinct successor of the rule, or of the top class, with full rendering, without stepping; /step name i commits to the i-th distinct successor of the named rule, the deterministic alternative to the sampled step./auto [n] steps n times (default 1), stopping at a deadlock./rules shows the enabled rules of the top priority class, the only class whose rules can currently fire. /rules --all lists every rule of every priority class: a rule with an occurrence in the current state shows its count, a rule with none is marked no match./preds reports the match status of every predicate in the current state; /preds <index> instead reads the labelling recorded for that state of the session path, so it always agrees with the exported transition system. /check <name> checks a single predicate (Tab completes the names after /check); a bare /check reports them all, and /check <index> <name> reads the recorded labelling for that state./history replays the session path: every step taken so far, with the rule fired, the number of possible rewritings, and the reducing rules auto-fired by each step./export [format] writes the session path as a transition system to trace files in the --export-path directory (default the current directory). A format argument selects one of txt, dot, prism, lab, srew, trew, svg, or json; a bare /export writes the session path in every --format format plus the PRISM formats (.tra, .csl, .rews, and .trew for ABRS models)./print [index] [format] writes a state from the session path to the --export-path directory (default the current directory), named by state index; the state defaults to the current one. A format argument selects one of txt, svg, dot, json, or tikz; a bare /print writes the state in every --format format./quit exits the session.When standard input is not a terminal, interactive switches to a machine-readable protocol: one JSON command per line on standard input, one JSON event per line on standard output. Commands are objects with a cmd field. The session below takes one step and quits:
$ bigrapher interactive --seed 42 examples/brs.big <<'JSON'
{"cmd":"step","name":"duplicate"}
{"cmd":"quit"}
JSONThe first event of a session is a session line carrying the seed, the model file (null when read from standard input), and the bigrapher version, so a saved NDJSON trace carries its provenance at the top; this run reports the initial state, the step, the deadlock, and the session summary:
{"type":"session","seed":42,"model":"examples/brs.big","version":"2.0.0~alpha"}
{"type":"state","index":0,"rules":[\
{"name":"close","occurrences":1},{"name":"duplicate","occurrences":1},\
{"name":"remove","occurrences":1,"reducing":true}],"predicates":[]}
{"type":"step","from":0,"to":1,"rule":"duplicate","occurrences":1,"reducing":[]}
{"type":"deadlock","index":1}
{"type":"summary","metrics":{ /* the --metrics-json record */ }}The command names are the TTY slash commands without the leading slash; the other fields are optional:
Command | Description |
|---|---|
| Step up to |
| Check a single predicate; an optional |
| Export the session path as a transition system; an optional |
| Return the command list as a |
| Replay the session path: every step taken so far, as a |
| Report the match status of every predicate. |
| Export a state from the session path; an optional |
| End the session. |
| List the enabled rules of the top priority class; an optional |
| Step one rule. An optional |
Events are objects with a type field. A state event lists the enabled rules with their occurrence counts (reducing marks reducing rules) and the matching predicates; a state with no enabled rules is reported as a deadlock event. A step event carries the sampled rule, the state indices, the number of possible rewritings, and the reducing rules auto-fired after the step. The rules, preds and check commands report their output as events of the same name, successors reports the distinct successors of a rule or of the top class, each with its full rendering, history reports the session path so far with one entry per step, print and export report the written files (one event per file), limit marks an auto run that used its step budget, and error carries a message on failure. A preds, check or print event for a past state carries the state's index. The last event of a session is a summary line carrying the run metrics — the record written by --metrics-json, nested under a metrics field — so a saved NDJSON trace ends with its own statistics. For the complete option list, see the manpage.
These sections cover parameterised definitions, variable scoping, elementary bigraphs, sharing, and constrained patterns.
Definitions can be parameterised using the keyword fun. Parameterised definitions are useful when a family of controls, bigraphs, or rules has the same structure but differs in some values.
fun ctrl Token(n) = 0;
fun big token(n) = Token(n).1;
fun react inc(n) = token(n) --> token(n + 1);
begin brs
int n = {0, 1};
init token(0);
rules = [ {inc(n)} ];
end$ bigrapher validate --quiet --warn-family=none examples/parameterised.big
OKThe keyword fun creates parameterised definitions. Here, fun ctrl Token(n) = 0; defines a parameterised control, fun big token(n) = Token(n).1; a parameterised bigraph, and fun react inc(n) = token(n) --> token(n + 1); a parameterised reaction rule that increments the token value for each n.
Inside the reactive system block, int n = {0, 1}; declares the values used to instantiate n. The rule declaration rules = [ {inc(n)} ]; then includes the corresponding rule instances in the priority class. Call arguments may be expressions over the BRS parameters: with n over two values and m over two values, rules = [ {r(n + 1, m + 10)} ]; produces the 2 \times 2 = 4 instances formed by applying the expressions to each domain value pair.
Parameter declarations appear inside the reactive system block and specify the concrete values for parameterised controls, bigraphs, and rules. The syntax is:
<type> <name>[, <name>, ...] = <values>;
where <type> is int, float, or string. Values can be a single expression, a brace-enclosed comma-separated list, or a range [<start>:<step>:<stop>] for int and float. Multiple parameter names can share the same value set.
Examples:
int n = {0, 1}; # Integer set
int bs = [0:1:b_max-1]; # Range from 0 to b_max-1
float rate = 0.5; # Single float value
string label = "x"; # Single string valueWarning. Parameter declarations generate one rule instance for each combination of parameter values: a parameterised rule with three parameters taking 5, 10, and 3 values respectively produces 5 \times 10 \times 3 = 150 rule instances, so use parameter values sparingly. A parameter is a domain of values, not a single value -- reading it where a value is expected is rejected (see the Variable n is a BRS parameter (a domain of values) entry in Common errors).
When a parameterised rule family varies one BRS parameter over exactly one control value on the left-hand side, BigraphER materialises the family as a single rule with a bracket guard that selects the domain values, instead of one rule per value. Factoring is automatic, preserves the transition system exactly, and has no command-line flag.
fun ctrl A(i) = 0;
fun ctrl B(i) = 0;
fun react r(k) = A(k).1 --> B(k + 1).1;
big s0 = A(2).1;
begin brs
int n = [1:1:5];
init s0;
rules = [ {r(n)} ];
end$ bigrapher full --no-colors -M 10 examples/factoring.big 2>&1 | grep -E 'Rules:'
Rules: 1In this example the parameter n also appears on the right-hand side, so the left-hand-side value position becomes a labelled capture (k: $ = 1 <= $ && $ <= 5) and the right-hand side references the capture in a value expression (B([[k + 1]]).1). Each factored family is named in an Info: Factored family ... line on standard error, shown with --verbose.
int domain becomes a range guard ([$ = 1 <= $ && $ <= 5]); any other int domain, and every float and string domain, becomes a disjunction of equalities.[$ = ...]), as in the constrained-parameter-pattern examples below.preds declaration is factored the same way: preds = [{p(n)}] over a qualifying family becomes one guarded predicate.A family does not qualify, and is enumerated one rule per value as before, when the parameter appears in a rule condition, in a rule or link label, in a parameterised bigraph call, or in two left-hand-side positions; when a call has more than one BRS parameter; or when the domain has fewer than three values. In the example corpus this cuts ABER_52's materialised rules from 125 to 115 (its incRank family) and rts_cts's from 487 to 475; the transition systems are unchanged.
Variables in BigraphER models can be declared at three levels, each with a distinct scope. When the same name appears at multiple levels, precedence rules determine which value is used.
The three declaration levels are:
int, float, string before begin brs) -- visible in all bigraph and reaction declarations in the model.int, float, string inside begin brs ... end) -- used to instantiate parameterised rules, bigraphs, and controls within the reactive system.-c name=value) -- the highest precedence, overriding any model-level declaration.When a name is declared at multiple levels, the following precedence applies (highest first):
-c)begin brs)begin brs)# Demonstrates BRS parameter overriding a global declaration.
# Without any override, the BRS-level int n = 3 takes precedence,
# producing four reachable states (par(3, A) -> par(3, B)).
atomic ctrl A = 0;
atomic ctrl B = 0;
int n = 2;
fun big s0(n) = par(n, A);
react r = A --> B;
begin brs
int n = 3;
init s0(n);
rules = [{r}];
end$ bigrapher validate --quiet examples/scoping-precedence.big 2>&1 | grep "W002"
Warning: W002 - Identifier n was already used at line 6, characters 0-9
1 warning (1 x W002)The global declaration sets n to 2, but the BRS parameter declaration int n = 3; takes precedence. The compiler emits a warning that n was already used. The initial state is s0(3), creating three A entities.
With a command-line override, the value can be changed without editing the model:
$ bigrapher full -M 10 -c n=5 examples/scoping-precedence.big 2>&1 | grep "States:"
States: 6With -c n=5, the initial state is par(5, A), creating five A entities. The rule A --> B converts one A to B at a time, producing six reachable states: 5A, 4A + 1B, 3A + 2B, 2A + 3B, 1A + 4B, 5B.
Multiple overrides are given as a comma-separated list:
$ bigrapher full -c "n=3,m=2" model.bigFormal parameters of fun definitions are local to the definition body. They are bound when the definition is called and do not interact with any global or BRS parameter of the same name:
# Demonstrates formal parameters of fun definitions are local to the body.
# The global n=10 is used by init; the formal n is used inside model().
atomic ctrl A = 0;
atomic ctrl B = 0;
int n = 10;
fun big model(n) = par(n, A);
react r = A --> B;
begin brs
init model(n);
rules = [{r}];
end$ bigrapher validate --quiet examples/scoping-formal.big
OKIn init model(n), the n refers to the global parameter (because it appears outside the definition). Inside the definition body of model, n refers to the formal parameter.
A frequent error is to declare a global parameter intending it to be used as an initial state value, but accidentally shadow it with a BRS parameter declaration:
# Demonstrates accidental shadowing: BRS param n=2 shadows global n=5.
# Produces three states (par(2, A) -> par(2, B)), not six.
atomic ctrl A = 0;
atomic ctrl B = 0;
int n = 5;
fun big s0(n) = par(n, A);
react r = A --> B;
begin brs
int n = 2;
init s0(n);
rules = [{r}];
end$ bigrapher full -M 10 examples/scoping-shadow.big 2>&1 | grep "States:"
States: 3The model produces three states (from par(2, A)), not six. The fix is either to remove the BRS parameter declaration (if the global value is the intended one), or to use a different name.
Declaration | Scope | Used in |
|---|---|---|
global | whole model | bigraph evaluation, init expressions |
BRS | BRS block | rule instantiation, init within BRS |
| definition body | the body of the |
captures ( | the rule | bound to the matched value; referenced on the RHS in a value expression ( |
| all | everything -- highest precedence |
BigraphER provides elementary bigraphs -- id, merge, split -- for constructing interfaces, placings, and wirings explicitly.
ctrl A = 1;
ctrl B = 1;
big names = id(1,{x}) * A{x}.1;
big closed = /x A{x}.1;
big renamed = x/{y} A{y}.1;
big two = A{x}.1 || B{x}.1;
big merged = merge * /x two;
big split_again = split * merged;
begin brs
init merged;
rules = [];
end$ bigrapher validate --quiet --warn-family=none examples/elementary.big
OKThe bigraph names composes id(1,{x}) -- an identity bigraph with one site and a propagating link name x -- with A{x}.1, placing the A-entity into the site while preserving the link interface.
The closure /x in closed hides the open name x in the following expression. Closure binds more tightly than merge product |, parallel product ||, tensor product +, and composition *.
The substitution x/{y} in renamed replaces y with x in the following expression.
The parallel product || in two places the entities in separate regions while sharing the common name x.
The bigraph merged composes merge with /x two. The elementary bigraph merge combines two regions into one.
The bigraph split_again composes split with merged. The elementary split is dual to merge: it divides one region into two.
All three accept an optional integer argument: id(2) is the identity on two sites, merge(3) merges three regions, and split(3) splits one region into three.
Bigraphs with sharing allow an entity to have more than one parent. BigraphER provides explicit placing syntax for describing place structure directly, and a share construct for introducing sharing.
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
ctrl D = 0;
big p = C.1 || D.1;
big psi = ([{0,1},{0}], 2);
big c = A | B;
big shared = share p by psi in c;
begin brs
init shared;
rules = [];
end$ bigrapher validate --quiet examples/sharing.big
OKThe placing psi uses explicit placing syntax ([parents], roots). The first component lists the parents of each site, the second gives the number of regions. In ([{0,1},{0}],2), the first site is shared by both regions while the second site has region 0 as its only parent.
The construct share p by psi in c builds a bigraph with sharing. The argument p is the placing to be shared, psi is the interface, and c is the context. In this example, C is shared by A and B, while D is nested inside A.
BigraphER provides iterated forms of merge product and parallel product. They are useful when the same bigraph must be repeated a fixed number of times.
ctrl A = 0;
ctrl B = 0;
big many_a = par(3, A.1);
big many_b = ppar(2, B.1);
big b = many_a | many_b;
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet examples/iterated.big
OKThe expression par(3, A.1) builds the merge product of three copies of A.1 as siblings in the same region. The expression ppar(2, B.1) builds the parallel product of two copies of B.1 in separate regions. In both cases, the first argument is the number of copies, the second is the bigraph to repeat.
Parameterised controls can be matched using parameter patterns. A pattern such as Token([x]) matches a Token and binds its parameter to the capture x.
fun ctrl Token(v) = 0;
ctrl Zero = 0;
ctrl Positive = 0;
ctrl Other = 0;
big zero = Token(0).1;
big one = Token(1).1;
big two = Token(2).1;
react is_zero =
Token([$ = 0]).1 --> Zero.1;
react is_positive =
Token([$ > 0]).1 --> Positive.1;
react is_small =
Token([$ <= 2]).1 --> Other.1;
big s0 = zero | one | two;
begin brs
init s0;
rules = [ {is_zero, is_positive, is_small} ];
end$ bigrapher validate --quiet examples/constraints.big
OKA constrained parameter pattern has the form [$ = constraint]: the symbol $ refers to the matched value, and the constraint must hold for the rule to match. No name is bound, so this form is enough for most guards. For example, Token([$ = 0]) matches a token whose value is 0, and Token([$ + 1 <= 5]) matches a token whose value plus 1 is at most 5. The legacy form [x, constraint] is no longer parsed; use [$ = constraint] for a nameless guard, and [x: $ = constraint] when the name is used elsewhere in the rule.
Label the capture when the matched value is needed elsewhere in the rule: the form [x: $ = constraint] checks the constraint and binds the capture x to the matched value. A label is only necessary when x is referenced on the right-hand side or inside its own constraint; otherwise the nameless form is simpler. The bare pattern [x] binds x without any constraint.
A labelled capture is referenced on the right-hand side inside a value expression, written with double brackets. For example, Token([x: $ <= 2]).1 --> Token([[x + 1]]).1 rewrites a token of value at most 2 into a token of value x + 1. A value expression can also reference the model's global values, and it supports the absolute value function abs, for example Token([[abs(x) - 2]]).1.
A capture name is not a value in its own right, so it cannot be written bare in a right-hand-side control argument: Token([x]).1 --> Token(x).1 is rejected at validate time, because x has no value before the rule matches. The right-hand side needs Token([[x]]).1 to use the captured value. A bare name in a control argument refers to a global value instead; a global int, float or string declared with the same name as a capture is legal and shadows the capture.
When the same capture appears at more than one parameter position in a rule's left-hand side, it binds to a single value. The rule fires only if the values matched at all of those positions agree, and the capture then takes that value on the right-hand side. If the matched values differ, the rule has zero occurrences in that bigraph -- even when the constraint at each position holds. The single-value check is independent of, and in addition to, the per-position constraints.
The degenerate-guard check (W022/W023) is a complete decision only for guards that are linear in the matched value: $ may occur at most to the first power, combined with constants by +, - and by multiplication or division by a constant.
abs is admitted: a guard linear apart from abs is decided by a split into the sign cases of each abs argument, so [abs($) = -1] is always false and [abs($) >= 0] always true.abs -- such as $ * $ > 1 or [abs($) * abs($) > 1] -- is still matched at run time, but is reported as warning W024 (see the Warnings section).^ is not permitted in a guard at all.The literals in a constraint are type-checked against the matched value by the same mechanism that types control arguments, so a constraint such as [$ >= 3.5] on an int-typed value is a type error.
BigraphER also decides statically whether a constraint can ever be satisfied. The decision is domain-aware: for an int-typed value the constraint is decided over the integers, so $ > 3 && $ < 4 admits no integer and is always false; for a string-typed value the constraint is decided over the string constants it contains plus the class of all other strings, which covers every value because a string constraint can only test equality and disequality; for any other value it is decided over the reals, where the same constraint holds 3.5. A constraint that is provably always true or always false is reported as warning W022; several brackets bound to the same variable whose constraints admit no common value are reported as W023.
BigraphER can report warnings about potential issues in your models. Warnings are non-fatal: the run proceeds and exits successfully. Each warning is printed with the relevant source location, in the form Warning: Wnnn - message, where Wnnn identifies the warning's family; when at least one warning has been reported, a one-line summary, for example 3 warnings (2 x W001, 1 x W004), is printed at the end of the run.
Warnings are grouped into families. They are enabled by default in validate and disabled by default in full and sim; use --warnings (or -w) to enable them in full and sim -- the lint families stay off there unless selected individually. Use --warn-family to select specific families, and none to suppress all warnings. The warnings page lists every family and explains how the flags combine.
These are frequent errors when writing BigraphER models, with their cause and fix.
The initial bigraph must be fully formed, meaning it cannot contain sites. This error usually occurs when a non-atomic entity is written without specifying its content:
ctrl A = 0;
big s0 = A;
begin brs
init s0;
rules = [];
end$ bigrapher validate --quiet examples/err-init-not-ground.big 2>&1 | grep -o 'Error:.*'
Error: Init bigraph is not ground.Fix: put an empty bigraph 1 in place of the implicit site:
ctrl A = 0;
big s0 = A.1;
begin brs
init s0;
rules = [];
end$ bigrapher validate --quiet examples/err-fix-init-ground.big
OKThe number of sites on the left-hand side of a rule must match the number of sites on the right-hand side, unless an instantiation map is provided. For example, the rule below has two sites on the left (A.id and B.id) but only one on the right (C.id):
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
react r = A.id | B.id --> C.id;
big s0 = A.1 | B.1;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-inner-interfaces.big 2>&1 | grep -o 'Error:.*'
Error: Invalid Reaction: Inner interfaces <2, {}> and <1, {}> do not match..Fix: either make the site counts equal, or add an instantiation map specifying how each right-hand site maps to a left-hand site:
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
react r = A.id | B.id --> C.id @[0];
big s0 = A.1 | B.1;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-fix-inner-interfaces.big
OKThe outer interface -- number of regions and open names -- must be preserved during a rewrite. Open names cannot be dropped, nor can regions disappear. For example:
ctrl A = 1;
react r = A{x}.1 --> 1;
big s0 = A{x}.1;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-outer-interfaces.big 2>&1 | grep -o 'Error:.*'
Error: Invalid Reaction: Outer interfaces <1, {x}> and <1, {}> do not match..Fix: if an open name is no longer needed, keep it idle on the right:
ctrl A = 1;
react r = A{x}.1 --> {x} | 1;
big s0 = A{x}.1;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-fix-outer-interfaces.big
OKThe instantiation map must have one entry for each site on the right-hand side, and each entry must refer to a valid site index on the left-hand side. For example, a map @[0, 5] is invalid if the left-hand side has only one site (index 0):
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
react r = A.id --> B.id | C.id @[0, 5];
big s0 = A.1;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-instantiation-map.big 2>&1 | grep -o 'Error:.*'
Error: Invalid Reaction: Instantiation map is not valid..Fix: ensure the map length matches the number of right-hand sites and all entries point to valid left-hand site indices:
ctrl A = 0;
ctrl B = 0;
ctrl C = 0;
react r = A.id --> B.id | C.id @[0, 0];
big s0 = A.1;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-fix-instantiation-map.big
OKAtomic controls do not allow any nesting below them. This error occurs when an atomic entity is used as a parent:
ctrl A = 0;
atomic ctrl Sensor = 0;
big b = Sensor.A.1;
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet examples/err-atomic-nesting.big 2>&1 | grep -o 'Error:.*'
Error: Control Sensor is atomic but it is here used in a nesting expression.Fix: use a non-atomic control for entities that nest other entities:
ctrl A = 0;
ctrl Sensor = 0;
big b = Sensor.A.1;
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet examples/err-fix-atomic-nesting.big
OKThe arity declared for a control must match how many distinct link names are connected to it in bigraph expressions. For example:
ctrl A = 0;
big b = A{x}.1;
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet examples/err-arity-mismatch.big 2>&1 | grep -o 'Error:.*'
Error: Control A has arity 0 but a control of arity 1 was expected.Fix: either increase the arity or remove the link:
ctrl A = 1;
big b = A{x}.1;
begin brs
init b;
rules = [];
end$ bigrapher validate --quiet examples/err-fix-arity-mismatch.big
OKWhen you call a parameterised bigraph, control, or reaction rule, the types of the arguments must match what the definition expects. BigraphER infers parameter types from first use, so inconsistencies appear when different calls use different types:
ctrl Token = 0;
fun ctrl Token(n) = 0;
fun big token(n) = Token(n).1;
big s0 = token(0);
begin brs
int n = {0, 1};
init token(3.14);
rules = [];
end$ bigrapher validate --quiet examples/err-type-mismatch.big 2>&1 | grep -A1 'Error:.*'
Error: This big expects arguments of type [int].
It was called with arguments of type [float].The call token(0) binds n to int. The later call token(3.14) passes a float, which cannot unify.
Fix: use consistent types across all calls:
ctrl Token = 0;
fun ctrl Token(n) = 0;
fun big token(n) = Token(n).1;
big s0 = token(0);
begin brs
int n = {0, 1};
init token(0);
rules = [];
end$ bigrapher validate --quiet examples/err-fix-type-mismatch.big 2>&1 | grep -o 'OK'
OKA BRS parameter declared with a range or set is a domain of values, not a single value. It is instantiated over its domain when passed to a parameterised declaration (fun react / fun big), including inside an argument expression such as r(n + 1). It is rejected when read as a single value inside a bracket, for example in a guard [$ = n]:
atomic fun ctrl A(i) = 0;
atomic ctrl B = 0;
react r = A([$ = n]) --> B;
big s0 = A(0);
begin brs
int n = [0:1:2];
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-param-as-value.big 2>&1 | grep -o 'Error:.*'
Error: Variable n is a BRS parameter (a domain of values) and cannot be used where a single value is expected. BRS parameters are only instantiated over their domain when passed to a parameterised declaration (fun react / fun big); to use a single value, declare a plain int, float or string instead.Fix: if you need a single value, declare it as a plain int, float, or string outside the brs section, rather than a BRS parameter:
atomic fun ctrl A(i) = 0;
atomic ctrl B = 0;
int n = 5;
react r = A([$ = n]) --> B;
big s0 = A(0);
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-fix-param-as-value.big
OKA capture name is not a value before the rule matches, so it cannot be written bare in a right-hand-side control argument:
atomic fun ctrl Tok(s) = 0;
big s0 = Tok("a");
react r = Tok([x]) --> Tok(x);
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-unbound-capture.big 2>&1 | grep -o 'Error:.*'
Error: Name x is a capture bound on the left-hand side of this rule, not a value: a capture has no value before the rule matches. Use [[x]] in the right-hand side to refer to the captured value; a global int, float or string of the same name is legal and shadows the capture.Fix: refer to the captured value with a value expression:
atomic fun ctrl Tok(s) = 0;
big s0 = Tok("a");
react r = Tok([x]) --> Tok([[x]]);
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-fix-unbound-capture.big
OKBrackets are pattern constructs: they are only meaningful in a reaction left-hand side or a condition. Using one where a value is expected, for example in a bigraph definition, is rejected:
atomic fun ctrl Token(i) = 0;
int k = 2;
big s0 = par(1, Token([$ = k]));
react r = Token([x]) --> Token(3);
begin brs
init s0;
rules = [{r}];
end$ bigrapher validate --quiet examples/err-bracket-in-value.big 2>&1 | grep -o 'Error:.*'
Error: A bracket pattern cannot be used where a control value is expected. Brackets are pattern constructs: they are only meaningful in a reaction left-hand side or a condition, where they are matched against the state.Fix: use a value, such as the global k:
atomic fun ctrl Token(i) = 0;
int k = 2;
big s0 = par(1, Token(k));
react r = Token([x]) --> Token(3);
begin brs
init s0;
rules = [{r}];
end$ bigrapher validate --quiet examples/err-fix-bracket-in-value.big
OKA guard may only refer to its own value -- via $ or its own capture name -- and to constants. A guard that reads another bracket's capture couples the guards into a system of equations the matcher cannot solve soundly, so the rule is rejected:
atomic fun ctrl Token(v) = 0;
big s0 = Token(1) | Token(3);
react m = Token([x: $ <= 2]) | Token([y: $ = x]) --> Token([[x+y+1]]);
begin brs
init s0;
rules = [ {m} ];
end$ bigrapher validate --quiet examples/err-guard-crossref.big 2>&1 | grep -o 'Error:.*'
Error: Guard references another bracket's capture: x. A guard may only refer to its own value (via $ or its own capture name) and to constants; to relate two captures, use an RHS value expression [[...]].Fix: keep the guards independent; to relate the two captures, use an RHS value expression:
atomic fun ctrl Token(v) = 0;
big s0 = Token(1) | Token(3);
react m = Token([x: $ <= 2]) | Token([$ <= 2]) --> Token([[x+1]]);
begin brs
init s0;
rules = [ {m} ];
end$ bigrapher validate --quiet examples/err-fix-guard-crossref.big
OKA bracket guard compares values with <, <=, > and >= only for numbers; strings support only = and !=. Ordering strings is rejected at validate time:
atomic fun ctrl Tok(s) = 0;
atomic ctrl Done = 0;
big s0 = Tok("a");
react r = Tok([$ > "b"]) --> Done;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-string-order.big 2>&1 | grep -o 'Error:.*'
Error: Strings cannot be ordered. A bracket guard compares values with <, <=, >, >= only for numbers; use = or != for strings.Fix: test equality or disequality; arithmetic applies only to numbers:
atomic fun ctrl Tok(s) = 0;
atomic ctrl Done = 0;
big s0 = Tok("a");
react r = Tok([$ = "b"]) --> Done;
begin brs
init s0;
rules = [ {r} ];
end$ bigrapher validate --quiet examples/err-fix-string-order.big
OK