Code generation

Generators of your own are in generators.md; every option of archec gen is in commands.md.

archec gen main.arche --target <t> [-o generated] writes source code from the model. Files you own (app.rs, main.rs, Cargo.toml) are written once and never overwritten; --check fails when a generated file is out of date (for CI). In VS Code: Arche: Generate code….

Monitors in the firmware (--monitors). archec gen --target c --monitors compiles the requirements into each binary of the deployment, the same checks archec replay makes on a log: an EARS requirement watches for its trigger (a message the part receives, a state it enters) and its response within its within (with none, right after the trigger is handled); a formal never/always/implies holds at every check; eventually C within 30ms holds by 30 ms after the binary starts, and A leads to B within 20ms each time A holds (or, for X receives M, M arrives) — the earliest answer awaited is the one that counts, so each takes one flag and one deadline: constant memory, constant time per check. With no within, eventually and leads to cannot fail at run time and are left out. A binary checks the requirements whose parts it runs. c/<binary>/monitors.h lists them; the wiring arms a monitor when the trigger arrives, before the part handles it, clears it when the part sends the message or reaches the state, and checks after each message and from a monitor thread. A violation calls arche_monitor_violation(req, at_ns), yours in monitor_hook.c (written once; it logs). No heap: one small struct per requirement. Define ARCHE_MONITOR_LOCK/UNLOCK as a critical section when the binary's threads preempt each other. With --trace as well, each verdict is also a trace record, arche-trace <ns> monitor <REQ> <1|0>: a failure always, a pass when a response arrives in time. --target embassy --monitors does the same in Rust: a Requirement enum, a Monitors struct behind a blocking mutex (a copy of each watched part's state, kept by its task), a monitor_task, and the MonitorHook trait, implemented by Hook in src/monitor_hook.rs (yours, written once).

One instant, deadlines and watchdogs. What happens at one instant happens in the order the specification gives — as in Lingua Franca, the model says it, not the machine: what is due first runs first, a part does one thing at a time, a message fires the innermost transition first, then the port's on-receive, then its handlers. The simulator (archec sim) and the C follow it. A port's or a transition's deadline with an on-deadline body runs that body instead, for a trigger the part starts on too late; a watchdog w { timeout 50ms; on-timeout … } runs out unless a body says kick w in time. Both are simulated and generated in C (arche_item_t.sent, <part>_kick, <part>_timeouts; the wiring's threads wait for the next timer) and in Rust: in the Embassy crate a channel into a part with a deadline carries (Instant, message), the task compares elapsed() with the deadline and calls on_deadline_<port> or on_deadline(t) instead; a part's watchdogs are a <Part>Watchdogs field (self.wd.kick(…)), and its task's select also waits on an embassy_time::Timer at the next one to run out, then calls on_timeout(w). With --trace, each is a line: arche-trace <ns> deadline <part>.<port or From->To> <µs late>, arche-trace <ns> watchdog <part>.<name> 0. archec difftest main.arche --seed 3 checks the C against the simulator: the same random inputs into both, the C built with a harness on a virtual clock, the two traces compared, the first difference shown.

Calls to another part. port.op(…) in the action language (an operation of an interface the port requires) is <part>_call_<port>_<op>(self, …) in C: the wiring gives it, calling the part at the other end of the link by which part asks; difftest checks it against the simulator. In Rust it is an Out method that sends a request to the provider's task (CALL_…, a channel) and awaits its reply (REPLY_…, a signal); in Go Call, in C++ a std::function member, both set by the binary's main (the specification).

Guards in UPPAAL and NuSMV. A variable of the component, such as var mode: Mode = MANUAL, is followed when two things hold. It must start at a value written in the model. Only the machine's transitions may change it, each time to a value written there too (/ self.mode = AUTO). It then becomes a small integer: the index of its value in the list of values it can take, which the export prints as a comment. A guard on it, such as [self.mode == MANUAL and not self.armed] or [self.tries < LIMIT], is translated exactly. Some variables are not followed, and the export notes each one:

• one no transition sets is an input;
• one other code also changes, such as a handler or a function;
• one a transition sets to a computed value.

The same goes for the rest of a guard: a message field, a call or an or. Those parts are dropped, so the checked model allows more than the real one, never less. A value that a test step or the physics writes into a followed variable is not seen.

Thread priorities are enforced with one executor per priority level, so a more urgent level preempts the ones below it (a slow handler on a low-priority thread cannot hold up the 1 ms loop):

• on a chip (hal stm32|nrf|rp|esp32), each level is an InterruptExecutor on a spare interrupt (stm32: UART4, UART5…; nrf: SWIn_EGUn; rp: SWI_IRQ_n; esp32: software interrupts 1–3, esp-hal's) at an interrupt priority in the same order, the most urgent level lowest-numbered, P0 left to the HAL. Change the interrupt in main.rs if your firmware uses it. More levels than the chip has priority bits (rp: 3): the least urgent ones share the last executor, and gen says so;
• on a host (hal std), each level is an executor on its own OS thread at that priority (thread-priority; on Linux, SCHED_FIFO needs CAP_SYS_NICE);
• tasks with no priority (bus tasks, threads without priority) run in thread mode, the lowest level; with none, the least urgent level takes thread mode. An isr with no priority is above every thread.

Within one level, and on a bare cortex-m skeleton, tasks are cooperative. archec check warns (handler-blocking) when a message handler on a periodic thread can hold its step past the deadline: it runs to its end first.

On a bus, an optional field is a presence byte then its value, a union a case byte then its largest case (the DBC multiplexes on it, or says in a comment when a signal counts). src/can.rs (yours once written) moves the frames between the bus channels and the hardware: Linux SocketCAN on a host (CAN FD when the bus is), bxCAN on CAN1 for hal stm32 (classic frames, up to 1 Mbit/s), the TWAI controller (TWAI0) for hal esp32 (classic frames, at the nearest of 125k/250k/500k/1M bit/s). Check the pins in main.rs. nRF chips, the RP2040 and the ESP32-C2 have no CAN controller, so the channels are left to your driver (an external one such as an MCP2515 on SPI). main.rs is yours once written: a crate generated before this does not start the levels; gen notes it.