Warning families

Warnings are grouped into families, each identified by a code. W003 needs the transition system to have been computed, so it is reported only by full and sim; every other family is checked when the model is read, without any exploration.

• W001 Unused declarations. A reaction rule, control, or bigraph is defined but never used.
• W002 Multiple declarations. An identifier is declared more than once.
• W003 No rules enabled from initial state. No rule can fire from the initial state, so the model will produce no transitions.
• W004 Trivial instantiation map. An instantiation map is the identity map, which is implicit and therefore unnecessary.
• W005 CLI override. A value provided via --const overrides a declaration in the model.
• W006 Unused numeric declarations. An integer, float, string, or parameter declaration is defined but never used.
• W007 Large parameter domain. A parameter domain (range or set) generates many values (>50), which can cause combinatorial explosion when used with parameterised declarations.
• W008 Combinatorial explosion. A parameterised declaration (fun react or fun big) is instantiated over BRS parameter domains whose product of sizes is large, materialising many rules.
• W009 Large rule LHS. A rule's left-hand side is large (size >=50), which is expensive to match.
• W012 Identity rewrite step. A reaction rule's LHS and RHS are isomorphic, so the rewrite step produces no structural change.
• W014 Contradictory conditions. The same predicate appears both positively and negatively in a rule's conditions, so the rule can never fire.
• W015 Unused parameters. A functional rule (fun react or fun big) declares parameters that are not used in its body, rate, or conditions.
• W018 Excessive condition count. A rule has an unusually large number of conditions (>=5), which may indicate it is overly complex.
• W020 Duplicate conditions. The same condition appears multiple times in a rule's conditions, which is redundant.
• W022 Degenerate bracket guard. A bracket guard is provably always true (the guard is redundant) or always false (the rule can never fire). Feasibility is decided over the integers when the captured value is int-typed, over the reals otherwise; a guard that is linear apart from an absolute value of the captured value is also decided, by a split into the sign cases of each abs. A string-typed guard, which can only compare the captured value for equality, is decided over the string constants it contains plus the class of all other strings.
• W023 Jointly unsatisfiable bracket guards. A rule has multiple brackets capturing the same value, and their guards together can never all be satisfied by a single value, so the rule can never fire.
• W024 Non-linear bracket guard. A bracket guard is not affine in the captured value, i.e. the value is multiplied or divided by a term that also depends on it (such as [$ * $ > 1]). The guard is still matched at run time, but the W022/W023 degenerate-guard check cannot analyse it. See the example below.

Examples

Each example below is a complete model that triggers exactly one warning, and the command that reports it.

A model with no transitions (W003)

W003 is the only family reported only by full and sim: it needs the initial state to have been matched. Here the rule requires a B in context, but the initial state holds only an A; every static check passes, so validate says nothing:

ctrl A = 0;
ctrl B = 0;

react r = B --> A;

big s0 = A.1;

begin brs
  init s0;
  rules = [{r}];
end

$ bigrapher full --quiet --warn-family=W003 -M 5 --solver=MCARD examples/err-no-rules-enabled.big 2>&1 | grep W003
Warning: W003 - No rules are enabled from the initial state. The model will produce no transitions.
1 warning (1 x W003)

Either the initial state or the rule's left-hand side is wrong.

Too many instantiated rules (W008)

A functional declaration is instantiated once per tuple of parameter values: three domains of 11 values each materialise 1331 rules.

ctrl Entity = 0;

fun react process(a, b, c) = Entity --> Entity;

big s0 = Entity.1;

begin brs
  int a = [0:1:10];
  int b = [0:1:10];
  int c = [0:1:10];
  init s0;
  rules = [{process(a, b, c)}];
end

$ bigrapher validate --quiet --warn-family=W008 examples/err-combinatorial-explosion.big 2>&1
File "err-combinatorial-explosion.big", line 12, characters 12-28:
  rules = [{process(a, b, c)}];
            ^^^^^^^^^^^^^^^^
Warning: W008 - Declaration 'process' is instantiated over BRS parameter domains whose product of sizes is 1331 (> 1000), materialising that many rules. Consider shrinking the domains or reducing the number of parameterised arguments.
OK
1 warning (1 x W008)

