Skip to content

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