Testing and Events
Frequently, a system under test (SUT) will emit events. Spec Explorer's view is that an event is a message from the SUT to a test case at test execution time. Spec Explorer's role is to construct the test case so that it can receive the event and act appropriately.
Modeling Events
From the model's perspective, an event is like any other action. The model itself does not implement, raise, or subscribe to events; it only specifies in which states the given event is expected. Semantically, the model is saying "This event can be raised by the SUT when the SUT is in this state; if this event is raised, transition to the appropriate next state". These semantics are identical to the semantics of any other action.
During model exploration, Spec Explorer will produce steps in the exploration graph for events that the SUT can emit. Note that the model must actually model the events; otherwise, the model is stating that no events are to be expected.
Testing
During the construction of a test case, Spec Explorer will select one of the possible call/return steps from a given state. However, all relevant event steps are selected. Thus, the test case will expect either a given call/return, or any of the possible events for that state.
When the test case is built, Spec Explorer will insert expect statements for each possible event.
From the SUT side, the SUT (or the test adapter) must declare event variables for each event declared as an action in the Cord script. Then, the SUT (or test adapter) must raise the event when it wants to notify the test case that something has happened.
When the test case is actually run, the test infrastructure will subscribe to the event variables declared in the SUT (or adapter).
One important thing to note is that an event from the SUT (or adapter) is placed on an event queue, for future consumption by an expect statement. Consumption of the event means that the test case compares the event to the allowed event steps for that state; if the event (and its arguments) matches one of the allowed event steps, the test proceeds to the next state. The event queue is a FIFO queue; the first event on the queue is examined, and if it does not match an expected event from the current state, a conformance error results. If the SUT emits multiple events, they are queued in the order in which they are received.