C

The C ABI is the smallest surface SENTIL ships, basically a header file and a compiled library file. The C++, Java, Julia, MATLAB, and embedded bindings sit on it, and any language with a C FFI can too; the one exception is Python, which binds the Rust core directly through PyO3.

Install

On Debian, Ubuntu, Fedora, and RHEL the distro package is the easiest way to install one: it drops the shared and static libraries, sentil.h, and sentil.pc under /usr. vcpkg and Conan carry the same prebuilt library on Linux, macOS, and Windows alike, and add a CMake package on top of it, so reach for one of those if your project already uses either. The release archive is a plain prefix you unpack wherever you like, for a project that uses neither. Build from source for an unreleased change or a platform the prebuilt bundles skip. Linux on arm64 is the one to know about: the library and header for a Raspberry Pi ride along in the ARM archives described on the CLI page, built with --no-default-features, so the 19 GPU symbols the reference marks as gated are absent from that library.

From apt or dnf

sudo apt install ./libsentil-dev_0.3.0_amd64.deb      # Debian, Ubuntu
sudo dnf install ./libsentil-devel-0.3.0.x86_64.rpm   # Fedora, RHEL

pkg-config --modversion sentil                                     # Debian, Ubuntu
PKG_CONFIG_PATH=/usr/lib/pkgconfig pkg-config --modversion sentil  # Fedora, RHEL

0.3.0

On Arch, the sentil package in the AUR carries the same four files, plus /usr/lib/cmake/Sentil/SentilConfig.cmake and the CLI. The CLI page has the two ways to install it.

From vcpkg or Conan

vcpkg install sentil

conan install --requires=sentil/0.3.0

find_package(Sentil CONFIG REQUIRED)
target_link_libraries(my_app PRIVATE Sentil::sentil)

export PKG_CONFIG_PATH=/path/to/vcpkg/installed/x64-linux/lib/pkgconfig:$PKG_CONFIG_PATH
cc my_app.c $(pkg-config --cflags --libs sentil) -o my_app

#include <sentil.h>
#include <stdio.h>

int main(void) {
    uint32_t major, minor, patch;
    sentil_version(&major, &minor, &patch);
    printf("%u.%u.%u\n", major, minor, patch);
    return 0;
}

cmake --build build
./build/my_app   # 0.3.0

From a GitHub release

The archive is a prefix rather than an installer. Inside are include/sentil.h, the shared library and the static libsentil.a under lib/, lib/pkgconfig/sentil.pc, and lib/cmake/Sentil/SentilConfig.cmake.

tar -xzf sentil-0.3.0-linux-x86_64.tar.gz
prefix=$PWD/sentil-0.3.0-linux-x86_64

tar -xzf sentil-0.3.0-macos-arm64.tar.gz
prefix=$PWD/sentil-0.3.0-macos-arm64

tar -xzf sentil-0.3.0-windows-x86_64.tar.gz
$prefix = "$PWD\sentil-0.3.0-windows-x86_64"

cmake -S . -B build -DCMAKE_PREFIX_PATH="$prefix"

export PKG_CONFIG_PATH=$prefix/lib/pkgconfig:$PKG_CONFIG_PATH
cc my_app.c $(pkg-config --define-variable=prefix=$prefix --cflags --libs sentil) \
    -Wl,-rpath,$prefix/lib -o my_app

pkg-config --define-variable=prefix=$prefix --modversion sentil

0.3.0

From source

You need a Rust toolchain from rustup.rs, a C compiler, and make. The shared from-source page covers the toolchain; what differs per system is the compiler.

xcode-select --install

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

make

make test-ffi   # the last line reads "all C tests passed"

cc -Iinclude my_app.c -L../target/release -lsentil -Wl,-rpath,"$PWD/../target/release" -lm -o my_app

make install PREFIX=$HOME/.local

PKG_CONFIG_PATH=$HOME/.local/lib/pkgconfig pkg-config --modversion sentil

0.3.0

