BigMC -- Bigraphical Model Checker

• Home
• Manual
• GitHub

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.