Here the parameters are not used anywhere (which W015 also flags), so a plain non-functional rule expresses the same model with one rule; more generally, a family whose parameters are used in bracket guards or rates may be folded into fewer bracket-guarded rules by the BRS family factoring (see the factoring counters of --metrics-json).

A rule that changes nothing (W012)

The LHS and RHS of the rule are isomorphic, so firing it produces no structural change:

ctrl A = 0;

react r = A.1 --> A.1;

big s0 = A.1;

begin brs
  init s0;
  rules = [{r}];
end

$ bigrapher validate --quiet --warn-family=W012 examples/err-identity-rewrite.big 2>&1
File "err-identity-rewrite.big", line 3, characters 0-21:
react r = A.1 --> A.1;
^^^^^^^^^^^^^^^^^^^^^
Warning: W012 - Reaction rule 'r' has isomorphic LHS and RHS, so the rewrite step produces no structural change.
OK
1 warning (1 x W012)

If the rule is meant to do something, its right-hand side is probably wrong; if it is deliberate, silence the family with --warn-family.

A rule that can never fire (W014)

The same predicate, G in ctx, appears both positively and negatively in the rule's conditions:

ctrl A = 0;
ctrl B = 0;
ctrl G = 0;

react r = A --> B if G in ctx, !G in ctx;

big s0 = A.1;

begin brs
  init s0;
  rules = [{r}];
end

$ bigrapher validate --quiet --warn-family=W014 examples/err-contradictory-conditions.big 2>&1
File "err-contradictory-conditions.big", line 5, characters 31-40:
react r = A --> B if G in ctx, !G in ctx;
                               ^^^^^^^^^
Warning: W014 - Reaction rule 'r' has contradictory conditions: the same predicate appears both positively (at line 5, characters 21-29) and negatively, making the rule never fire.
OK
1 warning (1 x W014)

One of the two conditions must be dropped, or made about a different predicate.

A non-linear bracket guard (W024)

The W022/W023 checks decide a guard over the value matched at the bracket, and are complete only for guards that are affine in that value. A guard is affine when the captured value appears only to the first power, i.e. each comparison has the form a * $ + b < c (a constant coefficient and offset, with any comparison operator), possibly under abs: i.e. [$ > 1], [2 * $ + 3 < 10] or [abs $ <= 4]. The values that satisfy such a guard form a finite union of intervals, so tautology and unsatisfiability are decided exactly. A guard is non-linear when the value is combined with itself, i.e. multiplied or divided by a term that also depends on it, such as [$ * $ > 1] (the value squared); the check cannot decide it and reports W024 instead. The guard is still evaluated normally at run time:

atomic fun ctrl Token(v) = 0;
atomic ctrl Done = 0;

react r = Token([$ * $ > 1]) --> Done;

big s0 = Token(2);

begin brs
  init s0;
  rules = [ {r} ];
end

$ bigrapher validate --quiet examples/err-guard-nonlinear.big 2>&1 | grep "W024"
Warning: W024 - Reaction rule 'r' has a non-linear guard on the [$ * $ > 1] bracket (the guard is not affine in the captured value); the guard is still matched at run time, but is not analysed by the W022/W023 degenerate-guard check.
1 warning (1 x W024)

The guard is affine again once the value stays to the first power:

atomic fun ctrl Token(v) = 0;
atomic ctrl Done = 0;

react r = Token([$ > 1]) --> Done;

big s0 = Token(2);

begin brs
  init s0;
  rules = [ {r} ];
end

$ bigrapher validate --quiet examples/err-fix-guard-nonlinear.big 2>&1 | grep -o 'OK'
OK

Controlling warnings

Warnings are controlled by two flags:

• By default, warnings are reported only by validate, with every family enabled. full, sim, interactive, and format report none.
• --warnings (or -w) enables all families, on full and sim as well. The families other than W001, W002, and W003 are lint checks; they stay off on full and sim even with --warnings, to keep exploration output free of lint noise, unless they are selected individually with --warn-family.
• --warn-family selects specific families by code (e.g. --warn-family=W001,W022); it takes precedence over --warnings, and --warn-family=none disables all warnings. W003 is reported only by full and sim, even when selected.