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 node and operation [bdd-perf-cache]

Prints metrics related to the BDD nodes and operations.

The BDD library that is used maintains an internal node table to store the nodes that comprise the various BDDs. If a node already exists in the node table, it is reused rather than creating a new one, to ensure each node exists only once in the node table. The library will use the node’s hash to determine where to find or store it in the node table. Due to hash collisions, the library may not be able to find or store the node at the entry corresponding with the hash. It will then consider subsequent entries in the node table.

The BDD library may perform operations on BDD nodes. An operation may operate on a single BDD, such as the the logical negation (not) operation. It may also operate on multiple BDDs, such as the logical conjunction (and) operation. Regardless, BDD operations are generally implemented recursively on their structures. They start at the root nodes, go further and further towards the terminal nodes, and recursively consider all relevant nodes as they encounter them. The BDD library uses caches to store previously computed results of operations, to prevent having to recalculate them time and again, speeding up calculations.

For more information, see also the section about BDD operation caches.

The BDD node and operation information is printed to the console, after execution, just before termination of the tool. The table below shows all metrics that are 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, regardless of whether this node is already present in the node table or not. This count includes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.
Node creation hits	The number of times a node creation is requested, while the node is already in the node table. This count excludes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.
Node creation misses	The number of times a node creation is requested, while the node is not already in the node table, and thus the node needs to be created and added to the node table. This count excludes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.
Node creation chain accesses	The number of extra node table entries that are checked in case of hash collisions. This count represents the number of times that an extra (non-first) entry of the node table is considered to find and/or store the node. If for a single node creation multiple extra entries are checked, each of these extra entries is counted separately. This count excludes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.
Operation count	The number of times a BDD operation is performed on one or more nodes. This includes not only root nodes of BDDs, but also all recursive operations for parts of the BDDs. This includes the trivial cases where the cache is not checked, e.g., for `not true`, `x and x`, `x and true`, `false and x`, etc.
Operation cache hits	The number of times a BDD operation is performed on one or more nodes, and the result is already in the cache. This includes not only root nodes of BDDs, but also all recursive operations for parts of the BDDs. This excludes the trivial cases where the cache is not checked.
Operation cache misses	The number of times a BDD operation is performed on one or more nodes, and the result is not already in the cache. This includes not only root nodes of BDDs, but also all recursive operations for parts of the BDDs. This excludes the trivial cases where the cache is not checked.

Node creation requests

The number of times a node creation is requested, regardless of whether this node is already present in the node table or not. This count includes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.

Node creation hits

The number of times a node creation is requested, while the node is already in the node table. This count excludes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.

Node creation misses

The number of times a node creation is requested, while the node is not already in the node table, and thus the node needs to be created and added to the node table. This count excludes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.

Node creation chain accesses

The number of extra node table entries that are checked in case of hash collisions. This count represents the number of times that an extra (non-first) entry of the node table is considered to find and/or store the node. If for a single node creation multiple extra entries are checked, each of these extra entries is counted separately. This count excludes nodes that are never stored, such as terminal nodes and nodes with the same low and high children.

Operation count

The number of times a BDD operation is performed on one or more nodes. This includes not only root nodes of BDDs, but also all recursive operations for parts of the BDDs. This includes the trivial cases where the cache is not checked, e.g., for not true, x and x, x and true, false and x, etc.

Operation cache hits

The number of times a BDD operation is performed on one or more nodes, and the result is already in the cache. This includes not only root nodes of BDDs, but also all recursive operations for parts of the BDDs. This excludes the trivial cases where the cache is not checked.

Operation cache misses

The number of times a BDD operation is performed on one or more nodes, and the result is not already in the cache. This includes not only root nodes of BDDs, but also all recursive operations for parts of the BDDs. 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 graphs.
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 graphs.

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