Embedded

The sentil-embedded target builds the SENTIL engine no_std for a microcontroller. You hand it a fixed block of memory once, feed it one sample per loop, and read back the robustness. The surface is a small C ABI declared in Sentil.h with a sketch-friendly SentilMonitor C++ class over it, and every packaging ships a precompiled libsentil_embedded.a per core at version 0.3.0; Rust enters only when you rebuild an archive yourself.

Scope

A microcontroller cannot host statistical model checking or the GPU paths, so the no_std build leaves them out, along with the MILP synthesis backend. Everything else runs on the chip: the streaming STL monitor, the multi-formula monitor, the ring buffer, offline robustness over a captured trace, the formula bank, open-loop planning by gradient or CMA-ES, the receding-horizon controller, and the safety filter. A P~p formula is refused with SENTIL_EMBEDDED_UNSUPPORTED, since deciding one needs the statistical layer; Probabilistic formulas shows what that looks like.

Two hardware limits sit alongside. The engine needs a 32-bit ARM or RISC-V core with a heap, so an 8-bit AVR such as the classic Uno or Nano has no room for it. And the bundled allocator guard covers a single core: on a dual-core part such as the RP2040, keep every SENTIL call on one core, or rebuild the archive without the bundled critical-section and link a multicore one from your board HAL.

Install

Three registries carry the library: the Arduino Library Manager, the PlatformIO registry, and the ESP Component Registry. Reach for the one your toolchain already uses. Zephyr and bare metal have no registry, so those two install from a tarball on the releases page, which also carries a bundle for each of the other three and the raw per-core archives. Every route ships the same pieces, Sentil.h, the Sentil.cpp wrapper, and the precompiled archives, so a Rust toolchain matters only when you rebuild one.

Whichever route you take, the board's core decides which archive you need, and the same core name is the folder name inside every bundle.

The Cortex-M7 archive is the Cortex-M4 build, which runs on both. There is no prebuilt archive for the Xtensa ESP32 and ESP32-S3, whose Rust target comes from the Espressif fork rather than a stock one; both build from source.

From a package manager

arduino-cli lib install Sentil

[env:pico]
platform = https://github.com/maxgerhardt/platform-raspberrypi.git
board = pico
framework = arduino
board_build.core = earlephilhower
lib_deps = sentil/Sentil@^0.3.0
build_flags = -L${PROJECT_DIR}/.pio/libdeps/pico/Sentil/src/cortex-m0plus -lsentil_embedded

idf.py add-dependency "sedislab/sentil"

idf.py build

From a GitHub release

The embedded assets carry no version in their names, so https://github.com/sedislab/SENTIL/releases/latest/download/<asset> always fetches the current build of one.

arduino-cli lib install --zip-path sentil-arduino.zip

build_flags = -L${PROJECT_DIR}/lib/Sentil/src/cortex-m0plus -lsentil_embedded

idf.py build

CONFIG_SENTIL=y
CONFIG_CPP=y
CONFIG_REQUIRES_FULL_LIBC=y

west build -b nucleo_f401re my_app \
  -- -DZEPHYR_EXTRA_MODULES=$PWD/sentil-zephyr-module \
     -DSENTIL_ARCHIVE=$PWD/sentil-zephyr-module/lib/cortex-m4/libsentil_embedded.a

arm-none-eabi-g++ -mcpu=cortex-m4 main.cpp src/Sentil.cpp lib/cortex-m4/libsentil_embedded.a -I include -o firmware.elf

set(SENTIL_ARCHIVE ${CMAKE_SOURCE_DIR}/lib/cortex-m4/libsentil_embedded.a)
add_subdirectory(third_party/sentil/packaging/bare-metal sentil)
target_link_libraries(my_firmware PRIVATE sentil_embedded)

The release also attaches each archive on its own as sentil-archive-<mcu>.a, outside any bundle. Those suit a build that already has its own layout, since SENTIL_ARCHIVE and a compiler command line both take the archive by path; you still need Sentil.h and, for the C++ class, Sentil.cpp from one of the bundles or from a checkout.

