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 |
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 |
Representation of BDDs in the output model |
Use |
|
Output |
BDD predicate simplify |
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 |
BDD initial variable ordering |
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 |
Better order for smaller BDD representations |
Choose the algorithm that produces the best order, depends on the model |
|
Order |
BDD DCSH variable ordering algorithm |
Better order for smaller BDD representations |
Enable for automatic ordering |
|
Order |
BDD FORCE variable ordering algorithm |
Better order for smaller BDD representations |
Enable for automatic ordering |
|
Order |
BDD sliding window variable ordering algorithm |
Better order for smaller BDD representations |
Enable for automatic ordering |
|
Order |
BDD sliding window size |
Better order for smaller BDD representations |
Larger windows might allow for more optimization, but take more time |
|
Order |
BDD advanced variable ordering |
Better order for smaller BDD representations |
Choose the best ordering, depends on the model |
|
Order |
Edge order for backward reachability |
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 |
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 workset algorithm |
Better order for less computations and smaller BDD representations |
Enable to dynamically determine the order in which edges are considered, which may improve performance |
|
Library |
BDD library initial node table size |
More storage for less resizes |
Increase size for less resizes, at the cost of less memory locality |
|
Library |
BDD library operation cache size/ratio |
Increase cache for less computations |
Enable, larger costs more memory, larger leads to less memory locality, size/ratio depends on model |
|
Algorithm |
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 on console |
Disable for better performance |
|
Debug |
BDD debug max nodes/paths |
Size of predicates in debug output |
The smaller, the less blowup, the better the performance |
|
Debug |
Statistics |
Statistics output on console or to file |
Disable for better performance |
|
Warnings |
Event warning |
Warning for never enabled events |
Disable for better performance |
|
Warnings |
Plants referencing requirements warnings |
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.