Command-line reference

NAME
       bigrapher-sim - Simulate a model.

SYNOPSIS
       bigrapher sim [OPTION]… [FILE]

ARGUMENTS
       FILE
           Input model. Read from stdin if omitted.

OPTIONS
       -a, --ascii-bar
           Use ASCII for the progress bar.

       -c ASSIGNMENT, --const=ASSIGNMENT
           Specify a comma-separated list of variable assignments. Example:
           x=4,t=.56.

       --checkpoint=ith
           Checkpoint every ith state in the format(s) specified by --format.
           The destination is inferred from option --export-ts if it is set.
           The current directory is used otherwise.

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

       --debug_extra, --debug-extra
           Print even more diagnostic information (implies --debug). Includes
           mean state size, solver time, and the solver matching metrics
           mirrored from --metrics-json (n/a under the GBS solver).

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

       -l FILE, --export-labels=FILE
           Export the labelling function in PRISM .csl format to FILE.

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

       -p FILE, --export-prism=FILE
           Export the transition system in PRISM .tra format to FILE.

       -q, --quiet (absent BIGQUIET env)
           Suppress all output (header, progress bar, statistics, trace).
           File exports and the exit status are unaffected. Flag --verbose is
           ignored if set.

       -R FILE, --export-transition-rewards=FILE
           Export transition rewards in PRISM .trew format to FILE.

       -r FILE, --export-state-rewards=FILE
           Export state rewards in PRISM .rews format to FILE.

       --running-time
           Print only the elapsed time on completion. Suppresses the header,
           progress bar, statistics table and coloured output.

       -S INT, --simulation-steps=INT
           Set the simulation limit: the simulation stops once the
           accumulated time exceeds the given value. This option is only
           valid for non-stochastic models (BRS, PBRS, ABRS), where the time
           is the step count.

       -s [DIR], --export-states[=DIR] (default=)
           Export each state to a file in DIR. State indices are used as file
           names. The directory is created if it does not exist. When DIR is
           omitted, it is inferred from option --export-ts.

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

       -T FLOAT, --simulation-time=FLOAT
           Set the maximum simulation time. This option is only valid for
           stochastic models (SBRS).

       -t FILE, --export-ts=FILE
           Export the transition system to FILE.

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

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

       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 all output (header, progress bar, statistics, trace).
           File exports and the exit status are unaffected. Flag --verbose is
           ignored if set.

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

       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
       Run an SBRS simulation for 100 time units:

         bigrapher sim --simulation-time=100 model.big

       Run a BRS/PBRS/ABRS simulation for 500 steps with a fixed seed:

         bigrapher sim --simulation-steps=500 --seed=42 model.big

       Export each visited state as a DOT file:

         bigrapher sim --export-states=model bigrapher/examples/hospital.big

PRISM EXPORT
       The options --export-prism, --export-labels, --export-state-rewards,
       and --export-transition-rewards produce output in the format expected
       by the PRISM probabilistic model checker
       (http://prismmodelchecker.org/).

       For stochastic (SBRS) models a transition's label is a rate. full
       --export-prism writes each edge with its static rate, while sim
       --export-prism writes each step of the simulated trace with the
       realized (sampled) exponential holding time for that step (the actual
       elapsed time, not the rate).

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
       }

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)