Language › Specification

Language

The arche-lang specification

arche-lang describes a system — what it is made of, what each part does, what it shall do and how that is verified — in plain text, and compiles to an Arche project. This document is the language itself: its lexical elements, its grammar, and what each construct means. The reference of every declaration and property is patterns.md; how to write a model well is style.md; a first model, step by step, is the tutorial.

Like Go, the language is small, has one way to write each thing, and one layout, which archec fmt writes. Every example below compiles as it is (the tests compile them); a block marked fragment is part of a declaration.

Notation#

The grammar is written in EBNF:

Production = name "=" Expression "." .
Expression = Term { "|" Term } .
Term       = Factor { Factor } .
Factor     = name | "literal" | "(" Expression ")" | "[" Expression "]" | "{" Expression "}" .

[ … ] is optional, { … } is zero or more, | separates alternatives; newline is the end of a line.

Source files#

A model is one or more UTF-8 files ending in .arche. One file is the main one; the others are included by it, directly or not. A file holds declarations; a file included inside a system or a component body holds part of that body.

File        = [ PackageClause ] { Include | Declaration } .
PackageClause = "package" QualifiedName newline .
Include     = ( "include" | "requires" ) string newline .

Lexical elements#

Element Form
Comment // to the end of the line, /* … */; /// … before a declaration is its description
Identifier letters, digits, _; a - inside (REQ-BRK-001, kria-parts) — so a subtraction has spaces around its -
Keyword contextual: a word is a keyword only where a declaration may start, so state, port or type stay usable as names
Number 42, 3.14, 1e-3, 0xFF, 0b1010, 1_000_000
Quantity a number and its unit, no space: 5ms, 100MHz, 3.3V, 2kg; ns us µs ms s min h make a duration
String "…" with \n \t \" \\; other backslashes are kept ("$\frac{a}{b}$"); """…""" spans lines
Translation after a string, en "…" (or de, fr…) on the same line or the next, indented deeper
Code ```ts … ```, ```python … ```, ```arche … ``` (or latex, yaml); a bare ``` is the project's handlers language; a few properties take a bare Python line (do send(x, M()))
Separator a newline ends a property or a declaration; inside a one-line block, ;
QualifiedName = identifier { "." identifier } .
Path          = identifier [ "[" Index "]" ] { "." identifier [ "[" Index "]" ] } .
Text          = string { language string } .

A project says the edition of the language it is written in, as go.mod names a Go version: edition "0.12". Without one, it is read as it always was; from edition 0.12 on, an old keyword spelling is an error, not a warning. archec fmt --edition 0.12 --write writes the standard spellings and the edition. An edition newer than archec knows is an error: update archec.

A keyword made of two words is written with a hyphen, as a noun phrase: port-type, test-plan, use-case, system-function, failure-mode, operating-mode. The fused spellings (porttype, testplan, usecase, statemachine) are old ones. And a word has one meaning: where an old spelling of one declaration is the standard word of something else, the warning says what to write and what the word is for — Write `state` (`mode` is for operating modes, `operating-mode`).

Word What it means What it no longer means: write instead
process an operating-system process of a deployment a workflow: workflow
contract an assume/guarantee contract inside a component an interface: interface
mode (an operating mode is operating-mode) a state: state
model the system a test plan or a simulation runs on a system: system
bus the bus itself: a component with kind bus, a route's over, a link's bus a port type: port-type
view the page a menu entry or a story step opens a viewpoint: viewpoint
goal the safety or security goal a hazard or a threat answers a mission: mission
function a system function (system-function) a chain step runs a function of a component: fn
tests the cases a verify block names a test plan: test-plan
kind a catalog kind a pseudo-state's kind: pseudo
source where code lives (a component, a function) where a requirement comes from: origin

Declarations#

Every declaration has the same shape: a keyword, a name, a label, what its keyword takes in the header, then a body of properties and nested declarations.

Declaration = keyword [ identifier ] [ Text ] { Header } [ "as" identifier ] [ Body ] newline .
Body        = "{" { Property | Group | Declaration } "}" .
Property    = key [ Values ] newline .
Group       = groupname "{" Property { ";" Property } "}" .
Values      = Value { "," Value } .
component Pump "Water pump" {
  description "Moves water from the tank to the field."
  kind device
  in power: power
  out flow: can sends FLOW
}

message FLOW: float32 "Flow"

system Field {
  part pump: Pump
}
  • The name is how the model refers to it. Its case says what it is, as in Go: PascalCase for what is defined (components, systems, types), snake_case for what is inside (parts, ports, functions, variables), SCREAMING_CASE for messages, constants and literals; requirement and test ids are written as their documents write them (REQ-BRK-001).
  • The label is the name people read, with its translations.
  • as id gives the element its id in Arche when it is not the name (an import keeps Arche's ids this way: component flash_memory "FLASH" as c-1793752253957).
  • A property is a key and its values, on one line; a value list continues on the next line after a ,. Properties that go together may be written as a group, which is the same as writing them one by one:
timing { latency 2ms; jitter 100us; bitrate 1Mbps }

The groups are timing, delivery (how messages are delivered), compute (a processor's cores, OS, memory, chip), physical (mass, power, cost) and errors (a part's error model: errors { produces omission; from a }).

The declarations come in sets (patterns.md lists them): the core — what every model is written with — and sets for a purpose: deployment, functional analysis and scenarios, safety/security/design space, the Arche app, project tooling.

Project tooling holds what extends archec: a generator (a code target), an importer (a file of another tool read into arche-lang: script or command, extensions, reads) and an exporter (the model written as one: templates, script or command, extension), each with its typed options. They are usually written in a plugin (plugins, generators).

importer melody "Melody CCM" { script "melody/import.ts"; extensions ".ccmproject" }
exporter melody "Melody CCM" { script "melody/export.ts"; extension ".ccmproject" }

Types and values#

Type      = [ "optional" ] [ "*" ] TypeName [ TypeArgs ] [ "[" [ Index ] "]" ] | string .
TypeName  = QualifiedName | "struct" Body .
TypeArgs  = "<" ( Type | number ) { "," ( Type | number ) } ">" .         // no space before "<"
Generic   = "struct" identifier "<" identifier [ ":" "int" ] { "," identifier [ ":" "int" ] } ">" Body .
Value     = number | quantity | Text | Code | "true" | "false" | "nil" | Path
          | "[" [ Values ] "]" | "{" [ Field { "," Field } ] "}" | Value ".." [ Value ] | Expression .

The scalar types are bool, int8…int64, uint8…uint64, float32, float64, char, byte, string, bytes, duration, timestamp; any is any of them. T[4] is an array, optional T may be absent, *T points to a T, "Vec<u8>" is a type of another language, kept as written.

const MAX_SPEED = 36 unit m/s

type Speed = float32 unit m/s range 0..70

enum Mode { MANUAL, AUTO }

struct Sample {
  speed: Speed
  mode: Mode
  stamp: optional uint64
}

union Command {
  stop
  go: Speed
}

A unit is written as it is (unit m/s²); archec checks that what is compared or added has one quantity. A product or a quotient has the quantity its dimensions make: V_BUS * I_MAX is a power, DIST / T_STOP a speed, 1 / 5ms a frequency, so const P = V_BUS * I_MAX { unit W } holds and { unit s } is a unit-mismatch. The same goes for a parameter's expr against its unit. A dimension with no usual name is written out (length·time⁻³). Nothing is converted: kWh and J are both energies, which is all archec checks.

A struct may take types and numbers: struct Ring<T, N: int>. Each use with its arguments, Ring<Sample, 64>, is a struct of its own, Ring_Sample_64, the fields with T and N replaced — what Arche, the codecs and the generated code see. The generic itself is not emitted.

struct Reading {
  value: float32
}

struct Ring<T, N: int> "Ring buffer" {
  items: T[N]
  head: uint16
}

message HISTORY {
  last: Ring<Reading, 8>
}

A type the code provides is native: its name in each language, and the header (C, C++) or the package (Go) that declares it. The generated code uses it as it is; archec does not look inside it.

type Iq native "IQ sample" {
  cpp "dsp::Iq" include "dsp/iq.h"
  c "iq_t" include "dsp/iq.h"
  rust "dsp::Iq"
  go "dsp.Iq" import "example.com/dsp"
}

A native type that names itself in no language is native-type.

Wire formats#

A message's bytes are its fields in order, little-endian, byte-aligned, unless it says its wire format, bit by bit, as a CAN DBC or ASN.1's ACN does. Any of byte-order and size on the message, or at, bits, scale, offset, signed, checksum, counter on a field, gives it one:

enum Gear { P, R, N, D }

message WHEEL_SPEED {
  byte-order big
  size 8
  speed: float32 unit km/h range 0..600 bits 16 scale 0.01
  gear: Gear
  temp: float32 range -40..215 bits 8 offset -40
  alive: uint8 bits 4 range 0..15 counter
  crc: uint8 at 56 checksum crc8
}
  • A field starts at bit at of the frame, or right after the field before. It takes bits bits: a bool 1, an enum as few as hold its literals, a number its type's size.
  • Bit k of the frame is in byte k / 8. Little-endian (byte-order little, the default, Intel): at is the field's least significant bit, bit k is bit k % 8 of its byte. Big-endian (big, Motorola): at is its most significant bit, bit k is bit 7 - k % 8, and the field runs towards the end of the frame. A field may say its own byte-order.
  • With scale or offset, a number travels as a whole one: raw = round((value - offset) / scale), saturated to what its bits hold; value = raw × scale + offset. A float without them travels as its IEEE bits, 32 or 64.
  • The raw value is signed when the field's type is, or with signed.
  • checksum crc8 (SAE J1850) or checksum xor8: one byte computed over the frame's other bytes; a frame whose checksum is wrong does not decode. counter: a rolling counter, which the generated C wiring counts up at each send.
  • The frame is size bytes, or as many as the fields reach; bits no field takes are zeros.

archec checks that no two fields share a bit (wire-overlap), that each fits the frame (wire-size), that a field's range is what its bits carry once scaled (wire-range), and that a message a route puts on a CAN bus fits its frame, 8 bytes or 64 on CAN FD (wire-frame). The DBC, ARXML, ICD, Renode and archec replay read the fields on their bits, and archec gen --target wire writes their codecs in C, Rust (no_std), Go and Python; --target c, embassy and go send and receive with the same code.

Names, packages and paths#

Every declaration with a name is known everywhere by it: names are global, as Arche's ids are. A package groups declarations under a name — written first in a file, package chassis puts the file in it — and chassis.BRAKE_CMD names one of them explicitly.

package chassis

message BRAKE_CMD: float32 "Brake"

An element inside another is named by its path: Car.ecu.can0 is the port can0 of the part ecu of the system Car. Inside a component, a path starts from it (ecu.can0). A part that shows another model's component (ref tile.tile) is walked into: what is in that component is in it.

Structure#

A system is one model of Arche: the parts it is made of and how they are linked. A component is a definition its parts are copies of; one written inside another is a part of it.

Port = ( "in" | "out" | "inout" ) identifier [ ":" Type ] [ Text ] [ ( "sends" | "receives" ) Values ] [ Body ] .
Link = [ "link" [ identifier ] ] Path "->" Path [ Text ] [ ":" Type ] [ "as" identifier ] [ Body ] .
message GO: bool "Go"

component Panel "Panel" {
  out button: can sends GO
}

component Motor "Motor" {
  in cmd: can receives GO
}

system Station {
  part panel: Panel
  part motor: Motor
  panel.button -> motor.cmd
}

A link's type and the messages it carries come from its ports; the editor shows them, and : type and carries say them on the link.

Code#

A part says which files of the code it is with source, on its component: a file, a folder, or a glob — * within a folder, ** across folders, {a,b} — from the main file's folder. A file belongs to the part whose source names it most closely: a file named outright before a glob, a longer folder before a shorter one. A function's source is its component's.

port-type call "Call" {
  handling message
}

component Planner "Planner" {
  source "src/planner/**"
  in api: call
}

component Shell "Command line" {
  source "src/cli.ts"
  source "src/cli/*.ts"
  out uses: call
}

system App {
  part shell: Shell
  part planner: Planner
  shell.uses -> planner.api
}

archec recover writes such a model from the code. archec conform checks that every import between two parts is one of the model's links, and reports the links no import is under. Two props say more to them: prop weak_links on a system or component lists pairs of its parts (["a -> b: 1 import"]) whose imports are allowed though no link is drawn, and prop recovered on a system says archec recover wrote it, so that archec diagram draws only its heaviest links (a link's weight is the number its label gives: "12 imports").

Services, dataflow and topics#

How two parts talk is said on their ports (and links): pattern, buffer, timeout… (deployment). Three more come from PYCOGEN's McCOFFEE components.

A service is called by its name, wherever it runs: service "name" on an out port calls it, on an in port serves it. No link is drawn. A name that no in port serves is no-service.

message JOB {
  id: uint32
}

component Planner "Planner" {
  out compute: data sends JOB { service "compute" }
}

component Worker "Worker" {
  in compute: data receives JOB { service "compute" }
}

Dataflow is signal processing: a source streams vectors of samples, and a sink runs when enough of them have come. Its properties go in a dataflow group (or one by one, which is the same), and give the port pattern dataflow.

Property Side What it says
vector T both the type of one sample (PYCOGEN's DataVector<T>)
header H both the header each vector carries
push-threshold n source samples gathered before they are pushed
transfer copy | share both the sink gets a copy (the default), or the same buffer
threshold n sink samples that must have come for it to run
history n sink samples of the vector before that each run sees again
max-processing n sink the most samples one run takes
backpressure on | off both the sink may make its source wait (off by default)
backpressure-threshold n sink samples waiting that make it ask
struct FrameHeader {
  seq: uint32
}

component Adc "ADC" {
  out iq: data {
    dataflow { vector float32; header FrameHeader; push-threshold 256 }
  }
}

component Fft "FFT" {
  in iq: data {
    dataflow { vector float32; header FrameHeader; threshold 1024; history 64 }
  }
}

system Receiver {
  part adc: Adc
  part fft: Fft
  adc.iq -> fft.iq
}

A sink linked to a port that is not a source, or to a source of another vector, is dataflow-source; two ends that do not say the same backpressure, dataflow-backpressure. A dataflow property on another pattern, or on the wrong side, is comm-property or wrong-side.

A topic names what a pub-sub port publishes or subscribes to. Its parts in braces are filled when a message is published, each from the message's field of that name, or of the type written ({sensor: uint8}): PYCOGEN's sub-topics. A port with a topic is matched by it — an in port of the same topic subscribes — so linking it too is topic-wired; a part that names nothing the message has is topic-part. archec sim delivers what such a port sends to every in port whose topic matches it (* a level, ** any number of them, a part in braces any value); a metric reaches the filters that match /<part path>/<metric> the same way.

message TRACK {
  id: uint32
  range: float32
}

component Radar "Radar" {
  out tracks: data sends TRACK { pattern pub-sub; topic "/tracks/{id}" }
}

component Display "Display" {
  in tracks: data receives TRACK { pattern pub-sub; topic "/tracks/{id}" }
}

The generator model gives each port and each link its pattern (a port that requires or provides an interface with operations is client-server), its topic and topicParts, service, and dataflow with the properties of both ends.

Behaviour#

A function's body is code, as Arche runs it: TypeScript, Python, or the action language — the project says which (handlers typescript | python | arche, a component may say its own, a block says its own: ```ts; see handlers.md). It is written in the model or in a .ts or .py file beside it (archec fmt --extract-code). A variable has a type and a value; a state machine has states and transitions:

Transition = ( Path | "*" ) "->" Path [ "as" identifier ] [ "on" ( identifier | string ) ] [ Guard ] [ "/" Action ] .
Guard      = "[" text "]" | "when" string .
message GO: bool

component Valve "Valve" {
  in cmd: can receives GO
  var open: bool = false

  fn toggle "Toggle" ```python
    self.open = not self.open

states { state Closed state Open Closed -> Open on GO [self.open] Open -> Closed on GO } }

system Plant { part valve: Valve }


A guard is written in brackets; `when "…"` is for a guard that is a sentence a
bracket could not hold (an apostrophe, an accent). `* -> Fault` leaves every state.

### Actions

A body may also be written in the action language, in a block marked `arche`
instead of `python`. archec checks it — the names it uses, their types, the ports
it sends on and what they carry, the states it goes to — and translates it: to the
Python Arche's simulator runs, to Rust in `archec gen --target embassy` (no TODO
left in `app.rs`), to C. Python stays for plant models and test code.

```text
Body      = { Statement newline } .
Statement = "var" identifier [ ":" Type ] [ "=" Expr ]
          | Target ( "=" | "+=" | "-=" | "*=" | "/=" ) Expr
          | "if" Expr Block { "else" "if" Expr Block } [ "else" Block ]
          | "while" Expr Block | "for" identifier "in" Expr ".." Expr Block
          | "send" identifier Expr          // a port, and a message: BRAKE_CMD { force: 1.0 }
          | "goto" identifier | "kick" identifier | "wait" Expr | "return" [ Expr ]
          | "log" Expr { "," Expr } | "break" | "continue" | Call .
Call      = identifier "(" [ Expr { "," Expr } ] ")"            // a function of the part, a builtin
          | identifier "." identifier "(" [ Expr { "," Expr } ] ")" .  // port.op(…): over the port's link
Expr      = or and not, == != < <= > >=, + - * / %, unary -, x.f, f(…), port.op(…),
            MSG { f: e }, { f: e } where a record is expected, 10ms, "text", true, false.

The names a body sees are its locals, the function's parameters, the part's variables and functions, constants and enum values (Mode.On); state == Ready tests the part's state. Builtins: now() (ns), abs min max clamp sqrt, sin cos atan2 (rad), int and float to convert, to_s and to_ms. Durations are 10ms, 50us, 2s; a 64-bit integer holds a time in ns and mixes with them. An integer divided by an integer is an integer, as in Rust and C.

const REACTION_TIME = 150ms
const MU_DRY = 0.7

message BRAKE_CMD { force: float32; emergency: bool }

component Planner "Planner" {
  out can_brake: can sends BRAKE_CMD
  var speed: float32 = 0
  var obstacle_m: float32 = 100

  fn plan "Trajectory planning" ```arche
    var d = speed * to_s(REACTION_TIME) + speed * speed / (2 * MU_DRY * 9.81)
    if obstacle_m < d * 1.2 {
      send can_brake BRAKE_CMD { force: 8000.0, emergency: true }
    }

}

system Car { part planner: Planner }


#### Calling another part

`port.op(…)` calls a function of the part at the other end of the port's link: an
operation of an interface the port `requires` (with what it extends). archec
checks the call against the interface — the port, the operation, as many
arguments as it takes, of its types, and what it gives — and the link's other end
provides the interface (`unprovided-interface`) with a function of that name
(`missing-operation`).

```arche
interface BrakeApi "Brake API" {
  fn apply(force: float32) -> bool
  fn release()
}

component Controller "Controller" {
  out brake: requires BrakeApi
  var applied: uint16 = 0

  fn step "Brake when asked" ```arche
    if brake.apply(2.5) {
      applied += 1
    } else {
      brake.release()
    }

}

component Brake "Brake" { in api: provides BrakeApi var force: float32 = 0

fn apply(f: float32) -> bool ```arche force = f return f > 1.0

fn release() ```arche
  force = 0.0

}

system Car { part ctl: Controller part brk: Brake ctl.brake -> brk.api }


The provider's function runs on the provider, its variables and state, and its
result comes back; the caller waits for it. How each target does it:

| Target | `brake.apply(2.5)` |
|---|---|
| `archec sim` | the function runs at once on `brk` (as a function call: no time, no queue, even if `brk` is busy) |
| Arche (Python, TypeScript) | `await component("brk").apply(2.5)` — the part named as the link's other end |
| C | `controller_call_brake_apply(self, 2.5f)`: the wiring calls `brake_apply(&part_brk, …)` by which part asks, in the caller's thread; without a deployment, in `controller_ports.c`, yours |
| C++ | `this->call_brake_apply(2.5f)`, a `std::function` main.cpp sets (unset, it throws) |
| Rust (Embassy) | `_out.call_brake_apply(2.5).await`: a request on a channel to `brk`'s task, which runs the function and signals the reply — so the two must be on two threads (on one, archec says so and the call gives the default value) |
| Go | `self.Call("brake", "apply", float32(2.5)).(bool)`: main.go calls `parts.Brk.Apply`, in the caller's goroutine |

In C, C++ and Go the provider's function runs in the caller's thread: the two
parts on one thread, or a function that only reads and writes its own
variables, are what keeps it safe. A part that is reached over a bus (another
binary) is not called: archec says so.

#### Operations, as in IDL

An operation says more, as CORBA's IDL and McCOFFEE's components do:

```text
Operation = [ "oneway" ] "fn" identifier "(" [ Arg { "," Arg } ] ")" [ "->" Type ] [ "raises" Path { "," Path } ] .
Arg       = [ "in" | "out" | "inout" ] identifier ":" Type .
Attribute = [ "readonly" ] "attribute" identifier ":" Type .
Exception = "exception" identifier [ Text ] Body .          // a struct
exception NotFound "Not found" {
  id: uint32
}

struct Track {
  id: uint32
  range: float32
}

interface Tracks "Tracks" {
  readonly attribute count: uint32
  attribute rate: float32
  fn lookup(id: uint32, out t: Track, inout hint: uint8) -> bool raises NotFound
  oneway fn forget(id: uint32)
}

interface TracksAdmin extends Tracks {
  fn clear()
}
  • An argument is in by default. The operation writes an out argument and reads and writes an inout one: at port.op(…), what is passed there is a variable (or a field), not a value.
  • A oneway operation has no result and the caller does not wait for it: no -> T, no out argument (oneway-result).
  • raises names exceptions: structs an operation may raise instead of its result (raises-not-exception for another type).
  • An attribute is a value the provider holds, which a client reads (and writes, unless it is readonly).
  • extends (in the header or in the body) adds another interface's operations, attributes and messages.

archec sim runs an out argument as an in one: its value does not come back. The generator model gives each operation with its arguments' directions, oneway and raises, for the generated code to say them.

Physical equations#

A port type with a potential and a flow is physical: a pin (voltage, current), a flange (velocity, force), a shaft, a heat port, a pipe. A part with such ports says its behaviour as equations with no direction, der(x) anywhere in them, a port's variables written port.name; a var that der names is a state (its value the start), one with a value and no der a parameter, one without a value an unknown. Its links join ports into nodes, where the potentials are equal and the flows into the parts add up to zero.

PortVar  = ( "potential" | "flow" ) identifier [ "unit" unit ] .
Equation = "equation" Expr "=" Expr .     // + - * / ^, der(x), t, functions; no comparison
port-type pin "Electrical pin" {
  potential v unit V
  flow i unit A
}

component Cell(v: float64 = 1.5V) "Cell" {
  inout p: pin
  inout n: pin
  equation p.v - n.v = v
  equation p.i + n.i = 0
}

component Resistor(r: float64 = 100Ω) "Resistor" {
  inout p: pin
  inout n: pin
  var i: float64 unit A
  equation p.v - n.v = r * i
  equation p.i = i
  equation p.i + n.i = 0
}

component Cap(c: float64 = 1mF) "Capacitor" {
  inout p: pin
  inout n: pin
  var v: float64 = 0 unit V
  equation v = p.v - n.v
  equation c * der(v) = p.i
  equation p.i + n.i = 0
}

component Ground "Ground" {
  inout p: pin
  equation p.v = 0
}

system Rc {
  part cell: Cell
  part r: Resistor
  part c: Cap
  part gnd: Ground
  cell.p -> r.p
  r.n -> c.p
  c.n -> cell.n
  cell.n -> gnd.p
}

A part has as many equations as unknowns — its variables without a value, its states, the potential of each of its ports (their flows come from the links) — and archec checks each network gives each unknown once. archec physics sorts and solves it, archec fit finds its parameters from measured data, archec fmi makes it an FMU, and Arche's simulator runs it as the equations of a part physics. The standard parts are in include "std/physics".

archec physics integrates at a fixed step with RK4 by default. A stiff network — a fast time constant beside a slow one — wants --integrator implicit or trapezoid (each step solved by Newton's method), and --tol 1e-6 lets the step adapt to the error it makes. archec physics … --linearize gives the network's A, B, C and D at an operating point, its modes (time constants, frequencies and damping) and, with --lqr Q,R, a state-feedback gain. --batch 100 --vary motor.r=0.8..1.2 runs it a hundred times over worker threads, a parameter drawn within its range each time, and sums the runs up (archec sim --batch does the same for the behaviour).

Bodies#

A part may say its body, for a physics engine: its shape, its mass, and the joint by which it moves in the part it is in (the world for a top part). Both go in the physical group.

Shape = "shape" ( "box" len "," len "," len | "sphere" len | ( "capsule" | "cylinder" ) len "," len ) [ "at" Vec ] [ "rot" Rot ] .
Joint = "joint" [ ( "hinge" | "slide" ) [ Axis ] | "ball" | "free" | "fixed" ] [ "at" Vec ] [ "rot" Rot ] [ "range" Value ".." Value ] [ "=" Value ] .
Axis  = "x" | "y" | "z" | "-x" | "-y" | "-z" | "[" Value "," Value "," Value "]" .
Vec   = len "," len "," len .
Rot   = angle "," angle "," angle | Axis angle .
component Link "Link" {
  physical {
    mass 1kg
    shape capsule 0.04m, 0.5m at 0, 0, -0.25m
  }
}

system Arm {
  part upper: Link {
    joint hinge y at 0, 0, 1.5m range -2..2 = 0.3
    part fore: Link {
      joint hinge y at 0, 0, -0.5m
    }
  }
}

A box's sizes are full sizes; a capsule's or a cylinder's are its radius and its length, along z. at is where the shape's centre is in the part's frame, or where the part's frame is in its parent's: the joint is there. rot turns the shape in the part's frame, or the part's frame in its parent's: roll, pitch, yaw (rot 0, 0, 90deg, about the parent's x, then y, then z: URDF's rpy) or an axis and an angle (rot z 90deg, rot [1, 1, 0] 45deg); an angle without a unit is in rad. The joint's axis, the shape, the sensors' and thrusters' places and the parts inside are in the turned frame (joint hinge y at 0, 0, 1m rot z 90deg swings about the parent's -x). A hinge's range and start are in rad, a slide's in m; the axis is z when not said. archec gen --target mujoco makes a body of each part with a mass or a shape, nested as the parts are.

archec import robot.urdf and archec import scene.xml (MJCF) write a robot this way: a part per body, its mass, its shape and its joint; what they do not say as prop records (prop shoulder = {damping: 0.1, effort: 20}, prop inertial = {…}, more geoms as prop rod = {geom: capsule, size: [0.02, 0.25]} in MuJoCo's sizes). An actuator is a kind actuator part in the body whose joint it drives, a sensor a kind sensor part in the body it measures; what they are comes from the unit of the message they receive or send. A sensor's noise and cutoff become its port's noise and its fields' range, an actuator's forcerange and filter its port's force-range and lag, and each <key> (the first one also the joints' starts) a keyframe of the system.

Sensors and actuators#

A sensor reads what is, not exactly; an actuator does what it is told, not at once. A kind sensor part says how it reads on its out port, a kind actuator part how it acts on its in port — the response group:

noise      σ of a gaussian noise on each float field of that quantity: 0.002rad, or 0.05m/s², 0.001rad/s
resolution the step a reading is rounded to: 0.0015rad
latency    how old the reading is (on an actuator's in port: its dead time)
gain       output = gain × command (1 when not said)
lag        a first-order lag from the command to the output: 20ms
force-range where the output saturates: -2..2
message ANGLE { angle: float64 unit rad range -3.2..3.2 }
message TORQUE { torque: float64 unit N·m range -1..1 }

component Encoder "Encoder" {
  kind sensor
  out angle: data sends ANGLE {
    noise 0.002rad
    resolution 0.0015rad
    latency 2ms
  }
}

component Motor "Motor" {
  kind actuator
  in cmd: data receives TORQUE {
    response { gain 2; lag 20ms; force-range -1.5..1.5 }
  }
}

A reading is the value plus its noise, saturated by the field's range (MuJoCo's cutoff), then rounded to the resolution; a noise in another unit of the field's quantity is converted (1deg on a field in rad), a bare number goes on every float field. A command is first clamped to its field's range (MuJoCo's ctrlrange): that is what the part's handlers see. The output follows it through the lag, times the gain, saturated by the force-range. A port's latency adds to its links'.

The noise is drawn from a seed (simulation { seed 7 }, --seed, 1 otherwise), with one generator everywhere: archec sim and its page, the MuJoCo bridge, the C of a sim build (-DARCHE_SIM: production firmware adds no noise; the clamps and the lag are always there), so a run repeats and archec difftest compares the two sides with the noise on. In a physical network an actuator's in signal takes its command at <port>.command and acts through its type's range, its lag (a state of the network: archec physics --linearize shows its mode), its gain and its force-range; a sensor's out signal is printed as it reads. archec warns of a noise where no sensor reads or a gain where no actuator acts (realism-port), a noise of a quantity none of the fields has (unit-mismatch), and a range the wrong way round (range-reversed).

Keyframes#

A keyframe in a system is a named start state, as MuJoCo's: each line sets a part's variable, the position of a part's joint (part.joint, rad or m) or the command an actuator starts with (its in port).

Keyframe = "keyframe" identifier [ Text ] "{" { Path "=" Value } "}" .
message TORQUE { torque: float64 unit N·m range -1..1 }

component Link "Link" {
  physical { mass 1kg; shape capsule 0.04m, 0.5m at 0, 0, -0.25m }
}

component Motor "Motor" {
  kind actuator
  in cmd: data receives TORQUE
}

component Ctrl "Controller" {
  out cmd: data sends TORQUE
  var target: float64 = 0
}

system Arm {
  part upper: Link {
    joint hinge y at 0, 0, 1.5m
    part motor: Motor
  }
  part ctrl: Ctrl
  ctrl.cmd -> upper.motor.cmd
  keyframe raised "Raised" {
    upper.joint = 1.2
    upper.motor.cmd = 0.3
    ctrl.target = 1.2
  }
}

archec sim --keyframe raised and archec physics --keyframe raised start from it (and --linearize --at raised linearizes there), archec gen --target mujoco writes it as a <key>, and a test case with keyframe raised starts from its variables. A line that names nothing it can set is an error (keyframe-name).

A joint's line depends on its kind, as MuJoCo's qpos and qvel do:

Joint Where it is How fast it moves
hinge, slide part.joint = 0.3 (rad, m) part.joint.vel = 1 (rad/s, m/s)
ball part.joint = [0, 0, 30deg] (roll, pitch, yaw) or [w, x, y, z] (a quaternion) part.joint.vel = [wx, wy, wz] (rad/s, in its frame)
free part.joint.at = [x, y, z] and part.joint.rot = [r, p, y] (or [w, x, y, z]), in the world part.joint.vel = [vx, vy, vz] (m/s, in the world), part.joint.spin = [wx, wy, wz] (rad/s, in its frame)

What a line does not set is where the joint starts: a free body where its parts place it.

One instant#

What happens at one instant happens in one order, which the model gives, not the machine — as in Lingua Franca. The simulator (archec sim) follows it, the C that archec gen writes follows it within a thread, and archec difftest checks that the two agree.

  • Time is logical: a body takes no time unless it waits (wait 10ms).
  • What is due at the same instant runs in the order it was scheduled: a message sent on a link with no latency comes after what was already due then.
  • At the start: each part's watchdogs are armed and its machine enters its initial state, the parts in the order the system declares them (a part's own parts after it); then each fn main starts; then the periodic threads, in the order the deployment declares them, the first call one period later.
  • A part does one thing at a time, to the end. What comes to it meanwhile waits in its mailbox, in the order it came.
  • A message to a part: first the one transition it triggers — from the innermost state the part is in outwards, in the order written at each level, * -> last (and not taken when the part is already in its target); the first whose guard holds — then the port's on-receive, then the port's handlers in the order written. A guard and an action see the message's fields by name.
  • A transition: the on-exit of each state it leaves, innermost first; its action; the on-enter of each state it enters, outermost first. It leaves and enters what is inside the innermost state around both its source and its target (for * -> and goto, the source is the state the part is in): so Up -> Up leaves Up, and the states in it, and enters it again.
  • on "after 500ms" counts from when the state was entered; entering it again starts it again; leaving it stops it.
  • A message sent where links fan out goes along them in the order they are written.
  • A variable keeps what its type holds: a uint8 at 255 plus 1 is 0, an integer divided by an integer is an integer, a float32 is rounded to one.
message BEAT { seq: uint16 }

component Monitor "Monitor" {
  in beat: can receives BEAT
  states {
    state Waiting
    state Up
    state Lost
    Waiting -> Up on BEAT
    Up -> Up on BEAT [seq > 0]
    Up -> Lost on "after 30ms"
    Lost -> Up on BEAT
  }
}

system Net {
  part monitor: Monitor
}

Each heartbeat with a seq above 0 enters Up again, so its 30 ms start again.

A part's life#

A part may say what it runs when it is made, starts, stops and is released, as McCOFFEE's components do: on-init, on-start, on-stop and on-release, each a body on the component.

component Filter "Filter" {
  var taps: uint16 = 0
  var running: bool = false

  on-init ```arche
    taps = 64

on-start ```arche running = true

on-stop ```arche
  running = false

on-release ```arche taps = 0

}

system Rx {
part filter: Filter
}

archec sim runs every part's on-init, then every part's on-start, at 0, in the order of the parts, before the state machines enter their first state and the fn mains start. At the end of the run (--for) it runs every part's on-stop, then every on-release. A definition built on another (extends) has the base's when it says none. The generator model gives them as each component's lifecycle, with their C, C++, Rust and Go.

Deadlines and watchdogs#

A port or a transition may say how late is too late: past its deadline — the part starts on the message later than that after it was sent, or on the timer later than that after it ran out — its on-deadline runs instead (on a port: instead of the transitions, on-receive and handlers; on a transition: once its guard holds, instead of the transition). A watchdog runs its on-timeout when no kick restarted it within its timeout; it is armed at the start, and once it has run out, only a kick arms it again.

message CMD { level: uint8 }

component Actuator "Actuator" {
  in cmd: can receives CMD {
    on-receive ```arche
      kick quiet
    ```
    deadline 5ms
    on-deadline ```arche
      late += 1
    ```
  }
  var late: uint16 = 0

  watchdog quiet "Commands stopped" {
    timeout 50ms
    on-timeout ```arche
      goto Safe
    ```
  }

  states {
    state Idle
    state Active
    state Safe
    Idle -> Active on CMD [level > 50]
    Active -> Idle on CMD [level < 20] {
      deadline 2ms
      on-deadline ```arche
        late += 1
      ```
    }
    Safe -> Idle on CMD [level == 0]
  }
}

system Plant {
  part act: Actuator
}

Both are simulated, and generated in C and in Rust (Embassy: what comes to a part with a deadline carries when it was sent, and the part's task waits for its next watchdog beside its inputs); Arche's own simulator does not have them yet.

Algorithms and dataflow#

A signal-processing algorithm is a component with kind algorithm. Its ports carry the data; its cycle is the functions it has of initialize, configure, execute_preprocessing, execute, execute_postprocessing and reset (archec sim runs initialize and configure at the start). Its instantiation parameters are the component's parameters; a var with parameter configuration is set again when it is configured, one with parameter internal is its own. working-memory saved 1KiB and working-memory tmp 4KiB say the memory it works in; a deployment's place says the allocator.

stereotype says what kind of algorithm it is: splitter (one input, several outputs), joiner (several inputs, one output), cylinder, macro-algo, do-not-use-sw-caches, pipeline, local-memory-only. On a part, disable-thresholds and bypass-config-threading are the instance's.

An algorithm with parts is a composite: its parts are its roles, its links the connections between them, its ports written = part.port its delegations. It is L1 when its parts are plain algorithms, LN when one is a composite. A part's after runs it after another part, with no data between them.

A metric is a message with kind metric. An out port that sends it publishes it on /<part path>/<metric> (or on its topic); an in port reads it, and its topic filters what it takes: * is one level, ** any. (The splitter and the joiner are written out in examples/mccoffee.)

message SNR { kind metric; value: float32 }

component Filter(taps: int32 = 16) {
  kind algorithm
  processing { stereotype pipeline; working-memory tmp 4KiB }
  var gain: float32 = 1.0 { parameter configuration }
  in input: data receives FRAME { handler FRAME -> execute }
  out output: data sends FRAME
  out snr: data sends SNR { pattern pub-sub }
  fn configure ```arche
    gain = clamp(gain, 0.0, 4.0)

fn execute(seq: uint32, level: float32) ```arche send output FRAME { seq: seq, level: level * gain } send snr SNR { value: level * gain }

}

component Chain {
kind algorithm
in input = split.input
out output = join.output
part split: Splitter
part f1: Filter(taps = 32)
part f2: Filter { after f1 }
part join: Joiner
split.left -> f1.input
split.right -> f2.input
f1.output -> join.left
f2.output -> join.right
}

The linter reports a stereotype on the wrong side (an instance's on a definition), a splitter or a joiner with the wrong ports, a part of a composite that is not an algorithm, parts that run after each other in a circle, a metric filter nothing publishes on, and a dataflow link whose two ends do not say back-pressure the same way (backpressure on at both ends, see Services, dataflow and topics).

Requirements and traces#

A requirement is a statement, with what it is (priority, status, method…). A trace links two elements; it is written where it starts, as a property (satisfies, verifies, derives, refines…), each value with its id if it has one:

TraceProperty = tracekey TraceValue { "," TraceValue } .
TraceValue    = Path [ "as" identifier ] .
TraceDecl     = "trace" tracekey Path "->" TraceValue { "," TraceValue } [ Text ] .
requirement REQ-1 "Start" {
  text "The pump shall start within 100 ms of a START command."
  priority high
}

component Pump "Pump" {
  satisfies REQ-1 as s-1
}

system Field {
  part pump: Pump
}

A requirement may be written in EARS, about the parts of the model, and proved:

ears   "[while <state>,] [when|if <trigger>,] <part> shall <response> [within <time>]"
         <trigger>  = <part> receives <MESSAGE> | <part> enters <State> | <state>
         <response> = be in <State> [or …] | not be in <State> | send <MESSAGE>
formal "never brakes in Fault" | "always …" | "eventually … [within <time>]"
       | "<a> leads to <b> [within <time>]" | "<a> implies <b>"

archec checks the parts, states and messages an ears sentence names; the sentence is the requirement's text when it has none, and gives its formal property. archec verify proves the formal properties with NuSMV (untimed: a within is checked by the monitors, archec replay and archec verify --conflicts); archec gen --target ears-tests writes a test case per EARS requirement. archec verify --conflicts finds requirements no implementation can satisfy together (bounded: time in ticks); archec verify --meaning draws what each property says on a timeline.

Verification#

A test plan holds cases; a case is a timeline of moments (at 10ms do …, within 100ms expect …) or of steps. Cases that differ only in their values are written once, with a table:

component Box {
  var speed: float32 = 0
}

system Rig {
  part box: Box
}

test-plan TP "Speeds" {
  cases "Speed {v}" {
    at 0ms do box.speed = {v}
    at 1ms expect box.speed == {v}
    rows {
      id   | v
      TC-1 | 10
      TC-2 | 30
    }
  }
}

Safety#

A hazard is rated (severity, exposure, controllability) and its ASIL derived; failure modes and gates make its fault tree when it is written by hand. A part may instead say what errors it makes and what becomes of those that reach it — its error model — and archec derives the tree:

ErrorType = "omission" | "commission" | "value" | "early" | "late" .
Produces  = "produces" ErrorType { "," ErrorType } .              // on an output
Contains  = "contains" ( ErrorType | "all" ) { "," ErrorType } .  // on an input
Turns     = "turns" ErrorType { "," ErrorType } "into" ErrorType .  // on an input
From      = ( "from" | "from-all" ) identifier { "," identifier } . // on an output: the inputs behind it
TopEvent  = "error" ErrorType { "," ErrorType } "on" Path .        // on a hazard
message SPEED: float32
message CMD: float32

component Sensor {
  out speed: can sends SPEED {
    produces omission
  }
}

component Ctrl {
  in a: can receives SPEED {
    turns value into omission
  }
  in b: can receives SPEED
  out cmd: can sends CMD {
    from-all a, b
  }
}

component Brake {
  in cmd: can receives CMD
}

system Car {
  part s1: Sensor
  part s2: Sensor
  part ctrl: Ctrl
  part brakes: Brake
  s1.speed -> ctrl.a
  s2.speed -> ctrl.b
  ctrl.cmd -> brakes.cmd
}

failure-mode FM-S1 "Sensor 1 dead" {
  of Car.s1
  produces omission
  probability 1e-5
}

hazard HZ-01 "No braking on demand" {
  severity S3
  exposure E4
  controllability C3
  goal SG-01
  error omission on Car.brakes.cmd
}

safety-goal SG-01 "Brake on demand" {
  safe-state "Braking"
}

An error goes along the links; through a part, from each input to every output (or those whose from names it), unless the input contains it; turns changes its type. from-all needs the error on every input named (an AND). The basic events are the failure modes that produce an error at their element, with their probability, or the part's produces alone, with no rate. A hazard written both ways is checked: the two trees must have the same minimal cut sets.

An STPA takes the architecture for its control structure: a control-action goes from a controller part to the part it controls, over the links. It holds its unsafe control actions, one or more for each of the four types (not-provided, provided, timing, duration) or the type said not-applicable; each uca names the hazards it causes and the requirement (constraint) that prevents it, and holds its loss-scenarios.

Views#

A viewpoint that says what it includes is a diagram of its own: a query over a system, not a drawing. Its terms are read in order, each exclude removing what an include before it added; the blocks it picks, at any depth, are drawn with the links between them, laid out automatically (archec diagram, the editor).

Term     = "*" | Path [ ".*" | ".**" ] | ( "kind" | "tag" | "layer" ) identifier
         | Selector ( "->" | "<->" ) Selector .
Selector = "*" | Path [ ".*" | ".**" ] | ( "kind" | "tag" | "layer" ) identifier .
message GO: bool

component Sensor { out o: can sends GO }
component Ctl { in i: can receives GO; out o: can sends GO }
component Brake { in i: can receives GO }

system Car {
  part lidar: Sensor
  part adcu: Ctl
  part brakes: Brake
  lidar.o -> adcu.i
  adcu.o -> brakes.i
}

viewpoint braking "Braking" {
  of Car
  include * -> adcu, adcu -> *
  exclude lidar
}

* is the system's top parts; adcu.* the parts of adcu, adcu.** every block inside it. * -> adcu is adcu and the blocks that send to it, each taken at adcu's level (a link from cam.isp to adcu brings cam); depth 2 goes two links away. A link between blocks that are not drawn is drawn between the nearest ones around its ends. A term that matches nothing is a view-empty warning; the names a term gives are references, so a rename in the editor renames them too.

Where the blocks of a diagram sit is not part of the model: the editor keeps the places dragged in a view in main.layout.json, beside the main file, by diagram and by element ("view:braking": { "Car.adcu": {"at": [420, 200]} }), and a rename renames them. A block placed in the source (at, a canvas line) keeps that place; the others are laid out automatically.

User interface#

A ui block, in the component (or system) that owns a display, describes the product's user interface (the guide). Inside it, and only there, the words below open declarations; elsewhere they are names like any other.

Ui        = "ui" "{" { UiProp | Screen } "}" .
Screen    = ( "screen" | "dialog" | "overlay" ) identifier [ string ] "{" { Prop | Item } "}" .
Item      = Layout | Element .
Layout    = ( "row" | "column" | "grid" | "stack" ) [ identifier ] [ "{" { Prop | Item } "}" ] .
Element   = ElementWord [ identifier ] [ string ] [ "{" { Prop | Binding | Event } "}" ] .
Binding   = ( "value" | "enabled" | "visible" ) Expression .
Event     = "on" ( "press" | "release" | "long-press" | "change" | "enter" | "exit" ) ( Statements | "{" Statements "}" | CodeBlock )
          | "on" Expression .

ElementWord is one of spacer label gauge bar chart telltale image list table button toggle slider select input stepper custom. A binding's Expression and an event's Statements are the action language's (Actions), read to the end of the line (or the block): its names are the part's variables (speed), its state, the last message received on a port (bus.STATUS.speed, bus.FAULT for a message that is one value), the state and the variables of a part beside it (ctrl.state, ctrl.speed) and the constants. An event sends (send port MSG(args), the arguments in field order, or MSG { field: value }), moves between screens (goto Screen, back), sets the part's own variables, decides (if), logs and calls the part's functions. A text says values with ${expression}.

message STATUS { speed: float32 unit km/h range 0..200 }
message STOP { hard: bool }

component Ctrl {
  in cmd: data receives STOP
  out st: data sends STATUS
  states {
    state Running
    state Stopped
    Running -> Stopped on STOP
  }
}

component Panel {
  in bus: data receives STATUS
  out cmd: data sends STOP

  ui {
    display 800x480
    screen Main "Main" {
      gauge speed "Speed" { value bus.STATUS.speed }
      label state { text "Now: ${ctrl.state}" }
      button stop "Stop" { style danger; enabled ctrl.state == Running; on press send cmd STOP(true) }
    }
  }
}

system Machine {
  part ctrl: Ctrl
  part panel: Panel
  ctrl.st -> panel.bus
  panel.cmd -> ctrl.cmd
}

The first screen is where the ui starts (initial says another); an overlay is over every screen. What each element is bound to is typed against what it shows, with its unit and range; what a press sends must reach a part that receives it; every screen must be reachable and left; a safety-relevant message must be seen on every screen; the content must fit the display; contrast and labels follow WCAG AA (the ui-* codes). archec ui prints the resolved model, UiModel in src/ui.ts.

Layout#

There is one layout, and archec fmt writes it; nothing about it is a choice:

  • two spaces per level; a block's } on a line of its own;
  • one property or declaration per line — ; only inside a block written on one line;
  • properties in one order: what the element is (description, text), how it is classified (kind, tags, status…), its type, the rest, its traces (satisfies, verifies…), its place on the canvas (at, size);
  • three or more properties of a group written as the group;
  • the standard spelling of every keyword (an old one is a warning, and goes in 0.12).

archec vet reports what fmt cannot fix: names out of their case, a long Python block in a model file, a declaration out of its set.