Skip to main content

global protocol

A whole conversation between components, written as one ordered sequence of exchanges.

component Radar;
component CommandPost;
component Launcher;

message struct TrackReport {
    track_id: uint32;
}

message struct EngageOrder {
    track_id: uint32;
}

global protocol Engage {
    exch any TrackReport into let latest: TrackReport from Radar to CommandPost;
    choice in CommandPost
    | latest.track_id > 0 => exch any EngageOrder from CommandPost to Launcher;
    | else =>
    end
}

Statements​

The name is a global declaration. The body is a sequence of statements, executed in order:

  • exch — one interaction between two components, a send and its matching receive as one step.
  • choice — one component picking an arm for the whole protocol.
  • loop and break.
  • parallel — branches whose statements interleave.
  • in C { … } — local statements executed in one component.
  • do — running another global protocol.
  • A standalone annotation.

let, var, and set are not statements here. A value the protocol needs later is bound by exch … into let, and state that belongs to one component lives in an in block.

Every statement names the components it involves, so the protocol says who talks to whom in the order it happens. What each component does on its own — the behavior a local protocol spells out — appears only where an in block puts it.

Errors​

Binding a variable directly in a global protocol​

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

global protocol Engage {
    var count: int32 = 0;   // error: unexpected
    exch any TrackReport from Radar to CommandPost;
}
  • local protocol — one component's view of the same conversation.
  • exch — the interaction statement and its payload forms.
  • choice — branching a global protocol.
  • in block — local statements and state inside a global protocol.
  • parallel — interleaving branches.