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.

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

Kind Option Section Effect Choose

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

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

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

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