Safety Rules and Maximum Duration

Errors are caught at compile time, in CI and in the editor, not during a pass. Beyond types and references, the compiler enforces safety rules on every step and procedure, and computes how long each can last at most. A library with an error cannot be compiled into a snapshot, so it never reaches the executor.

Hazardous telecommands#

A telecommand declared hazardous: true in the catalogue needs a human confirmation before it leaves. The rule: each send of a hazardous telecommand follows, in the same step, an ask operator "…" confirmation that no other hazardous send has used.

procedure "Blank firing"
  uses sat: platform-v3
  input tcu: tcu_id

  step "Fire the blank"
    ask operator "Fire the blank on the TCU?"
    send blank_firing to sat.tcu[tcu]

• The confirmation is an ask operator without as … into: a typed answer does not confirm anything.
• It is in the same step, before the send.
• One confirmation per hazardous send: two hazardous sends need two ask.

Otherwise the compiler reports procedure::unconfirmed-hazardous:

procedure::unconfirmed-hazardous

  × `blank_firing` is hazardous and needs a confirmation
   ╭─[test.proc:4:3]
 4 │   send blank_firing to sat.tcu[tcu]
   ·   ─────────────────────────────────
  help: add `ask operator "…"` before it in the step: one confirmation per hazardous
        telecommand

The text marks where the confirmation happens; the environment decides who confirms: nobody without human orchestration (acknowledged automatically and logged), the operator in IVV, the operator then a supervisor in orbit. See Hazardous Confirmations. The procedure text stays the same in every environment.

Every wait is bounded#

• expect and wait until require within (procedure::missing-timeout).
• retry requires a count or a total duration (procedure::unbounded-retry).
• There is no loop in the language.
• The durations of within, wait, every and for are literals (procedure::non-constant-duration), with a time unit (procedure::not-a-duration).

The only unbounded wait is a human one: the answer to an ask, or an operator decision. For a run bound to a pass, the executor bounds the wait of a confirmation by the LOS of the pass minus scheduler.margin: past it, the step fails and nothing is sent.

No recursion#

A procedure cannot call itself, directly or through other procedures: a cycle of run is a compile error (procedure::recursion), which shows the cycle:

× `Check TCU` calls itself: `Check TCU` → `Recover` → `Check TCU`

Steps call nothing, so they cannot recurse.

Retries only where safe#

A retry on a step or a call that sends a telecommand changing the on-board state is an error (procedure::retry-not-allowed). See Retries.

Maximum duration#

The compiler computes the maximum duration of every step and procedure. The scheduler compares it with the window of a pass before accepting a schedule, and the API with the pass in progress before launching a run.

One attempt of a step adds up its statements:

For platform-v3, configure sat for Survival sends set_mode (verified within 10 s, read back within 10 s) and set_anode_voltage (echo only, read back within the default 10 s) to each of the three TCUs: 3 × 20 s + 3 × 10 s = 90 s. Each of these setters reads back one parameter; a setter reading back two would count its window twice.

A configure is also subject to the other rules of this page, for each telecommand it sends: a hazardous setter needs its own ask operator before the configure in the step (procedure::unconfirmed-hazardous), and a setter that changes the on-board state (the default) makes the step ineligible for retries.

A step with its retry policy is bounded by the formula of Retries: d + N × max(d, e) for N times, max(d, T) for for T, the smaller of the two with both. An eligible step without retry is bounded with executor.default_retry.

A procedure adds up its actions: each step call with its policy, each sub-procedure (with its own retry if the call has one), each inline step, and every if failed block, since a block may run.

Example, "Hot standby test" of the example library, with the default policy {times: 1, every: 2s}:

Alarm reactions#

An alarm of a catalogue may run a procedure when it is raised (on_raise: run "Safe TCU"). The reaction runs without anyone to confirm anything, so the compiler checks, against the libraries compiled for the platform of the alarm:

The executor binds the role to the target of the alarm and the input to its instance. See Alarms and Alarm Handling.

procedure "Safe TCU"
  uses sat: platform-v3
  input tcu: tcu_id

  step "Command safe mode"
    send safe_mode to sat.tcu[tcu]
    expect sat.tcu[tcu].mode is SAFE_MODE within 10 s

Summary of the diagnostics#