Performance measuring of data-based synthesis
In his graduation work, Sander Thuijsman worked on performance measurements of data-based synthesis in CIF. He proposed to use the following two metrics to measure computational effort:
- Total BDD operations. This is the total number of BDD operations performed by the tool excluding cache hits, which relates to time effort.
- Max BDD nodes. This is the maximum number of nodes of the BDD encountered during synthesis, which relates to space effort.
More information on these statistics can be found in his Master Thesis or in the paper Thuijsman et al., Computational Effort of BDD-Based Supervisor Synthesis of Extended Finite Automata, IEEE Conference on Automation Science and Engineering, 2019, DOI:10.1109/COASE.2019.8843327.
During his thesis project, Sander adopted the JavaBDD package to collect these statistics. I made his code available in the TUE-RWS branch, but it hasn't been included in the public version of CIF. I have cleaned up and enhanced Sander's code such that, for example, an end user can request these synthesis statistics with the regular data-based synthesis options (and not by changing hard coded variables in the source code as Sander originally did).
One of the discussions Albert and I had was how to correctly deal with the license of JavaBDD. I quote Albert's comment from the TUE-RWS branch:
The SF site says JavaBDD has a LGPLv2 license, so we have to follow those rules for the changes in JavaBDD.
The project only has a
javabdd_version.txtfile with version number and download instructions. I think it would be useful to add a text file describing what code is coming from where, links to publications, and a way to get the full source of our modifications.
For the latter, a git revision is theoretically sufficient, but generating a diff file and adding that may be simpler and more robust in the long term. (Depending on size, is could be compressed as we have no intention of ever changing it.)
The patch could likely also be offered to the author of JavaBDD for considering to include it in the program, if that's allowed. Such a path may be have more work behind it, if the author wants changes. SF site says last update was in 2013, don't know what was modified.
I have no experience with licenses, so I don't know the best way to move forward. Any help in this is welcome. Given this license, would it be fine for me if I create a merge request (possibly with WIP status) with the changes, as the merge request effectively publishes the changes?