10.5.4.3 Formal Binding

A formal binding binds a member variable to an out or inout formal parameter. At the moment of the reply, the value of the bound member variable is assigned to the formal parameter. A formal binding can be used in blocking context or synchronous out event context.

trigger        ::= port-name "." event-name "(" formal-list? ")"
formal-list    ::= formal ("," formal)*
formal         ::= identifier | (identifier formal-binding)
formal-binding ::= "<-" identifier

The identifier in formal-binding must be a member variable of the component.

For example:

extern int $int$;
component blocking_binding
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    int g = $123$;
    bool busy = false;
    [!busy] on h.hello (n <- g): blocking {w.hello (); busy = true;}
    [busy] on w.world (): {g = $456$; h.reply (); busy = false;}
    [busy] on w.cruel (): {h.reply (); g = $456$; busy = false;}
  }
}

in the case of w.world the assignment of g = $456$ before the release of the blocked thread by h.reply () ensures that parameter n returns with value 456. However in the case of w.cruel the caller of h.hello receives 123 via parameter n.

For a synchronous interface iworld with behavior:

on hello: world;
on hello: cruel;

a formal binding can be used in synchronous out event context:

extern int $int$;
component synchronous_out_event_binding
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    int g = $123$;

    on h.hello (n <- g): w.hello ();
    on w.world (): {g = $456$; h.reply (true);}
    on w.cruel (): {h.reply (true); g = $456$; ;}
  }
}

in the case of w.world the assignment of g = $456$ before the reply by h.reply () ensures that parameter n returns with value 456. However in the case of w.cruel the caller of h.hello receives 123 via parameter n.

For a void event without reply:

extern int $int$;
component synchronous_out_event_binding
{
  provides ihello h;
  requires iworld w;

  behavior
  {
    int g = $123$;

    on h.hello (n <- g): w.hello ();
    on w.world (): g = $456$;
  }
}

the caller receives the caller of h.hello receives the last assigned value: 456.

Note: The intent is to simplify this specific behavior in the future when data flow verification is added.