## Performance

There are quite a few factors that influence the performance of data-based synthesis. Here are some of those factors, which affect both the time it takes to complete a synthesis and the memory that is used for it:

- Obviously, the actual model that is used has a large impact. A model with more variables often has to longer synthesis time and requires more memory. However, the predicates that are used may also significantly impact performance.

- The modeling style used when modeling the plants and requirements can also have a significant impact on the performance. See for instance these suggestions.

- Several options of the data-based synthesis tool impact its performance. A list of such option is given below.

If you run out of memory, here are some potential solutions:

- Increase the memory available to the synthesis tool. For more information, see the page of the Eclipse ESCET general toolkit documentation on resolving performance and memory problems.

- Decrease the size of the BDD operation caches, to make sure more memory remains available for the actual data used during synthesis. While decreasing the size of caches may increase the synthesis time, it is better to be able to synthesize a supervisor in a longer time than to not be able to synthesize it at all.

### Performance-related options

The following options have an effect on the performance of data-based synthesis:

Kind | Option | Section | Effect | Choose
--- | --- | --- | --- | ---
Input | State requirement invariant enforcement | State requirement invariants | Impacts the up-front effort, size of the controlled behavior, number of iterations to reach fixed points, and the post-synthesis effort | Complex trade-off between different effects, depends on the model
Input | Edge granularity | Edge granularity | Impacts the size of the edge representations, size of the controlled behavior, number of iterations to reach fixed points, and the post-synthesis effort | Choose the best representation, depends on the model
Output | BDD output mode | BDD representation in CIF | Representation of BDDs in the output model | Use `nodes` output variant for best performance
Output | BDD predicate simplify | Predicate simplification | Potentially smaller BDDs in the output | Enable for smaller output, although simplification itself also takes time
Order | Fixed-point computations order | Fixed-point computations order | Better order for less computations and smaller BDD representations | Choose the best ordering, depends on the model
Order | Exploration strategy | Edge order | Better order for less computations and smaller BDD representations | The `saturation` strategy likely gives best performance
Order | BDD initial variable ordering | Initial variable orders | Better order for smaller BDD representations | Choose the best ordering, depends on the model, (reversed) model/sorted usually good choices, custom order allows for best performance
Order | BDD hyper-edge creation algorithm | Automatic variable ordering | Better order for smaller BDD representations | Choose the algorithm that produces the best order, depends on the model
Order | BDD DCSH variable ordering algorithm | Automatic variable ordering | Better order for smaller BDD representations | Enable for automatic ordering
Order | BDD FORCE variable ordering algorithm | Automatic variable ordering | Better order for smaller BDD representations | Enable for automatic ordering
Order | BDD sliding window variable ordering algorithm | Automatic variable ordering | Better order for smaller BDD representations | Enable for automatic ordering
Order | BDD sliding window size | Automatic variable ordering | Better order for smaller BDD representations | Larger windows might allow for more optimization, but take more time
Order | BDD advanced variable ordering | Advanced variable ordering configuration | Better order for smaller BDD representations | Choose the best ordering, depends on the model
Order | Edge order for backward reachability | Edge order | Better order for less computations and smaller BDD representations | Choose the best order, depends on the model, custom order allows for best performance
Order | Edge order for forward reachability | Edge order | Better order for less computations and smaller BDD representations | Choose the best order, depends on the model, custom order allows for best performance
Library | BDD library initial node table size | Statistics | More storage for less resizes | Increase size for less resizes, at the cost of less memory locality
Library | BDD library operation cache size/ratio | BDD operation cache | Increase cache for less computations | Enable, larger costs more memory, larger leads to less memory locality, size/ratio depends on model
Algorithm | Forward reachability | Forward reachability | Explore only reachable state space | Enable to reduce state space, although calculation itself may also be expensive, depends on model
Debug | Output mode | Debug output | Debug output on console | Disable for better performance
Debug | BDD debug max nodes/paths | Debug output | Size of predicates in debug output | The smaller, the less blowup, the better the performance
Debug | Statistics | Statistics | Statistics output on console or to file | Disable for better performance
Warnings | Event warning | Early problem detection and Resulting supervisor | Warning for never enabled events | Disable for better performance
Warnings | Plants referencing requirements warnings | Early problem detection | Warning for plants that reference requirement state | Disable for better performance

The first column categorizes the different options a bit, for different kind of options. The second column lists the different options. The third column indicates in which section of the data-based synthesis tool documentation you can find more information about that option. The fourth column indicates the effect of the option. The fifth column indicates what to choose for the option, for best performance, although a trade-off may be involved.