Skip to main content

listen

A decision made inside a local protocol by the message that arrives. Each arm is guarded by a recv.

component Radar;
component CommandPost;

message struct Ack {
    track_id: uint32;
}

message struct Reject {
    track_id: uint32;
}

message struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    send any TrackReport to CommandPost;
    listen
    | recv _: Ack from CommandPost =>
    | recv _: Reject from CommandPost =>
    end
}

Arms​

Each arm is a |, a recv without its semicolon, =>, and the statements to run. The block closes with end.

  • An arm's recv obeys the recv rules: the message type is message data, an assuming predicate is bit, and the connection clause receives at this component.
  • A let binding in an arm's guard is in scope in that arm and nowhere else.
  • Arms are distinguished by the message they receive. Two arms receiving the same type from the same component are not a choice the sender can direct.
  • An arm's statements are local-protocol statements, and an arm may run nothing.
component Radar;
component CommandPost;

message struct Ack {
    track_id: uint32;
}

message struct Reject {
    track_id: uint32;
    reason: string;
}

message struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    var rejected: int32 = 0;

    send any TrackReport to CommandPost;
    listen
    | recv let ack: Ack from CommandPost =>
        send any TrackReport to CommandPost;
    | recv let reject: Reject assuming reject.track_id > 0 from CommandPost =>
        set rejected = rejected + 1;
    end
}

Errors​

An arm receiving a type that has no wire form​

component Radar;
component CommandPost;

struct Ack {
    track_id: uint32;
}

message struct Reject {
    track_id: uint32;
}

local protocol Sweep in Radar {
    listen
    | recv _: Ack from CommandPost =>       // error: message-data-type
    | recv _: Reject from CommandPost =>
    end
}

An arm receiving from the wrong end​

component Radar;
component CommandPost;

message struct Ack {
    track_id: uint32;
}

local protocol Sweep in Radar {
    listen
    | recv _: Ack from Radar to CommandPost =>   // error: connection-directionality
    end
}
  • recv — the statement each arm is guarded by.
  • branch — the same shape, with guards the component evaluates itself.
  • choice — the global protocol's branching statement.