In #1, we noted that adapting BDDFactory needs updates for every factory implementation, not just JFactory. If we don't use any other factories, besides JFactory, we could opt to remove the other factories, to easy maintenance.
I've looked at which factories there are besides JFactory.
MicroFactory
* <p>BDD factory where each node only takes 16 bytes.
* This is accomplished by tightly packing the bits and limiting the
* maximum number of BDD variables to 2^10 = 1024.</p>
*
* <p>Because of the extra computation required for packing/unpacking,
* this BDD factory is a little slower than JFactory, but it also uses
* 20% less memory.</p>
UberMicroFactory
* <p>BDD factory where each node only takes 16 bytes.
* This is accomplished by tightly packing the bits, eliminating
* the refcount, splitting out the unique table and limiting the
* maximum number of BDD variables to 2^11 = 2048.</p>
*
* <p>This BDD factory is not only more memory efficient than
* JFactory, it also seems to perform better, probably due to
* better memory locality. It performs cache-aware BDD node
* placement.</p>
TestBDDFactory
* This BDD factory is used to test other BDD factories. It is a wrapper around
* two BDD factories, and all operations are performed on both factories. It
* throws an exception if the results from the two implementations do not match.
TypedBDDFactory
* <p>This BDD factory keeps track of what domains each BDD uses, and complains
* if you try to do an operation where the domains do not match.</p>
MicroFactory and UberMicroFactory use less memory. MicroFactory may actually be slower, while UberMicroFactory is indicated to be a bit faster. However, both are more restricted than JFactory in the number of variables, nodes, references, etc they can story (due to using less bits to represent a node). From a practical point of view, for Eclipse ESCET we already run out of memory (Java array size) for large supervisor synthesis inputs. As such, I can imagine just removing these micro-variants from the code base here.
I see that TestBDDFactory is not used anywhere, and neither is TypedBDDFactory. We could opt to remove these as well. In fact, we could get rid of anything we don't use in practice.
@magoorden What do you think?
In #1, we noted that adapting
BDDFactoryneeds updates for every factory implementation, not justJFactory. If we don't use any other factories, besidesJFactory, we could opt to remove the other factories, to easy maintenance.I've looked at which factories there are besides
JFactory.MicroFactoryandUberMicroFactoryuse less memory.MicroFactorymay actually be slower, whileUberMicroFactoryis indicated to be a bit faster. However, both are more restricted thanJFactoryin the number of variables, nodes, references, etc they can story (due to using less bits to represent a node). From a practical point of view, for Eclipse ESCET we already run out of memory (Java array size) for large supervisor synthesis inputs. As such, I can imagine just removing these micro-variants from the code base here.I see that
TestBDDFactoryis not used anywhere, and neither isTypedBDDFactory. We could opt to remove these as well. In fact, we could get rid of anything we don't use in practice.@magoorden What do you think?