C++

The C++ binding is one header, sentil/sentil.hpp, over the C ABI. Every wrapper class owns its C handle and frees it in its destructor, so you never call a _destroy function, and every fallible operation throws a sentil::SentilError carrying the core's own message. A robustness call through the wrapper measures about 134 ns in the cross-language benchmark, against 74 ns for raw C. It requires C++17 or newer.

Install

The wrapper is header-only, so an install is two things in place: libsentil with its C header where the linker looks, and sentil/sentil.hpp on your include path. vcpkg and Conan do both at once through the sentil-cpp package, which is the route to reach for. The releases page has no C++ archive; the bundle published there is the C ABI alone, so that route means the bundle plus the headers from a checkout. A build from source produces both halves out of one tree.

From vcpkg or Conan

vcpkg install sentil-cpp

conan install --requires=sentil-cpp/0.3.0

find_package(SentilCpp CONFIG REQUIRED)
target_link_libraries(my_app PRIVATE Sentil::cpp)

c++ -std=c++17 my_app.cpp $(pkg-config --cflags --libs sentil) -o my_app

#include <sentil/sentil.hpp>
#include <cstdio>

int main() {
    sentil::Version v = sentil::version();
    std::printf("sentil %u.%u.%u\n", v.major, v.minor, v.patch);
    return 0;
}

./check_install

sentil 0.3.0

From a GitHub release

tar -xzf sentil-0.3.0-linux-x86_64.tar.gz

git clone https://github.com/sedislab/SENTIL

prefix=$PWD/sentil-0.3.0-linux-x86_64
export PKG_CONFIG_PATH=$prefix/lib/pkgconfig:$PKG_CONFIG_PATH
c++ -std=c++17 check_install.cpp -I SENTIL/sentil-cpp/include \
    $(pkg-config --define-variable=prefix=$prefix --cflags --libs sentil) \
    -Wl,-rpath,$prefix/lib -o check_install
./check_install

sentil 0.3.0

From source

You need CMake 3.16 or newer, a C++17 compiler, and a Rust toolchain from rustup.rs for the core. Where the compiler and CMake come from differs by system.

xcode-select --install

git clone https://github.com/sedislab/SENTIL
cd SENTIL
cmake -S sentil-cpp -B sentil-cpp/build
cmake --build sentil-cpp/build

ctest --test-dir sentil-cpp/build

100% tests passed, 0 tests failed out of 10

c++ -std=c++17 check_install.cpp -I sentil-cpp/include -I sentil-ffi/include \
    -L target/release -lsentil -Wl,-rpath,$PWD/target/release -o check_install
./check_install

sentil 0.3.0

The shared entry point for building the whole workspace is install from source; on a Raspberry Pi the ARM archives and the board mapping are on the CLI page.

Including <sentil/sentil.hpp> brings in the whole surface; it is split internally into sentil/types.hpp (enums and value structs) and sentil/errors.hpp (the exception hierarchy), which you can include alone.

First monitor

The first program reads two things off one formula: the robustness and the spans where it fails.

#include <sentil/sentil.hpp>
#include <iostream>

int main() {
    sentil::Trace trace({0, 1, 2, 3, 4}, "speed", {12.0, 9.0, 7.0, 4.0, 6.0});
    sentil::Formula phi = sentil::Formula::parse("G (speed > 5)");

    std::cout << "robustness: " << phi.robustness(trace) << "\n";
    for (const sentil::Interval& v : phi.violations(trace)) {
        std::cout << "violation [" << v.start << ", " << v.end << "]\n";
    }
    return 0;
}

robustness: -1
violation [0, 3]

The dip to 4 at t = 3 decides the result: G, read always, takes the minimum margin, and the minimum is -1. How to read robustness is covered once in what STL is; this page sticks to the API. robustness_signal(trace) returns the value at every sample, robustness_dense(trace) evaluates between samples too, and violations(trace) returns the spans where the property fails, here every evaluation time from 0 through 3 because each of those windows contains the dip.

Traces

Signals in a Trace share one strictly increasing time vector and match its length. Build one inline as above, from CSV or TSV text, or from a file whose format is chosen by extension.

sentil::Trace trace = sentil::Trace::from_csv("time,speed\n0,12\n1,9\n2,7\n3,4\n4,6");
trace.size();               // 5
trace["speed"][3];          // 4.0
trace.signal("altitude");   // std::nullopt