make dist packs the build into target/dist/sentil-0.3.0-<os>-<arch>.tar.gz if you want to move it to another machine. The layout matches the release archive, with a SentilConfigVersion.cmake the release archive leaves out, so a versioned find_package resolves against this one.

However the library arrives, the header is sentil.h, the link flag is -lsentil, and the CMake target is Sentil::sentil. SENTIL_LIB_DIR belongs to the C++ and Java builds, which take it as a CMake cache variable naming a directory that holds libsentil; a C project has no use for it. The archive and the distro packages carry the C ABI only, so the C++ wrapper header comes from the C++ binding.

First monitor

Five samples of a speed signal, one rule, and a result you can check by eye. The rule needs speed above 5 and the trace dips to 4 at t=3, so the margin is 4 - 5 = -1 and the robustness is -1.0 exactly.

#include <stdio.h>
#include <sentil.h>

int main(void) {
    const double times[] = {0, 1, 2, 3, 4};
    const double speed[] = {12, 9, 7, 4, 6};
    sentil_trace_t *trace = sentil_trace_from_signal(times, 5, "speed", speed, 5);
    sentil_formula_t *phi = sentil_formula_parse("G (speed > 5)");
    double rho;
    if (!trace || !phi || sentil_formula_robustness(phi, trace, &rho) != SENTIL_OK) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }
    printf("%f\n", rho);
    sentil_formula_destroy(phi);
    sentil_trace_destroy(trace);
    return 0;
}

cc check.c $(pkg-config --cflags --libs sentil) -o check
./check

-1.000000

What robustness measures builds the intuition behind the number. Every C-ABI habit is already in these few lines. A constructor returns a handle or NULL. A computing call writes through an out-pointer and returns a sentil_error_t, SENTIL_OK on success. Each handle goes back through its own _destroy, and the failure branch reads the thread-local message covered under errors. sentil_formula_robustness_dense scores the same pair in dense time, catching threshold crossings between samples; on this trace it also returns -1.0.

Traces

A trace holds named signals on a shared time grid, times strictly increasing. Build one incrementally with sentil_trace_create plus sentil_trace_add_signal, in one call with sentil_trace_from_signal, or with integer times 0 through n-1 via sentil_trace_indexed. For recorded data, sentil_trace_from_csv and sentil_trace_from_tsv parse text with a header row and an auto-detected time column, and sentil_trace_from_path dispatches on file extension, reading csv, tsv, parquet, arrow, sqlite, mat, and more; the trace formats page lists them.

#include <sentil.h>
#include <stdio.h>

int main(void) {
    sentil_trace_t *trace = sentil_trace_from_csv("time,speed\n0,12\n1,9\n2,7\n3,4\n4,6");
    if (trace == NULL) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }
    printf("%zu samples\n", sentil_trace_len(trace));

    size_t n = 0;
    const double *speed = sentil_trace_signal(trace, "speed", &n);
    printf("speed[3] = %g\n", speed[3]);

    const double fine_times[] = {0.0, 0.5, 1.0, 1.5, 2.0};
    sentil_trace_t *fine = sentil_trace_resample(trace, fine_times, 5, SENTIL_INTERP_LINEAR);
    const double *fs = sentil_trace_signal(fine, "speed", &n);
    printf("speed at t=0.5: %g\n", fs[1]);

    sentil_trace_destroy(fine);
    sentil_trace_destroy(trace);
    return 0;
}

5 samples
speed[3] = 4
speed at t=0.5: 10.5

sentil_trace_times and sentil_trace_signal return borrowed pointers, valid until the trace changes or is freed; copy anything you need to keep. When one trace resamples onto many grids, sentil_trace_prepare fixes the interpolation coefficients once and each sentil_prepared_trace_resample reuses them.

Streaming

sentil_monitor_parse builds a streaming monitor, and each sentil_monitor_update feeds it one timestamped sample. Every update fills a sentil_robustness_t whose fields are resolved, satisfied, value, lower, and upper; while the temporal window is still open, resolved stays false and value splits the difference between the bounds.

#include <sentil.h>
#include <math.h>
#include <stdio.h>

