10.5.5.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.

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.

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