BIGRAPHER-SIM(1) General Commands Manual BIGRAPHER-SIM(1)

NAME

bigrapher simSimulate a model

SYNOPSIS

bigrapher sim [-c assignment] [-d dir] [-f format] [-h] [-l file] [-m file] [-n] [-p file] [-q] [-S int] [-s [dir]] [-T float] [-t file] [-v] [model]

DESCRIPTION

bigrapher sim computes the transition system of the Bigraphical Reactive System defined in model, a file with extension big. If model is absent, a bigraphical model is read from the standard input.
The options are as follows:
 
 
-c assignment, --const assignment
Specify a comma-separated list of variable assignments. Example format for assignment: “x=4,t=.56”.
 
 
-d dir, --export-decs dir
Export each declaration in the model (bigraphs and reaction rules) to a distinct file in dir. Dummy values are used to instantiate functional values.
 
 
-f format, --format format
Specify a comma-separated list of output formats for options -d, --export-decs, -t, --export-ts, -s, and --export-states. Supported formats are “dot”, “json”, “svg” and “txt”. This is equivalent to setting BIGFORMAT to format.
 
 
-h, --help
Display the list of options.
 
 
-l file, --export-labels file
Export the labelling function in PRISM csl format to file.
 
 
-m file, --export-ml file
Export the model in OCaml format to file.
 
 
-n, --no-colors
Disable colored output. This is equivalent to setting BIGNOCOLORS to a non-empty value.
 
 
-p file, --export-prism file
Export the transition system in PRISM tra format to file.
 
 
-q, --quiet
Disable all output. This is equivalent to setting BIGQUIET to a non-empty value.
 
 
-S int, --simulation-steps int
Set the maximum number of simulation steps. This option is valid only for deterministic and probabilistic models.
 
 
-s dir, --export-states dir
Export each state to a file in dir. State indices are used as file names. When dir is omitted, it is inferred from option -t.
 
 
-T float, --simulation-time float
Set the maximum simulation time. This option is valid only for stochastic models.
 
 
-t file, --export-ts file
Export the transition system to file.
 
 
-v, --verbose
Be more verbose. This is equivalent to setting BIGVERBOSE to a non-empty value.

ENVIRONMENT

 
 
BIGFORMAT
See option -f.
 
 
BIGQUIET
See option -q.
 
 
BIGVERBOSE
See option -v.

EXAMPLES

The following computes the transition system of the Bigraphical Reactive System sepcified in “model.big” and export it to file “ts.tra” in PRISM .tra format:
$ bigrapher full -p ts.tra model.big

SEE ALSO

bigrapher(1), bigrapher-full(1), bigrapher-validate(1)
The following references provide more in-depth details on bigraphs and the implementation of the BigraphER tool:
R. Milner, The Space and Motion of Communicating Agents, Cambridge University Press, 2009.
M. Sevegnani and M. Calder, BigraphER: Rewriting and Analysis Engine for Bigraphs, Computer Aided Verification: 28th International Conference, CAV 2016, Toronto, ON, Canada, July 17-23, 2016, Proceedings, Part II, Springer International Publishing, http://doi.org/10.1007/978-3-319-41540-6_27, 494 - 501, 2016.
M. Sevegnani and M. Calder, Bigraphs with Sharing, Elsevier, Theoretical Computer Science, 0, 577, http://doi.org/10.1016/j.tcs.2015.02.011, 43 - 73, 2015.
Refer to http://www.dcs.gla.ac.uk/~michele/bigrapher.html for more examples and a complete reference of the big format for bigraphical models.

AUTHORS

Michele Sevegnani <michele.sevegnani@glasgow.ac.uk>
February 19, 2018 Darwin 17.4.0