bigrapher sim —
Simulate a model
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] |
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.
-
-
BIGFORMAT
- See option -f.
-
-
BIGQUIET
- See option -q.
-
-
BIGVERBOSE
- See option -v.
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
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.
Michele Sevegnani
<
michele.sevegnani@glasgow.ac.uk>