sentil::Trace half = trace.resample({0.0, 0.5, 1.0, 1.5, 2.0});
half["speed"][1];           // 10.5, linear between 12 and 9

trace[name] copies a signal out and throws std::out_of_range for a name the trace does not carry; signal(name) is the non-throwing sibling returning an optional, and contains(name) asks without copying. from_path reads csv, tsv, and txt everywhere and MATLAB .mat files in the default build; parquet, arrow, sqlite, hdf5, and mcap follow the Cargo features the linked core was built with, sqlite being on by default. The format details live in trace formats. For repeated resampling, prepare(interp) fixes the interpolation coefficients once and returns a PreparedTrace.

Streaming

sentil::OnlineMonitor is built for the control loop: an update is O(1) amortized, and state never outgrows the largest temporal window no matter how long the run. Both bounds come from the monotonic deque.

#include <sentil/sentil.hpp>
#include <cmath>
#include <cstdio>

int main() {
    sentil::OnlineMonitor monitor("G[0, 10] (x > -0.9)");
    for (int t = 0; t < 60; ++t) {
        double x = std::sin(t * 0.3);
        sentil::Robustness verdict = monitor.update(static_cast<double>(t), {{"x", x}});
        if (verdict.resolved && !verdict.satisfied) {
            std::printf("violated at t=%d, robustness=%.3f\n", t, verdict.value);
            return 0;
        }
    }
    std::printf("held over the whole stream\n");
    return 0;
}

violated at t=15, robustness=-0.078

The sine wave first drops below -0.9 at t = 15, which lands inside the window of the evaluation time being decided, so the verdict resolves negative on that very update. Until a window has fully passed, resolved stays false and value sits halfway between lower and upper.

The map form hashes every name on every call. symbol_index(name) maps each variable to its packed slot once, and update_packed(time, values) then crosses the FFI boundary with a plain array. Packed order is sorted by variable name, not appearance order, so always ask.

sentil::OnlineMonitor monitor("G[0, 10] (speed > 5 & accel < 3)");
std::size_t i_accel = *monitor.symbol_index("accel");   // 0
std::size_t i_speed = *monitor.symbol_index("speed");   // 1

std::vector<double> packed(monitor.variable_count());
packed[i_speed] = 12.0;
packed[i_accel] = 1.0;
monitor.update_packed(0.0, packed);

reset() clears the streaming state for a fresh run, and run(trace) replays a whole recorded trace through the same engine, returning the per-sample verdicts. To drive many formulas under one clock, use MultiMonitor, whose table is in the reference below.

Nothing restricts streaming to deterministic formulas. OnlineMonitor::with_lifting lifts each incoming reading into a particle ensemble through a LiftingRegistry, and last_probability() exposes the running satisfaction estimate next to the verdict:

sentil::Formula phi = sentil::Formula::parse("P>=0.9 (G[0, 5] (x > 0))");
sentil::LiftingRegistry lifting;
lifting.register_noise("x", sentil::NoiseModel::gaussian(0.0, 0.3));

sentil::OnlineMonitor monitor = sentil::OnlineMonitor::with_lifting(phi, lifting);
for (int t = 0; t < 20; ++t) {
    double x = 0.4 + 0.05 * t;
    monitor.update(static_cast<double>(t), {{"x", x}});
    if (t % 6 == 5) {
        std::printf("t=%d  P=%.4f\n", t, *monitor.last_probability());
    }
}

t=5  P=0.7526
t=11  P=0.9752
t=17  P=0.9990

The signal ramps away from the threshold, so the estimated probability of holding the 5-sample window climbs with it. last_probability() returns std::nullopt for a deterministic formula or before the first update, and the same accessor exists on Monitor and per id on MultiMonitor.

Probabilistic checking

The workflow is a registry of per-variable noise models, then one check call; the operator itself is taught in what PrSTL is.

#include <sentil/sentil.hpp>
#include <cstdio>
#include <vector>

int main() {
    std::vector<double> times, values;
    for (int i = 0; i < 20; ++i) {
        times.push_back(i);
        values.push_back(0.4 + 0.05 * i);
    }
    sentil::Trace trace(times, "x", values);

    sentil::LiftingRegistry lifting;
    lifting.register_noise("x", sentil::NoiseModel::gaussian(0.0, 0.3));

    sentil::Formula phi = sentil::Formula::parse("P>=0.9 (G (x > 0))");
    sentil::SmcConfig config;
    config.samples = 5000;
    sentil::SmcResult result = phi.check(trace, lifting, config);
    std::printf("probability %.4f, interval [%.4f, %.4f], holds %s\n", result.probability,
                result.interval.lower, result.interval.upper, result.holds ? "true" : "false");
    return 0;
}

