3 Invoking bigmc
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>
bigmc> prompt indicates that the interactive environment is ready to accept
model definitions, properties and finally the
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:
- display usage information and exit.
- 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.
- print version information and exit.
- increase the verbosity of the information that is output during execution.
- if set, output a graphviz file suitable for rendering with dot to file.
- set the maximum number of steps of reaction that may be performed.
- print new states as they are discovered.
- set the frequency with which statistics about the graph and work queue
are output while running.
- instruct the checker to run threads parallel threads. Defaults to 2.
Table of Contents
- 1 Introduction
- 2 Obtaining BigMC
- 3 Invoking bigmc
- 4 BGM file structure
- 5 Term language
- 6 Property language
- 7 Checking
- 8 Example