CIF to CIF linearization blow-up detection and fixes

Changes to consider:

• Improved linearization algorithm that doesn't blow up as much, but still preserves all behavior (!1418 (merged))
• Don't compute all combinations and then convert them, but stream them instead (!1431 (merged))
• Detect blow-up at runtime and warn the user about it

Original description

During my research internship at the Radboud university we encountered a model which would not get past linearization, as the program ran out of memory after 158 seconds. The problem was that one event got over one million linearized edges. This event clearly sticks out in the graph below, showing the average linearization time per 100 iterations. As linearization continues, the problematic event required more and more memory, which in turn affected the time per iteration.

The resulting number of linearized edges is equal to the product of edges over an event. This aspect was the root of the problem for a model, as the requirement definition below was used to construct thirteen automata using the same event for reset. This resulted in 2^13 linearized edges as each instantiation of Observer using the same event for reset multiplies the possibilities by two, one for the self-loop created due to the monitoring of reset and one for the other edge.

We can transform this automaton definition to only have one edge over reset and include a conditional expression updating state, as can be seen in the figure below. Now the resulting linearized edges over reset is equal to 1^13.

Currently, it is hard to know when to apply this transformation, as it is difficult to find out which event caused linearization to blow-up. A linearization blow-up detection would be a nice addition to the ESCET toolkit as it can inform developers what event caused linearization to blow-up. Time seems to be exponentially correlated to the total number of linearization iterations over one event. Therefore, a possible solution could be to apply linear regression on the logarithm of the linearization iteration time, of a given event, to predict the total required time. Time is probably a good variable to use as it adjusts alongside, possible, future linearization changes. We suggest not to start to early with the prediction of the total linearization time, as early time growth might not be representative for the overall time function. We also advise to issue a linearization blow-up warning relative conservatively, for example, when linearization requires more than 150 seconds. Contact @ddennis for more information.