int main(void) {
    sentil_monitor_t *monitor = sentil_monitor_parse("G[0, 10] (x > -0.9)", NULL);
    if (monitor == NULL) {
        fprintf(stderr, "parse error: %s\n", sentil_get_last_error());
        return 1;
    }

    const char *names[] = {"x"};
    for (int t = 0; t < 60; ++t) {
        double x = sin(t * 0.3);
        sentil_robustness_t out;
        if (sentil_monitor_update(monitor, (double)t, names, &x, 1, &out) != SENTIL_OK) {
            fprintf(stderr, "update error: %s\n", sentil_get_last_error());
            sentil_monitor_destroy(monitor);
            return 1;
        }
        if (out.resolved && !out.satisfied) {
            printf("violated at t=%d, robustness=%.3f\n", t, out.value);
            sentil_monitor_destroy(monitor);
            return 0;
        }
    }

    printf("held over the whole stream\n");
    sentil_monitor_destroy(monitor);
    return 0;
}

cc stream.c $(pkg-config --cflags --libs sentil) -lm -o stream
./stream

violated at t=15, robustness=-0.078

The per-sample cost is flat regardless of trace length, which is the monotonic deque at work. A named update compares strings to find each slot; resolve every variable once with sentil_monitor_symbol_index, and sentil_monitor_update_packed then takes values in index order with no strcmp in the loop. sentil_monitor_reset clears streaming state for a fresh trace. Passing NULL for the config gives discrete time; build a sentil_monitor_config_t with sentil_monitor_config_create and sentil_monitor_config_set_time to evaluate in dense time. To run many formulas over one stream, sentil_multi_monitor_create holds them under string ids and sentil_multi_monitor_update advances all of them per sample.

Live probability

The statistical layer streams too: sentil_stream_monitor_with_lifting tracks a P~p formula over a particle ensemble drawn through a lifting registry, and sentil_stream_monitor_last_probability reads the running satisfaction estimate after any update. The registry and config are explained under probabilistic checking below.

#include <sentil.h>
#include <math.h>
#include <stdio.h>

int main(void) {
    sentil_formula_t *phi = sentil_formula_parse("P>=0.9 (G[0, 10] (x > -0.9))");
    sentil_lifting_registry_t *lifting = sentil_lifting_registry_create();
    sentil_lifting_registry_register(lifting, "x", sentil_noise_gaussian(0.0, 0.05),
                                     SENTIL_NOISE_ADDITIVE);
    sentil_smc_config_t config = sentil_smc_config_default();
    config.samples = 500;

    sentil_stream_monitor_t *monitor = sentil_stream_monitor_with_lifting(phi, lifting, &config);
    if (monitor == NULL) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }

    const char *names[] = {"x"};
    for (int t = 0; t < 17; ++t) {
        double x = sin(t * 0.3);
        sentil_robustness_t out;
        sentil_stream_monitor_update(monitor, (double)t, names, &x, 1, &out);
        if (t >= 12) {
            printf("t=%d  P=%.3f  satisfied=%s\n", t,
                   sentil_stream_monitor_last_probability(monitor),
                   out.satisfied ? "true" : "false");
        }
    }

    sentil_stream_monitor_destroy(monitor);
    sentil_lifting_registry_destroy(lifting);
    sentil_formula_destroy(phi);
    return 0;
}

t=12  P=1.000  satisfied=true
t=13  P=1.000  satisfied=true
t=14  P=0.748  satisfied=false
t=15  P=0.048  satisfied=false
t=16  P=0.000  satisfied=false

The estimate follows the trailing window. The signal dips below -0.9 near t=15; as the dip enters the [0, 10] window the estimate collapses from 1.000 through 0.748 to 0.048 in three samples, and the verdict flips the moment it crosses the 0.9 threshold. The accessor returns NaN for a deterministic formula. For a P~p formula it reports the settled share, the fraction of particles whose own window has already closed satisfied, which is why it reads 0 for the first ten samples here and jumps to 1.000 at t=10 when the [0, 10] window first fills. Over those first ten samples the verdict beside it comes back with resolved false and value NaN rather than a pass the monitor has not earned, so gate on out.resolved before you read out.satisfied. The same accessor exists as sentil_monitor_last_probability, and per id as sentil_multi_monitor_probability after sentil_multi_monitor_add_probabilistic.

