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 withGUARDS_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 ofGUARDS_CTRL_BEH
, the guard will be simplified totrue
. 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 ifPerform forward reachability
is enabled, otherwise the predicate is not available. IfPerform 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