While a refinement tree diagram shows how a chain of refinement of Event-B machines, an event transition diagram focuses more on how events in a machine interact with each other. The main purpose of this diagram is to help stakeholders understand how a system behaves through a flow of events. The information appeared in this diagram is from the refinement tree diagram. Hence, the event transition diagram is always used with the refinement tree diagram.
For the event transition diagram, we define that after an event is executed, the actions of the event might trigger some other events. Then, the system make a transition from the former event to the execution of the next event. This causes a chain of execution of events (a flow of events).
The following subsections explained components and links of the event transition dia-gram and its association with the refinement tree diadia-gram.
4.4.1 Components and links
The transitions of events are similar to transitions of states of a system. There are various diagrams for demonstrating transitions of states such as UML state diagram [SB06], and finite state machine diagram [Gil70]. Usually, a state is denoted by a circle and a transition is denoted by an arrow from one state to another. We also apply this concept to define our event transition diagram.
Event
An event is denoted by a circle with the name of the event is written inside. Figure 4.10 shows the appearance of an event in the event transition diagram.
Event
Figure 4.10: An event
Note that the name written in the circle must conform to the name of the event in a refinement tree diagram. This is for cross-reference between two diagrams.
Since every Event-B machine must contain an initialization event for initiating variables, the notation of the initialization is also defined in our diagram. The initialization event is denoted a black circle as in Figure 4.11.
Event
Figure 4.11: An initialization event
Event transition
After an event is executed, the state of variables of a system is changed. This might cause another event to be executed. We represent the transition from one event to another by using an arrow from the former event to the next event. This arrow might be tagged with
‘before’ relationship to show that one event is executed before another. We can name the relation and write the name after the ‘before’ relation. If we name the relation, the name must also appear in the refinement tree diagram in the level which corresponds with the event transition diagram. Figure 4.12 shows a one-to-one transition from one event to another.
Event1 [Before] Event2
Transition_name
Figure 4.12: One-to-one transition
Some event might be able to trigger more than one event. In this case, two or more arrows which has the same event as their origin are allowed. This can be regarded as one-to-many transitions. Figure 4.13 shows an example of the one-to-many transitions.
Note that the one-to-many transitions defined here mean that after the former event is executes, there is only one event to be executed at a time, depending on the results of the former event.
Parallelized event
The one-to-many transitions mean that one event is triggered at a time. In the case of more than one event can be triggered and they can be executed in parallel, the parallelized events are grouped into one rectangle. If there is a transition from an event to a group of parallelized events, an arrow can be pointed directly to the rectangle representing the
Event1
Event2
Event3
Event4
Figure 4.13: One-to-many transition
group of events. The parallelized events might have distinct destination of transitions, so each event can have its own transition arrows to trigger some other events. Figure 4.14 shows an example of a transition from an event to a group of parallelized event and then each parallelized event has a distinct transition to some other events.
Event2 Event3
Event1
Event5 Event4
Figure 4.14: Transitions of parallelized event
Note that, according to the semantics of Event-B specification, the execution of paral-lelized events does not overlap, but it means that the order of execution is arbitrary.
4.4.2 Association with the refinement tree diagram
As mentioned before, the information appeared in the event transition diagram must be traceable to the corresponding level of a refinement tree diagram. The associations between elements of the refinement tree diagram and the event transition diagram are thoroughly described in this subsection.
Event
All events appeared in a level of a refinement tree must also be in the corresponding event transition diagram. The name of events appeared in both diagrams must be the same.
‘Before’ relationship
When there is a ‘before’ relation from one event to another, the relation must appeared in both the event transition diagram. The direction of a relation in an event transition diagram can be specified through the direction of an arrow. However, the direction of the relation in the corresponding refinement tree diagram is vague, because the the bold line itself has no direction. In facts, the direction can be shown in both left-to-right and right-to-left ways. Figure 4.15 respectively shows the left-to-right and right-to-left ways to represent the ‘before’ relationship from Figure 4.12 in a refinement tree diagram.
Event2 When G_2 Then Act_2 Event1
When G_1 Then Act_1
[Before >]
Transition_name
(a) Left-to-right ‘before’ relationship
Event1 When G_1 Then Act_1 Event2
When G_2 Then Act_2
[< Before]
Transition_name
(b) Right-to-left ‘before’ relationship
Figure 4.15: ‘Before’ relationship in a refinement tree diagram
Parallelized events
Events in the same group of parallelized events can be shown in the refinement tree diagram through the ‘parallel’ relationship. Figure 4.16 shows how to represent the events Event2 and Event3 from Figure 4.14 in a refinement tree diagram.
4.4.3 Example
Figure 4.17 shows an example of a event transition diagram. In this example, after the initialization, Event1 will be executed. The results of execution of both Event1 and Event2 can trigger the same group of parallelized events Event3 and Event4. Event4
Event1 When G_1 Then Act_1 Event2
When G_2 Then Act_2
[Parallel]
Figure 4.16: ‘Parallel’ relationship in a refinement tree diagram
Event3
Event1
Event4
[Before]
transition1 Event2
[Before]
transition2
Figure 4.17: An example event transition diagram
does not trigger any event after its execution. Lastly, Event3 can trigger both Event1 and Event2, but just one event at a time.