2.7 Options

The Options menu allows access to a number of internal aspects of FDR's operation.

Supercompilation

Clicking this option toggles FDR's use of an internal mask-based representation for finite-state machine compositions. It should be left enabled for all standard operations.

Bisimulate leaves

Clicking this option toggles FDR's automatic bisimulation of all leaf processes. It should be left enabled for all standard operations.

Messages

This submenu allows control of the amount of feedback added to the status log by FDR's internal state-machine manipulation and testing functions.

The default, Auto, does not report operations covering fewer than two hundred states, indicates progress every hundred states to two thousand, every thousand states to four hundred thousand, every ten thousand states to eighty million, and every hundred thousand thereafter.

Full verbosity gives details of all such operations; None inhibits all such status information. To view this log information, use the Show Status option.

Compaction

This allows control over the compaction used on FDR's main data storage. The Normal setting is recommended for most examples. Selecting Off will approximately double the storage consumed during a check. High decreases the storage used by approximately a third, at the cost of increasing the amount of processor time taken (this is useful for problems which might otherwise exceed the available storage, or on machines with fast processors).

Examples per check

This allows the user to control how many counterexamples may be generated by a single check. By default at most one may be generated. (This option was previously controlled from the status window.)

Show status

This causes FDR to open a scrollable text window which will be updated as it carries out the compilation and checking processes. This status window also receives detailed error messages describing syntax or semantic errors detected by the CSP compiler.

A Restart option is displayed on the options menu of some releases of FDR. At the present time this is intended for internal use only.