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?