Command-line reference

NAME
       bigrapher-interactive - Explore a model interactively, choosing at
       each step which rule to apply.

SYNOPSIS
       bigrapher interactive [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 in GraphViz DOT format.
           The directory is created if it does not exist.

       -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.

       -i FILE, --initfile=FILE
           Use bigraph specified in FILE as the initial state. Input is
           assumed to be in json format.

       --metrics-json=FILE
           Output run metadata, execution statistics, and matching metrics as
           JSON to FILE.

       -n, --no-colors (absent NO_COLOR env)
           Disable colored output.

       --no-inst
           Treat reducing (instantaneous) rules as non-instantaneous: they
           must be explicitly chosen rather than auto-firing after each step.

       --no-preds
           Disable automatic predicate checking on each state.

       -q, --quiet (absent BIGQUIET env)
           Suppress normal output. In a TTY session, suppresses the state
           display and all feedback messages (only the prompt remains); the
           pipe protocol is unaffected. Model-loading messages are suppressed
           in all modes.

       -s DIR, --export-path=DIR
           Directory for the files written by the /print and /export
           commands. /print uses state indices as file names; /export writes
           the session trace as a trace file. The directory is created if it
           does not exist. The current directory is used when omitted.

       --seed=INT
           Initialise the pseudo-random number generator using INT as seed.
           Used by sim and interactive, which sample their rewrite steps.

       --solver=VAL (absent=MCARD or BIGSOLVER env)
           Select solver for matching engine. Supported solvers are MSAT
           (SAT), MCARD (cardinality), and GBS (graph-based).

       --tikzconf=FILE
           Configuration for TikZ export in json format.

       -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).

       --wildcard-threshold=INT (absent=3)
           Threshold for matching strategy selection. For groups with fewer
           than INT rules, each rule is matched independently; larger groups
           use a more efficient batch matching strategy. Default is 3.

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 interactive 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
       interactive:

       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 normal output. In a TTY session, suppresses the state
           display and all feedback messages (only the prompt remains); the
           pipe protocol is unaffected. Model-loading messages are suppressed
           in all modes.

       BIGSOLVER
           Select solver for matching engine. Supported solvers are MSAT
           (SAT), MCARD (cardinality), and GBS (graph-based).

       NO_COLOR
           Disable colored output.

EXAMPLES
       It lets the user build a simulation of the reactive system by choosing
       at each step which rewrite rule to apply, as opposed to a randomly
       picked one in sim mode:

         bigrapher interactive model.big

       Each step samples one occurrence according to the model's semantics
       (uniform for BRS, weight- or rate-proportional for PBRS, ABRS, and
       SBRS). The seed is shown at session start (banner in TTY mode,
       {"type":"session"} line in pipe mode); pass it back with --seed to
       replay the same session:

         bigrapher interactive --seed=42 model.big

       Pipe mode for external tools (one JSON command per line on stdin, one
       JSON event per line on stdout):

         echo '{"cmd":"step","name":"swap"}' | bigrapher interactive model.big

       Show the distinct successors of a rule before stepping (no state
       change); commit to one with the "nth" field:

         echo '{"cmd":"step","name":"swap","list":true}' | \
         bigrapher interactive model.big

       Replay the session path taken so far (one JSON event per step):

         echo '{"cmd":"history"}' | bigrapher interactive model.big

       Export the session path as a transition system (a format argument
       selects a single format; without it, every --format and PRISM format
       is written):

         echo '{"cmd":"export","format":"dot"}' | \
         bigrapher interactive --export-path=out --format=dot,svg model.big

       Treat reducing rules as normal rules (no auto-fire):

         bigrapher interactive --no-inst model.big

       Disable automatic predicate checking on each state:

         bigrapher interactive --no-preds model.big

PIPE PROTOCOL
       When standard input is not a terminal, the session reads one JSON
       command object per line on standard input and writes one JSON event
       per line on standard output. A command is an object with a cmd field;
       the command names are the slash commands of the terminal session
       without the leading slash, and the other fields are optional:

       auto
           Step up to n times (default 1), stopping at a deadlock.

       check
           Check a single predicate; name selects it; without it, all
           predicates are checked; with index, the answer is read from the
           labelling recorded for that state.

       export
           Export the session path as a transition system; format selects
           txt, dot, prism, lab, srew, trew, svg or json; without it, every
           --format format is written plus the PRISM formats (.tra, .csl,
           .rews, and .trew for ABRS models). Files go to the --export-path
           directory, the current directory when omitted.

       help
           Return the command list as a help event.

       history
           Replay the session path: every step taken so far, as a history
           event.

       preds
           Report the match status of every predicate.

       print
           Export a state from the session path; index selects it (default:
           the current state); format selects txt, svg, dot, json or tikz;
           without it, every --format format is written. Files go to the
           --export-path directory, the current directory when omitted.

       quit
           End the session.

       rules
           List the enabled rules of the top priority class; all (boolean,
           default false) lists every rule of every class.

       step
           Step one rule. name selects the rule; without it, one occurrence
           is sampled from the top priority class. A named SBRS step is the
           path conditioned on the rule firing: the successor is drawn from
           the rule's occurrences and the sojourn at the exit rate of the
           full class. With list (boolean), no step is taken: the distinct
           successors of the rule, or of the top class, are reported with
           full rendering as a successors event. With nth, the step commits
           to the nth distinct successor of the named rule (1-based).

       Events are objects with a type field. The first event of a session is
       session and carries the seed. state reports the enabled rules and the
       matching predicates; step the sampled rule, the state indices, the
       occurrence count and the auto-fired reducing rules; successors the
       distinct successors of a rule or of the top class, each with its full
       rendering; rules, preds and check the output of the same-named
       commands; history the session path so far, one entry per step; print
       and export the written files (one event per file); limit an auto run
       that used its step budget; and deadlock a state with no enabled rules.
       A preds, check or print event for a past state carries the state's
       index. Failures are reported as error events carrying a message field.

