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:

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

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

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

Order

Edge workset algorithm

Edge order

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

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.