Probabilistic checking

Attach a noise model to each noisy signal in a sentil_lifting_registry_t, then call sentil_formula_check; the P~p operator itself has its own page, what PrSTL is. Seventeen noise families ship, from sentil_noise_gaussian to sentil_noise_mixture, and the fitters sentil_noise_fit_gaussian, sentil_noise_fit_bootstrap, and sentil_noise_fit_gaussian_mixture learn a model from calibration residuals instead of parameters you guess.

#include <sentil.h>
#include <stdio.h>

int main(void) {
    double times[20], values[20];
    for (int i = 0; i < 20; ++i) {
        times[i] = i;
        values[i] = 0.4 + 0.05 * i;
    }
    sentil_trace_t *trace = sentil_trace_from_signal(times, 20, "x", values, 20);

    sentil_lifting_registry_t *lifting = sentil_lifting_registry_create();
    sentil_lifting_registry_register(lifting, "x", sentil_noise_gaussian(0.0, 0.3),
                                     SENTIL_NOISE_ADDITIVE);

    sentil_formula_t *phi = sentil_formula_parse("P>=0.9 (G (x > 0))");
    sentil_smc_config_t config = sentil_smc_config_default();
    config.samples = 5000;

    sentil_smc_result_t result;
    if (sentil_formula_check(phi, trace, lifting, &config, &result) != SENTIL_OK) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }
    printf("probability %.3f, interval [%.3f, %.3f], holds %s\n", result.probability,
           result.interval.lower, result.interval.upper, result.holds ? "true" : "false");

    sentil_formula_destroy(phi);
    sentil_lifting_registry_destroy(lifting);
    sentil_trace_destroy(trace);
    return 0;
}

probability 0.733, interval [0.721, 0.745], holds false

sentil_smc_config_default() gives 10000 samples, 0.95 confidence, seed 42, and the Wilson interval; set the fields you want to change, as the example does with samples. sentil_formula_check_conservative runs the same estimate but always reports the exact Clopper-Pearson interval, and sentil_formula_check_distribution additionally fills a sentil_robustness_distribution_t with the mean, spread, and range of robustness across the ensemble. How the interval turns into the holds verdict is on the confidence intervals page.

Sequential and Bayesian tests

A fixed sample budget spends 5000 simulations whether the answer is obvious or marginal. The sequential tests stop as soon as the evidence is clear, at a bounded error rate.

sentil_sprt_config_t sprt = {0.85, 0.95, 0.05, 0.05, 100000, 42};
sentil_sprt_result_t sr;
if (sentil_formula_check_sequential(phi, trace, lifting, &sprt, &sr) == SENTIL_OK) {
    printf("sprt: %s after %llu samples\n",
           sr.verdict == SENTIL_SPRT_ACCEPT_H1 ? "accept H1" : "accept H0",
           (unsigned long long)sr.samples);
}

sentil_bayes_config_t bayes = {0.9, 100.0, 100000, 42};
sentil_bayes_result_t br;
if (sentil_formula_check_bayesian(phi, trace, lifting, &bayes, &br) == SENTIL_OK) {
    printf("bayes: %s after %llu samples, posterior %.4f\n",
           br.verdict == SENTIL_BAYES_HOLDS ? "holds" : "fails",
           (unsigned long long)br.samples, br.posterior);
}

On the trace and lifting from the example above, both tests reach the answer the 5000-sample estimate gave, in a fraction of the work:

sprt: accept H0 after 32 samples
bayes: fails after 60 samples, posterior 0.0008

The SPRT config is {p0, p1, alpha, beta, max_samples, seed} and requires 0 < p0 < p1 < 1, both error rates in (0, 1), and a positive sample cap; accepting H0 means the satisfaction probability sits at or below p0. The Bayes config is {threshold, bayes_factor, max_samples, seed} with threshold in (0, 1) and bayes_factor > 1, and its result carries the posterior probability that the threshold claim is true. Both tests also run over your own Bernoulli source through sentil_sequential_test and sentil_bayes_sequential_test, no trace involved.