probability 0.7332, interval [0.7208, 0.7453], holds false

With noise of standard deviation 0.3 on a signal that starts only 0.4 above the threshold, about a quarter of the sampled realizations dip below zero somewhere, so the estimate misses the 0.9 the formula demands and holds is false. The interval is a Wilson score interval at the 0.95 level by default; how to read it, and when to prefer another method, is on confidence intervals. register_noise consumes the model it is given, defaults the interaction to additive, and is so named because register is a reserved word. Seventeen noise families and the fitting constructors are enumerated in the reference below.

Three variations on the same call. check_conservative always reports the exact Clopper-Pearson interval, [0.7207, 0.7454] on the run above, slightly wider than Wilson. check_distribution additionally returns a RobustnessDistribution summarizing robustness across the ensemble, which tells you how close the misses were, here mean 0.1037 with minimum -0.7163. And Monitor::check runs the check with whatever SMC settings the monitor carries, which matters when the monitor came preloaded from the specifications library.

For a sequential decision instead of a fixed budget, check_sequential runs Wald's SPRT and check_bayesian runs a Bayesian test with a Beta prior; both stop as soon as the evidence is decisive. SprtConfig requires p0 and p1, the two hypothesis probabilities, and BayesConfig requires threshold. On the trace above, SPRT between p0 = 0.85 and p1 = 0.95 accepts H0 after 32 samples, and the Bayesian test at threshold 0.9 returns BayesVerdict::Fails after 60 samples with posterior 0.0008.

When the probability you are after is far below what a Monte Carlo budget can see, check_rare_event estimates it by adaptive multilevel splitting over a StochasticSystem, a model the engine can sample. The declarative way to build one is SimExpr update terms in a SimModel:

using sentil::SimExpr;
std::vector<SimExpr> init;
init.push_back(SimExpr::constant(0.0));
std::vector<SimExpr> advance;
advance.push_back(SimExpr::prev(0) * 0.8 + SimExpr::noise(0));
std::vector<sentil::NoiseModel> noise;
noise.push_back(sentil::NoiseModel::gaussian(0.0, 1.0));
sentil::SimModel model({"x"}, 1.0, 50, std::move(init), std::move(advance), std::move(noise));

sentil::Formula phi = sentil::Formula::parse("P>=0.9999 (G[0, 50] (x < 6.5))");
sentil::RareEventResult result = phi.check_rare_event(model.to_stochastic_system());
std::printf("violation probability %.3e over %llu simulations, holds %s\n",
            result.violation_probability, (unsigned long long)result.simulations,
            result.holds ? "true" : "false");

violation probability 1.614e-03 over 746930 simulations, holds false

The AR(1) state rarely wanders past 6.5, and the splitter resolves that tail instead of returning zero; probability and violation_probability sum to one. Systems with arbitrary host dynamics come from StochasticSystem::custom, whose callbacks may run on several threads and must be thread-safe. On a machine with a GPU, Formula::check_rare_event_gpu runs fixed-effort splitting on the device for P >= p (G[0, b] psi) formulas over a SimModel; sentil::gpu::is_available() reports whether a device is usable, and without one the call throws a typed error (GPU run failed: no compatible GPU adapter for the splitting path) rather than falling back silently. The method itself is described in rare events.

Synthesis

The example is a single integrator, x' = x + u from x0 = 1, with three inputs bounded to [-1, 1] and a spec that x stay positive.

#include <sentil/sentil.hpp>
#include <cstdio>

int main() {
    sentil::SystemModel model = sentil::SystemModel::linear({{1.0}}, {{1.0}}, {1.0}, {"x"}, 1.0, 3);
    sentil::Formula spec = sentil::Formula::parse("G (x > 0)");
    sentil::Bounds bounds({-1.0, -1.0, -1.0}, {1.0, 1.0, 1.0});

    sentil::SynthesisResult result = sentil::synthesis::synthesize(model, spec, &bounds);
    std::printf("robustness %.1f, holds %s, input [%.0f, %.0f, %.0f]\n", result.robustness,
                result.holds ? "true" : "false", result.input[0], result.input[1], result.input[2]);
    return 0;
}

