Next: BGM file structure, Previous: Obtaining BigMC, Up: Top
3 Invoking bigmc
Running bigmc
alone will enter the interactive environment:
$ bigmc BigMC version 0.1-dev (http://www.itu.dk/~gdpe/bigmc) Copyright (c) 2011 Gian Perrone <gdpe at itu.dk> bigmc>
The bigmc>
prompt indicates that the interactive environment is ready to accept
model definitions, properties and finally the check
command.
To exit the interactive environment, enter quit
or C-d. It is often more useful to invoke bigmc
with a model file. The full command line options are:
bigmc [-hlpvV] [-G file] [-m steps] [-r steps] [-t threads] [file]
3.1 Command Line Options
Several options are available to control the runtime behaviour of the checking process:
-h
- display usage information and exit.
-l
- employ only local checking. This avoids building the transition system
and saves memory when checking large models, but limits the properties
that you can check to those relating only to a single agent.
-v
- print version information and exit.
-V -VV
- increase the verbosity of the information that is output during execution.
-G
file- if set, output a graphviz file suitable for rendering with dot to file.
-m
steps- set the maximum number of steps of reaction that may be performed.
-p
- print new states as they are discovered.
-r
steps- set the frequency with which statistics about the graph and work queue
are output while running.
-t
threads- instruct the checker to run threads parallel threads. Defaults to 2.
This work funded in part by the Danish Research Agency (grant no.: 2106-080046) and the IT University of Copenhagen (the Jingling Genies project)