Rare events

10000 samples of a 2.7e-7 event almost never contain even one hit, so at that scale a plain Monte Carlo estimate is zero. sentil_formula_check_rare_event estimates such probabilities by adaptive multilevel splitting over a sentil_stochastic_system_t you define with callbacks. Two rules keep the callbacks correct: derive all randomness from the seed argument, because the callbacks run on several threads at once, and give the inner formula a safety shape like G, read always, since the estimator hunts the rare violation.

#include <sentil.h>
#include <stdio.h>

/* splitmix64: one uniform draw in [0, 1) from a seed */
static double uniform(uint64_t seed) {
    uint64_t z = seed + 0x9e3779b97f4a7c15ull;
    z = (z ^ (z >> 30)) * 0xbf58476d1ce4e5b9ull;
    z = (z ^ (z >> 27)) * 0x94d049bb133111ebull;
    z = z ^ (z >> 31);
    return (double)(z >> 11) / 9007199254740992.0;
}

static void init(void *userdata, uint64_t seed, double *out_state, size_t n) {
    (void)userdata; (void)seed;
    for (size_t i = 0; i < n; ++i) out_state[i] = 0.0;
}

static void step(void *userdata, const double *prev, size_t n, double time, uint64_t seed,
                 double *out_state) {
    (void)userdata; (void)time;
    for (size_t i = 0; i < n; ++i) out_state[i] = prev[i] + 0.2 * (uniform(seed) - 0.5);
}

int main(void) {
    const char *vars[] = {"x"};
    sentil_system_callbacks_t callbacks = {NULL, init, step};
    sentil_stochastic_system_t *system = sentil_stochastic_system_create(vars, 1, 1.0, 50, callbacks);

    sentil_formula_t *phi = sentil_formula_parse("P>=0.999 (G (x < 2))");
    sentil_rare_event_config_t config = sentil_rare_event_config_default();

    sentil_rare_event_result_t result;
    if (sentil_formula_check_rare_event(phi, system, &config, &result) != SENTIL_OK) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }
    printf("violation probability %.2e, holds %s, %llu simulations\n", result.violation_probability,
           result.holds ? "true" : "false", (unsigned long long)result.simulations);

    sentil_formula_destroy(phi);
    sentil_stochastic_system_destroy(system);
    return 0;
}

violation probability 2.68e-07, holds true, 726298 simulations

The random walk takes uniform steps of at most 0.1 per sample, so reaching 2 within 50 steps is a genuine tail event, resolved here in 726298 simulations. The defaults are 4096 particles, margin 0, seed 42; widen particles to tighten the estimate. With a GPU present, sentil_formula_check_rare_event_gpu runs fixed-effort splitting on the device over a declarative sentil_sim_model_t. The method is on the rare events page.

Synthesis

One call covers open-loop synthesis: hand sentil_synthesize a model, bounds, and a spec, and it fills a result with the best input sequence it found. When the spec cannot be met the result holds the least violating input rather than nothing.

#include <sentil.h>
#include <stdio.h>

int main(void) {
    const double a[] = {1.0};
    const double b[] = {1.0};
    const double x0[] = {1.0};
    const char *vars[] = {"x"};
    sentil_system_model_t *model = sentil_linear_model_create(a, 1, b, 1, x0, vars, 1, 1.0, 3);

    sentil_formula_t *spec = sentil_formula_parse("G (x > 0)");
    const double lower[] = {-1.0, -1.0, -1.0};
    const double upper[] = {1.0, 1.0, 1.0};
    sentil_bounds_t *bounds = sentil_bounds_create(lower, upper, 3);

    sentil_synthesis_result_t result;
    if (sentil_synthesize(model, spec, bounds, NULL, 0, SENTIL_BACKEND_AUTO, 0, &result) != SENTIL_OK) {
        fprintf(stderr, "%s\n", sentil_get_last_error());
        return 1;
    }
    printf("robustness %.3f, holds %s, inputs", result.robustness, result.holds ? "true" : "false");
    for (size_t i = 0; i < result.input_len; ++i) printf(" %.3f", result.input[i]);
    printf("\n");

    sentil_free_doubles(result.input, result.input_len);
    sentil_bounds_destroy(bounds);
    sentil_formula_destroy(spec);
    sentil_system_model_destroy(model);
    return 0;
}