From source

You build an archive yourself to bring up a core the release does not cover, or to pick up a change to the engine before it ships. This is the only route that needs Rust; the shared setup installs a toolchain.

git clone https://github.com/sedislab/SENTIL
cd SENTIL/sentil-embedded/rust

rustup target add thumbv7em-none-eabihf
cargo build --release --features mcu --target thumbv7em-none-eabihf

cargo build --release --no-default-features --features mcu --target thumbv6m-none-eabi

make -C sentil-embedded test

Your first monitor

Include Sentil.h, hand the engine a fixed region of memory once in setup(), then update the monitor each loop. This sketch replays the trace every SENTIL binding's first example uses: speed readings 12, 9, 7, 4, 6 against the property that speed stays above 5.

#include <Sentil.h>

static SentilMonitor monitor;
static uint8_t sentil_heap[4096];

static const double speed[] = {12, 9, 7, 4, 6};
static unsigned long step = 0;

void setup() {
  Serial.begin(115200);
  sentil_embedded_init(sentil_heap, sizeof(sentil_heap));
  monitor.begin("H (speed > 5)");
}

void loop() {
  if (step < 5) {
    double packed[1] = {speed[step]};
    sentil_embedded_robustness_t r;
    if (monitor.update((double)step, packed, 1, r) == SENTIL_EMBEDDED_OK) {
      Serial.print("speed=");
      Serial.print(packed[0]);
      Serial.print("  robustness=");
      Serial.print(r.value);
      Serial.println(r.satisfied ? "  (holds)" : "  (violated)");
    }
    step++;
  }
  delay(500);
}

Over serial at 115200 baud:

speed=12.00  robustness=7.00  (holds)
speed=9.00  robustness=4.00  (holds)
speed=7.00  robustness=2.00  (holds)
speed=4.00  robustness=-1.00  (violated)
speed=6.00  robustness=-1.00  (violated)

The predicate scores speed - 5 at each sample, and H, read historically, keeps the running infimum of those margins: 7, then 4, then 2, then -1 when the trace dips to 4, where it stays. The final -1.0 is the same robustness the offline G (speed > 5) gives this trace in every other binding. The sketch uses the past-time operator because a stream cannot see the future: H settles at every step, a bounded window such as G[0, 10] resolves once its window has passed, and an unbounded future G, read always, never resolves on a stream, reporting an unresolved negative-infinity value for as long as the stream lives, since a later dip can never be ruled out. What STL measures is the deeper story on reading robustness values; the O(1) window machinery underneath is the monotonic deque.

Offline traces

When a whole trace is already buffered there is no need to stream it: build a sentil_embedded_trace_t and evaluate a parsed formula over it in one call, in discrete or dense time, with the per-sample signal and the violation intervals available from the same pair of handles.

const double times[] = {0, 1, 2, 3, 4};
const double speed[] = {12, 9, 7, 4, 6};
sentil_embedded_trace_t *trace = NULL;
sentil_embedded_trace_create(times, 5, &trace);
sentil_embedded_trace_add_signal(trace, "speed", speed, 5);

sentil_embedded_formula_t *phi = NULL;
sentil_embedded_formula_create("G (speed > 5)", &phi);

double rho;
sentil_embedded_robustness(phi, trace, &rho);          /* -1.0 */

double starts[4], ends[4];
size_t count;
sentil_embedded_violation_intervals(phi, trace, starts, ends, 4, &count);
/* count = 1, the interval [0.0, 3.0] */

sentil_embedded_trace_destroy(trace);
sentil_embedded_formula_destroy(phi);

The violation interval runs from 0.0 to 3.0 because the per-sample robustness of G (speed > 5) is -1 at every start time whose window still contains the dip, and turns positive only at the last sample, where the remaining suffix is the single reading 6. sentil_embedded_robustness_signal hands you that whole signal, -1, -1, -1, -1, 1 here, and a formula bank evaluates many formulas over one trace in a single call.

Streaming

The shipped StreamingThreshold sketch is the shape of a real deployment: a bounded past window over a live analog reading, driving a pin.

