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 FDR: construct a CSP script file with the required assertions (using "include" to pull in any process definitions required) and launch FDR 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. Where a process permits a prohibited event, it will be surrounded by BEGIN ALLOWS and END ALLOWS.

-refusals

Setting this option will result in the refusals and acceptances associated with each result being printed. The refusals and acceptances will be surrounded by BEGIN REFUSALS, END REFUSALS and BEGIN ACCEPTANCES, END ACCEPTANCES respectively. This option implies -trace.

-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.

-depth levels

If -trace has been selected, then report traces for sub-processes as well as the root processes. This is the same as expanding the specified number of levels of the tree in the FDR debugger, noting down the traces for each sub-process. The BEGIN TRACE/END TRACE lines carry additional information indicating the path through from the root to the sub-process which generate the particular trace.

A typical use of -depth is when the CSP script uses hiding and compression and extracting the full counter-example requires ‘tunneling’ inside those sub-processes. This is often the case when the CSP has been automatically generated from some other notation.

This document was generated by Phil Armstrong on May 17, 2012 using texi2html 1.82.