STATE AND DECLARATION EXPORT
       The /print command exports a state from the session path and the
       /export command exports the session trace, both into the directory
       given by --export-path, the current directory when omitted; the state
       defaults to the current one. /print with a format argument selects one
       of dot, svg, txt, json, or tikz; without it, it writes the state in
       every format given by --format. /export with a format argument writes
       the trace in that format; without it, it writes the trace in every
       --format format plus the PRISM formats (.tra, .csl, .rews, and .trew
       for ABRS models). --export-decls exports each declaration in GraphViz
       DOT format.

       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.

         /print svg

       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
       }

MATCHING METRICS
       The --metrics-json option writes a JSON file with run metadata,
       execution statistics, and accumulated statistics across all matching
       calls in the run. It is the machine-readable superset of the --debug
       and --debug-extra output, and of the summary an interactive session
       prints at exit. Example output of a full run:

       {
         "type": "BRS", // reaction system kind: BRS, PBRS, SBRS or ABRS
         "execution": "full", // command: full, sim, or interactive
         "model": "ccs.big", // model file (null when read from stdin)
         "version": "2.0.0~alpha", // bigrapher version
         "solver": "MiniCARD", // MiniSAT, MiniCARD, or Glasgow Subgraph Solver
         "rules": 1, // number of rules in the run
         "seed": null, // simulation seed (sim runs and interactive sessions)
         "max_states": 1000, // -M bound (full runs only)
         "max_sim_steps": null, // -S bound (sim runs only)
         // how the run ended: exhausted | state_limit, limit | deadlock, quit
         "terminated": "exhausted",
         "time": 0.0009, // run time in seconds
         "states": 3, // number of states in the transition system
         "transitions": 2, // number of transitions
         "occurrences": 2, // rule occurrences applied
         "rules_fired": 1, // distinct rules that fired at least once
         "rules_factored_families": 0, // fun react instantiations factored into guarded rules
         "rules_not_materialised": 0, // enumeration rules replaced by the factored rules
         "predicates_factored_families": 0, // fun big instantiations factored into guarded bases
         "predicates_not_materialised": 0, // enumeration members subsumed by the guarded bases
         "mean_state_size": 6.0, // mean state size (null when not collected)
         "max_state_size": 6.0, // largest state size (null when not collected)
         "mean_match_size": 5.0, // mean size of the matches
         "state_table": { // transition table statistics (null for interactive)
           "bindings": 3,
           "buckets": 64,
           "max_bucket": 1
         },
         "filtered_occs": 2, // occurrences after symmetry filtering
         "solver_vars": 118, // total SAT variables across all encodings
         "solver_clauses": 372, // total SAT clauses across all encodings
         "solver_max_enc": 42, // largest single encoding (variables)
         "solver_max_clauses": 174, // largest single encoding (clauses)
         "solver_matches": 4, // number of SAT encoding calls
         "solver_time_ms": 0.4, // total solver time in ms
         "trivial_matches": 0 // matches resolved without SAT
       }

       Options that do not apply to the command are set to [null] (the seed
       and step bound on full runs, the state bound on sim runs; the state
       and step bounds and [state_table] on interactive sessions, where
       [terminated] is [quit] and [execution] is [interactive]).
       [mean_state_size] and [max_state_size] are [null] when the pass over
       the states is not requested: on interactive sessions, --metrics-json
       itself. Under the GBS solver (--solver=GBS) the seven SAT matching
       metrics are [null], since GBS uses native isomorphism testing rather
       than SAT encoding. [solver_time_ms] is still reported: it is the wall
       time spent inside the C++ subgraph-isomorphism solve, measured by the
       solver's own clock. The four factoring fields count the automatic BRS
       family factoring: how many fun react / fun big instantiations were
       folded into bracket-guarded rules / bases, and how many of the
       enumeration's members were thereby not materialised (the per-value
       predicate variants are still materialised, as state labels).

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)