C.1 Batch interface

The `fdrBatch.tcl' script can be used to check all the assertions in a number of CSP scripts automatically. To start it, use the supplied `fdr2' shell-script from the `bin' directory with a `batch' argument. For example,

fdr2 batch options $FDRHOME/demo/abp.csp

will run all the assertions in the `abp.csp' script.

In general, the batch script is the simplest way of driving FDR2: construct a CSP script file with the required assertions (using "include" to pull in any process definitions required) and launch FDR2 with the `batch' argument described above.

The batch interface accepts a number of options. These will affect any files listed as arguments after them.

-trace

Selecting this option will report the traces associated with each result. For each process involved, and for each generated counterexample, a number of lines representing the trace may be printed. The trace will be surrounded by BEGIN TRACE and END TRACE lines indicating which counterexample and process the trace belongs to. Not all processes need produce a trace in a given counterexample.

-max examples

Each check will generate at most the indicated number of counterexamples. Unless -trace has been selected, this will have no detectable effect. By default at most one counterexample per check is generated. This option is equivalent to the Examples per check control in the Options menu.

Go to the Next or Previous section, the Detailed Contents, or the FS(E)L Home Page.