See: https://gitlab.eclipse.org/eclipse/escet/escet/-/issues/144#note_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 ```