Statistics

> > > >

The data-based synthesis tool supports printing various kinds of statistics. By default, no statistics are printed. Statistics can be enabled using the Statistics option (see the options section). The following statistics are available:

BDD garbage collection [bdd-gc-collect]

Prints BDD garbage collection information before and after each garbage collection.

The BDD library that is used maintains an internal node table. Whenever new nodes no longer fit in the node table, a garbage collection is started by the BDD library, to clean out all nodes that are no longer needed. See also the BDD library initial node table size option (see the options section).

BDD garbage collection information is printed to the console before and after each garbage collection. The printed information includes the size of the node table, the number of free nodes, timing information, etc.
BDD node table resize [bdd-gc-resize]

Prints BDD node table resize information each time a BDD node table resize is performed.

The BDD library that is used maintains an internal node table. Whenever new nodes no longer fit in the node table, a garbage collection is started by the BDD library, to clean out all nodes that are no longer needed. If only very limited space could be reclaimed by garbage collection, the size of the node table is increased. See also the BDD library initial node table size option (see the options section).

BDD node table resize information is printed to the console each time the node table is resized. The printed information includes the old and new sizes of the node table.

BDD cache [bdd-perf-cache]

Prints metrics related to the BDD cache.

The BDD library that is used implements a cache to speed up the calculations. For more information, see the section about BDD operation caches.

The information is printed to the console, after execution, just before termination of the tool. The table below shows all metrics printed and their meaning.

Note that collecting these metrics makes synthesis take longer than without collecting it.

Metric Description

Metric	Description
Node creation requests	The number of times a node creation is requested. This includes the trivial cases where the cache is not checked, e.g. when both child nodes are the same.
Node creation chain accesses	The number of times a node creation is requested, and a next node in the cache needs to be checked. This excludes the trivial cases where the cache is not checked.
Node creation cache hits	The number of times a node creation is requested, and the node is already in the cache. This excludes the trivial cases where the cache is not checked.
Node creation cache misses	The number of times a node creation is requested, and the node is not already in the cache. This excludes the trivial cases where the cache is not checked.
Operation count	The number of times a BDD operation is performed on a node or a pair of nodes. This includes the trivial cases where the cache is not checked, e.g. for `x and x`, `x and true`, `false and x`, etc.
Operation cache hits	The number of times a BDD operation is performed on a node or a pair of nodes, and the result is already in the cache. This excludes the trivial cases where the cache is not checked.
Operation cache misses	The number of times a BDD operation is performed on a node or a pair of nodes, and the result is not already in the cache. This excludes the trivial cases where the cache is not checked.

Node creation requests

The number of times a node creation is requested. This includes the trivial cases where the cache is not checked, e.g. when both child nodes are the same.

Node creation chain accesses

The number of times a node creation is requested, and a next node in the cache needs to be checked. This excludes the trivial cases where the cache is not checked.

Node creation cache hits

The number of times a node creation is requested, and the node is already in the cache. This excludes the trivial cases where the cache is not checked.

Node creation cache misses

The number of times a node creation is requested, and the node is not already in the cache. This excludes the trivial cases where the cache is not checked.

Operation count

The number of times a BDD operation is performed on a node or a pair of nodes. This includes the trivial cases where the cache is not checked, e.g. for x and x, x and true, false and x, etc.

Operation cache hits

The number of times a BDD operation is performed on a node or a pair of nodes, and the result is already in the cache. This excludes the trivial cases where the cache is not checked.

Operation cache misses

The number of times a BDD operation is performed on a node or a pair of nodes, and the result is not already in the cache. This excludes the trivial cases where the cache is not checked.

Continuous BDD performance statistics [bdd-perf-cont]

Prints continuously collected platform and machine independent BDD performance related metrics.

This statistic continuously collects the platform and machine independent BDD performance metrics described in the table below. These metrics are discussed in more detail in [Thuijsman et al. (2019)].

The information is printed to a CSV file that can be configured using the Continuous performance statistics file option. The file is written after execution, just before termination of the tool.

Note that collecting these metrics makes synthesis take longer than without collecting it.

Metric	Description
Operations	The number of BDD operations performed on BDD nodes so far during synthesis, for which the cache is checked and the result is not already in the cache. The number of operations performed on BDD nodes is a platform and machine independent measure of the amount of time needed to perform BDD operations, due to BDD operations being implemented recursively on their node trees.
Used BBD nodes	The number of BDD nodes currently in use to represent all BDDs. The size of a BDD, expressed as the number of nodes used, is a platform and machine independent measure of the amount of memory needed to store it.

