Skip to main content

choice

A decision about which arm of a global protocol runs, made by the components named after in.

component Radar;
component CommandPost;
component Launcher;

message struct TrackReport {
    track_id: uint32;
    bearing_deg: float32;
}

message struct EngageOrder {
    track_id: uint32;
}

message struct Standby {
    track_id: uint32;
}

message struct Abort {
    track_id: uint32;
}

global protocol Engage {
    exch any TrackReport into let latest: TrackReport from Radar to CommandPost;
    choice in CommandPost
    | latest.bearing_deg > 180.0 => exch any EngageOrder from CommandPost to Launcher;
    | latest.bearing_deg < 90.0 => exch any Standby from CommandPost to Launcher;
    | else => exch any Abort from CommandPost to Launcher;
    end
}

Each arm sends Launcher a different message, so Launcher can tell which one ran.

Arms​

Each arm is a |, a guard, =>, and the statements to run. The block closes with end, not a brace.

  • The component after in is the one that decides, and it names a component.
  • A guard has type bit. It may name what an earlier exch bound, and what an earlier in block on the deciding component declared — the state of another component is not something this one can read.
  • Exactly one arm runs.
  • | else => is optional and may appear only as the last arm. Without one, a decision where no guard holds has no arm to take. The guards are not retried, so the deciding component is stuck at the block, and so is every component waiting on a message an arm would have sent.
  • Arms are not tried in order. Where two guards hold, either one may run.
  • An arm's statements are the global protocol's own, so an arm may hold an exch, a loop, a nested choice, or nothing at all.
  • Naming more than one component after in makes it a synchronized choice, which restricts the guards further.

Synchronized​

Name more than one component after in and each of them decides for itself, with no message between them, so all of them have to reach the same answer. A where clause is what makes that possible: it defines the variables the guards may read, and gives each component its own expression for each one.

  • A definition is a name, =, and one in C { … } expression for every component named after choice in, comma separated. A second definition follows the first with nothing between them.
  • Every expression of one definition has the same type.
  • An expression is evaluated by its own component, and reads only what that component can see.
  • Only these variables may appear in the arm guards. A guard naming anything else is an error, even a binding that is in scope for one of the components.
  • A guard has type bit.
  • The arms cannot be nondeterministic: the components would not agree on which one to run.
component Radar;
component CommandPost;
component Launcher;

message struct TrackReport {
    track_id: uint32;
    bearing_deg: float32;
}

message struct EngageOrder {
    track_id: uint32;
}

message struct Ack {
    track_id: uint32;
}

global protocol Engage {
    exch any TrackReport into let at_post: TrackReport from Radar to CommandPost;
    exch any TrackReport into let at_launcher: TrackReport from Radar to Launcher;
    choice in CommandPost, Launcher
    where engaging = in CommandPost { at_post.bearing_deg > 180.0 },
                     in Launcher { at_launcher.bearing_deg > 180.0 }
          reporting = in CommandPost { at_post.track_id > 0 },
                      in Launcher { at_launcher.track_id > 0 }
    | engaging && reporting => exch any EngageOrder from CommandPost to Launcher;
    | reporting => exch any Ack from Launcher to CommandPost;
    | else =>
    end
}

Errors​

Deciding in something that is not a component​

A group holds components, but it is not one, so it cannot decide.

component Radar;
component CommandPost;
component Launcher;

message struct EngageOrder {
    track_id: uint32;
}

group Command {
    CommandPost;
    Launcher;
}

global protocol Engage {
    choice in Command   // error: choice-component-not-component
    | true => exch any EngageOrder from CommandPost to Launcher;
    | else =>
    end
}

A guard naming another component's state​

sweeps belongs to Radar, so a choice in Launcher cannot read it.

component Radar;
component CommandPost;
component Launcher;

message struct TrackReport {
    track_id: uint32;
}

message struct EngageOrder {
    track_id: uint32;
}

global protocol Engage {
    exch any TrackReport from Radar to CommandPost;
    in Radar {
        var sweeps: int32 = 0;
    }
    choice in Launcher
    | sweeps > 0 => exch any EngageOrder from Launcher to CommandPost;   // error: unresolved-reference
    | else =>
    end
}

A synchronized guard naming something other than a synchronized variable​

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 at_post: TrackReport from Radar to CommandPost;
    exch any TrackReport into let at_launcher: TrackReport from Radar to Launcher;
    choice in CommandPost, Launcher
    where engaging = in CommandPost { at_post.track_id > 0 },
                     in Launcher { at_launcher.track_id > 0 }
    | at_post.track_id > 0 => exch any EngageOrder from CommandPost to Launcher;   // error: sync-choice-guard
    | else =>
    end
}

A synchronized guard that is not a condition​

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 at_post: TrackReport from Radar to CommandPost;
    exch any TrackReport into let at_launcher: TrackReport from Radar to Launcher;
    choice in CommandPost, Launcher
    where engaging = in CommandPost { at_post.track_id > 0 },
                     in Launcher { at_launcher.track_id > 0 }
    | 1 => exch any EngageOrder from CommandPost to Launcher;   // error: sync-choice-guard
    | else =>
    end
}
  • branch — the same decision inside one component's local protocol.
  • global protocol — the statement sequence an arm holds.
  • exch — the exchanges that give each component something to decide on.
  • in block — where a deciding component's own state comes from.