Please enable JavaScript.

Coggle requires JavaScript to display documents.

bmotion - Coggle Diagram

- - - - ProB Events view
  - - - selector [Type: string, Required]
        
        A selector that matches a set of graphical elements in the visualization
      - formulas [Type: list, Required]
        
        Define a list of formulas (e.g. expressions, predicates or single variables) which should be evaluated in each state. The results of the formulas are passed to the trigger function
      - translate [Type: boolean, Default: false]
        
        In general the result of the formulas are passed as strings to the trigger function. Set this option to true to translate B-structures to JavaScript structures.
      - trigger [Type: function(origin, values), Required]
        
        The trigger function will be called after every state change with its origin reference set to the graphical element that the observer is attached to and the values of the formula
      - Observers are used to link graphical elements with the model. An observer is notified whenever a model has changed its state, i.e. whenever an event has been executed. In response, the observer will query the model’s state and triggers actions on the linked graphical elements in respect to the new state.
    - - selector [Type: string, Required]
        
        A selector that matches a set of graphical elements in the visualization
      - 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
      - events [Type: list, Required]
        
        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.
        
        event a json object containing some data of the respective event
        
        origin as the reference to the graphical element where the execute event handler is attached to
    - - A selector matches a set of graphical elements in the visualization (e.g. images or shapes)
      - Each observer and event handler needs to define a selector