Performance

> > >

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

Kind Option Section Effect Choose

Kind	Option	Section	Effect	Choose
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	BDD variable order	BDD variable order	Better order for smaller BDD representations	Choose the best order, depends on the model, (reversed) model/sorted usually good choices, custom order allows for best performance
Order	BDD hyper-edge creation algorithm	BDD variable order	Better order for smaller BDD representations	Choose the algorithms that produces the best order, depends on the model
Order	BDD DCSH variable ordering algorithm	BDD variable order	Better order for smaller BDD representations	Enable for automatic ordering
Order	BDD FORCE variable ordering algorithm	BDD variable order	Better order for smaller BDD representations	Enable for automatic ordering
Order	BDD sliding window variable ordering algorithm	BDD variable order	Better order for smaller BDD representations	Enable for automatic ordering
Order	BDD sliding window size	BDD variable order	Better order for smaller BDD representations	Larger windows might allow for more optimization, but take more time
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
Order	Edge order	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
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

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

BDD variable order