Metric

Description

Operations

The number of BDD operations performed on BDD nodes so far during synthesis, for which the cache is checked and the result is not already in the cache. The number of operations performed on BDD nodes is a platform and machine independent measure of the amount of time needed to perform BDD operations, due to BDD operations being implemented recursively on their node trees.

Used BBD nodes

The number of BDD nodes currently in use to represent all BDDs. The size of a BDD, expressed as the number of nodes used, is a platform and machine independent measure of the amount of memory needed to store it.

Controlled system states [ctrl-sys-states]

Prints the number of states in the resulting controlled system (the uncontrolled system restricted by the synthesized supervisor).

If the resulting supervisor (and thus the controlled system) is empty, or if forward reachability is enabled, the number of states that is printed is an exact number (e.g. exactly 0 states, exactly 1 state, exactly 1,234 states). In other situations, the controlled behavior predicate that is used to determine the number potentially gives an over-approximation, and an upper bound on the number of states is printed (e.g. at most 1,234 states).

This metric is printed to the console, after the supervisor is computed, and before it is simplified and written to a file.
Maximum used BDD nodes [bdd-perf-max-nodes]

Prints the maximum number of BDD nodes used during synthesis.

The size of a BDD, expressed as the number of nodes used, is a platform and machine independent measure of the amount of memory needed to store it. This metric is discussed in more detail in [Thuijsman et al. (2019)].

This metric is printed to the console, after execution, just before termination of the tool. It prints the maximum number of BDD nodes used during synthesis.

Note that collecting this metric makes synthesis take longer than without collecting it.
Timing [timing]

Print information for timing of various parts of the tool.

Timing is only collected for parts of the tool that were actually executed. Timing is represented as a tree. The root of the tree represents the total time of the synthesis tool. For some parts of the tool, timing is also collected for sub-parts.

Timing information is printed to the console, after execution, just before termination of the tool. Durations are all printed in milliseconds, to make it easier to compare timing for various parts.

When measuring timing performance, always perform multiple measurements, and take the average. Also, use a warm-up phase, to avoid skewed results.
Maximum used memory [max-memory]

Prints the maximum memory used during synthesis.

Measuring the memory usage may be useful, for instance to see how close you are to memory limits. It may especially be useful if you want to subsequently extend your model, making it more complex and potentially requiring more memory for synthesis.

This metric is printed to the console, after execution, just before termination of the tool. It prints the maximum amount of memory used during synthesis, in number of bytes and in a more readable representation such as mebibytes or gibibytes.

Note that collecting this metric may make synthesis take longer than without collecting it.

The CIF data-based synthesis tool is written in Java, a managed language with a garbage collector. Hence, the measured memory usage is a best-effort approximation, and may not be correct.

When measuring memory usage, always perform multiple measurements, and take the average.

If memory usage is measured using the Eclipse ESCET IDE, make sure not to perform multiple syntheses in parallel, and make sure the Eclipse ESCET IDE is not performing any other operations. However, when measuring the memory usage in the Eclipse ESCET IDE, the IDE itself, as well as editor content, console content, and so on, are also included in the memory usage. It is therefore highly recommended to use the Eclipse ESCET command line scripts rather than the Eclipse ESCET IDE to perform memory usage measurements.

To ensure the best result, let Java perform a garbage collection before starting the data-based synthesis tool. This ensures that synthesis starts with 'clean' memory. This is particularly relevant if multiple syntheses are performed one after the other, to ensure that any previous syntheses do not affect subsequent measurements. Both synthesis and garbage collection may conveniently be executed via a ToolDef script. For example, using a ToolDef script like this:
```
from "lib:cif" import *;
import java.lang.System.gc;
gc();
cifdatasynth(...);
```
The maximum used memory statistics obtained in this way are an easy way to get an approximation of the memory used during synthesis. For a more comprehensive way to measure memory usage, use a tool like VisualVM.

In the option dialog, each of the different kinds of statistics can be enabled and disabled individually, using a checkbox.

From the command line, using the --stats option, the names of the different kinds of statistics, as indicated above between square brackets, should be used, separated by commas. For instance, use --stats=bdd-gc-collect,bdd-gc-resize to enable both BDD garbage collection statistics and BDD node table resize statistics, but keep all other statistics disabled.

Specifying a statistics kind twice leads to a warning being printed to the console.