robustness 1.000, holds true, inputs 1.000 -1.000 0.000

SENTIL_BACKEND_AUTO picks by problem structure; SENTIL_BACKEND_GRADIENT, SENTIL_BACKEND_CMA_ES, and SENTIL_BACKEND_MILP force one, and the backends page says when each wins. The receding-horizon controller, the safety filter, chance constraints, falsification, and parameter mining each have a reference section below.

Errors

Nothing in the library aborts the process. Every failure comes back as a sentil_error_t code or a NULL handle, with a message describing what went wrong left on a per-thread slot. sentil_get_last_error_code() reads the code and sentil_get_last_error() the message; the pointer is borrowed and valid only until the next sentil_* call on the same thread, and passing it to sentil_free_string is an error. To keep a message past the next call, size a copy with a null buffer, then fill it:

#include <sentil.h>
#include <stdio.h>
#include <stdlib.h>

int main(void) {
    sentil_formula_t *phi = sentil_formula_parse("G (speed >");
    if (phi == NULL) {
        printf("code %d: %s\n", (int)sentil_get_last_error_code(), sentil_get_last_error());

        size_t needed = sentil_get_last_error_message(NULL, 0);
        char *copy = malloc(needed);
        sentil_get_last_error_message(copy, needed);
        printf("kept: %s\n", copy);
        free(copy);
    }
    return 0;
}

code 3: parse error at line 1, column 11: expected a value or `(`, found end of input
kept: parse error at line 1, column 11: expected a value or `(`, found end of input

The full sentil_error_t enumeration, all 18 constants:

A failure that would panic in the core is caught at the boundary and surfaces as SENTIL_ERR_PANIC, never as an abort. The mapping from each code to the Rust error variant behind it is on the error codes page.

Reference

All 267 exported functions follow, with signatures verbatim from sentil.h. The header carries the same one-line descriptions inline, so it doubles as offline documentation. Exactly 19 symbols depend on a build feature: the 17 sentil_sim_* functions, sentil_gpu_is_available, and sentil_formula_check_rare_event_gpu exist only when sentil-ffi is built with the gpu feature, which is on by default; a --no-default-features build for an embedded target omits them, and no synthesis symbol is gated.

Version and errors

The version is available at compile time as the macros SENTIL_VERSION_MAJOR, SENTIL_VERSION_MINOR, and SENTIL_VERSION_PATCH, currently 0, 3, 0.

Ownership and freeing

Every handle a constructor returns is yours to free with its _destroy, and NULL is a no-op for every _destroy and sentil_free_* call. The 21 opaque handle types:

Some builders consume the handles you pass them, whether the call succeeds or returns NULL, so never free those afterward. The consuming calls: the sentil_expr_* combinators and sentil_sim_expr_* combinators consume their operands, the sentil_formula_* builders consume their children, sentil_noise_mixture consumes its component models, sentil_lifting_registry_register consumes the model, sentil_monitor_create consumes the formula, sentil_sim_model_create consumes its init, advance, and noise handles, sentil_controller_create consumes the model and spec, sentil_safety_filter_create consumes the bounds, sentil_chance_constraint_create consumes the spec, and sentil_spec_builder_with_variant, sentil_spec_builder_with_param, and sentil_spec_builder_into_monitor consume the builder.

Arrays and strings the library returns are freed by a matching free function:

Formula parsing and inspection

Parse once, evaluate many times; a formula handle is immutable.

Formula builders

Build a formula programmatically instead of parsing a string, from expressions upward. Every builder consumes the handles passed to it, which is the mistake to watch for: after wrapping a formula in sentil_formula_always, the inner handle is gone and freeing it is a double free.

