4.1.7 Add Event Handler

In this Section we learn how we can enhance our visualization with interactive features, e.g. executing an Event-B event by clicking on a graphical element.

Checkout Section 4.2.3 for more details about event handlers.

Let’s add an interactive feature, where the user can click on a floor label to order the lift on the corresponding floor. Add this code snippet to your script.js file:

bms.executeEvent({
  selector: "text[data-floor]",
  events: [
    {
      name: "push_call_button", 
      predicate: function (origin) {
        return "b=" + origin.attr("data-floor")
      }
    }
  ]
});

In line 1 we register an execute event handler for each graphical element that matches the defined selector “text[data-floor]” (line 2). In particular, the selector matches the three floor labels (see Figure 4.1). In line 3 to 10 we define the list of events that should be wired with the graphical elements. Every event should contain the name. In addition, the user may enter a predicate that defines the event’s arguments. If the user defines more than one event, a tooltip will be shown with a list of the defined events after clicking on the graphical element. In our example we define only one event with the name and the predicate that is determined by a closure that passes a reference to the element (origin). In particular, we use the value of the attribute data-floor of the corresponding floor label (origin) to define the event parameter (line 6).

Apply these changes by clicking on the Reload button and try to click on a floor label. This should call the Event-B event push_call_button with the corresponding predicate/parameter.

Let’s add another interactive feature, where the user can click on the graphical element that represents the door to open or close the door respectively. Add the following code snippet to your script.js file:

bms.executeEvent({
  selector: "#door",
  events: [
    { name: "close_door" }, 
    { name: "open_door" }
  ]
});

This execute event handler will bind to events to the graphical element that matches the selector “#door”.