curiosity_rover_ogma: Introduce Ogma demonstration (#159)

curiosity_rover_ogma/.gitignore

@@ -0,0 +1,23 @@
+dist
+dist-*
+cabal-dev
+*.o
+*.hi
+*.hie
+*.chi
+*.chs.h
+*.dyn_o
+*.dyn_hi
+.hpc
+.hsenv
+.cabal-sandbox/
+cabal.sandbox.config
+*.prof
+*.aux
+*.hp
+*.eventlog
+.stack-work/
+cabal.project.local
+cabal.project.local~
+.HTF/
+.ghc.environment.*

curiosity_rover_ogma/Dockerfile

@@ -0,0 +1,75 @@
+# Copyright 2026 United States Government as represented by the Administrator
+# of the National Aeronautics and Space Administration. All Rights Reserved.
+#
+# Disclaimers
+#
+# Licensed under the Apache License, Version 2.0 (the "License"); you may
+# not use this file except in compliance with the License. You may obtain a
+# copy of the License at
+#
+#      https://www.apache.org/licenses/LICENSE-2.0
+#
+# Unless required by applicable law or agreed to in writing, software
+# distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
+# WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
+# License for the specific language governing permissions and limitations
+# under the License.
+FROM ubuntu:26.04 AS builder
+
+SHELL ["/bin/bash", "-c"]
+WORKDIR /root/
+
+# Do not ask questions during installation
+ENV DEBIAN_FRONTEND=noninteractive
+
+# Install dependencies
+RUN apt-get update && \
+    apt-get install --yes --no-install-recommends \
+      cabal-install \
+      ca-certificates \
+      cmake \
+      curl \
+      g++ \
+      ghc \
+      git \
+      libbz2-dev \
+      libexpat1-dev \
+      libz-dev \
+      make \
+      pkg-config \
+    && apt-get clean \
+    && rm -rf /var/lib/apt/lists/*
+
+# Set up Cabal
+RUN cabal update
+ENV PATH=/root/.local/bin:$PATH
+
+# Install Copilot and Ogma.
+#
+# In this case, we install and expose all Copilot libraries in the user's
+# package env because this is just for demonstration purposes, and to
+# facilitate compilation of the `Copilot.hs` file later.
+RUN cabal install --lib \
+      copilot \
+      copilot-c99 \
+      copilot-core \
+      copilot-interpreter \
+      copilot-language \
+      copilot-libraries \
+      copilot-prettyprinter \
+      copilot-theorem
+RUN git clone https://github.com/nasa/ogma
+RUN cd ogma && cabal install ogma-cli:ogma
+
+COPY manifest /tmp/space-ros/manifest
+
+# Generate ROS project and compile Copilot spec.
+RUN cd /tmp/space-ros && \
+    ogma ros --project manifest/project.ogma && \
+    find && \
+    cd /tmp/space-ros/monitor/copilot/src/ && \
+    runhaskell Copilot.hs
+
+# Copy the files generated by Ogma to the outside
+FROM scratch AS export-stage
+COPY --from=builder /tmp/space-ros/monitor /

curiosity_rover_ogma/README.md

@@ -0,0 +1,112 @@
+# Generating runtime monitors for the Curiosity Rover
+
+This directory contains a project that can be used with
+[Ogma](https://github.com/nasa/ogma) to generate a runtime monitor for the
+Curiosity Rover demo included with Space ROS.
+
+In particular, it helps quickly create nodes that detect if certain
+properties are violated.
+
+For the purposes of illustrating how to use this tool, the project included in
+this directory checks if the absolute value of the rover's X coordinate in the
+odometry's pose becomes greater than 2.5. When that happens, the generated node
+starts sending out violation messages.
+
+The property in question is listed in the file `document.json`, which lists the
+following property, where `input_signal` represents the rover's X coordinate:
+
+```
+{ "id":          "KeepRoverInCheck",
+  "formula":     "abs input_signal <= 2.5",
+  "description": "The rover stays near the starting point"
+}
+```
+
+The rest of this README explains how to compile this property into a ROS 2 node
+that will run alongside the Curiosity rover demo and check its position at all
+times.
+
+# Compilation
+
+To compile everything, run, from this specific demo's directory:
+
+```sh
+./build.sh
+```
+
+# Execution
+
+To run the demo, we need at least 4 terminals.
+
+## Terminal 1
+
+Start the curiosity rover demo from its own directory:
+
+```sh
+cd ../curiosity_rover
+./run.sh
+```
+
+## Terminal 2
+
+Start the monitoring node from this specific demo's directory.
+
+```sh
+./run.sh
+```
+
+Once the container starts, run:
+
+```sh
+$ source install/setup.bash
+$ ros2 run copilot copilot
+```
+
+That node does not print any output.
+
+## Terminal 3
+
+Log into this demo's container and listen for runtime monitoring
+violations:
+
+```sh
+$ docker exec -it osrf_space-ros-curiosity-rover-ogma /bin/bash
+$ source install/setup.bash
+$ ros2 topic echo /copilot/handlerKeepRoverInCheck \
+    | while IFS= read -r line; do \
+        echo "$(date '+%Y-%m-%d %H:%M:%S') $line"; \
+      done
+```
+
+## Terminal 4
+
+Instruct the rover to move forward by executing a call from the Curiosity demo
+container:
+
+```sh
+$ docker exec -it curiosity_rover-curiosity_demo-1 /bin/bash
+$ ros2 service call /move_forward std_srvs/srv/Empty
+```
+
+After approximately 1 minute (when the absolute value of the X coordinate of
+the rover's odometry's pose becomes greater than 2.5), Terminal 3 will start
+printing messages like the following:
+
+```
+2026-09-03 13:34:26 {}
+2026-09-03 13:34:26 ---
+2026-09-03 13:34:27 {}
+2026-09-03 13:34:27 ---
+2026-09-03 13:34:28 {}
+2026-09-03 13:34:28 ---
+2026-09-03 13:34:28 {}
+2026-09-03 13:34:28 ---
+2026-09-03 13:34:29 {}
+2026-09-03 13:34:29 ---
+```
+
+Each of those indicates a violation has occurred, meaning that the rover has
+left the "safe" zone. If you turn the rover around to get closer to the
+starting point (where the absolute value of the X coordinate becomes less than
+2.5), the messages will stop, and will resume if the rover distances itself
+from the starting point again.

curiosity_rover_ogma/build.sh

@@ -0,0 +1,49 @@
+#!/usr/bin/env bash
+
+echo ""
+echo "##### Building Space ROS Demo Docker Image #####"
+echo ""
+
+# Build dependency
+
+ORG=nasa
+IMAGE=ogma
+TAG=latest
+
+VCS_REF=""
+VERSION=preview
+
+# Exit script with failure if build fails
+set -eo pipefail
+
+# Build the image that contains Ogma
+docker build \
+    --target builder \
+    -t $ORG/$IMAGE:$TAG \
+    --build-arg VCS_REF="$VCS_REF" \
+    --build-arg VERSION="$VERSION" .
+
+# Run Ogma on this project and collect the output
+docker build --output type=local,dest=./monitor .
+
+# Build dependency used for this demo
+if ! docker image inspect "osrf/space-ros:curiosity_demo" >/dev/null 2>&1; then
+  pushd ../curiosity_rover/
+  ./build.sh
+  popd
+fi
+
+# Build generated app itself
+ORG=osrf
+IMAGE=space-ros-curiosity-rover-ogma
+TAG=latest
+
+VCS_REF=""
+VERSION=preview
+
+docker build -t $ORG/$IMAGE:$TAG \
+    --build-arg VCS_REF="$VCS_REF" \
+    --build-arg VERSION="$VERSION" monitor/
+
+echo ""
+echo "##### Done! #####"

curiosity_rover_ogma/manifest/document.json

@@ -0,0 +1,10 @@
+{
+  "auxiliary_defs": [],
+  "inputs": [ { "name":"input_signal", "type":"Double", "meaning": "InputF64" } ],
+  "properties": [
+    { "id":          "KeepRoverInCheck",
+      "formula":     "abs input_signal <= 2.5",
+      "description": "The rover stays near the starting point"
+    }
+  ]
+}

curiosity_rover_ogma/manifest/extra-vars.json

@@ -0,0 +1,5 @@
+{ "target_extra_dependencies": [ "nav_msgs" ]
+, "package_extra_depend": [ "nav_msgs" ]
+, "impl_extra_header": [ "#include \"nav_msgs/msg/odometry.hpp\"" ]
+, "BASE_DOCKER_IMAGE": "osrf/space-ros:curiosity_demo"
+}

curiosity_rover_ogma/manifest/project.ogma

@@ -0,0 +1,11 @@
+{
+  "projectName": "Curiosity rover demo",
+  "projectInputFiles": [ [ "document.json", "cwd:default", "literal" ] ],
+  "projectVariableFiles": null,
+  "projectVariableDBFile": "vars-db.json",
+  "projectHandlerFile": null,
+  "projectCommandPropVia": null,
+  "projectTemplateDir": null,
+  "projectTargetDir": "cwd:monitor",
+  "projectExtraJSONFile": "extra-vars.json"
+}

curiosity_rover_ogma/manifest/vars-db.json

@@ -0,0 +1,27 @@
+{ "inputs":
+     [ { "name": "input_signal"
+       , "type": "double"
+       , "active": true
+       , "connections":
+           [ { "scope": "ros/message"
+             , "topic": "/model/curiosity_mars_rover/odometry"
+             , "field": "pose.pose.position.x"
+             }
+           ]
+       }
+     ]
+, "topics":
+     [ { "scope": "ros/message"
+       , "topic": "/model/curiosity_mars_rover/odometry"
+       , "type":  "nav_msgs::msg::Odometry"
+       }
+     ]
+, "types": [
+       { "fromScope": "ros/message"
+       , "fromType":  "nav_msgs::msg::Odometry"
+       , "fromField": "pose.pose.position.x"
+       , "toScope":   "C"
+       , "toType":    "double"
+       }
+     ]
+}

curiosity_rover_ogma/run.sh

@@ -0,0 +1,21 @@
+#!/usr/bin/env bash
+
+# Runs a docker container with the image created by build.bash
+# Requires:
+#   docker
+
+IMG_NAME=osrf/space-ros-curiosity-rover-ogma
+IMG_TAG=latest
+
+# Replace `/` with `_` to comply with docker container naming
+CONTAINER_NAME="$(tr '/' '_' <<< "$IMG_NAME")"
+
+# Start the container
+docker run \
+  --rm \
+  -it \
+  --name "${CONTAINER_NAME}" \
+  --network host \
+  -e TERM \
+  "${IMG_NAME}:${IMG_TAG}" \
+  /bin/bash