Skip to content

CIF may produce false warning for globally disabled event that is monitored

While working on #298 (closed) I noticed the following. Consider the following specification:

group def D():
    event a;
end

automaton def A(D x):
    alphabet x.a;
    monitor x.a;
    location l1:
        initial;
end

X: D();
Y: D();
B: A(X);

It has the following warning:

The alphabet of automaton "A" globally disables event "D.a", as the event is not used on any of the edges of the automaton.

Which is incorrect. The warning should be:

Automaton "A" monitors event "D.a", but the event is not used on any of the edges of the automaton.

The problem is in AutScope, line 398. There we check whether eventRef is contained within monitorSet. However, eventRef is unwrapped whereas the events within monitorSet are wrapped.

Edited by Ferdie Reijnen