sentil_formula_t *pred = sentil_formula_predicate(
    sentil_expr_variable("speed"), SENTIL_CMP_GT, sentil_expr_literal(5.0));
sentil_formula_t *phi = sentil_formula_always(0.0, 0.0, false, pred);
/* pred is consumed; free only phi */

This builds G (speed > 5) and scores -1.0 on the first-monitor trace, matching the parsed form exactly.

The three builder enums, with every constant:

Offline evaluation

Robustness straight off a formula and a trace, no monitor needed. The dense forms catch threshold crossings between samples; the plain forms read the grid.

sentil_interval_t is { double start; double end }.

Formula banks

A bank evaluates many formulas over one trace in a single call, for batch offline checking.

sentil_bank_result_t is { char *id; bool ok; double value; sentil_error_t code }; when one formula errors, its ok is false with value NaN and code set, and the rest still evaluate.

Trace handling

sentil_interpolation_t: SENTIL_INTERP_LINEAR 0, SENTIL_INTERP_HOLD 1, SENTIL_INTERP_CUBIC 2.

Ring buffers

A fixed-capacity buffer of timestamped values with running statistics.

sentil_sample_t is { bool found; double time; double value }; found is false when a query had no answer, for instance popping an empty buffer.

Monitors

The full-featured monitor: streaming updates, offline evaluation honoring a time mode, and the probabilistic checks in one handle.

sentil_time_mode_t: SENTIL_TIME_DISCRETE 0, SENTIL_TIME_DENSE 1. sentil_robustness_t is { bool resolved; bool satisfied; double value; double lower; double upper }.

Streaming monitors

A leaner monitor for pure streaming, plus the probabilistic ensemble form.

Multi-formula monitors

One update call advances every formula, deterministic and probabilistic mixed.

sentil_named_robustness_t is { char *id; sentil_robustness_t robustness }; the id is owned by the result array.

Noise models

Seventeen family constructors, each returning an owned model or NULL when a parameter is invalid, plus fitters that learn a model from calibration data.

sentil_noise_interaction_t: SENTIL_NOISE_ADDITIVE 0 for residuals y - g, SENTIL_NOISE_MULTIPLICATIVE 1 for y / g.

Lifting registries

The registry maps signal names to noise models; lifting draws one noisy realization of a trace.

Statistical model checking

Fixed-budget estimation of a P~p formula over the lifted ensemble. Each call needs a formula with a top-level probabilistic operator, or it returns SENTIL_ERR_NOT_PROBABILISTIC.

The structs:

Confidence intervals and sample sizing

Free-standing binomial statistics, usable with or without a formula. Fifty successes in a hundred trials at level 0.95 gives a Wilson interval of [0.4038, 0.5962], and sentil_z_score(0.95) is 1.959964. Watch the naming: sentil_clopper_pearson and sentil_agresti_coull carry no _interval suffix.

sentil_interval_method_t: SENTIL_WILSON 0, SENTIL_CLOPPER_PEARSON 1, SENTIL_JEFFREYS 2, SENTIL_AGRESTI_COULL 3. sentil_confidence_interval_t is { double lower; double upper; double level }.

Sequential tests

SPRT and Bayesian testing over a formula, or over any Bernoulli source you supply through a callback.

The callback is typedef bool (*sentil_bernoulli_fn)(void *userdata);, returning the next sample. The structs and verdicts:

sentil_sprt_verdict_t: SENTIL_SPRT_ACCEPT_H0 0, SENTIL_SPRT_ACCEPT_H1 1, SENTIL_SPRT_INCONCLUSIVE 2. sentil_bayes_verdict_t: SENTIL_BAYES_HOLDS 0, SENTIL_BAYES_FAILS 1, SENTIL_BAYES_INCONCLUSIVE 2.

Rare-event estimation

Adaptive multilevel splitting on the CPU, over a formula and system or over a raw simulator you define.

Stochastic systems

A trajectory generator defined by callbacks, feeding the rare-event path and chance-constraint validation.

