⚠ Diagrams couldn't load from the CDN (Mermaid.js) — check your connection and reload the page.
Leadout turns a coach's structured interval workout into something a participant's watch can walk them through, lap by lap, with nobody needing to remember the plan themselves. An instructor builds a programme — an ordered list of blocks, each block an ordered list of segments — and publishes it to a channel that participants subscribe to. On the day it's scheduled for, a participant's watch syncs the programme down in the background, the participant picks it from the watch widget, and from then on the data field on their wrist drives the run: hold this pace for this long, then cover this distance, then reach this waypoint, then loop a group of segments until a rep count or a time or distance target is met, then rest until the whole group presses lap together to start the next block.
Three actors carry the story, and each has a genuinely different relationship to the system. An Instructor owns channels and authors programmes on the web, identified only by a stable anonymous hash from Garmin Connect OAuth — never a name or email. A participant's web identity is an Account, created the instant they first sign in with Google; from there they subscribe to channels and register the watches that will run their programmes. And a Device — the actual watch install — is the third party, with its own lifecycle that runs independently of any human decision: it syncs programmes in the background on a cadence that depends on which generation of Garmin's Connect IQ runtime it's running, whether or not anyone is looking at it.
A programme's segments come in three flavours that drive their own completion: time-based (a duration elapses), distance-based (the watch's GPS reports enough distance covered), and location-based (the participant enters a radius around a waypoint). A fourth kind, the Repeat marker, turns the segments between it and the previous marker into a loop — exiting on a rep count, an elapsed time, or a distance target — and system-provided pyramid templates can generate a whole ascending-then-descending block of paired effort/recovery segments in one step, rather than building it segment by segment.
flowchart LR
subgraph instructor_side["Instructor"]
Instructor(["Instructor"])
Channel["Channel"]
Instructor -->|publishes a programme to| Channel
end
subgraph participant_side["Participant"]
Participant(["Participant"])
end
subgraph watch_side["Participant's watch"]
Watch["Watch"]
end
Participant -->|subscribes to| Channel
Participant -->|owns| Watch
Channel -.->|downloads the programme| Watch
Four actors making their own decisions on their own schedules, and the records their decisions leave behind.
Owns channels and authors the interval programmes published to them — building blocks and segments from scratch, from a template, or by cloning a previous programme onto a new date. Identified only by a stable anonymous hash from Garmin Connect OAuth; no name or email is ever stored.
Subscribes to channels and registers the watches that will run their programmes — the web-side identity a participant uses before ever touching their watch. Created the moment someone first signs in with Google; no personal information is stored beyond that stable identifier.
A single day's structured workout that everything else in the system organises around: an instructor authors it, a participant's watch downloads it, and a Session tracks a run through it. It reacts to the calendar entirely on its own — once its scheduled date passes, it expires and locks out every further edit, whether or not anyone was watching.
A watch installation of the Leadout data field — syncing programmes and running sessions on its own schedule, independent of whether anyone is looking at it. It reacts constantly: to registration, to every background poll, to every lap press and every segment boundary during a run. Its device_code is the anonymous string that bridges an unclaimed watch to a signed-in Account during registration.
A named channel an instructor shares via a permanent link — a WhatsApp group is the typical delivery mechanism. Participants subscribe once and receive every programme it ever publishes from then on, with no need to subscribe again.
A synchronisation point within a programme: the group starts a block together with a lap press, then its segments run back-to-back automatically until the block ends and everyone regroups for the next one.
Created the moment a participant picks today's programme, a Session is what actually drives the run: which block and segment are current, whether the participant is inside a repeat loop, and whether they're holding the segment's target pace. It becomes complete once the last segment of the last block finishes, and stays that way — there's no declared way back into an in-progress session once it's done.
Eleven moments, in the order each depends on the last — instructors setting things up, participants and their watches finding each other, and finally a group of participants pressing lap together.
Everything in this spec traces back to an instructor deciding to run a channel — the permanent, shareable home for every programme they'll ever publish to one group of participants.
On their channel admin page, the instructor names a new channel. InstructorCreatesChannel creates it there and then, owned by whoever created it, timestamped to the moment.
sequenceDiagram
actor Instructor
participant Admin as InstructorChannelAdmin
Instructor->>Admin: name a new channel
Admin->>Admin: InstructorCreatesChannel
Admin-->>Instructor: Channel created
The channel this creates is the anchor for everything that follows — every programme, subscription, and device sync in this document traces back to one. Next, the instructor fills it with something to run — see An instructor publishes a programme.
With a channel to publish to, the instructor puts together a specific day's workout — one of three ways.
From scratch: the instructor names a new programme, picks a scheduled date, and optionally a pace assumption. InstructorCreatesProgramme requires they actually own the channel, then creates an empty programme — no blocks yet — with the pace defaulting to the spec-wide default_pace_assumption config value if none is given.
Cloned: or the instructor clones an existing programme in the same channel onto a new date. ProgrammeCloned copies every block and segment verbatim, inheriting name and pace too — only the date changes. The deep-copy logic itself is a deferred specification (ProgrammeCopy.from), described in prose rather than modelled step by step.
From a template: or the instructor picks one of the system-provided templates (currently pyramid shapes only — ascending then descending effort/recovery pairs). ProgrammeCreatedFromTemplate creates the empty programme exactly as the from-scratch path does, then immediately expands the template into a single starting block at position 0. Template authoring by instructors themselves isn't modelled yet — only the system-provided pyramid shapes exist today.
flowchart LR
I(["Instructor"]) -->|from scratch| A[InstructorCreatesProgramme]
I -->|clone| B[ProgrammeCloned]
I -->|from template| C[ProgrammeCreatedFromTemplate]
A --> P["Programme<br/>(empty)"]
B --> P2["Programme<br/>(blocks/segments copied)"]
C --> P3["Programme<br/>(one generated block)"]
The same three actions are also offered from a channel's own detail page; the explorer is simply the instructor's dedicated starting point for authoring. Whichever way it started, the programme is still just a shell (or, for the template path, a shell plus one generated block) until it's actually built out — see the next journey.
From the programme editor, the instructor builds out a shell programme into an actual sequence of blocks and segments — or comes back later to change one. Every action below is only available while the programme hasn't expired yet.
ProgrammeEdited covers top-level changes — rename, reschedule, or change the pace assumption. This and every block/segment edit below also fires ProgrammeModifiedTimestamp, bumping the programme's updated_at — the field devices compare their own synced copy against to know whether they're current.
If the programme is scheduled for today, the editor is expected to warn that participants may not sync in time to see the change before they run it — advisory only; the edit proceeds either way.
Block management: InstructorAddsBlankBlock appends an empty block at the end; BlockGeneratedFromTemplate appends one generated from a template instead. InstructorReordersBlock and InstructorDeletesBlock reorder or remove one.
Keeping block positions a contiguous 0..n-1 sequence after a reorder is left to the implementation — the spec defers the exact renumbering algorithm as an Allium limitation around imperative list manipulation.
Segment management, symmetrically: InstructorAddsSegment, InstructorConfiguresSegment (name and target pace only — kind-specific fields like duration, target distance, or waypoint go through their own variant-specific triggers, not modelled here), InstructorReordersSegment, and InstructorDeletesSegment.
sequenceDiagram
actor Instructor
participant Editor as InstructorProgrammeEditor
participant Prog as Programme
Instructor->>Editor: edit fields / add, reorder, delete block or segment
Editor->>Prog: field(s) updated
Editor->>Prog: ProgrammeModified
Prog->>Prog: ProgrammeModifiedTimestamp (updated_at = now)
Later, once participants' watches start syncing, the instructor can check how far each of these edits has actually reached — see An instructor checks how far a programme has reached.
Before any of the participant-side journeys below make sense, someone has to sign in with Google and get an Account.
ParticipantFirstSignIn fires on a ParticipantSignsIn(google_id) trigger and creates an Account, provided one doesn't already exist for that google_id.
Nothing in this spec actually exposes a way to fire ParticipantSignsIn — no surface provides it, and both allium's checker and its analyser flag the trigger as unreachable. Every participant-facing surface documented below (subscribing, registering a device, the dashboard) simply assumes an Account already exists. The spec's own scope note explicitly excludes "Garmin Connect OAuth internals (external identity provider)" — this is presumably where an equivalent Google sign-in integration is meant to plug in on the participant side, it's just not written down.
sequenceDiagram
participant Nobody as No surface provides this
participant Rule as ParticipantFirstSignIn
participant Acc as Account
Nobody--xRule: ParticipantSignsIn - never actually fires
Rule->>Acc: created, if reached
Meanwhile, on the hardware side, a participant installs the Leadout data field on their Garmin watch and opens it for the first time — entirely independent of whether they've signed in anywhere yet.
The platform reports the watch's device_code, whether it holds a cached programme locally, and which Connect IQ SDK generation it's running. Because no Device exists yet for this code, DataFieldOpenedUnregistered creates a pre-session view — then, immediately afterward, ViewInitialisedUnregistered sets its status to unregistered.
Unregistered, the watch shows its device_code and a URL to register on the website, and starts checking for a claim. On a new-SDK watch, RegistrationPollSeed fires immediately on view creation to seed the very first check, then RegistrationPollTimerFired repeats it every 10 seconds from the foreground. An old-SDK watch can't poll from the foreground at all — it relies on BackgroundSyncWhileUnregistered, a platform-delivered background timer running at a much coarser 5-minute cadence, so registration take-up is visibly slower on older watches.
sequenceDiagram
actor P as Participant
participant Lifecycle as WatchDataFieldLifecycle
participant View as WatchDataFieldView
P->>Lifecycle: opens the Leadout data field
Lifecycle->>View: DataFieldOpenedUnregistered (no Device yet)
View->>View: ViewInitialisedUnregistered → status = unregistered
loop every 10s (new SDK) / every 5min (old SDK, background)
View->>View: poll for a claim
end
This device_code is what the participant needs next — they'll enter it on the website to claim the watch. See A participant registers their watch.
A participant follows a channel's link — typically dropped into a WhatsApp group by the instructor — and, once signed in, subscribes to it.
ParticipantSubscribes requires they aren't already subscribed, then creates the Subscription. From then on, every programme that channel ever publishes reaches this participant's devices automatically — no need to subscribe again per programme.
They can leave at any time from their dashboard or the channel's own detail view — ParticipantUnsubscribes just removes the link.
sequenceDiagram
actor P as Participant
participant Page as ParticipantSubscriptionPage
P->>Page: follow channel link, subscribe
Page->>Page: ParticipantSubscribes
Page-->>P: Subscription created
This Subscription is exactly what a device's next background poll checks against — see below.
Signed in on the website, the participant enters the device_code shown on their watch — the one from a couple of journeys back.
ParticipantRegistersDevice requires that no Device already exists for that code — a code can only ever be claimed once, and the server rejects duplicate claims — then creates the Device against their Account.
sequenceDiagram
actor P as Participant
participant Page as DeviceRegistrationPage
P->>Page: enter device_code from watch
Page->>Page: ParticipantRegistersDevice
Page-->>P: Device created
Registering doesn't instantly update the watch — it still has to notice. That's the next journey.
Whether it's the watch from a few journeys back finally getting claimed, or an already-registered watch simply being opened on an ordinary morning, everything funnels through the same sync machinery.
Bridging from unregistered: back on the watch that's still polling, the next poll after registration finally finds a Device. TokenReceived moves the view from unregistered straight to syncing and issues a fresh poll immediately.
The ordinary case: any time the participant opens the data field on an already-registered watch, DataFieldOpenedRegistered creates the view and kicks off a poll in the same breath; ViewInitialisedRegistered sets it straight to syncing, skipping the unregistered detour entirely.
Every poll — whichever of the three pathways triggered it — crosses the same boundary. RegisteredDevicePoll (device exists) returns every non-expired programme across all the account's subscribed channels and writes or refreshes a ProgrammeSyncRecord per programme; UnregisteredDevicePoll (device doesn't exist) tells the watch registration is still required. The surface formalising this crossing, WatchSyncAPI, has no human facing it at all — a pure device-to-server boundary, deliberately the single entry point for all three sync pathways in this spec.
The response lands back on the view as one of four outcomes, carried as flags on the same SyncSucceeded trigger rather than the watch re-reading server state directly: SyncSucceededReady (something's scheduled today), SyncSucceededUpcoming (nothing today, something later), SyncSucceededNoProgramme (subscribed, nothing scheduled at all), SyncSucceededNoSubscriptions (not subscribed to anything).
If the poll fails outright, SyncFailedNoCache surfaces the error and drops the view to sync_failed — but only when the watch has no cached programme to fall back on. If it does, SyncFailedWithCache keeps the view showing whatever it already had and says nothing: a participant mid-run on patchy connectivity should never see an error overlay.
Once there, sync_failed, no_subscriptions, no_programme, upcoming, and ready all share one property allium's checker calls out directly: none of the five declares an exit anywhere except back to syncing, on the next retry.
Independent of whether the data field is even open, two temporal rules keep an already-registered device in sync automatically: BackgroundSyncFires polls on the device's effective interval once it has synced at least once; BackgroundSyncInitialFire covers the gap before that — the very first background sync after registration, timed off registered_at since there's no last_synced_at yet to measure from. The interval is user-configurable (5–720 minutes), but a never-synced watch on the old SDK is forced to a fixed 5-minute cadence regardless of that setting, precisely because it has no foreground fallback for detecting a fresh registration.
If the participant leaves the data field screen before a Session ever takes over, DataFieldHidden simply discards the pre-session view — it's rebuilt fresh next time the data field opens. But if a ready view is what they were looking at, they don't have to leave at all.
stateDiagram-v2
[*] --> unregistered
[*] --> syncing: Device already exists
unregistered --> syncing: TokenReceived
syncing --> sync_failed: SyncFailed, no cache
syncing --> no_subscriptions: SyncSucceeded
syncing --> no_programme: SyncSucceeded
syncing --> upcoming: SyncSucceeded
syncing --> ready: SyncSucceeded
sync_failed --> syncing: retry
no_subscriptions --> syncing: retry
no_programme --> syncing: retry
upcoming --> syncing: retry
ready --> syncing: retry
note right of sync_failed
these five states only declare
an exit back to syncing
end note
Once a view reaches ready, the participant has one thing left to do — see the next journey.
From a ready pre-session view, the participant opens the watch widget and picks one of today's synced programmes — the moment everything else in this document was in service of.
ParticipantSelectsProgramme requires the programme is actually scheduled for today and that the participant's account is still subscribed to its channel, then creates a Session for the device and programme.
SessionInitialised fires immediately and sets the session to waiting, block 0 — the moment the watch widget hands off to the data field. The pre-session view is superseded; from here the data field shows the programme's name and the name of the first block, prompting the group to press lap when they're ready.
When the group presses lap, BlockStarted moves the session to active, segment 0 of the current block, and starts its timer. If this is the very first lap press for this programme on this device — block 0 — ParticipantStartsSession also records a Participation: proof the participant actually started, not just that their watch received the programme.
From here, each segment completes however its own kind demands: TimeSegmentComplete once its duration has elapsed, DistanceSegmentComplete once the watch's GPS reports enough distance covered, LocationSegmentComplete once the participant enters the radius around a waypoint. All three converge on the same next step.
Repeat loops — a branch worth its own telling: if the segment after the one that just finished is a Repeat marker, RepeatMarkerReached hands off to evaluating its exit condition instead of simply moving forward. Three exit kinds, each with a loop-back/exit-now pair: count (RepeatLoopsCount / RepeatExitsCount), elapsed time (RepeatLoopsTime / RepeatExitsTime), and distance covered since the loop began (RepeatLoopsDistance / RepeatExitsDistance). Looping jumps the session's current segment straight back to the first segment of the group and increments the rep counter; exiting hands off to RepeatExitContinues, which clears all the loop-tracking state and steps past the marker to whatever comes after it — or, via RepeatExitEndsBlock / RepeatExitCompletesSession, ends the block or the whole session outright if the marker was the last thing in it.
Entering a loop for the first time is handled separately: EnterRepeatGroup fires instead of the ordinary continue-to-next-segment rule the moment the segment two steps ahead is a Repeat marker, recording where the group starts and initialising the rep counter to 1 before any loop-evaluation rule ever runs.
With no repeat marker involved, SegmentContinues just moves to the next segment in the block.
Once the block's last segment finishes, one of two things happens depending on whether more blocks remain: BlockCompletes drops the session back to waiting and advances to the next block, ready for the whole group to press lap together again; SessionCompletes instead marks the session complete — and it's terminal. There is no transition back out of complete once it's reached.
stateDiagram-v2
[*] --> waiting: SessionInitialised
waiting --> active: BlockStarted (lap press)
active --> waiting: BlockCompletes (more blocks remain)
active --> complete: SessionCompletes / RepeatExitCompletesSession
complete --> [*]
note right of complete
terminal - no way back
once a session completes
end note
Once devices are syncing and participants are starting sessions, an instructor can look back at any published programme and see how well it's actually landed.
For every device subscribed to the channel, the instructor sees when it last synced and whether that copy is current against the programme's latest updated_at — each row backed directly by a ProgrammeSyncRecord and its is_current derived value, alongside how many participants have actually started the programme (its Participation count).
The spec's own guidance frames "fully propagated" as every subscriber account having at least one current device, and calls for reinforcing the same late-edit warning from the programme editor when the programme is scheduled for today and some devices are still behind.
flowchart LR
D["Device polls"] --> R["ProgrammeSyncRecord<br/>synced_at, programme_version"]
R -->|is_current = programme_version = programme.updated_at| V["Propagation view"]
P["Participation"] -->|count| V
No one has to do anything for this one — it's purely a consequence of the calendar moving forward.
The moment a programme's scheduled date falls into the past, ProgrammeExpires fires. It's modelled here as a hard delete, though the spec notes implementations may defer the actual purge. From that point the server excludes it from its API entirely, and every editing rule from the reshaping journey above explicitly requires the programme not be expired — so nothing can be authored onto a programme once its day has passed.
Watches may purge their own local copies of expired programmes too, though that's left to the implementation rather than specified here.
Everything above told the story; this is the lookup material behind it, organised the conventional way for when you need the exact shape of one construct.
| Parameter | Type | Default | Notes |
|---|---|---|---|
geofence_radius | Distance | 30.metres | |
default_pace_assumption | Pace | default_pace | |
background_sync_interval_while_unregistered | Duration | 5.minutes | |
default_background_sync_interval | Duration | 60.minutes | |
registration_poll_interval | Duration | 10.seconds |
| Field | Type | Present when | |
|---|---|---|---|
oauth_id | String |
⚠ warning No governing specification import was found for this external entity in this module — plausibly because Garmin Connect OAuth is deliberately out of scope (see the spec's own scope note), but allium's checker can't confirm that's the reason.
ⓘ info oauth_id is declared but never referenced by any rule or surface in this spec.
| Field | Type | Present when | |
|---|---|---|---|
google_id | String | ||
created_at | Timestamp | ||
has_programme_for_today | subscriptions.any(s => s.channel.upcoming_programmes.any(p => p.is_for_today)) | ||
has_future_programme | subscriptions.any(s => s.channel.upcoming_programmes.any(p => not p.is_for_today)) |
Relationships
subscriptions → Subscriptiondevices → Deviceⓘ info has_programme_for_today and has_future_programme are declared but never referenced — see The watch keeps itself in sync, where the equivalent branching actually runs off flags carried on the SyncSucceeded trigger instead.
| Field | Type | Present when | |
|---|---|---|---|
device_code | String | ||
account | Account | ||
registered_at | Timestamp | ||
last_synced_at | Timestamp? | optional | |
is_new_sdk | Boolean | ||
background_sync_interval | Duration? | optional | |
effective_background_sync_interval | if not has_synced_once and not is_new_sdk:
config.background_sync_interval_while_unregistered
else:
background_sync_interval ?? config.default_background_sync_interval | ||
has_synced_once | derived |
Relationships
sync_records → ProgrammeSyncRecord| Field | Type | Present when | |
|---|---|---|---|
instructor | Instructor | ||
name | String | ||
created_at | Timestamp |
Relationships
programmes → ProgrammeProjections
upcoming_programmes (filtered view of programmes)| Field | Type | Present when | |
|---|---|---|---|
channel | Channel | ||
name | String | ||
scheduled_date | Date | ||
pace_assumption | Pace | ||
blocks | List<Block> | ||
published_at | Timestamp | ||
updated_at | Timestamp | ||
participation_count | participations.count | ||
is_expired | derived | ||
is_for_today | derived |
Relationships
sync_records → ProgrammeSyncRecordparticipations → Participation⛔ critical allium's checker can't resolve Pace (used by pace_assumption) as a declared or imported type in this module — likely a missing shared-unit import rather than a modelling gap.
| Field | Type | Present when | |
|---|---|---|---|
programme | Programme | ||
name | String | ||
position | Integer | ||
segments | List<Segment> |
| Field | Type | Present when | |
|---|---|---|---|
block | Block | ||
name | String | ||
position | Integer | ||
kind | TimeBased | DistanceBased | LocationBased | Repeat | ||
target_pace | Pace? | optional |
⛔ critical Same unresolved Pace type as Programme.pace_assumption.
| Field | Type | Present when | |
|---|---|---|---|
name | String | ||
kind | PyramidTemplate |
| Field | Type | Present when | |
|---|---|---|---|
account | Account | ||
channel | Channel |
| Field | Type | Present when | |
|---|---|---|---|
device | Device | ||
programme | Programme | ||
synced_at | Timestamp | ||
programme_version | Timestamp | ||
is_current | derived |
| Field | Type | Present when | |
|---|---|---|---|
device | Device | ||
programme | Programme | ||
started_at | Timestamp |
| Field | Type | Present when | |
|---|---|---|---|
device | Device | ||
programme | Programme | ||
status | waiting | active | complete | ||
current_block_index | Integer | when status = waiting or active | |
current_segment_index | Integer | when status = active | |
segment_started_at | Timestamp | when status = active | |
current_block | programme.blocks where position = current_block_index | when status = waiting or active | |
current_segment | current_block.segments where position = current_segment_index | when status = active | |
next_segment | current_block.segments where position = current_segment_index + 1 | when status = active | |
is_last_segment_in_block | not exists next_segment | when status = active | |
next_block | programme.blocks where position = current_block_index + 1 | when status = active | |
is_last_block | not exists next_block | when status = active | |
segment_timer_elapsed | segment_started_at + current_segment.duration <= now
when status = active and current_segment.kind = TimeBased | ||
repeat_segment_index | Integer | when status = active | |
repeat_started_at | Timestamp | when status = active | |
repeat_distance_at_start | Distance | when status = active | |
current_rep | Integer | when status = active | |
has_pace_guidance | current_segment.target_pace != null | when status = active |
Transitions (status)
waiting → activeactive → waitingactive → completeTerminal: complete
⛔ critical allium's checker can't resolve Distance (used by repeat_distance_at_start) as a declared or imported type — same missing shared-unit import pattern as Pace above.
⚠ warning .created() (see ParticipantSelectsProgramme) omits status; the initial state is set by a follow-up rule (SessionInitialised), not at the point of creation itself. See the run journey.
| Field | Type | Present when | |
|---|---|---|---|
device_code | String | ||
status | unregistered | syncing | sync_failed | no_subscriptions | no_programme | upcoming | ready | ||
last_error | String | when status = sync_failed | |
cached_programme | Boolean | ||
is_new_sdk | Boolean | ||
last_registration_poll_at | Timestamp? | when status = unregistered | optional |
Transitions (status)
unregistered → syncingsyncing → sync_failedsyncing → no_subscriptionssyncing → no_programmesyncing → upcomingsyncing → readysync_failed → syncingno_subscriptions → syncingno_programme → syncingupcoming → syncingready → syncing⚠ warning sync_failed, no_subscriptions, no_programme, upcoming, and ready each declare no exit to anywhere except back to syncing — flagged individually by allium's checker for all five. See The watch keeps itself in sync.
⚠ warning .created() omits status in both creation rules (DataFieldOpenedRegistered, DataFieldOpenedUnregistered); a follow-up rule sets it immediately in both cases (ViewInitialisedRegistered / ViewInitialisedUnregistered).
allium model does not carry variant-specific fields — hand-authored from the spec text.
| Field | Type |
|---|---|
duration | Duration |
Completes once duration elapses from when the segment started.
| Field | Type |
|---|---|
target_distance | Distance |
Completes once the watch's GPS reports at least target_distance covered since the segment started.
| Field | Type |
|---|---|
waypoint | Location |
trigger_radius | Distance |
Completes once the participant enters trigger_radius of waypoint.
| Field | Type |
|---|---|
exit | CountExit | TimeExit | DistanceExit |
A structural marker, not a segment a participant sees: the group of segments between this marker and the previous one (or the block start) forms a loop, governed by exit. Repeat segments never carry a target_pace and are invisible at runtime — the watch jumps straight to the next iteration's first segment, or past the marker on exit, without ever displaying it.
| Field | Type |
|---|---|
repeat_count | Integer |
Loop runs exactly repeat_count times in total.
| Field | Type |
|---|---|
target_duration | Duration |
Loop runs until elapsed time since the first iteration meets or exceeds target_duration — exits immediately when met, even mid-segment.
| Field | Type |
|---|---|
target_distance | Distance |
Loop runs until total distance covered since the first iteration meets or exceeds target_distance — exits immediately when met, even mid-segment.
| Field | Type |
|---|---|
shape | TimePyramid | DistancePyramid |
fast_name | String |
recovery_name | String |
Ascends from a minimum to a maximum in steps, then descends back to the minimum, alternating a "fast" effort segment with a "recovery" segment at each step. Example (time pyramid, min 60s, max 180s, increment 60s): Fast 60s, Easy 60s, Fast 120s, Easy 120s, Fast 180s, Easy 180s, Fast 120s, Easy 120s, Fast 60s, Easy 60s. The expansion itself is a deferred specification (TemplateExpansion.into).
| Field | Type |
|---|---|
min_duration | Duration |
max_duration | Duration |
duration_increment | Duration |
| Field | Type |
|---|---|
min_distance | Distance |
max_distance | Distance |
distance_increment | Distance |
allium plan carries test obligations, not rule declarations — hand-authored from the spec text (no when/requires/ensures text exists in either model or plan JSON output). Grouped as the spec itself groups them.
When: an instructor creates a channel, giving it a name.
Ensures: a Channel is created, owned by the instructor, timestamped now.
When: an instructor creates a programme from scratch — channel, name, scheduled date, optional pace assumption.
Requires: the instructor owns the channel.
Ensures: an empty Programme is created (no blocks), with pace defaulting to config.default_pace_assumption if none given.
When: an instructor clones an existing programme in the same channel onto a new date.
Requires: the instructor owns the source programme's channel.
Ensures: a new programme is created with all blocks/segments copied verbatim (deferred spec ProgrammeCopy.from) and a fresh updated_at; every other field is inherited.
⛔ critical allium's checker flags ProgrammeCopy as an undefined type — it's a deferred specification invoked with creation syntax, not a declared entity.
When: an instructor creates a programme from a system-provided template.
Requires: the instructor owns the channel.
Ensures: an empty Programme is created exactly as InstructorCreatesProgramme, then the template is expanded (deferred spec TemplateExpansion.into) into a single block at position 0.
⛔ critical Same deferred-spec checker flag on TemplateExpansion.
When: an instructor edits a programme's name, scheduled date, and/or pace assumption.
Requires: the instructor owns the channel; the programme has not expired.
Ensures: the given field(s) update; chains into ProgrammeModified. The "participants may not sync in time" warning for today-scheduled programmes is advisory only — the edit proceeds regardless.
When: any programme, block, or segment edit fires ProgrammeModified.
Ensures: the programme's updated_at becomes now — what devices compare their synced copy against.
When: a programme's scheduled_date falls into the past.
Ensures: the programme no longer exists (modelled as hard delete; implementations may defer the actual purge).
When: an instructor adds a blank block to a programme, giving it a name.
Requires: instructor owns the channel; programme not expired.
Ensures: a Block is created at the end of the programme's block list; chains into ProgrammeModified.
When: an instructor adds a block generated from a template to an existing programme.
Requires: instructor owns the channel; programme not expired.
Ensures: the template is expanded (deferred spec TemplateExpansion.into) at the end of the block list; chains into ProgrammeModified.
⛔ critical Same deferred-spec TemplateExpansion checker flag as ProgrammeCreatedFromTemplate.
When: an instructor moves a block to a new position.
Requires: instructor owns the channel; programme not expired.
Ensures: the block's position updates; chains into ProgrammeModified.
Guidance: implementations must keep positions a contiguous 0..n-1 sequence after any reorder — the exact renumbering algorithm is deferred (an Allium limitation around imperative list manipulation).
When: an instructor deletes a block.
Requires: instructor owns the channel; programme not expired.
Ensures: the block no longer exists; chains into ProgrammeModified.
When: an instructor adds a segment to a block.
Requires: instructor owns the channel; programme not expired.
Ensures: the segment is attached to the block at the end of its segment list; chains into ProgrammeModified.
When: an instructor edits a segment's name and/or target pace.
Requires: instructor owns the channel; programme not expired.
Ensures: the given field(s) update; chains into ProgrammeModified.
Kind-specific fields (duration, target distance, waypoint, trigger radius) go through their own variant-specific triggers — not modelled by this rule, to avoid crossing variant boundaries.
When: an instructor moves a segment to a new position.
Requires: instructor owns the channel; programme not expired.
Ensures: the segment's position updates; chains into ProgrammeModified.
When: an instructor deletes a segment.
Requires: instructor owns the channel; programme not expired.
Ensures: the segment no longer exists; chains into ProgrammeModified.
When: a participant subscribes to a channel.
Requires: not already subscribed.
Ensures: a Subscription linking the account and channel is created.
When: a participant unsubscribes from a channel.
Requires: currently subscribed.
Ensures: the Subscription no longer exists.
When: a participant selects a programme for today's session (primarily from the watch widget).
Requires: the programme is scheduled for today; the account is still subscribed to its channel.
Ensures: a Session is created for the device and programme.
⚠ warning .created() omits status — the initial state is unspecified at this exact point (fixed immediately by SessionInitialised). See the run journey.
When: a participant signs in with Google.
Requires: no Account already exists for this google_id.
Ensures: an Account is created.
⚠ warning No surface provides ParticipantSignsIn — unreachable per both the checker and the analyser. See A participant signs in for the first time.
When: a participant enters their watch's device_code on the website.
Requires: no Device already exists for that device_code (a code can only ever be claimed once).
Ensures: a Device is created against the account.
When: a device polls the server.
Requires: a Device exists for the device_code.
Ensures: last_synced_at updates to now; a ProgrammeSyncRecord is created or refreshed for every non-expired programme across all subscribed channels.
When: a device polls the server.
Requires: no Device exists for the device_code.
Ensures: a WatchRegistrationRequired signal is returned; the watch keeps showing its device_code and registration URL.
When: the participant opens the data field (platform reports device_code, cached-programme flag, SDK generation).
Requires: a Device already exists for the device_code.
Ensures: a WatchDataFieldView is created; a poll is issued immediately.
⚠ warning .created() omits status — set immediately after by ViewInitialisedRegistered.
When: the participant opens the data field.
Requires: no Device exists for the device_code.
Ensures: a WatchDataFieldView is created.
⚠ warning Same missing-initial-status pattern; set by ViewInitialisedUnregistered.
When: a WatchDataFieldView is created.
Requires: a Device exists for the view's device_code.
Ensures: status becomes syncing.
When: a WatchDataFieldView is created.
Requires: no Device exists for the view's device_code.
Ensures: status becomes unregistered.
When: a sync succeeds, carrying has_today / has_future / has_subscriptions flags from the response.
Requires: view was syncing; has_today.
Ensures: status becomes ready.
Requires: view was syncing; not has_today; has_future.
Ensures: status becomes upcoming.
Requires: view was syncing; not has_today; not has_future; has_subscriptions.
Ensures: status becomes no_programme.
Requires: view was syncing; not has_subscriptions.
Ensures: status becomes no_subscriptions.
When: a sync fails.
Requires: view was syncing; no cached programme.
Ensures: status becomes sync_failed; the error is recorded. Retry relies entirely on the next background sync — no foreground retry loop.
When: a sync fails.
Requires: view was syncing; a cached programme exists.
Ensures: nothing changes — the view silently keeps its prior display state (the SilentOfflineFallback guarantee).
When: registration_poll_interval (10s) has elapsed since the view's last registration poll.
Requires: view is unregistered; new SDK.
Ensures: a poll is issued; last_registration_poll_at updates to now.
When: a WatchDataFieldView is created.
Requires: unregistered; new SDK.
Ensures: last_registration_poll_at is seeded to now and a poll is issued immediately — otherwise the timer-based rule above would have nothing to measure from on the very first check.
When: the server signals that a device_code has just been claimed.
Requires: view is unregistered.
Ensures: status becomes syncing; the registration-poll timestamp clears; a poll is issued.
When: a registered device's effective_background_sync_interval has elapsed since last_synced_at.
Ensures: a poll is issued.
When: the effective interval has elapsed since registered_at.
Requires: last_synced_at is still null (no sync has ever completed).
Ensures: a poll is issued — covers the gap before BackgroundSyncFires has anything to measure from.
When: the platform fires its old-SDK 5-minute background timer for a device_code.
Requires: no Device exists yet for that code.
Ensures: a poll is issued — the only path by which an old-SDK unregistered watch discovers a claim, since it cannot poll from the foreground.
When: the data field becomes hidden.
Ensures: the pre-session view no longer exists. Does not fire once a Session has taken over the screen.
When: a Session is created.
Ensures: status becomes waiting; current block index becomes 0.
When: the lap button is pressed.
Requires: session is waiting.
Ensures: status becomes active; current segment index becomes 0; segment timer starts.
When: the very first lap press for a given device/programme pair (block 0 starting).
Ensures: a Participation is recorded.
When: a time-based segment's derived timer condition (segment_timer_elapsed) becomes true.
Ensures: SegmentAdvance fires.
When: the watch reports distance covered.
Requires: session active; current segment is distance-based; distance covered meets the target.
Ensures: SegmentAdvance fires.
When: the watch reports the waypoint reached.
Requires: session active; current segment is location-based.
Ensures: SegmentAdvance fires.
When: SegmentAdvance fires.
Requires: session active; not the block's last segment; the next segment is a Repeat marker.
Ensures: RepeatEvaluate fires (evaluate the marker's exit condition).
Requires: exit kind is CountExit; current rep < repeat_count.
Ensures: current segment jumps back to the group's start; rep counter increments; segment timer restarts.
Requires: exit kind is CountExit; current rep ≥ repeat_count.
Ensures: RepeatExited fires.
Requires: exit kind is TimeExit; target duration not yet reached.
Ensures: loop back, as RepeatLoopsCount.
Requires: exit kind is TimeExit; target duration reached.
Ensures: RepeatExited fires immediately (even mid-segment).
Requires: exit kind is DistanceExit; target distance not yet covered.
Ensures: loop back, as RepeatLoopsCount.
Requires: exit kind is DistanceExit; target distance covered.
Ensures: RepeatExited fires immediately (even mid-segment).
When: RepeatExited fires.
Requires: not the block's last segment.
Ensures: current segment advances two positions (past the marker); all loop-tracking state clears; segment timer restarts.
Requires: the marker was the block's last segment; more blocks remain.
Ensures: status becomes waiting; block index advances; segment/loop state clears.
Requires: the marker was the last segment of the last block.
Ensures: status becomes complete (terminal); segment/loop state clears.
When: SegmentAdvance fires.
Requires: session active; not the block's last segment; the next segment is not a Repeat marker; not entering a repeat group for the first time.
Ensures: current segment advances by one; segment timer restarts.
When: SegmentAdvance fires.
Requires: session active; not the block's last segment; next segment is not itself a Repeat marker; not already inside a repeat group; a Repeat marker exists later in the block.
Ensures: current segment advances by one; that position is recorded as the group's start; rep counter initialises to 1; segment/loop timers start.
When: SegmentAdvance fires.
Requires: session active; block's last segment; more blocks remain.
Ensures: status becomes waiting; block index advances; segment/loop state clears.
When: SegmentAdvance fires.
Requires: session active; block's last segment; last block.
Ensures: status becomes complete (terminal); segment/loop state clears.
Fifteen surfaces total. Three — WatchDataFieldLifecycle, WatchRunSensors, WatchSyncAPI — declare no facing actor and no exposes: they're pure platform/hardware boundaries, not screens a person looks at, so no wireframe was generated for them. The spec declares no related links between any surfaces — navigation shown in the wireframes below is illustrative, not spec-derived.
Facing: Instructor. Exposes: the instructor's own channels (name, created_at). Provides: InstructorCreatesChannel.
Facing: Instructor, within one owned channel. Exposes: channel name/created_at, subscriber count, and per programme: name, scheduled date, expired?, for today?, updated_at, participation count, and per sync record: device_code, synced_at, is_current. Provides: InstructorCreatesProgramme; InstructorClonesProgramme (when the channel has a source programme to clone); InstructorCreatesProgrammeFromTemplate.
Facing: Instructor, within one owned channel — the authoring starting point. Exposes: channel name, all programmes (name, scheduled date, expired?, for today?) — recent-first, remainder grouped by year/month is a display suggestion, not a domain requirement. Provides: the same three creation actions as InstructorChannelPage.
Facing: Instructor, within one owned programme. Exposes: programme name/date/pace/for-today, and the full block→segment tree (name, position, kind, target pace). Provides: InstructorEditsProgramme, InstructorAddsBlankBlock, InstructorAddsBlockFromTemplate, InstructorReordersBlock, InstructorDeletesBlock, InstructorAddsSegment, InstructorConfiguresSegment, InstructorReordersSegment, InstructorDeletesSegment — all gated on the programme not being expired. Guarantees: TimelinePlacement (segment width derives from target pace, falling back to the programme's pace assumption), MinimumSegmentWidth (every segment stays tappable regardless of derived duration).
Facing: a visiting Account, opened from an instructor's shared channel link. Exposes: channel name and owning instructor. Provides: ParticipantSubscribes.
Facing: Account — the participant's home view. Exposes: their devices (code, registered_at, last_synced_at) and subscriptions (channel name, upcoming programmes). Provides: ParticipantRegistersDevice; ParticipantUnsubscribes (when subscribed).
Facing: Account, within one subscribed channel. Exposes: channel name/instructor, upcoming programmes. Provides: ParticipantUnsubscribes (when subscribed).
Facing: Account, signed in. Provides: ParticipantRegistersDevice.
Facing: the participant, via their Device. Exposes: subscribed channels and, per channel, today-only programmes (name, scheduled date). Provides: ParticipantSelectsProgramme (when for today).
Facing: the participant, via Device, in the context of an active Session. Exposes: programme/block name while waiting; segment name/kind/target pace/start time/next segment/pace-guidance flag/rep progress while active. Provides: LapButtonPressed (when waiting); SessionStarted (when waiting on block 0). Guarantees: RepeatProgressHeader (loop progress display), PaceIndication (meeting target pace or not).
Facing: the participant, via Device, before any Session exists. Exposes: device_code (when unregistered), status, last_error (when sync_failed). Provides: DataFieldHidden, SyncSucceeded, SyncFailed, TokenReceived — all platform-delivered, firing when the watch's HTTP callback completes rather than from any tap. Timeout: RegistrationPollTimerFired. Guarantees: RegistrationDisplay (device_code + URL shown while unregistered), SilentOfflineFallback (no error shown when a cached programme covers a failed sync).
No facing actor — a platform boundary. Provides: DataFieldOpened, BackgroundSyncTimerFired. No wireframe: not a screen.
Facing: the participant, via Device, in the context of an active Session — but exposes nothing to look at. Provides: DistanceCovered (distance-based segments), WaypointReached (location-based segments) — hardware-delivered, not user actions. No wireframe: not a screen.
No facing actor — the single boundary entry-point for all three sync pathways (initial sync, foreground registration polling, background sync). Provides: DevicePollsServer. No wireframe: not a screen.
Facing: Instructor, within one owned programme. Exposes: programme name/updated_at/participation count, subscriber count, and per sync record: device_code, synced_at, is_current. Read-only — no provides.
stateDiagram-v2
[*] --> waiting
waiting --> active
active --> waiting
active --> complete
complete --> [*]
note right of complete: terminal
See A participant picks today's programme and runs it for the annotated version with rule cross-references.
stateDiagram-v2
[*] --> unregistered
[*] --> syncing
unregistered --> syncing
syncing --> sync_failed
syncing --> no_subscriptions
syncing --> no_programme
syncing --> upcoming
syncing --> ready
sync_failed --> syncing
no_subscriptions --> syncing
no_programme --> syncing
upcoming --> syncing
ready --> syncing
See The watch keeps itself in sync for the annotated version with rule cross-references.
Three findings name no single entity, rule, or surface — they're about deferred specifications, which aren't indexed as a construct of their own.
distance_covered_since (line 1561) is missing a location hint — a documentation-quality note, not a behavioural gap; the deferred spec is still described in prose in the reference appendix above (under RepeatLoopsDistance / RepeatExitsDistance, which call it).ProgrammeCopy.from (line 1565) — same missing-location-hint note; described in prose at ProgrammeCloned.TemplateExpansion.into (line 1571) — same missing-location-hint note; described in prose at ProgrammeCreatedFromTemplate and BlockGeneratedFromTemplate.Generated by the alluminate skill from spec/leadout.allium on 2026-08-07.
allium check, allium model, allium plan, and allium analyse all ran, against allium-cli 3.5.2 (language versions 1–3). 22 check diagnostics and 1 analyse finding (the analyse finding confirms one of the 22 — the unreachable ParticipantSignsIn trigger). 19 of the 22 diagnostics are attributed inline, at the journey step, cast card, and/or reference-appendix construct they concern; the remaining 3 (missing location hints on deferred specifications) appear only in the Validation appendix above, since deferred specs aren't indexed as an attributable construct.allium plan carries test obligations, not rule when/requires/ensures bodies or surface provides text, in this CLI version. Journeys, the Rules reference, the Surfaces reference, and the Cast introductions were all produced from this same close reading, done once.This file is fully regenerated on each run — treat it as generated output, not a hand-edited file; local edits won't survive the next regeneration.