#include <Sentil.h>

static SentilMonitor monitor;
static uint8_t sentil_heap[4096];
static unsigned long step = 0;

void setup() {
  pinMode(LED_BUILTIN, OUTPUT);
  sentil_embedded_init(sentil_heap, sizeof(sentil_heap));
  // analogRead returns 0..1023; alarm if the recent window approached the rail.
  monitor.begin("H[0, 8](level < 900)");
}

void loop() {
  double level = (double)analogRead(A0);
  double packed[1] = {level};
  sentil_embedded_robustness_t robustness;
  if (monitor.update((double)step, packed, 1, robustness) == SENTIL_EMBEDDED_OK) {
    digitalWrite(LED_BUILTIN, robustness.satisfied ? LOW : HIGH);
  }
  step++;
  delay(50);
}

The window makes one noisy spike insufficient to trip the alarm: H[0, 8] asks that the reading stayed below 900 over the last eight time units, so a stray sample pulls the margin down for eight steps and then ages out.

Three disciplines keep a stream healthy. Timestamps must strictly increase across update calls, which is why the sketches count steps rather than read a wall clock; millis() / 1000.0 hands the monitor the same value for every loop pass inside a second, and update refuses a time that does not move forward. Interval bounds share whatever unit your timestamps use, so with a step counter [0, 8] spans eight steps. And the packed values array is ordered by sorted variable name, not by appearance in the formula: for G (speed > 5 & brake < 1), brake takes slot 0 and speed slot 1. Ask sentil_embedded_symbol_index at runtime, or read the packed order the compile tool prints:

size_t idx;
bool found;
sentil_embedded_symbol_index(monitor, "speed", &idx, &found);  /* idx = 1, found = true */

To reuse a monitor on a fresh stream, sentil_embedded_reset clears its state without reparsing, and the multi-formula monitor folds one sample into a whole set of properties at once. The ring buffer smooths or thresholds a raw signal before the monitor sees it.

Probabilistic formulas

A P~p formula asks for a satisfaction probability, and estimating one takes the noise models and the statistical layer the no_std build leaves out. The board refuses rather than approximates:

sentil_embedded_monitor_t *m = NULL;
sentil_embedded_status_t status = sentil_embedded_create("P>=0.95 (G (speed > 5))", &m);
/* status = SENTIL_EMBEDDED_UNSUPPORTED:
   "the formula uses an operator the streaming monitor cannot run online" */

sentil_embedded_formula_is_probabilistic screens a formula before it ships, and the compile tool builds a specification's deterministic form, refusing any spec that resolves to a probabilistic formula with a message telling you to pick a deterministic variant. The deterministic robustness the board does compute is the same quantity the statistical layer samples on a bigger machine, so a common split runs the streaming monitor on the microcontroller and the probabilistic check on the Linux side of the system, over the CLI or any full binding.

Synthesis

The synthesis surface plans inputs against a spec, runs a controller online, and shields a nominal input, all on the chip. Build a linear model x_{t+1} = A x_t + B u_t, parse a spec, bound the inputs, and plan:

double a[1] = {1.0}, b[1] = {1.0}, x0[1] = {2.0};
const char *vars[1] = {"x"};
sentil_embedded_model_t *model = NULL;
sentil_embedded_linear_model_create(a, 1, b, 1, x0, vars, 1.0, 5, &model);

sentil_embedded_formula_t *spec = NULL;
sentil_embedded_formula_create("G (x > 0)", &spec);

double lo[5] = {-1, -1, -1, -1, -1}, hi[5] = {1, 1, 1, 1, 1};
sentil_embedded_bounds_t *bounds = NULL;
sentil_embedded_bounds_create(lo, hi, 5, &bounds);

double u[5], rho;
bool holds;
sentil_embedded_synthesize(model, spec, bounds, 0, 150, u, &rho, &holds);
/* rho = 2.0, holds = true */

