CifValueUtils: Always optimize generated conjunctions and disjunctions

I was looking at cif2uppaal, and [EDIT: found] many conditions with and false, or true, etc in the test output.

At first I thought to change that by using the optimized variations of createConjunction and createDisjunction, but while looking into that I wondered: "Why would we ever want non-optimized conditions?"

As an experiment I changed the plain create*junction functions to also emit optimized conditions, and ran all CIF tests. That gives the following diff output (deleted all the Test ..... lines that didn't report a change): test_output_changes.diff

• Look for ^--- to jump to the next diff.
• In general, I think the output improved. Many output lines became shorter and/or more readable.

  --- cif2uppaal/group_locref_inv.xml
  +++ cif2uppaal/group_locref_inv.xml.real
  @@ -29,7 +29,7 @@
       <transition>
         <source ref="id2"/>
         <target ref="id2"/>
  -      <label kind="guard">((LP_g_a == 0) &amp;&amp; (true)) || ((LP_g_a == 1) &amp;&amp; (false))</label>
  +      <label kind="guard">LP_g_a == 0</label>
         <label kind="synchronisation">e!</label>
         <label kind="assignment">OLDLP_g_a = LP_g_a</label>
       </transition>

• Codegen tends to shuffle the nodes a bit, eg

  --- codegen/databased_supervisor_c99/databased_supervisor_engine.c
  +++ codegen/databased_supervisor_c99_real/databased_supervisor_engine.c
  @@ -442,7 +442,7 @@
    */
   static BoolType execEdge3(void) {
       A6BType deref_store3 = bdd_values_();
  -    BoolType guard = (((Cycle_) == (_databased_supervisor_TurnLampOff)) && ((Lamp_) == (_databased_supervisor_On))) && (bdd_eval_(5, &deref_store3));
  +    BoolType guard = ((Cycle_) == (_databased_supervisor_TurnLampOff)) && (((Lamp_) == (_databased_supervisor_On)) && (bdd_eval_(5, &deref_store3)));
       if (!guard) return FALSE;

  Not sure, but I think this happens due to balancing the left and right nodes.
• Data-based synthesis has lots of changes.
  • It seems to affect the BDD representation, but not sure what the numbers mean:

    -        Backward uncontrolled bad-state: <bdd 65n 212,405,593p> [fixed point].
    +        Backward uncontrolled bad-state: <bdd 65n 212,406,593p> [fixed point].

  • Produced output is sometimes longer:

    -        Edge: (event: p.c8) (guard: (not p.l1 or p.v8 != 0) and (not p.l3 and not p.l2) -> false)
    +        Edge: (event: p.c8) (guard: p.v8 = 8 and p.l1 or p.v8 = 4 and p.l1 or ((p.v8 = 2 or (p.v8 = 6 or p.v8 = 10)) and p.l1 or (p.v8 = 1 or p.v8 = 3 or (p.v8 = 5 or (p.v8 = 7 or p.v8 = 9))) and p.l1) -> false)

In general I think this is a good step to implement, but I am worried about the synthesis changes.

What do you think?

assigned to @ahofkamp

changed the description

added CIF TypeEnhancement labels

I've added labels.

I've improved the title.

changed title from Always optimize generated conjunctions and disjunctions to CifValueUtils: Always optimize generated conjunctions and disjunctions

Some random thoughts that pop up:

• The optimized variant does more work, which could perhaps have performance implications. Not sure if that is significant enough to notice. Also, having simpler predicates in the remainder of the program or subsequent programs that are executed could win that back.
• For CIF to CIF linearization tests, it is less obvious whether the linearization works, as some parts are gone from the output. We could now see how the predicates are created, while with the change some parts of predicates are gone. The tests could have been created in a way that the truthness isn't the only thing that matters, but instead also the constructed predicates show what happens. This could mean we could be losing out on some testing usefulness, perhaps.
• It could be seen as separation of concerns. Linearization gives you a correct result. If you want a simplified result, use also 'simplify values' CIF to CIF transformation after it. Not sure this is a very strong argument. From the end user perspective, it is nicer if the predicates are automatically simpler.
• For codegen, it seems we get guards that are not shorter, but instead have different parentheses. If a conjunction has no 'true' or 'false' parts, apparently optimization can change something, but from the code I don't immediately see what happens then that causes it.
• For data-based synthesis, it affects the guards on edges, which affects the variable ordering heuristics. That predicates becomes larger for some tests is then not perse a bad thing. These are not benchmark models, so we can't conclude whether it improves or worsens performance in real cases, on average. We should probably run the benchmarks on develop and with this change, to see how that compares. Maybe it even improves synthesis performance? (If you want to do this, in a runtime, import the benchmarks project, edit benchmark__settings.tooldef so that get_benchmark_configurations returns ["", ""] (twice the default configuration). Then adapt get_benchmark_configurations_subset to return [1] and run it in develop (to run it, run each benchmark script as described in README.txt). Then adapt get_benchmark_configurations_subset to return [2] and run all benchmarks again, with the changed code. This way, the outputs of both runs are collected in the project. You can then run benchmark__generate_overview.tooldef to generate a single overview that includes both.

The optimized variant does more work, which could perhaps have performance implications.

It does one additional class check. If positive, it then improves the result. As you typically just created the nodes, its data likely still cached, so it's likely pretty much a free check. If it improves the result, you may also avoid a re-allocation of the array.

For CIF to CIF linearization tests, it is less obvious whether the linearization works, as some parts are gone from the output.

One way out of this is to set the default to true optimization, and in the above case disable it. Probably that is not a proper solution though.

The current test is lazy and uses the standard conversion back-end. It's thus not testing only linearization, it's also testing the conversion back-end.
For a clean test it should just linearize and then directly check it has the expected form, rather than do a conversion by some other code which may give wrong or fake answers.

I don't consider this a valid counter-argument.

If you want a simplified result, use also 'simplify values' CIF to CIF transformation after it.

If a user handles the specification, sure. From a performance point of view that is a horrible solution, just looking for the guards again takes more time than optimizing them as you create them.

It also doesn't work for applications that do these conversions internally without at least large costs as the user has to do them, and then the tool does them all again. With some unparsing and parsing of the specification in-between.

For a clean test it should just linearize and then directly check it has the expected form, rather than do a conversion by some other code which may give wrong or fake answers.

The CIF pretty printer doesn't do that much. It won't simplify conjunctions.

I don't consider this a valid counter-argument.

My point was that it affects the usefulness of existing tests, so maybe the tests should then be adapted/improved. It was not meant as argument not to make the change, only that it has consequences that may need to be mitigated as well then.

If you want a simplified result, use also 'simplify values' CIF to CIF transformation after it.

If a user handles the specification, sure. From a performance point of view that is a horrible solution, just looking for the guards again takes more time than optimizing them as you create them.

It also doesn't work for applications that do these conversions internally without at least large costs as the user has to do them, and then the tool does them all again. With some unparsing and parsing of the specification in-between.

Indeed, performance is better if done immediately. And I agree that if the output is not a CIF file, then you can't apply a CIF to CIF transformation. I agree it would be better to do it automatically, as that is nicer for users.

I ran the test, here is the result: _overview.html

Most models have no difference at all, and some have a small difference.

The wafer model was the only exception, where the number of BDD operations decreased noticably:

This is good news, I think. Seems nothing that is important enough is in the way of doing this change.

We may however still need to think of how it affects the tests then, and whether it is necessary for them to be adapted afterwards in some way. And I'm still confused by the different parentheses for codegen output.

Could be good to also do a usage check, for where the methods are used directly and indirectly, to see if anything else is possibly affected that doesn't show up in the output of tests. The Eclipse IDE's 'Call Hierarchy' function can answer this. May need this information also to determine what to write in the release notes at some point.

About codegen: I hacked the program a bit, and printed the guard of the execEdge3 output method while it was processed:

• execEdge3 guard text is produced with CifTextUtils.exprToStr(guard), while
• code guard is the c99 codegen conversion output (also listed in the description of this issue).

exprToStr is somewhat smart in detecting that it doesn't need to generate parentheses in a case like here (lines 460-480).

Original

execEdge3: guard = M.Cycle = TurnLampOff and M.Lamp = On and bdd_eval(5, bdd_values)
code: (((Cycle_) == (_databased_supervisor_TurnLampOff)) && ((Lamp_) == (_databased_supervisor_On))) && (bdd_eval_(5, &deref_store3))

Optimized

execEdge3: guard = M.Cycle = TurnLampOff and (M.Lamp = On and bdd_eval(5, bdd_values))
code: ((Cycle_) == (_databased_supervisor_TurnLampOff)) && (((Lamp_) == (_databased_supervisor_On)) && (bdd_eval_(5, &deref_store3)))

The difference is that the original guard from LinearizeMerge was (A and B) and C, while tree balancing in the optimized case produces A and (B and C).
Codegen isn't smart at all in handling parentheses, it just follows the CIF expression tree and thus parentheses are 'moved'.

I don't see an easy answer for linearize-merge tests.

The LinearMerge class generates guards and optimizes them in the same call. cif2cif app class does pretty-printing, but that is too late anyway.

You would somewhat need to have a skipOptimize flag, and then magically set it, just for this test. Alternatively, it would need its own guard creation code, but that is a bit stupid too.

Maybe the existing tests are more about cif2cif app rather than linearize. I didn't check what LinearizeMerge is doing, but if we split the linearisation away from the other code, we could write tests around that. The trouble is then that you don't have easy input facilities like you have now, but maybe that isn't actually needed anyway, depending on the scale of the tests.

The difference is that the original guard from LinearizeMerge was (A and B) and C, while tree balancing in the optimized case produces A and (B and C).
Codegen isn't smart at all in handling parentheses, it just follows the CIF expression tree and thus parentheses are 'moved'.

I still don't why there is a difference in the parentheses. CifValueUtils.createConjunction always flattens binary expressions and builds a balanced tree. With optimization enabled, the only extra thing it does is to optimize for true and false boolean literal entries. Since there are no true and false boolean literals in this example, I don't see why turning on optimization would lead to a difference here, as it should have no effect. I must be missing something, but what?

You would somewhat need to have a skipOptimize flag, and then magically set it, just for this test. Alternatively, it would need its own guard creation code, but that is a bit stupid too.

We could do that. Add the flag to the transformation. And then have a TestLinearizeMerge or so derived class that sets it. Then we can test that one instead. However, then we'd also need a custom application, that has different transformations registered, as we don't want end users to see this transformation being listed. All in all, not a great design, I think.

Maybe the existing tests are more about cif2cif app rather than linearize. I didn't check what LinearizeMerge is doing, but if we split the linearisation away from the other code, we could write tests around that. The trouble is then that you don't have easy input facilities like you have now, but maybe that isn't actually needed anyway, depending on the scale of the tests.

The CIF to CIF transformer doesn't do more than load, transform, save, so it is about as basic an integration test we can have for a CIF to CIF transformation. In general, it works well and easy, as we can just have some input files and check that what comes out is as expected. It is easy to extend to more tests and more transformations. And for most of these transformations, and end-to-end/integration test is sufficient. It is just practical.

---

I looked at the diff again. It seems the changes are in initialization, marking and edge guards only. I could imagine creating some new/additional unit tests for those, and then just accepting the changes to the integration test output. So, only creating some new unit tests for:

• LinearizeBase.mergeLocInvInitMarked: Make it package private. Then in the test create an instance of it, and invoke the method for some automata that we create in memory. Shouldn't be too much work.
• LinearizeMerge.createEdges and LinearizeProduct.createEdges: Can be done similarly. Already protected, so doesn't need a change in access modifier.

I checked all calls to the methods that would change:

• Controller properties checker (due to CIF to BDD changes): may get different performance and debug output.
• Data-based synthesis (due to CIF to BDD changes): may get different performance and debug output.
• CIF to CIF linearization product/merge transformations: they may get different output for edge guards, for urgency guards, and for initialization/marker predicates from locations.
• CIF to CIF eliminate monitors: may get different output for edge guards and send values.
• CIF to UPPAAL: may get different output for edge guards.
• CIF to Supremica: may get different output for edge guards and state invariant predicates.

Maybe need to test LinearizeBase.handleUrgency as well.

I still don't why there is a difference in the parentheses.

Call to balancing:

        // flattenedChildren = list [A, B, C].

        int treeSize = flattenedChildren.size();
        return createBalancedBinaryTree(flattenedChildren, 0, treeSize, operator);

Function

public static Expression createBalancedBinaryTree(List<Expression> exprs, int lower, int upper, BinaryOperator operator)

        // Omitted base-case handling.

        // Get mid point index.
        int size = upper - lower;   // = 3 - 0 = 3
        int left = size / 2;        // = 3 / 2 = 1
        int mid = lower + left;     // = 0 + 1 = 1

        // Recursive call:
        rslt.setLeft(createBalancedBinaryTree(exprs, lower, mid, operator));   // That is, exprs[0..1)  -> list [A]
        rslt.setRight(createBalancedBinaryTree(exprs, mid, upper, operator));  // That is, exprs[1..3)  -> list [B, C]

Yes, I get that flattening and rebalancing can change the parentheses. But, whether we do optimization or not, CifValueUtils.createConjunction always flattens and rebalances. That doesn't change by enabling optimization. So, why is the output different if all we do differently is optimize, and optimize only affects true and false literals, which we don't have (there are no true or false literals in M.Cycle = TurnLampOff and M.Lamp = On and bdd_eval(5, bdd_values)).

Ah right. I don't know :p

Euhm, no. That is not true.

LinearizeMerge doesn't optimize currently: Near line 309 (and there is another such pair near line 393 for loc/guards/updates):

                        // Add 'loc and guards' : 'value' pair.
                        Expression lexpr = lpIntroducer.createLocRef(loc);
                        Expression guards = createConjunction(deepclone(edge.getGuards()));
                        EdgeSend sendEdge = (EdgeSend)edgeEvent;
                        Pair<Expression, Expression> pair;
                        pair = pair(createConjunction(list(lexpr, guards)), deepclone(sendEdge.getValue()));

This calls createConjunction, but it doesn't have true as second argument. It's thus not optimizing in the original situation.

We had the non-optimizing variant, and added an optimize parameter, which is by default false in the original situation. In the optimized situation, linearization is also optimizing, and you get a different execEdge3 expression from LinearizeMerge.

Codegen itself doesn't use createConjunction at all.

So, codegen isn't using it by itself, but only via linearization. That's fine.

If LinearizeMerge is now optimizing, and it wasn't before, then I still don't get the parentheses changes in codegen output. The optimization, as I've stated before, only differs in handling of true and false literals. See here. It always does flattening and rebalancing. The example that has changed parentheses doesn't have true or false literals.

In any case, the answer is in LinearizeMerge I think.

If you've only changed CifValueUtils.createConjunction, and linearization hasn't been changed, then the output change must be due to CifValueUtils.createConjunction changes and calls to it. It is maybe good to create a minimal example that shows the different parentheses problem for codegen. And then trace where the old/new situation start to differ, as there must be such a moment.

Makes sense.

I pulled databased_supervisor.cif through linearize-merge in develop and the optimizing branch.

The difference is in the generated M automaton for monitoring events. For the c_off event, the output is:

// develop
edge .Lamp.c_off
    when
            (Cycle = .Cycle.WaitForButtonPush and false
        or Cycle = .Cycle.TurnLampOn and false
        or (Cycle = .Cycle.StartTimer and false
        or (Cycle = .Cycle.WaitForTimeout and false
        or Cycle = .Cycle.TurnLampOff and true)))
    and (Lamp = .Lamp.Off and false
        or Lamp = .Lamp.On and true)
    and (true and bdd_eval(5, bdd_values))
    do Cycle := .Cycle.WaitForButtonPush, Lamp := .Lamp.Off;

// optimized:
edge .Lamp.c_off
    when
        Cycle = .Cycle.TurnLampOff
    and (Lamp = .Lamp.On
        and bdd_eval(5, bdd_values))
    do Cycle := .Cycle.WaitForButtonPush, Lamp := .Lamp.Off;

In develop, the guard has or sub-trees at the left that needs brackets. In the optimized case it's only and so these can be taken together.

I think the culprit is that in a tree with nested and/or operators, we handle sub-trees by operator. If a sub-tree becomes a single node, it can become part of optimizing one level higher.

I don't see that happening in create{doc,dis}junctions.

I think the culprit is that in a tree with nested and/or operators, we handle sub-trees by operator. If a sub-tree becomes a single node, it can become part of optimizing one level higher. I don't see that happening in create{doc,dis}junctions.

We always flatten and rebalance, regardless of whether we optimize or not.

I pulled databased_supervisor.cif through linearize-merge in develop and the optimizing branch. The difference is in the generated M automaton for monitoring events. For the c_off event, the output is: [...]

I think we should do the analysis on this example, not the one from data-based synthesis. In that example, no parts are optimized away, it seems, but still we get different parentheses.

I think we should do the analysis on this example ...

The above is that example.

databased_supervisor.cif is in codegen tests.

We always flatten and rebalance, regardless of whether we optimize or not.

If you flatten and optimize top-down, it will miss cases like X and ((A and B and C) or false).

Note that create{con,dis}junction doesn't traverse sub-trees with a different operator, and rebalance just recursively shifts the mid-point.

That is, any combining of trees with a different operator is done outside the create*junctions functions.

Dump patch against develop:

diff --git a/cif/org.eclipse.escet.cif.cif2cif/src/org/eclipse/escet/cif/cif2cif/LinearizeMerge.java b/cif/org.eclips
e.escet.cif.cif2cif/src/org/eclipse/escet/cif/cif2cif/LinearizeMerge.java
index f5a21625c..e63e17604 100644
--- a/cif/org.eclipse.escet.cif.cif2cif/src/org/eclipse/escet/cif/cif2cif/LinearizeMerge.java
+++ b/cif/org.eclipse.escet.cif.cif2cif/src/org/eclipse/escet/cif/cif2cif/LinearizeMerge.java
@@ -158,6 +158,10 @@ public class LinearizeMerge extends LinearizeBase {
         for (int i = 0; i < events.size(); i++) {
             Expression guard = CifGuardUtils.mergeGuards(syncAuts.get(i), sendAuts.get(i), recvAuts.get(i),
                     moniAuts.get(i), events.get(i), creator);
+                        if ("c_off".equals(events.get(i).getName())) {
+                                System.out.printf("LinMerge, line 160, c_off event: merged guards: %s\n",
 CifTextUtils.exprToStr(guard));
+                            }
+
             guards.add(guard);
         }
 
diff --git a/cif/org.eclipse.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/CodeGen.java b/cif/org.eclipse.escet
.cif.codegen/src/org/eclipse/escet/cif/codegen/CodeGen.java
index a3430415a..afcac0f03 100644
--- a/cif/org.eclipse.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/CodeGen.java
+++ b/cif/org.eclipse.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/CodeGen.java
@@ -879,6 +879,23 @@ public abstract class CodeGen {
             String prev = origDeclNames.put(entry.getKey(), entry.getValue());
             Assert.check(prev == null);
         }
+        List<Automaton> automata = listc(1);
+        CifCollectUtils.collectAutomata(spec, automata);
+        Assert.check(automata.size() == 1);
+        Automaton aut = first(automata);
+        Assert.check(aut.getLocations().size() == 1);
+        Location loc = first(aut.getLocations());
+        List<Edge> edges = loc.getEdges();
+        List<Edge> controllableEdges = edges.stream().filter(edge -> {
+            Event evt = CifEventUtils.getEvent(edge);
+            return evt.getControllable();
+        }).toList();
+        for (Edge edge: controllableEdges) {
+            EdgeEvent edgeEvent = edge.getEvents().get(0);
+            Event event = ((EventExpression)edgeEvent.getEvent()).getEvent();
+            if (!"c_off".equals(event.getName())) continue;
+            System.out.printf("after-linearize: controllable edge %s: %s\n", event.getName(), CifTextUtil
s.exprsToStr(edge.getGuards()));
+        }
 
         // Eliminate type declarations for easier code generation.
         new ElimTypeDecls().transform(spec);
@@ -898,8 +915,28 @@ public abstract class CodeGen {
         // variant, for performance reasons.
         new SimplifyValuesNoRefsOptimized().transform(spec);
 
+        automata = listc(1);
+        CifCollectUtils.collectAutomata(spec, automata);
+        Assert.check(automata.size() == 1);
+        aut = first(automata);
+        Assert.check(aut.getLocations().size() == 1);
+        loc = first(aut.getLocations());
+        edges = loc.getEdges();
+        controllableEdges = edges.stream().filter(edge -> {
+            Event evt = CifEventUtils.getEvent(edge);
+            return evt.getControllable();
+        }).toList();
+        for (Edge edge: controllableEdges) {
+            EdgeEvent edgeEvent = edge.getEvents().get(0);
+            Event event = ((EventExpression)edgeEvent.getEvent()).getEvent();
+            if (!"c_off".equals(event.getName())) continue;
+            System.out.printf("simplify: controllable edge %s: %s\n", event.getName(), CifTextUtils.exprs
ToStr(edge.getGuards()));
+        }
+
         // Add default initial values for easier code generation.
         new AddDefaultInitialValues().transform(spec);
+
+
     }
 
     /**
@@ -1053,6 +1090,12 @@ public abstract class CodeGen {
             Event evt = CifEventUtils.getEvent(edge);
             return evt.getControllable() && !svgInEvents.contains(evt);
         }).toList();
+        for (Edge edge: controllableEdges) {
+            EdgeEvent edgeEvent = edge.getEvents().get(0);
+            Event event = ((EventExpression)edgeEvent.getEvent()).getEvent();
+            if (!"c_off".equals(event.getName())) continue;
+            System.out.printf("generateCode: controllable edge %s: %s\n", event.getName(), CifTextUtils.e
xprsToStr(edge.getGuards()));
+        }
         Assert.areEqual(edges.size(), svgInEdges.size() + uncontrollableEdges.size() + controllableEdges.size());
         addEdges(ctxt, cifSpecFileDir);
 
diff --git a/cif/org.eclipse.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/c99/C99CodeGen.java b/cif/org.eclips
e.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/c99/C99CodeGen.java
index 7bc1379b1..10d5108c7 100644
--- a/cif/org.eclipse.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/c99/C99CodeGen.java
+++ b/cif/org.eclipse.escet.cif.codegen/src/org/eclipse/escet/cif/codegen/c99/C99CodeGen.java
@@ -58,6 +58,7 @@ import org.eclipse.escet.cif.codegen.updates.tree.LhsProjection;
 import org.eclipse.escet.cif.codegen.updates.tree.LhsTupleProjection;
 import org.eclipse.escet.cif.codegen.updates.tree.SingleVariableAssignment;
 import org.eclipse.escet.cif.common.CifDocAnnotationUtils;
+import org.eclipse.escet.cif.common.CifTextUtils;
 import org.eclipse.escet.cif.metamodel.cif.automata.Edge;
 import org.eclipse.escet.cif.metamodel.cif.declarations.AlgVariable;
 import org.eclipse.escet.cif.metamodel.cif.declarations.Constant;
@@ -1106,8 +1107,15 @@ public class C99CodeGen extends CodeGen {
             // Add edge code.
             if (guard != null) {
                 ExprCode guardCode = ctxt.exprToTarget(guard, null);
-                codeMethods.add(guardCode.getCode());
-                codeMethods.add("BoolType guard = %s;", guardCode.getData());
+                CodeBox code1 = guardCode.getCode();
+                codeMethods.add(code1);
+
+                String data = guardCode.getData();
+                codeMethods.add("BoolType guard = %s;", data);
+                if (eventName.equals("Lamp.c_off")) {
+                    System.out.printf("guard c_off: %s\n", CifTextUtils.exprToStr(guard));
+                    System.out.printf("code: %s\n", data);
+                }
                 codeMethods.add("if (!guard) return FALSE;");
                 codeMethods.add();
             }

always optimize patch:

diff --git a/cif/org.eclipse.escet.cif.common/src/org/eclipse/escet/cif/common/CifValueUtils.java b/cif/org.eclipse.e
scet.cif.common/src/org/eclipse/escet/cif/common/CifValueUtils.java
index 4bbd40be1..f17c0473c 100644
--- a/cif/org.eclipse.escet.cif.common/src/org/eclipse/escet/cif/common/CifValueUtils.java
+++ b/cif/org.eclipse.escet.cif.common/src/org/eclipse/escet/cif/common/CifValueUtils.java
@@ -2306,7 +2306,7 @@ public class CifValueUtils {
         // For the downside of balanced trees, and potential solutions,
         // see the 'createConjunction(List, boolean)' method.
 
-        return createConjunction(exprs, false);
+        return createConjunction(exprs, true);
     }
 
     /**
@@ -2416,7 +2416,7 @@ public class CifValueUtils {
         // For the downside of balanced trees, and potential solutions,
         // see the 'createConjunction(List, boolean)' method.
 
-        return createDisjunction(exprs, false);
+        return createDisjunction(exprs, true);
     }
 
     /**

Output for develop + dump patch for codegen test databased_supervisor.cif:

LinMerge, line 160, c_off event: merged guards: (M.Cycle = Cycle.WaitForButtonPush and false or M.Cycle = Cycle.TurnLampOn and false or (M.Cycle = Cycle.StartTimer and false or (M.Cycle = Cycle.WaitForTimeout and false or M.Cycle = Cycle.TurnLampOff and true))) and (M.Lamp = Lamp.Off and false or M.Lamp = Lamp.On and true) and (true and bdd_eval(5, bdd_values))
after-linearize: controllable edge c_off: (M.Cycle = Cycle.WaitForButtonPush and false or M.Cycle = Cycle.TurnLampOn and false or (M.Cycle = Cycle.StartTimer and false or (M.Cycle = Cycle.WaitForTimeout and false or M.Cycle = Cycle.TurnLampOff and true))) and (M.Lamp = Lamp.Off and false or M.Lamp = Lamp.On and true) and (true and bdd_eval(5, bdd_values))
simplify: controllable edge c_off: M.Cycle = TurnLampOff and M.Lamp = On and bdd_eval(5, bdd_values)
generateCode: controllable edge c_off: M.Cycle = TurnLampOff and M.Lamp = On and bdd_eval(5, bdd_values)
guard c_off: M.Cycle = TurnLampOff and M.Lamp = On and bdd_eval(5, bdd_values)
code: (((Cycle_) == (_databased_supervisor_TurnLampOff)) && ((Lamp_) == (_databased_supervisor_On))) && (bdd_eval_(5, &deref_store3))

With the optimize patch in as well:

LinMerge, line 160, c_off event: merged guards: M.Cycle = Cycle.TurnLampOff and (M.Lamp = Lamp.On and bdd_eval(5, bdd_values))
after-linearize: controllable edge c_off: M.Cycle = Cycle.TurnLampOff and (M.Lamp = Lamp.On and bdd_eval(5, bdd_values))
simplify: controllable edge c_off: M.Cycle = TurnLampOff and (M.Lamp = On and bdd_eval(5, bdd_values))
generateCode: controllable edge c_off: M.Cycle = TurnLampOff and (M.Lamp = On and bdd_eval(5, bdd_values))
guard c_off: M.Cycle = TurnLampOff and (M.Lamp = On and bdd_eval(5, bdd_values))
code: ((Cycle_) == (_databased_supervisor_TurnLampOff)) && (((Lamp_) == (_databased_supervisor_On)) && (bdd_eval_(5, &deref_store3)))

It seems the cause is that simplify doesn't balance the result.

So, before, the simplification happened by the CIF to CIF 'simplify other' transformation after linearization. It just recurses over the model and replaces certain cases like X and true by X, etc. It then proceeds to the parent, etc, etc. That indeed does not rebalance.

Now, we do prevent it from even being created like that in linearization, and as you pointed out, that allows to also rebalance and optimize over multiple levels.

Makes sense. Thanks for figuring it out. Now that we understand the cause, I don't have a problem with this change occurring.

changed milestone to %v7.0

Since the issue is assigned, I've added the current milestone.

mentioned in commit 3ec3b8cd

mentioned in commit 03b40c49

mentioned in merge request !1257 (merged)

mentioned in commit 6b2f6531

mentioned in commit 3abe757e

closed with merge request !1257 (merged)