Data-based synthesis tool needs complexity reduction

The CIF data-based synthesis tool has grown over time. It now has quite a few classes with many lines of code. Some things seem to have become a bit intertwined. It is becoming more and more complex the more we add to it. It may now be time to consider improvements to keep it understandable, extensible and maintainable for the future.

From another discussion (!159 (comment 384528)):

In general about this issue/branch: it has been a few weeks since I last looked at this issue. It feels very complex. Every time I look at it I have to spend a lot of time getting into it again, and understanding the subtleties. Not sure whether it just is complex, or I'm not grasping it completely yet. I do realize now this is the reason I haven't looked into it sooner. It feels like a hurdle to get over every time, leading to me postponing the review each time. It also means that I've not yet been able to convince myself that it is all correct. I also worry about this having to be maintained.

Do you feel the same way? Is it complex, or does it just feel that way (to me)? If it is complex, where does this stem from, and could the complexity be reduced?

No doubt, it is really complex. Even before this branch and even before adding state/event exclusion plant invariants.

I feel that there are many 'concepts' we have to preconvert, all in a different manner, before we can actually do synthesis. We have state plant invariants, state requirement invariants, state/event exclusion plant invariants, state/event exclusion requirement invariants, variable ranges, plant edge guards, requirements automata, initial predicates, marked predicates.

The file is also very long, it does preconversion, synthesis, simplification, warn for disabled events, and print debug output. Might be good to move some to their own class, maybe?

Also a lot of 'emptying' BDDs and lists which all results in extra code.

Potential things to consider/discuss:

• Better/more documentation:
  • Document in the developer documentation the 'pseudocode' or step of the algorithm, such that we know what we handle, where we handle it, and in what order?
  • Document how to work with BDDs, and in particular the JavaBDD library that we use.
• Improve the code structure and data structures:
  • Split up the code into more files, each with a clear purpose?
  • Split things that represent the specification from things that are only for checking the input?
  • Split things that relate to synthesis from things that don't (such as representing the input, manipulating BDDs, etc)? (#706 (closed))
  • Split things that represent the uncontrolled system, requirements, controlled system?
  • Settings:
    • Don't pass all the settings around, but only the needed parts. See also !760 (comment 1608771).
    • Consider how to not pass all the settings as a long list of arguments to the constructor, and related issues. See #706 (comment 1700168), #706 (comment 1700403) #706 (comment 1700406) and #706 (comment 1700421). (!773 (merged))
  • Conversion from CIF to BDD could be improved:
    • Do more of the precondition checks before the conversion, leaving only the checks that can't be (easily) done to be checked during conversion. E.g. the non-determinism check.
    • Split it into more classes, with clear goal and that convert different aspects of the specification.
    • Split representation of the CIF specification in BDD form from data collected for debugging purposes, or only for synthesis. Makes it possible to later use the conversion to BDDs.
• Consider abstraction levels:
  • Abstractions to simplify the code we have, that hide some of the complexities of the top-level algorithms etc to some lower-level classes.
  • Abstractions around BDD. See e.g. !931 (comment 2471650).
  • Consider an abstraction layer to hide some of the details of BDDs:
    • Ideally we don't have to free manually to prevent memory leaks. See also #267.
    • Ideally we could hide some of the integer representation details. also for other CIF tools.
• Consider improving JavaBDD:
  • JavaBDD is a Java version of the BuDDy library. It has too much of a 'C' smell.
  • JavaBDD was also written in an old Java version. It could benefit from modernization using newer features.
• Other improvements
  • Use CIF common functionality where possible, rather than own code. (!797 (closed))

This issue is an overview of changes to consider. When we have a plan and start to address things, we should separate issues for them. That keeps it all easily traceable (clear connection to releases) and lean (addressing things one by one). This way we can progressively improve things one step at a time.