CIF multilevel partial specification builder doesn't replace discrete variables correctly
For a student, I quickly created a new plug-in to expose the partial specification builder, as part of multilevel synthesis, to end-users. (In case you're interested, see https://gitlab.eclipse.org/mgoorden7u4/escet/-/tree/expose-sub-specification?ref_type=heads.) Using this, I found the following bug where a discrete variable is not replaced by an algebraic variable.
Consider the following specification:
plant A:
controllable c;
disc int[0..2] x = 0;
location l1:
initial;
edge c do x := 1 goto l2;
location l2:
marked;
end
plant B:
controllable c;
location:
initial; marked;
edge c when A.x > 0;
end
If I run the partial spec builder code to keep only plant B, I get
group A:
disc int[0..2] x = 0;
end
plant automaton B:
controllable c;
location:
initial;
marked;
edge c when A.x > 0;
end
In this partial specification, disc int[0..2] x = 0; in group A should have been alg int[0..2] x = 0;.
This bug will never appear in running multilevel splitter, since either the source automaton of the discrete variable and the reference automaton will be part of the same plant group or requirement group as one of the first steps in multilevel splitting, or if it is a reference between an plant model and an requirement model, multilevel splitting will always place them in the same node.