Apollo

The sentil-apollo module drops into an Apollo workspace as modules/sentil and runs the SENTIL engine as Cyber RT components. A monitor watches Apollo channels against STL and probabilistic STL specifications and publishes a verdict per formula. A control component shields Apollo's nominal command inside a specification's bounds, or synthesizes its own command from the specification. Everything is configured in protobuf text, so a deployment is a config file plus a launch command, with no glue code. The build links the staged core through the @sentil_cpp Bazel external repository; once the tree is staged, Bazel never touches Rust. Cyber RT runs on Linux only.

Install

Apollo has no package registry, and the releases page carries no Apollo asset. One route exists: the module is source, copied into an Apollo workspace as modules/sentil and built there by Apollo's buildtool on top of Bazel. The operating system to think about is the dev container's rather than the host's, and since Cyber RT is Linux only there is no macOS or Windows workspace to drop into. Apollo 9.0 and newer build modules with the package method these steps use.

From source

aem start

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

curl -L https://github.com/sedislab/SENTIL/archive/refs/tags/v0.3.0.tar.gz -o sentil.tar.gz
tar -xzf sentil.tar.gz
cd SENTIL-0.3.0

cargo build --release -p sentil-ffi
install -d /opt/sentil/include/sentil /opt/sentil/lib /opt/sentil/share/sentil
cp sentil-cpp/include/sentil/*.hpp /opt/sentil/include/sentil/
install -m644 sentil-ffi/include/sentil.h /opt/sentil/include/sentil.h
install -m644 target/release/libsentil.so /opt/sentil/lib/libsentil.so
install -m644 benchmarks/deterministic/oracle.json /opt/sentil/share/sentil/oracle.json

/opt/sentil
├── include
│   ├── sentil.h
│   └── sentil
│       ├── sentil.hpp
│       ├── types.hpp
│       └── errors.hpp
├── lib
│   └── libsentil.so
└── share
    └── sentil
        └── oracle.json

g++ -std=c++17 -I/opt/sentil/include sentil-apollo/tests/symbol_reference.cc \
  -L/opt/sentil/lib -lsentil -o symbol_reference
LD_LIBRARY_PATH=/opt/sentil/lib ./symbol_reference

cd /path/to/apollo-workspace
cp -r /path/to/SENTIL/sentil-apollo modules/sentil

new_local_repository(
    name = "sentil_cpp",
    path = "/opt/sentil",
    build_file = "//modules/sentil:bzl/sentil_cpp.BUILD",
)

buildtool build -p sentil
buildtool install sentil
bazel test //modules/sentil/tests/...

Your first monitor

Write a formula and a field mapping into the config the monitor dag points at, then launch. This is the shipped examples/ego_speed_monitor.pb.txt shape: the ego speed must stay under 20 m/s over any five second window.

formulas {
  id: 1
  expression: "G[0, 5.0] (ego_speed < 20.0)"
}
input_channels {
  channel: "/apollo/canbus/chassis"
  message_type: "apollo.canbus.Chassis"
  fields {
    variable: "ego_speed"
    field_path: "speed_mps"
  }
}
output_channel: "/apollo/sentil/status"

cyber_launch start modules/sentil/monitor/launch/sentil_monitor.launch
cyber_monitor -c /apollo/sentil/status

The predicate ego_speed < 20.0 scores 20 - ego_speed, so a chassis reading of 17.2 m/s carries a margin of 2.8 and a reading of 21.0 scores -1.0; G, read always, keeps the worst margin in the window, so one bad second decides the verdict. That worst margin is the robustness each FormulaResult on the status carries, alongside a satisfied flag, a severity, and an all_satisfied flag across the set. The engine folds each message at O(1) amortized cost per sample through the monotonic deque, so the monitor holds a real-time loop.

Channels as signals

Each input_channels entry names a channel, its fully qualified message_type, and the fields to read. A field binds a formula variable to either a field_path or a builtin.

A field_path is a dotted, optionally indexed path into the message: speed_mps, pose.position.x, perception_obstacle[0].position.x. Paths resolve against the message descriptor when the component initializes, so a typo fails at startup instead of reading as a silent zero mid-drive.

A builtin reduces the whole obstacle list to one number. A fixed index like perception_obstacle[0] names whichever obstacle perception listed first, not the nearest, so the reductions a safety formula actually wants are built in:

Where the readers come from differs by shell. The fused monitor's readers are declared in its dag file. The timed monitor creates its own readers, matching each mapping to a reader by message_type and taking the mapping's channel, with the standard perception, localization, and chassis channels as the fallback.

Streaming and the two monitor shells

SentilMonitorComponent, the default, is a fused component triggered by perception with localization and chassis as co-channels, so each verdict reflects one consistent message set. SentilTimedMonitorComponent reads the same channels through pull readers and evaluates on a timer, every 100 ms as shipped in its dag; reach for it when a steady verdict cadence matters more than reacting to each perception frame.

Both shells share one engine and one readiness discipline. Each tick is stamped with the perception header time, falling back to the Cyber RT clock, and a stalled or rewound stamp skips the tick rather than feeding the engine a non-monotonic time. No status is published until every variable a formula binds has been seen at least once. While a bounded window is still open the verdict is unresolved: the status reports the robustness as a min and max bound with is_concrete false and the severity WARN, and it tightens to a concrete value once the window closes.

For a P formula the status also carries the live probability on every tick: prob_result holds the running estimate with its Wilson interval at the configured confidence, which is the same live-probability accessor the other bindings expose, delivered as a message field.

Downstream, planning subscribes to /apollo/sentil/status and falls back when all_satisfied goes false or a probabilistic interval drops below its floor. examples/safety_planner_subscriber.cc is the small standalone version of that contract; it tests interval().lower() against the floor, the pessimistic end, since waiting for the upper end would fall back only after even the optimistic estimate had failed.

Probabilistic monitoring

A formula selects the probabilistic path with its leading P and nothing else; the P operator is the whole switch. For each such formula the monitor builds a probabilistic monitor from lifting_registry, lifts each reading into a sample_budget ensemble, and reports the satisfaction estimate with a Wilson interval at confidence. The shipped examples/follow_distance_prstl.pb.txt holds a follow distance under Gaussian perception noise:

formulas {
  id: 1
  expression: "P>=0.99(G[0, 2.0] (front_gap > 5.0))"
}
input_channels {
  channel: "/apollo/perception/obstacles"
  message_type: "apollo.perception.PerceptionObstacles"
  fields {
    variable: "front_gap"
    builtin: "FRONT_GAP"
  }
}
output_channel: "/apollo/sentil/status"
lifting_registry {
  variable: "front_gap"
  noise {
    gaussian {
      mean: 0.0
      std_dev: 0.25
    }
  }
  interaction: ADDITIVE
}
sample_budget: 1000
confidence: 0.99

The noise oneof accepts eight families, listed with their parameters in the monitor config reference below, and interaction is ADDITIVE or MULTIPLICATIVE. The full theory behind the families lives in noise models.

For the heavier statistics a per-tick budget cannot afford, sentil_record_analyzer replays a recorded drive over the same config:

sentil_record_analyzer --config=modules/sentil/monitor/conf/sentil_monitor.pb.txt --record=drive.record

The analyzer reads the record into a trace by sample and hold: each message updates its variables, and a row is appended once every configured variable has been seen, on a strictly increasing time axis. It then runs the configured algorithm per formula. DETERMINISTIC computes the robustness, dense or discrete per semantics. SMC estimates the probability with its interval. SPRT runs Wald's sequential test between p0 and p1; the sprt_config defaults are p0 0.90, p1 0.95, alpha and beta 0.05, and sample_budget caps the sample count, so an undecided run reports inconclusive when the budget runs out. AMS is rejected with an error: rare-event splitting runs over a stochastic model, not a recorded trace, so reach for the rare events path in the library or the CLI.

Synthesis and control

SentilControlComponent turns a specification into a ControlCommand, in one of three modes set in control/conf/sentil_control.pb.txt.

SHIELD, the default, guards Apollo's own controller. Each tick it takes the latest nominal command off nominal_channel, reads the actuation fields named by control_outputs, projects them into bounds through the safety filter, and writes the projected command with the rest of the nominal command intact. Until a nominal command has been observed it publishes nothing; the timer fires, the tick passes, no command is written.

SYNTHESIZE makes SENTIL the controller. Each tick it builds the state vector, plans over the model's horizon inside a hard budget of deadline_fraction * control_period_ms, and writes this step's synthesized input onto the command through control_outputs. The controller is anytime, emitting the best feasible input found within the budget. When the state cannot be built yet, because a variable has not been seen, the tick is skipped without publishing.

ADVISORY plans exactly as SYNTHESIZE but publishes to /apollo/sentil/control_advice with no actuation authority, so a synthesized controller can be judged against a live drive before it is trusted. In this mode the fixed advice channel overrides output_channel.

Two contracts here differ from the monitor. First, the state readers are hardcoded to /apollo/localization/pose and /apollo/canbus/chassis; a state_inputs entry selects what to extract through its message_type and fields, and its channel value is not used to place a reader. Second, a ControlOutput.field_path must name a top-level float or double field of ControlCommand, such as throttle, brake, steering_target, or acceleration; unlike the monitor's field_path it accepts no dotted or indexed paths, and an entry whose index reaches input_width or whose field is not floating point fails at startup. bounds is optional and an omitted bounds means unbounded inputs. The shipped dag ticks every 10 ms to match the default control_period_ms; if you change the period, change the dag interval with it. The launch file sets exception_handler: respawn, so a crashed control process restarts rather than staying dead.

The design-time half is sentil_synthesizer, which reads a SYNTHESIZE-shaped config carrying a model and needs no Cyber RT runtime:

sentil_synthesizer --config=examples/synthesize_control.pb.txt --op=plan

--op=plan synthesizes the open-loop input sequence over the horizon, reporting its robustness and whether it holds, so an infeasible spec comes back as the closest plan with holds false rather than nothing. --op=witness searches for a counterexample input that violates the spec, and requires bounds to search over. --op=chance perturbs the model's autonomous dynamics with Gaussian process noise of --process_std and checks that the spec holds with probability at least --probability at confidence --confidence. The shipped examples/synthesize_control.pb.txt is a runnable double integrator held between 1 and 9 metres; examples/synthesize_then_monitor.cc is the same loop as a standalone program, synthesizing offline and then checking the plan with the engine the monitor runs online. Backend selection and the smooth semantics behind all of this are covered in synthesis backends.

Errors

The module fails loudly at startup and stays quiet at runtime. Init() returns false, and the component does not start, on a config that does not parse, on a FieldResolutionError from a path or builtin that does not resolve against its message type, or on a std::invalid_argument from a bad control_outputs entry, so a misconfiguration surfaces at cyber_launch rather than on the road. At runtime the monitor catches an evaluation exception, logs it, and skips the tick; the process never crashes on input. A control tick that throws logs the failure, and the launch file's respawn brings the process back. The offline tools exit 1 on an engine error and sentil_synthesizer exits 2 on a usage error: a missing config, an unknown --op, or witness without bounds.

Components and runtime files

The three components, their shells, and their cadence:

Channels

Monitor config (SentilConfig)

The monitor reads a SentilConfig in protobuf text (proto/sentil_config.proto), default monitor/conf/sentil_monitor.pb.txt. The read-by column is honest: two fields in the schema have no consumer anywhere in the module.

The nested messages:

The NoiseModel oneof carries eight families:

Status message (SentilStatus)

Published on output_channel, defined in proto/sentil_status.proto.

Control config (SentilControlConfig)

The control component reads a SentilControlConfig (proto/sentil_control_config.proto), default control/conf/sentil_control.pb.txt.

Bazel targets

Everything the module builds. The components and libraries are public, so an extension component can depend on them.

Offline tool flags

sentil_record_analyzer takes two flags:

sentil_synthesizer takes five; the last three apply to --op=chance:

The C++ bridge

The engine bridge and the extractor are ordinary Bazel-public libraries, so a custom component can link them and reuse the module's plumbing. The headers are monitor/monitor_engine.h, common/field_extractor.h, and common/engine_config.h.

The types under these signatures are the module's protos and the engine surface from sentil.hpp, documented on the C++ page.

Shipped examples

Related