This page describes how the list of enabled message events for a runtime state is computed. This computation is necessary after each invocation of the performStep method. Which events will become enabled depends on the active scenarios in the state.

Message Event exclusion rules

The update algorithm works as follows

1. Clean the old list
2. determine, if a safety violation was caused in either a specification or in an assumption scenario. If this is the case, see the section below.
3. Visit all active copies of scenarios and gather potentially enabled message events.
4. Exclude events that are blocked or stalled and add the remaining to the enabled events list.
5. Select the appropriate subset of message events (depending on expectations on system or environment)
6. Post-process the selected subset (remove messages excluded by object system state or parameter values, expand wildcards)

TODO are channels considered appropriately?

Step 3 (Gathering Phase)

From all active scenarios in the runtime state the following events are collected

• All environment events that appear in a scenario.
• from active specification scenarios: if the current enabled fragment is a modal message, collect all message events that are enabled by it, unless the modal message has expectedKind NONE or it is monitored. Also, the execution kind of the modal message is recorded.
• from active assumption scenarios: if the current enabled fragment is a modal message, collect all message events that are enabled by it, unless the sender is controllable, or the modal message is monitored. Also, the execution kind of the modal message is recorded.

Step 4 (Exclusion Phase)

From all events collected in step #3 remove all events, for which one of the following cases apply:

• The event is uncontrollable, but blocked by an assumption scenario
• The event is uncontrollable and non-spontaneous and there is no active assumption scenario with enabled message that is unifiable with the event.
• The event is controllable, but blocked by a specification scenario.

In each of the following cases a safety violation must be recorded in the runtime state:

• There exist committed controllable events, but they are all blocked. This is a safety violation of the specification.
• There exist urgent controllable events, but all controllable events are blocked. This is a violation of the specification.
• There exist committed uncontrollable events, but they are all blocked. This is a safety violation of the assumptions.

Step 5 (Selection Phase)

From the remaining events, enable ONE of the following subsets, when the condition is met

• if a committed system message is enabled in a specification scenario: all remaining committed controllable events
• if an urgent system message is enabled in a specification scenario: all remaining controllable events
• if there are remaining requested controllable events: all remaining controllable events
• if a committed environment message is enabled in an assumption scenario: all remaining committed uncontrollable events
• otherwise: all remaining uncontrollable events.

Step 6 (Post-Processing Phase)

Message events with wildcard parameters are merged. Message events that cause side effects are removed, if the side effects are not possible in the current state. Message events with parameter values outside of the allowed range are removed. Finally, the remaining events are added to the list of enabled message events of the runtime state.

When a safety violation occurred in the specification

TODO complete this.

When a safety violation occurred in the assumptions

TODO complete this.