TransformationToolContest / ttc2019-tt2bdd

Free form TTC contest (Truth tables to Binary Decision Diagrams, from ATL Zoo)
MIT License
5 stars 7 forks source link

Review of SCROLL - Artur Boronat #14

Open arturboronat opened 5 years ago

arturboronat commented 5 years ago

Does it highlight a promising research direction?

Correctness

Completeness

Understandability

Uses scala for implementing the transformation and there is some distance between the description of the solution in the paper and the actual implementation of each solution variant.

Performance

The transformation is more efficient than the reference ATL transformation, yet it scales worse than other solutions - see other review on SCROLL.

Optimality

Models with one single output port have been generated in order to measure the size of the BDD representing a standard boolean function, which is the general case, instead of considering a set of boolean functions.

Sizes (number of objects) for the generated output models for each of the tools have been gathered below, where JAST-ADD (ROBDD) and YAMTL produce the most compact BDDs.

input ports RelationalRAG-BDD-reduced-natural YAMTL RelationalRAG-BDD-reduced-heuristic RSyncBDDUnordered RsyncBDD RSyncBDTUnordered RSyncBDT RelationalRAG-BDD-dynamic-natural RelationalRAG-BDD-dynamic-natural RelationalRAG-BDT-ordered-natural EMFTVM Fulib
2 9 9 9 9 9 9 9 9 9 15 15 15
4 19 19 18 19 19 32 35 38 38 53 53 53
8 88 88 87 178 191 453 570 531 531 777 777 777
16 8321 8321 8338 timeout timeout timeout timeout 141137 141137 196625 196625 196625

STROLL (RSync) also provides compact BDDs but it is not able to cope with large truth tables in reasonable time.

I am assuming the output model sizes for the input models provided for testing will be provided during the workshop.

Quality of software artifacts

The solution could be executed without problems.