4.2.3 Event Handler

4.2.3.1 Execute Events

The execute event handler binds a click handler that executed an event (Event-B) or an operation (Classical-B) on the element(s) that matches the selector. The user can also define a list of events (or operations). In this case, a tooltip that lists the available events (disabled and enabled) will be shown when hovering the matched element. The following options can be passed:

• selector [Type: string, Required]:
  A selector that matches a set of graphical elements in the visualization (see Section 4.2.1).

• events [Type: list, Required]:
  Define a list of events with name and predicate that should be bind with the matched graphical elements.

  • name [Type: string, Required]:
    The name of the event. If the value is a function it takes the return value of the function.

  • predicate [Type: string*]:
    The predicate that defines the parameters of the event to be executed. If the value is a function it takes the return value of the function.

• label [Type: function(event, origin)]:
  A function that returns a custom label (string) to be shown in the tooltip. You can also return an HTML element, e.g. span or strong. The function provides two arguments: event a json object containing some data of the respective event and origin as the reference to the graphical element where the execute event handler is attached to.

*This attribute also accepts a function that should return its value. The reference to the graphical element that the observer is attached to (origin) is passed to the function.

Example execute event handler:

bms.executeEvent({
  selector: "text[data-some]",
  events: [
    { 
      name: "event1", 
      predicate: function (origin) {
        return "x=" + origin.attr("data-some") 
      }
    },
    { name: "event2", predicate: "y=3" },
    { name: "event3" } 
  ],
  label: function(event, origin) {
     return "<strong>" + event.name + "." + event.predicate + "</strong>";
  }
});