loop, break

A block that repeats until something inside it breaks out. Both a local and a global protocol may hold one.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

message struct Ack {
    track_id: uint32;
}

local protocol Sweep in Radar {
    loop {
        send any TrackReport to CommandPost;
        recv let ack: Ack from CommandPost;
        branch
        | ack.track_id == 0 => break;
        | else =>
        end
    }
}

Bodies

• An empty body is legal, and repeats nothing forever.
• The optional name after loop is a label — loop reporting { … }. It exists so a break can say which loop it leaves, which only matters once loops nest.
• A loop with no reachable break repeats forever, which is a legitimate description of a component that runs until it is switched off.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

global protocol Stream {
    in CommandPost {
        var latest: TrackReport = TrackReport { track_id = 1; };
    }

    loop reporting {
        exch any TrackReport into latest from Radar to CommandPost;
        choice in CommandPost
        | latest.track_id == 0 => break reporting;
        | else =>
        end
    }
}

Invariants

An invariant is an assertion about the loop, not a condition for leaving it: a claim that something is true each time the loop begins an iteration. Leaving is break's job.

• An invariant may appear on a loop in a local protocol, or on a loop inside an in block.
• A loop in a global protocol takes no invariant.
• The expression has type bit.
• It begins with a reference to a var or let in scope. invariant 5 == 5 is rejected — it holds, and says nothing about the loop.
• An invariant over state the body never changes is accepted, and says nothing about the loop either.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

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

    loop invariant count < 10 {
        send any TrackReport to CommandPost;
        set count = count + 1;
        branch
        | count >= 10 => break;
        | else =>
        end
    }
}

break

break leaves a loop. A bare break leaves the innermost one; break L leaves the loop labeled L.

• A break sits inside the loop it leaves.
• A labeled break names a loop that encloses it, which is how an inner loop leaves an outer one.
• Execution continues after the loop it left.

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

message struct Ack {
    track_id: uint32;
}

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

    loop reporting {
        loop {
            send any TrackReport to CommandPost;
            set count = count + 1;
            branch
            | count >= 10 => break reporting;
            | else => break;
            end
        }
        recv _: Ack from CommandPost;
    }
}

Errors

A break outside every loop

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    send any TrackReport to CommandPost;
    break;   // error: break-outside-loop
}

A break naming a loop that does not enclose it

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    loop {
        send any TrackReport to CommandPost;
        break reporting;   // error: break-outside-loop
    }
}

An invariant that does not begin with a bound variable

component Radar;
component CommandPost;

message struct TrackReport {
    track_id: uint32;
}

local protocol Sweep in Radar {
    loop invariant 5 == 5 {   // error: loop-invariant-expression
        send any TrackReport to CommandPost;
    }
}

Related

• branch — how a loop in a local protocol usually decides to leave.
• choice — how a loop in a global protocol does.
• do — repetition by tail call instead of by loop.
• local protocol — the var an invariant reads.