Skip to content

Fix EdgeNoPartialVarAssignCheck for projections in multi-assignments

Adding the following to the EdgeNoPartialVarAssignCheck.cif test does not make that test fail, even though there is a new projected variable assignment on an edge, because the projection is inside a multi-assignment.

automaton partialInMulti:
  disc int x;
  disc tuple(int a, b) y;

  location:
    initial;
    edge do (x, y[0]) := (1, 2);
end

Note that:

  • The check is not used anywhere directly.
  • The check is part of EdgeOnlySimpleAssignmentsCheck, which is used by CIF to Supremica and CIF to UPPAAL. Neither supports multi-assignments.
  • As such, the bug is currently (on 2024-03-17) not visible to end users.
  • The multi-level synthesis tool will include EdgeOnlySimpleAssignmentsCheck as well, in !696 (merged). So that one is not affected either.
Edited by Dennis Hendriks