robustness 1.0, holds true, input [1, -1, 0]

synthesize borrows the model and spec, takes the bounds and smoothing config as optional pointers, and reports in result.backend which optimizer actually ran; on this affine model the Auto choice is the complete MILP encoding, so backend comes back Backend::Milp. The backend choices and when each wins are on synthesis backends.

The rest of the subsystem follows the same shapes. Controller re-solves a short-horizon problem at every step against a hard nanosecond deadline and control(state) returns the next input. SafetyFilter is a control-barrier shield that projects a nominal input to the nearest safe one. ChanceConstraint demands a spec hold with a target probability and validate measures it by sampling a StochasticSystem. Going the other way, phi.falsify(model, bounds) and phi.find_counterexample(model, bounds) search for a violating trajectory and return a Witness whose negative robustness certifies the counterexample; on the model above with four free steps, falsification drives x to -3. And mine_tightest_parameter binary-searches a spec parameter for the tightest value that still holds on a set of traces: mining G (speed > c) over the first-monitor trace returns c = 4, the trace minimum.

Errors

Everything that can fail throws a subclass of sentil::SentilError, which derives from std::exception. Catch the base to handle everything, or a subclass to separate the kinds. what() carries the core's own message, down to the construct and position that caused it, and code() is the stable C status behind it, one of the values on the error codes page.

try {
    sentil::Formula phi = sentil::Formula::parse("G (speed >");
    (void)phi;
} catch (const sentil::ParseError& e) {
    std::cerr << "could not parse: " << e.what() << "\n";
}

could not parse: parse error at line 1, column 11: expected a value or `(`, found end of input

Evaluating a formula against a trace missing one of its variables, for instance, throws a SemanticError reading no value available for variable `speed`; add a signal named `speed` to the trace, or include it in the streaming update. Two accessors step outside this hierarchy by design: trace[name] and RingBuffer::operator[] throw std::out_of_range, matching what C++ eyes expect from an index operator, and each has an optional-returning sibling (signal, get) when you would rather test than catch. If you mix in raw C ABI calls, the free function ensure(code) converts a non-OK status into the matching thrown subclass. Host callbacks, in StochasticSystem::custom, SystemModel::custom, stats::sequential_test, adaptive_multilevel_splitting, and mine_tightest_parameter, must not unwind through the engine, so an exception a callback throws is captured and rethrown after the call returns.

What consumes what

The wrappers are move-only owners, and several operations consume their operands, meaning the moved-from object must not be used again. The temporal and boolean member combinators on Formula are &&-qualified, so they chain on temporaries and a named formula must be std::moved into them; the free-function spellings below do the moving for you. The Expr and SimExpr arithmetic operators consume both operands, so write an expression as one inline chain:

using sentil::Expr;
Expr margin = Expr::var("altitude") - Expr::var("floor_limit");
sentil::Formula phi = sentil::always(std::move(margin) > 100.0);   // robustness 200 on {900, 800} vs {500, 500}

Also consuming: LiftingRegistry::register_noise takes its NoiseModel, NoiseModel::mixture takes its components, the SimModel constructor takes its expressions and noise models, Monitor construction takes its Formula, Controller takes its model and spec, SafetyFilter takes its bounds, ChanceConstraint takes its spec, and the SpecBuilder chain methods consume the builder even when the variant or parameter is rejected. OnlineMonitor(const Formula&), MultiMonitor::add, FormulaBank::add, and synthesis::synthesize borrow instead.

Reference

The complete surface of sentil.hpp, types.hpp, and errors.hpp. Signatures elide std:: and trailing const for width; the headers carry the exact declarations. detail:: is internal and not listed.

Version

Enums

All scoped enums convert to their C constants by exact cast.

Configuration structs

Plain aggregates with the core's defaults; set only what you change. SprtConfig::p0/p1 and BayesConfig::threshold have no default and must be set.

Result structs

Formula

A move-only owner of a parsed PrSTL tree. Build from text or JSON, inspect it, evaluate it, check it.

The combinator members implies, next, always, eventually, historically, once, until, since, and probability are &&-qualified and consume their operands; their free-function spellings below are the usual way to write them.

Expr and the operator DSL

