There are no warnings for uncontrollable events that are never enabled in the controlled system for datasynth
Consider the following example. Event u_synch
is never enabled. However, there is no warning for that. We should compute the and
of the linearized guard(s)(?) and the ctrlBeh
predicate and check whether that isZero()
.
controllable c_off, c_on;
uncontrollable u_synch;
plant a:
location l1:
initial; marked;
edge c_off goto l2;
edge u_synch;
location l2:
marked;
edge c_on;
end
plant b:
location l1:
initial; marked;
edge c_off goto l2;
location l2:
marked;
edge c_on;
edge u_synch;
end