The options are catagorised according to what they affected below.
compiler.check_for_immediate_recursions¶| Default: | On |
|---|
If true, FDR will check to see if any processes of the form P = P [] STOP
are defined. If this option is not set then such a process will cause FDR
to fail at runtime, generally with a segmentation fault. If you know that, by
construction, no such processes can be contained within your file then this
option can be disabled to reduce the time required to compile processes. Note
that this will only have an impact on huge processes, that contain millions
of names. On anything smaller the different will be negligible.
compiler.leaf_compression¶| Default: | sbisim |
|---|
The compression that is used for compressing arguments of high-level
machines. This may either be none, indicating that no compression should
be used, or sbisim or wbisim, to indicate that the strong or
weak bisimulation compression function should be used, respectively.
compiler.recursive_high_level¶| Default: | On |
|---|
If true FDR will compile processes of the form P = Q ; P in an optimised
format. It is recommended that this is not disabled, unless it is producing
poor results on such a process.
compiler.reuse_machines¶| Default: | On |
|---|
If true FDR will, at the cost of increased memory usage, re-use named state machines in different assertions. If the same state machine is not being used in more than one assertion then it may make sense to disable this as it will decrease memory use.
cspm.evaluator_heap_size¶| Default: | A default value chosen by FDR. |
|---|
This option allows for more memory to be allocated for the evaluator up
front and can be used to improve performance in some cases. If the value
is suffixed by K, M, or G, it is a size in kilobytes, megabytes,
or gigabytes, respectively. Otherwise, it is a size in bytes.
Warning
This option will not take effect until FDR is restarted.
cspm.profiling.active¶| Default: | Off |
|---|
If set to On, then simple profiling statistics are collected that detail how many times each function has been called, and by which other functions. For further details on profiling see Profiling. Note that turning on this option will reduce the performance of the evaluator and therefore, this option should only be kept activated for as long as necessary.
cspm.profiling.flatten_recursion¶| Default: | On |
|---|
This option affects how profiling statistics are reported (and is therefore
only relevant assuming cspm.profiling.active is On). If this
option is Off, then recursive functions, such as:
f(0) = 0
f(x) = f(x-1)
will result in a hierarchy that is as deep as the longest possible chain of recursive calls, causing profiling to be slower and making the data more accurate, but potentially more difficult to interpret. See Profiling for further details.
cspm.runtime_range_checks¶| Default: | On |
|---|
If Off, then FDR will not check to see if the values that are dotted with channel or datatype constructors are in the defined sets. For example, consider the following script:
channel c : {0..1}
datatype X = Y.{0..1}
If this option is On, then FDR would throw an error if c.2 or Y.2
were evaluated. Turning this option off will suppress these errors.
This option should only be used for performance reasons in circumstances in
which you are confident that it would be impossible for this error to be
produced. In particular, whilst turning this option off will never cause FDR
to emit further errors, it is possible to construct processes that are
incorrect. For example, in theory, hiding Events should result in a
process that can perform no visible events, but (c.2 -> STOP) \ Events is
equivalent to c.2 -> STOP, since c.2 is not a valid event and is
therefore not in Events.
gui.close_windows_on_load¶| Deafult: | Off |
|---|
If set to On, then whenever a load or
reload command is executed, all windows
relating to the current session will be closed.
gui.console.history_length¶| Default: | 100 |
|---|
The number of history entries to keep in the command prompt. Any integer strictly greater than 0 is permitted for this option.
refinement.bfs.workers¶| Default: | The number of available cores. |
|---|
The number of workers to use for a refinement check that is using breadth first search. This may be set to any value strictly greater than 0. If 1 core is selected then the algorithm used is identical to the algorithm of FDR2 (at least conceptually). If more than 1 worker is required then a parallelised version of breadth first search is used, as explained in Refinement Checking.
refinement.cluster.homogeneous¶| Default: | false |
|---|
If set to true, FDR will assume that the nodes in the cluster are homogeneous (i.e. each node has the same number of cores of the same speed), rather than trying to calculate the speed of each machine.
If you are operating on a homogeneous cluster, it is strongly recommended that this flag should be set, as otherwise the cluster may end up being imbalanced.
refinement.desired_counterexample_count¶| Default: | 1 |
|---|
The number of counterexamples that FDR should attempt to find during a refinement check. Note that FDR may not be able to find this many counterexamples, but will continue to search until it has either found the desired number, or until every state pair has been explored.
See Uniqueness for further details on what FDR considers to be a unique counterexample. See Debug Viewer for a description on how to view the different counterexamples.
refinement.explorer.storage.type¶| Default: | A default value chosen by FDR. |
|---|
The data structure used for storing states to visit on the next ply of the breadth first search. The permitted values are:
refinement.storage.compressor¶| Default: | A default value chosen by FDR. |
|---|
The type of compressor to use for the block-based storage used during refinement checking.
refinement.storage.file.path¶| Default: | None |
|---|
If set to a comma-separated list of writeable directory paths FDR will use
on-disk storage to store data during refinement checks, rather than relying
on the system’s swap implementation. In particular, FDR will still make use
of RAM to cache data, but when the cache is filled, FDR will evict data to
files stored in the directory as set above. The size of the in-memory cache
can be set using refinement.storage.file.cache_size. For
example, setting this to /scratch/disk1,/scratch/disk2 will cause FDR
to write data to both folders.
This option is only useful if the amount of memory required to complete a check exceeds the available RAM. In such cases, setting this option to a valid directory path typically increases performance. Further, it allows FDR to allocate more memory than is available to the system (which can only use RAM and swap).
For maximum performance this directory should point to a location on a solid-state drive (SSD). Use of traditional disk drives is not recommended since FDR is not optimised for such cases.
When this option is selected it may be necessary to increase the maximum number of files that are allowed to be simultaneously open. On large checks that consume several hundred gigabytes of storage, FDR will easily require several thousand files to be simultaneously open. The required number of files can be estimated by dividing the number of megabytes of storage required for the check by 64 (which is the file size FDR uses by default). To adjust the maximum number consult the documentation for your Linux distribution (searching for “set maximum number of open files” generates useful results). FDR checks at runtime if this value is sufficient for operation.
See also
refinement.storage.file.cache_sizerefinement.storage.file.checksumrefinement.storage.file.compressorrefinement.storage.file.cache_size¶| Default: | 90% |
|---|
If file based storage is being used (see
refinement.storage.file.path), this specified the amount of
memory to use before evicting data to disk. This can be specified either as a
percentage of the available system RAM at the point the refinement check
starts, or as an absolute number of bytes. For example, specifying 50%
will cause FDR to use 50% of the remaining system RAM at the point the check
starts, whilst 100GB would cause FDR to use 100GB of RAM for the cache.
KB, MB, GB and TB may be used as suffixes to specify the
amount of RAM to use for the cache.
For maximum performance this value should be set as high as possible, but must not be set so high that FDR would start to use swap for its in-memory cache.
refinement.storage.file.checksum¶| Default: | Off |
|---|
If file based storage is being used (see
refinement.storage.file.path) and this option is set to On,
this will cause FDR to verify data that is read from disk. This can be useful
as a guard against disk corruption. If FDR detects a corrupted block it will
abort the check (there is no way to simply revisit the affected states,
unfortunately). This causes a small increase in runtime, generally around 5%.
refinement.storage.file.compressor¶| Default: | None |
|---|
If file based storage is being used (see
refinement.storage.file.path) and this is set to a value other
than None, this specifies an additional type of compression to apply to
blocks that evicted to disk. This can be useful to minimise the amount of
disk storage that is being used, but does result in the time to check a
property increasing by anywhere between 5 and 50% (depending on the problem).
This may be set to any of the values that
refinement.storage.compressor can be set to, in addition to the
value None.
refinement.track_history¶| Default: | On |
|---|
This option controls whether FDR will record information that enables it to reconstruct traces if a counterexample is found. If this option is disabled, FDR will require less memory (up to 50% less), but will not be able to report any counterexamples. This option should only be used if the check passes, since FDR will not provide any information about why the check fails if the assertion does not pass.