Command-line reference
NAME
bigrapher-validate - Parse a model and check its validity.
SYNOPSIS
bigrapher validate [OPTION]… [FILE]
ARGUMENTS
FILE
Input model. Read from stdin if omitted.
OPTIONS
-c ASSIGNMENT, --const=ASSIGNMENT
Specify a comma-separated list of variable assignments. Example:
x=4,t=.56.
-d DIR, --export-decls=DIR
Export each declaration to a file in DIR. Output formats are
specified by option --format. The directory is created if it does
not exist.
--debug
Print extra diagnostic information (e.g. internal statistics).
Disables coloured output.
-f FORMAT, --format=FORMAT (absent=dot or BIGFORMAT env)
A comma-separated list of output formats. Supported formats are
dot, json, svg, txt, and tikz. Flag --tikzconf allows to configure
TikZ export.
-n, --no-colors (absent NO_COLOR env)
Disable colored output.
-q, --quiet (absent BIGQUIET env)
Suppress output; prints OK on success. Flag --verbose is ignored
if set.
--tikzconf=FILE
Configuration for TikZ export in json format.
-v, --verbose (absent BIGVERBOSE env)
Print file output status messages (exporting, saving) and
operational detail (e.g. file sizes). By default only errors and
results are printed.
-w, --warnings
Enable all warning families. Use --warn-family for fine-grained
control over individual families.
--warn-family=FAMILIES
Enable specific warning families (comma-separated, e.g.
W001,W003). Takes precedence over --warnings. Can be used in any
command (including format). Use 'none' to disable all warnings
(e.g. --warn-family=none).
COMMON OPTIONS
--help[=FMT] (default=auto)
Show this help in format FMT. The value FMT must be one of auto,
pager, groff or plain. With auto, the format is pager or plain
whenever the TERM env var is dumb or undefined.
--version
Show version information.
EXIT STATUS
bigrapher validate exits with:
0 on success.
1 on model errors (parse, validation, type, flag mismatch), export
failures, or missing external dependencies (e.g. `dot').
124 on command line parsing errors.
125 on unexpected internal errors (bugs).
ENVIRONMENT
These environment variables affect the execution of bigrapher
validate:
BIGFORMAT
A comma-separated list of output formats. Supported formats are
dot, json, svg, txt, and tikz. Flag --tikzconf allows to configure
TikZ export.
BIGQUIET
Suppress output; prints OK on success. Flag --verbose is ignored
if set.
BIGVERBOSE
Print file output status messages (exporting, saving) and
operational detail (e.g. file sizes). By default only errors and
results are printed.
NO_COLOR
Disable colored output.
EXAMPLES
Validate a model:
bigrapher validate model.big
Validate silently (prints OK on success):
bigrapher validate --quiet model.big
Export declarations as TikZ with custom configuration:
bigrapher validate -f tikz -d out/ --tikzconf=config.json model.big
GRAPHVIZ EXPORT
The options --export-states and --export-decls produce output in
GraphViz DOT format or SVG, controlled by the --format flag.
DOT files (.dot) are plain-text graph descriptions. SVG files (.svg)
are vector graphics generated by running the dot layout engine on the
DOT output.
For SVG export, GraphViz must be installed on the system.
Examples:
bigrapher full --export-states=out -f svg model.big
bigrapher validate --export-decls=out -f dot model.big
See also https://graphviz.org/ for GraphViz documentation and tools.
TikZ CONFIGURATION
The --tikzconf option accepts a JSON file with the following fields:
{
"spacing": 1.0, // horizontal node spacing
"link_step_size": 50, // port separation angle (degrees)
"numerical_instmap": false, // use numeric instantiation maps
"vertical_rules": false // draw rules vertically
}
WARNING FAMILIES
BigraphER reports warnings about model issues. Warnings are grouped
into families, each identified by a code (e.g. W001).
By default, warnings are disabled in all commands except validate,
where all families are enabled. --warnings (alias -w) enables all
warning families. --warn-family enables only the specified families
(comma-separated, e.g. --warn-family=W001,W003). If both flags are
given, --warn-family takes precedence. --warn-family can be used in
any command (including format). Use 'none' to disable all warnings.
W001
Unused declarations -- A reaction rule, control, or bigraph
binding is defined but never used.
W002
Multiple declarations -- An identifier was declared more than
once.
W003
No rules enabled from initial state -- The model will produce no
transitions. Only reported during full and sim.
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 may cause combinatorial
explosion with parameterised declarations.
W008
Combinatorial explosion -- A parameterised declaration (fun react,
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, making the rule
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 [$ = C] (or [v: $ = C]
when the capture is labelled) is provably always true (the
captured value always satisfies it, so the guard is redundant) or
always false (no value satisfies it, so 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 [$ = C] (or [v: $ = C]
when the capture is labelled) is not affine in the captured value
(it contains products or divisions of terms that reference the
value). The guard is still matched at run time, but the W022/W023
degenerate-guard check cannot analyse it.
Warning family W003 is only reported during transition system
computation (full and sim), since it requires a computed transition
system to determine whether any rules are enabled from the initial
state.
SEE ALSO
bigrapher(1)