sentil_system_callbacks_t is { void *userdata; void (*init)(void *userdata, uint64_t seed, double *out_state, size_t n); void (*step)(void *userdata, const double *prev, size_t n, double time, uint64_t seed, double *out_state) }; the callbacks may run on several threads at once, so derive randomness from the seed argument.

Simulation models

A declarative model built from expressions instead of callbacks, which is what lets the GPU path transpile it. These 17 functions exist only in a gpu-feature build, which is the default.

GPU entry points

Both exist only in a gpu-feature build. Without a device they return a typed error rather than silently falling back; the CPU rare-event check stays available.

sentil_gpu_splitting_estimate_t is { double violation_probability; size_t particles; uint32_t levels }.

Smooth robustness

The differentiable surrogate synthesis climbs: soft min and max with a temperature, and gradients with respect to signals or inputs.

sentil_smooth_config_t is { double temperature; sentil_soft_kind_t kind }; the temperature must be finite and positive, and the arithmetic-geometric-mean kind ignores it. sentil_soft_kind_t: SENTIL_SOFT_LOG_SUM_EXP 0, SENTIL_SOFT_ARITHMETIC_GEOMETRIC_MEAN 1.

Bounds

Box constraints per input coordinate, shared by every optimizer and the safety filter.

System models

The plant a synthesizer or controller drives: linear time-invariant, or custom through a rollout callback.

sentil_model_vtable_t is { void *userdata; size_t input_dimension; const double *initial_state; void (*rollout)(void *userdata, const double *initial, size_t n_state, const double *input, size_t n_input, double *out_signals) }; rollout fills one row of horizon + 1 samples per variable and may run on several threads.

Open-loop synthesis

sentil_backend_t: SENTIL_BACKEND_AUTO 0, SENTIL_BACKEND_GRADIENT 1, SENTIL_BACKEND_CMA_ES 2, SENTIL_BACKEND_MILP 3. sentil_synthesis_result_t is { double *input; size_t input_len; double robustness; bool holds; sentil_backend_t backend }; the input array is yours, freed with sentil_free_doubles.

Optimizers

The optimizers behind synthesis, exposed for your own objectives.

The callback typedefs: typedef void (*sentil_gradient_fn)(void *userdata, const double *x, size_t n, double *out_value, double *out_gradient); fills the value and gradient at a point, typedef double (*sentil_objective_fn)(void *userdata, const double *x, size_t n); scores one point, and typedef void (*sentil_batch_objective_fn)(void *userdata, const double *points, size_t population, size_t dim, double *out_scores); scores population row-major points at once. sentil_cma_config_t is { size_t population; size_t max_generations; double initial_step; double tol_step; uint64_t seed }.

Numerics

Small dense solvers used by the convex synthesis path. Matrices are row-major and output buffers are caller-allocated.

Controllers

The receding-horizon controller: plan a short horizon each step, return the best input found within a hard wall-clock budget.

Safety filters

A control-barrier shield: pass a nominal input through, minimally corrected to satisfy the barriers and bounds.

Chance constraints

A probabilistic requirement carried as an object: the spec must hold with at least the given probability, validated by sampling as the system runs.

sentil_chance_report_t is { double estimate; double lower_bound; uint64_t samples; bool holds }.

Witnesses and falsification

Search for an input that breaks the spec instead of one that satisfies it, generating counterexamples and test cases.

sentil_witness_t is { double *input; size_t input_len; double robustness; sentil_trace_t *trace }; free the input with sentil_free_doubles and the trace with sentil_trace_destroy. Negative robustness means a genuine counterexample.

Parameter mining

The callback is typedef sentil_formula_t *(*sentil_formula_fn)(void *userdata, double param);, returning an owned formula per parameter value.

Specification library

Premade, standards-derived specifications by name, with variants, parameter overrides, and the verification settings each spec recommends.

The settings structs: sentil_spec_smc_settings_t is { double confidence; uint64_t sample_budget }, sentil_spec_sprt_settings_t is { double p0; double p1; double alpha; double beta; size_t max_samples }, and sentil_spec_ams_settings_t is { size_t num_particles; size_t max_steps }.

Related