bigrapher validate —
Parse a model and check its validity
| bigrapher validate |
[-c
assignment]
[-d
dir]
[-f
format]
[-h]
[-m
file]
[-n]
[-q]
[-v]
[model] |
bigrapher validate checks the validity 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. Note, the transition system is not computed at this
stage.
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.
-
-
- -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.
-
-
- -q,
--quiet
- Disable all output. This is equivalent to setting
BIGQUIET to a non-empty value.
-
-
- -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 command is useful to debug a model. It stores in directory
“decs” the graphical representation in
.svg format of every bigraph and reaction rule
defined in “model.big”.
$ bigrapher validate -d decs -f svg
model.big
bigrapher(1),
bigrapher-full(1),
bigrapher-sim(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>