The planned robustness is 2.0, a number you can check by hand: the state starts at 2.0, no admissible input drives the trajectory's worst margin above its starting point, and the planner finds inputs that never dip below it. out_input must hold sentil_embedded_model_input_dimension(model) doubles, the horizon times the input columns, 5 here. The backend argument is 0 for auto, 1 for gradient, 2 for CMA-ES; auto plans by gradient on a board, and the backends page covers when each wins.

The receding-horizon controller replans from the live state on every call, inside a step budget:

sentil_embedded_controller_t *controller = NULL;
sentil_embedded_controller_create(model, spec, 1, 150, bounds, &controller);
sentil_embedded_bounds_destroy(bounds);   /* bounds are borrowed, still yours */

double state[1] = {2.0}, input[1];
sentil_embedded_controller_control(controller, state, 1, input);

sentil_embedded_controller_create consumes the model and the spec, even when it fails, so free neither afterward; the bounds stay yours. max_iters is a gradient-step budget, not a clock, because a board has none, so pick it for the per-step time the chip can spare; each control call returns the best input its budget found. The Controller example sketch runs this loop on hardware. The safety filter shields a nominal input: given box bounds and optional linear barriers, it returns the closest admissible input, so a filter built on bounds of [-1, 1] clamps a nominal 2.5 to 1.0. Synthesis needs more heap than the bare monitor; the shipped example reserves 8 KB.

Errors

Bad input comes back as a status code, never a crash and never an exception, since Arduino builds compile with exceptions off. Every fallible call returns a sentil_embedded_status_t, zero is SENTIL_EMBEDDED_OK, and sentil_embedded_status_message turns any code into a short static string you never free:

sentil_embedded_monitor_t *m = NULL;
sentil_embedded_status_t status = sentil_embedded_create("G (speed >", &m);
if (status != SENTIL_EMBEDDED_OK) {
  Serial.println(sentil_embedded_status_message(status));  /* "could not parse the formula" */
}

The three codes a working sketch actually meets: SENTIL_EMBEDDED_PARSE for a malformed formula, SENTIL_EMBEDDED_PACKED_LENGTH when an update passes fewer values than the formula has variables, and SENTIL_EMBEDDED_UNKNOWN_VARIABLE when a multi-monitor update leaves out a variable some formula needs. The full table is below.

Reference

The signature column drops the sentil_embedded_ prefix from type names, so status_t stands for sentil_embedded_status_t and monitor_t for sentil_embedded_monitor_t; function names are spelled in full, exactly as Sentil.h declares them.

Handles and ownership

Ten opaque handle types, two plain structs, and the status enum. Every destroy accepts NULL as a no-op. Two creates consume an argument: sentil_embedded_controller_create takes ownership of its model and spec even on failure, and sentil_embedded_safety_filter_create takes ownership of its bounds. Everything else you free.

Lifecycle and the streaming monitor

One allocator call, then create, update, and destroy.

The robustness struct

Each update writes a sentil_embedded_robustness_t.

The SentilMonitor class

The C++ class owns the handle and frees it in its destructor, so a monitor in a global or static needs no cleanup. It is default-constructible, non-copyable, and exception-free; every call returns a status.

Formula introspection

A parsed formula backs the offline calls, the bank, and synthesis. Build one from text or a blob, inspect it, free it.

sentil_embedded_formula_variable is the two-call pattern: ask with a NULL buffer, allocate, ask again. For G (speed > 5 & brake < 1) the variable at index 0 is brake and needs 6 bytes.

Synthesis calls

Present in archives built with the synthesis feature, the default. Matrices are row-major throughout.

The last five are the dense numerics underneath the planner, callable directly from a control loop's own math.

Ring buffer

The ring buffer holds the newest capacity timed samples and keeps their statistics current in O(1) per push; use it to condition a raw reading before a monitor sees it. It allocates once at create and never grows. Pushing into a full buffer evicts the oldest sample. Every statistic returns NaN on an empty buffer.

Concretely: push samples at times 0 through 5 with values 10 through 15 into a buffer of capacity 4, and it holds the last four, mean 13.5, min 12, max 15. at_time(3.0) returns 13.0, at_time(3.5) returns NaN because no sample carries that timestamp, and closest_to_time(3.4) returns the sample at time 3.0.

