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:
PascalCasefor what is defined (components, systems, types),snake_casefor what is inside (parts, ports, functions, variables),SCREAMING_CASEfor 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 idgives 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
atof the frame, or right after the field before. It takesbitsbits: 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):atis the field's least significant bit, bit k is bit k % 8 of its byte. Big-endian (big, Motorola):atis 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 ownbyte-order. - With
scaleoroffset, 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) orchecksum 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
sizebytes, 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
inby default. The operation writes anoutargument and reads and writes aninoutone: atport.op(…), what is passed there is a variable (or a field), not a value. - A
onewayoperation has no result and the caller does not wait for it: no-> T, nooutargument (oneway-result). raisesnamesexceptions: structs an operation may raise instead of its result (raises-not-exceptionfor another type).- An
attributeis a value the provider holds, which a client reads (and writes, unless it isreadonly). 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 mainstarts; 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'son-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-exitof each state it leaves, innermost first; its action; theon-enterof each state it enters, outermost first. It leaves and enters what is inside the innermost state around both its source and its target (for* ->andgoto, the source is the state the part is in): soUp -> UpleavesUp, 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
uint8at 255 plus 1 is 0, an integer divided by an integer is an integer, afloat32is 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.