Keyboard shortcuts

Press ← or → to navigate between chapters

Press S or / to search in the book

Press ? to show this help

Press Esc to hide this help

Inputs

Select exactly one CLI input mode. A finite file provides timestamped rows and lets the checker exit; MQTT, Redis, Redis knowledge, ROS 2, and named multi-source inputs are live sources whose process lifetime follows the source.

Input modes

ModeCLI selectionWire or file shapeProcess shape
Finite trace--input-file PATHtimestamp: variable = JSON5 value rowsFinite; exits at end of file
Generic MQTT--mqtt-inputJSON/JSON5 payload on a topic named after the model inputLive; one decoded message normally becomes one update
MQTT route catalog--input-mqtt-file PATHCompact variable-to-route JSON5 objectLive; routes can differ from variable names
Redis Pub/Sub--redis-inputJSON/JSON5 payload on a channel named after the model inputLive; one decoded message normally becomes one update
Redis route catalog--input-redis-file PATHCompact variable-to-channel JSON5 objectLive
Redis knowledge state--redis-knowledge-inputSelected Redis keys plus keyspace notificationsLive; startup snapshot is enabled by default
ROS 2 route catalog--input-ros-file PATHCompact route object with [topic, message type/codec] entriesLive; requires --features ros
Named sources--input-config PATHJSON5 source registry with MQTT, Redis, Redis knowledge, or ROS sourcesSource-dependent; variables have one owner

--input-config is exclusive with the other input-selection flags. Generic MQTT and Redis routes default to the model variable names. Redis knowledge mappings are explicit: use --redis-knowledge-key INPUT=KEY or a redis-knowledge source's keys object; the checker never derives a key implicitly from a variable name.

MQTT selectors use protocol 3.1.1 by default. Pass --mqtt-protocol 5 to select MQTT 5; a named MQTT source can set its own protocol field, and inherits the CLI selection when that field is omitted.

Route catalogs

The compact route form is a JSON5 object. A string supplies a route. A two-element array supplies a route and codec for transports, such as ROS, whose mapping needs one:

{
  x: "/robot/input/x",
  pose: ["/robot/pose", "Pose2D"],
}

MQTT and Redis inputs always decode JSON/JSON5 values; use string routes for them because an input codec in the two-element form is not applied by those adapters. ROS routes require a message-type codec, so the two-element form is meaningful there. The corresponding output route-file options use the same compact shape, but their codec behavior is output-specific. Validate a route catalog by passing it to the matching CLI option; parsing succeeds before the transport is opened.

Logical ticks and windows

A file timestamp groups assignments into one simultaneous logical tick. A transport message normally creates an independent InputBatch::update; messages from several sources are composed in the order observed by this process, not a distributed total order.

For example, this program adds two MQTT inputs:

in x: Int
in y: Int
out z: Int
z = x + y

The repository stores it as examples/simple_add.dsrv. Use an input window when nearby MQTT arrivals need local grouping:

cargo run -- examples/simple_add.dsrv \
  --mqtt-input \
  --output-stdout \
  --input-window-ms 25 \
  --input-window-mode batch

batch preserves logical ticks. atomic-step reduces updates in a window to one simultaneous step using last-update-wins for each variable. A window threshold is a flush threshold; a complete logical tick is never split, so an indivisible tick may cross the nominal update limit.

Redis knowledge state

Redis Pub/Sub is for transient events. Redis knowledge input reads current selected keys and uses keyspace notifications as invalidation signals. Its defaults are database 2 and an enabled startup snapshot. A missing key becomes NoVal; the stdout sink suppresses that value rather than printing a replacement. The complete walkthrough is Redis knowledge-state input.

Deeper references