Add warning message for event not enabled in controlled state space for databased synthesis.

See: #144 (comment 91143)

Whenever we enable Perform forward reachability, we compute a "Controlled-behavior predicate of the system". This predicate contains all reachable states in the controlled behavior. We use that for simplifying the supervisor guard with GUARDS_CTRL_BEH.

It can be that an event is never enabled because the state where it is enabled is never reached. Currently, a user is aware of this because the supervisor guard is false. For these cases, we generate the warning message that the supervisor disables this event (which is not really true, I'll get to that). When we simplify the supervisor's guard under the assumption of GUARDS_CTRL_BEH, the guard will be simplified to true. Hence, the user will not receive a warning message.

Suggestion: we should generate a warning message "Warning event "<event>" is never enabled in the controlled state-space.". Specifically, the event should be disabled before taking into account the supervisor guards for that event. This error message we can only generate if Perform forward reachability is enabled, otherwise the predicate is not available. If Perform forward reachability is not enabled, we'll get the "event disabled by supervisor"-warning message.

Ideally, we would want to differentiate between the uncontrolled state-space and the controlled state-space, for warning messages. However, since we don't generate a predicate for the uncontrolled state-space that is not possible. For example, for the models below, even though the events are not enabled in the input specification, we don't have that information available. We only know that these events are not enabled in the controlled state-space. Still, it gives more information than the current approach.

Example model where it is easy to see that event c_on is never enabled:

controllable c_on;

plant a:
  location l1:
    initial; marked;
  location l2:
    marked;
    edge c_on;
end

Example model where is more difficult to see that c_synch is never enabled:

controllable c_off, c_synch;

plant a:
  location l1:
    initial; marked;
    edge c_off goto l2;
    edge c_synch;
  location l2:
    marked;
end

plant b:
  location l1:
    initial; marked;
    edge c_off goto l2;
  location l2:
    marked;
    edge c_synch;
end