Formulas can be built in C++ instead of parsed. Expr::var(name) and Expr::constant(value) make terms, arithmetic combines them, and comparing two terms yields a Formula; doubles convert wherever a term is expected.

The operator semantics themselves are on the operators reference.

Trace and PreparedTrace

RingBuffer

A fixed-capacity rolling window over timed samples with running statistics. Pushing past capacity evicts the oldest.

sentil::RingBuffer window(3);
window.push(0.0, 12.0);
window.push(1.0, 9.0);
window.push(2.0, 7.0);
window.push(3.0, 4.0);   // returns the evicted Sample at t=0
*window.mean();          // 6.667 over {9, 7, 4}

Monitors

Four monitor shapes share the verdict and update vocabulary. Config holds the evaluation settings: Config(TimeMode::Dense) switches a Monitor to dense time, and time() reads the mode back.

FormulaBank scores a named set over a full trace in one call: add(id, formula) in both spellings, ids, size, and empty as above, and robustness(const Trace&) or robustness_dense(const Trace&) returning a map<string, double> keyed by id.

Noise models and lifting

NoiseModel is a distribution for stochastic signal lifting, built from a named family, fitted from calibration residuals, or combined into a mixture. All 17 families:

Fitting starts from residuals: NoiseModel::residuals(ground_truth, sensor, interaction) differences paired readings under the chosen NoiseInteraction, then fit_gaussian(samples) fits by maximum likelihood, fit_bootstrap(samples) keeps the empirical distribution, fit_bootstrap_reservoir(samples, max_samples) caps its memory, and fit_gaussian_mixture(samples, components, max_iters) runs expectation-maximization. On a model, mean() and variance() return the analytic moments as optional (Cauchy has neither), and to_json(), from_json(json), and from_file(path) round-trip the model for storage. Guidance on choosing a family is on noise models.

LiftingRegistry maps variables to models: register_noise(variable, model, interaction = Additive) consumes the model, variables() lists the registered names, empty() tests for none, and lift(trace, seed = 42) draws one seeded noisy realization of a trace.

The stats namespace

The statistical primitives under the model checker, callable directly.

The derivations behind these live in statistical methods.

Stochastic simulators and rare events

A SimExpr is one update term: SimExpr::prev(i) for variable i at the previous step, SimExpr::time() for the clock, SimExpr::constant(v) for a literal, and SimExpr::noise(j) for a draw from noise source j. The arithmetic operators + - * / (with mixed-double overloads and unary -) and the functions abs, sin, cos, tan, sqrt, exp, log, ln, floor, ceil, min, and max combine them, consuming operands like Expr.

Synthesis toolkit

The objective aliases: GradientObjective returns a value and its gradient, Objective a value, and BatchObjective a vector of values for a population of points.

The specifications library

The embedded registry ships 54 cited PrSTL specifications in 0.3.0, browsable under specifications; SpecBuilder resolves one by name.

std::printf("%zu specifications\n", sentil::SpecBuilder::available().size());

sentil::SpecBuilder builder("controls/overshoot");
for (const std::string& v : builder.available_variants()) {
    std::printf("variant: %s\n", v.c_str());
}
std::printf("%s\n", builder.build_deterministic().c_str());

sentil::Formula phi =
    std::move(builder).with_param("max_overshoot", 0.1).build_formula();

54 specifications
variant: bidirectional
variant: step_down
variant: step_up
always[0, 30.0](output - reference < 0.05 * 1.0)

Each spec documents its parameters and their valid ranges; parameters_json() shows the resolved values, and a parameter outside its range, or one the spec does not define, throws. with_variant, with_param, and build_monitor consume the builder even when they reject the input, so chain them on a temporary or a moved builder and rebuild from the name to retry.

The settings structs are SpecSmcSettings { confidence, sample_budget }, SpecSprtSettings { p0, p1, alpha, beta, max_samples }, and SpecAmsSettings { num_particles, max_steps }.

Raw handles

Every wrapper class also carries an interop trio for mixing with the C ABI: an explicit Class(raw_handle*) constructor that takes ownership of a C handle, get() returning the raw handle while the wrapper keeps ownership, and, on the eight classes whose handles a C call can consume (Formula, Expr, Trace, NoiseModel, SimExpr, Bounds, SystemModel, SpecBuilder), release() which gives ownership up. Pair them with ensure from the errors section and the two layers compose cleanly.

Related pages