The simulation encoding may model more traces than the one that is simulated.
The issue happen when there are more callbacks in the trace that do not contain any callin.
In that case the encoding cannot distinguish between the two callbacks, with the consequence that another trace (different from the original one) may be simulated.
The encoding is more permissive, so we can say that a trace can be simulated while in reality it is not the case.
with the specification: SPEC [CB] [ENTRY] [Z] void m1() |- [CB] [ENTRY] [M] void m2()
cannot be simulated, because m1 disable m2 and m1 must be executed before.
The current encoding can "simulate" the trace (in reality, visiting the sequence m2, m1).
Technically, the current encoding of simulation does not predicate on the message labels but on the transitions and enabled state.
The simulation encoding may model more traces than the one that is simulated.
The issue happen when there are more callbacks in the trace that do not contain any callin. In that case the encoding cannot distinguish between the two callbacks, with the consequence that another trace (different from the original one) may be simulated.
The encoding is more permissive, so we can say that a trace can be simulated while in reality it is not the case.
For example, the trace
with the specification:
SPEC [CB] [ENTRY] [Z] void m1() |- [CB] [ENTRY] [M] void m2()cannot be simulated, because
m1disablem2andm1must be executed before. The current encoding can "simulate" the trace (in reality, visiting the sequencem2,m1).Technically, the current encoding of simulation does not predicate on the message labels but on the transitions and enabled state.