Multi-formula monitor

One sample fans out to a whole set of streaming formulas, each keyed by an id. Its update takes parallel names and values arrays, a different convention from the single monitor's packed order, so one call can serve formulas over different variables.

sentil_embedded_multi_monitor_t *multi = NULL;
sentil_embedded_multi_create(&multi);
sentil_embedded_multi_add(multi, "speed-floor", "H (speed > 5)");
sentil_embedded_multi_add(multi, "temp-cap", "H (temp < 90)");

const char *names[] = {"speed", "temp"};
double values[] = {12.0, 71.5};
sentil_embedded_multi_update(multi, 0.0, names, values, 2);

sentil_embedded_robustness_t r;
sentil_embedded_multi_result(multi, 0, &r);  /* speed-floor: 7.0, holds */
sentil_embedded_multi_result(multi, 1, &r);  /* temp-cap: 18.5, holds */

Leaving temp out of that update returns SENTIL_EMBEDDED_UNKNOWN_VARIABLE, since a formula in the set needs it.

Offline robustness

The trace calls behind the worked example above.

Formula bank

The offline counterpart of the multi-monitor: one trace, many formulas, one evaluation call, results read back by index.

On the trace from the offline example, a bank holding G (speed > 5) and F (speed > 10) reports -1.0 and 2.0.

Status codes

Zero is success; the rest name their failure.

SENTIL_EMBEDDED_UNKNOWN_VARIABLE points in the direction people do not expect: not a stray name in the formula, but a required variable missing from a multi-monitor update. sentil_embedded_symbol_index also returns it for a name that is not valid UTF-8.

Cargo features

The Rust crate's features decide what an archive carries.

So default = ["parser", "synthesis"], a board build adds --features mcu, and the smallest build is --no-default-features --features mcu.

The Rust crate

The library is the sentil-embedded crate under sentil-embedded/rust, lib name sentil_embedded, built as a static archive for boards. Its C ABI is the surface documented above; a handful of Rust-only items are public for the host tool and for Rust firmware that links the crate directly.

Compiling a formula on a workstation

A board short on flash drops the parser and loads a formula compiled ahead of time. The sentil-compile-formula tool ships in the repository, not in the packagings, so clone github.com/sedislab/SENTIL and run it from sentil-embedded/rust:

cargo run --features std --bin sentil-compile-formula -- "G (speed > 5 & brake < 1)"

packed order (2 variables):
  [0] brake
  [1] speed
static const unsigned char SENTIL_FORMULA[] = {
    0x53, 0x45, 0x4e, 0x31, 0x05, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00,
    0x00, 0x00, 0x02, 0x00, 0x03, 0x05, 0x00, 0x00, 0x00, 0x73, 0x70, 0x65,
    0x65, 0x64, 0x02, 0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0x14, 0x40,
    0x00, 0x03, 0x05, 0x00, 0x00, 0x00, 0x62, 0x72, 0x61, 0x6b, 0x65, 0x00,
    0x02, 0x00, 0x00, 0x00, 0x00, 0x00, 0x00, 0xf0, 0x3f,
};
static const unsigned int SENTIL_FORMULA_LEN = 57;

Paste the array into the sketch and load it with beginCompiled(SENTIL_FORMULA, SENTIL_FORMULA_LEN) or sentil_embedded_create_compiled. The packed order lines go to stderr, one [index] name per variable, and they are the packed layout your updates must follow, the same sorted order sentil_embedded_symbol_index reports at runtime.

The spec flags need a build with the spec library on, --features "std specs". This reaches the whole specification library, so a board gets a vetted property while only the one formula ships in flash:

cargo run --features "std specs" --bin sentil-compile-formula -- --list-specs
cargo run --features "std specs" --bin sentil-compile-formula -- --spec controls/overshoot --variant step_down --param max_overshoot=0.2 -o overshoot.bin

A spec resolving to a probabilistic formula is refused, as above; pick a deterministic variant.

Related