Trustworthiness Checker - Tutorial ================================= **Repository:** `link `_ This tutorial walks you through building, configuring, and running the Trustworthiness Checker from this repository. You will learn how to use file traces, MQTT, Redis, and ROS 2 as I/O backends, and how to try distributed execution modes and the work scheduler. Prerequisites ------------- - Rust toolchain (Rust 1.85+ recommended) with Cargo - Optional backends depending on what you want to try: - MQTT broker (e.g., EMQX, Mosquitto). A ready-to-use EMQX service is provided via ``docker/docker-compose.yaml``. - Redis server (only if trying Redis I/O) - ROS 2 Humble (only if trying ROS I/O). The Dockerfile targets Humble. - Python is not required for the core tool, but some scripts under ``scripts/`` may use it. Build from source ----------------- 1. Clone this repository and change into it. 2. Build in debug or release mode: - Debug (faster builds):: cargo build - Release (faster runtime):: cargo build --release Set logging verbosity (optional) by setting ``RUST_LOG`` before running, for example ``info`` or ``debug``. In PowerShell:: $env:RUST_LOG = "info" A quick look at the CLI ----------------------- The executable is the default run target for the crate and supports multiple I/O backends and distribution modes. Common flags: - Model/specification file: ```` (first positional) - Input (choose one): - ``--input-file `` - ``--input-mqtt-topics ...`` or ``--mqtt-input`` - ``--input-redis-topics ...`` or ``--redis-input`` - ``--input-ros-topics `` (ROS 2 feature) - ``--input-map-mqtt-topics ...`` (structured/generic MQTT input) - Output (choose one): - ``--output-stdout`` - ``--output-mqtt-topics ...`` or ``--mqtt-output`` - ``--output-redis-topics ...`` or ``--redis-output`` - ``--output-ros-topics ...`` (not implemented yet) - Distribution (optional): see the section "Distributed execution" below. - Ports (optional): ``--mqtt-port ``, ``--redis-port `` - Parser/language (optional): ``--parser-mode combinator|lalr``, ``--language dynsrv|lola`` (LOLA is an alias for DynSRV). Data format ----------- Values are exchanged as JSON. For integer values, wrap in a variant object:: { "Int": 42 } To send an unknown value, use:: { "Unknown": null } The tool also supports richer types in examples that use lists and records (see ``examples/distributed/mqtt_dist_echo.lola``). Quick start: file input and stdout output ---------------------------------------- Use the minimal example in ``examples/simple_add.lola`` and a matching trace in ``examples/simple_add.input``. - Model (``examples/simple_add.lola``):: in x in y out z z = x + y - Trace (``examples/simple_add.input``):: 0: x = 1 y = 2 1: x = 3 y = 4 Run the monitor and print results to stdout:: cargo run -- examples/simple_add.lola --input-file examples/simple_add.input --output-stdout MQTT I/O -------- A working MQTT broker is required. You can use the EMQX service defined in ``docker/docker-compose.yaml``. Publish/subscribe topics are bound by name to stream variables when you use ``--input-mqtt-topics`` and ``--output-mqtt-topics``. Example: add two inputs and publish the result on topic ``z``:: cargo run -- examples/simple_add.lola --input-mqtt-topics x y --output-mqtt-topics z Then publish two messages (e.g., with MQTT Explorer) to topics ``x`` and ``y`` respectively:: { "Int": 42 } You should see the output on topic ``z``:: { "Int": 84 } Notes ^^^^^ - If your specification declares auxiliary streams, current MQTT output requires listing them in ``--output-mqtt-topics`` even if they aren’t actually published (limitation). - You can also use the generic mapping mode with ``--input-map-mqtt-topics`` for structured payloads (see ``examples/distributed/mqtt_dist_echo.lola``). Redis I/O --------- Use Redis as a transport for input and/or output. Example:: cargo run -- examples/simple_add.lola --input-redis-topics x y --output-redis-topics z Publish JSON messages to Redis channels ``x`` and ``y`` that match the value format (e.g., using ``redis-cli``), and subscribe to ``z`` to read outputs. ROS 2 I/O (feature) ------------------- ROS 2 support is behind the ``ros`` feature and uses a mapping file that binds ROS topics and message fields to stream variables. Build and run:: cargo run --features ros -- --input-ros-topics examples/counter_ros_map.json examples/counter.lola In another ROS 2-sourced terminal, publish:: ros2 topic pub /x std_msgs/msg/Int32 "{data: 1}" The monitor should begin counting. You must have sourced ROS 2 Humble and built the custom message interfaces if required (see Docker section). Distributed execution --------------------- The tool supports several distributed modes coordinated over MQTT. You can use the provided EMQX service in ``docker/docker-compose.yaml``. Centralised monitor (default) ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ No extra flags are needed; this is the default. Localised monitor ^^^^^^^^^^^^^^^^^ Run a local monitor for variables assigned to a given node in a distribution graph. Provide the graph and your local node id:: cargo run -- examples/simple_add.lola \ --distribution-graph examples/simple_add_distribution_graph.json \ --local-node A \ --output-stdout Alternatively, specify variables directly for local monitoring:: cargo run -- examples/simple_add.lola --local-topics x y --output-stdout MQTT-based distributed modes ^^^^^^^^^^^^^^^^^^^^^^^^^^^^ - Centralised distributed over locations:: cargo run -- examples/simple_add.lola --mqtt-centralised-distributed A B C --output-stdout - Randomised distributed over locations:: cargo run -- examples/simple_add.lola --mqtt-randomized-distributed A B C --output-stdout - Static or dynamic optimisation (requires constraints variables):: cargo run -- examples/simple_add_distributable.lola \ --mqtt-static-optimized A B C \ --distribution-constraints w v \ --output-stdout cargo run -- examples/simple_add_distributable.lola \ --mqtt-dynamic-optimized A B C \ --distribution-constraints w v \ --output-stdout Waiting for scheduler assignment ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ A node can wait to receive its assignment from a scheduler via MQTT:: cargo run -- examples/simple_add_distributable.lola --distributed-work --local-node A --output-stdout Work scheduler ^^^^^^^^^^^^^^ A separate binary, ``work_scheduler``, can compute and send assignments. Run it with a distribution graph:: cargo run --bin work_scheduler -- --distribution-graph examples/simple_add_distribution_graph.json Docker support -------------- A multi-stage Dockerfile is provided: - ``docker/Dockerfile`` has two targets: - ``base``: ROS 2 Humble + tooling + custom interfaces build - ``dev``: adds a non-root user and installs Rust toolchain - ``docker/DockerfileDeploy`` builds and runs the release binary. A compose file starts EMQX and a dev container: - Start EMQX only:: docker compose -f docker/docker-compose.yaml up -d emqx - Start dev environment (includes Rust):: docker compose -f docker/docker-compose.yaml up -d dev emqx The dev container runs ``sleep infinity``; exec into it to build and run with Cargo. ROS 2 Humble is available in the base image. The ``ros_interfaces`` are built during image creation. Examples gallery ---------------- - ``examples/simple_add.lola`` — integer addition - ``examples/simple_add_typed.lola`` — typed variant - ``examples/past.lola``, ``examples/future.lola`` — temporal operators - ``examples/dynamic_lola/*.lola`` — dynamic features like ``eval`` and ``default`` - ``examples/distributed/*.lola`` — distributed MQTT examples Troubleshooting --------------- - MQTT or Redis connection issues - Check broker/server is running and reachable - Set explicit ports via ``--mqtt-port`` / ``--redis-port`` if needed - Parser/language - Default parser mode is ``combinator`` and language is ``dynsrv`` (LOLA alias). Use ``--parser-mode`` and ``--language`` if necessary. - Logging - Increase verbosity with ``RUST_LOG=debug`` when diagnosing issues. Further reading --------------- - Source code for I/O backends: ``src/io`` - CLI definitions and flags: ``src/cli/args.rs`` - Runtime builder and distribution modes: ``src/runtime/builder.rs`` - Examples and fixtures: ``examples/`` Acknowledgement --------------- The work presented here is supported by the RoboSAPIENS project funded by the European Commission's Horizon Europe programme under grant agreement number 101133807.