From 4c5a5a1150bf4a1da134f9ac3ca2cd830a0f26ef Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sat, 1 Aug 2026 13:54:45 -0700 Subject: [PATCH 1/4] curiosity_rover_ogma: Add Gitignore file (#159). --- curiosity_rover_ogma/.gitignore | 23 +++++++++++++++++++++++ 1 file changed, 23 insertions(+) create mode 100644 curiosity_rover_ogma/.gitignore diff --git a/curiosity_rover_ogma/.gitignore b/curiosity_rover_ogma/.gitignore new file mode 100644 index 00000000..4c9e245b --- /dev/null +++ b/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.* From 5aca7af3806c5404e916b1c6842d92acdfef100d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 24 Jul 2026 11:30:40 -0700 Subject: [PATCH 2/4] curiosity_rover_ogma: Add Ogma project, auxiliary files (#159). --- curiosity_rover_ogma/manifest/document.json | 10 +++++++ curiosity_rover_ogma/manifest/extra-vars.json | 5 ++++ curiosity_rover_ogma/manifest/project.ogma | 11 ++++++++ curiosity_rover_ogma/manifest/vars-db.json | 27 +++++++++++++++++++ 4 files changed, 53 insertions(+) create mode 100644 curiosity_rover_ogma/manifest/document.json create mode 100644 curiosity_rover_ogma/manifest/extra-vars.json create mode 100644 curiosity_rover_ogma/manifest/project.ogma create mode 100644 curiosity_rover_ogma/manifest/vars-db.json diff --git a/curiosity_rover_ogma/manifest/document.json b/curiosity_rover_ogma/manifest/document.json new file mode 100644 index 00000000..75054528 --- /dev/null +++ b/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" + } + ] +} diff --git a/curiosity_rover_ogma/manifest/extra-vars.json b/curiosity_rover_ogma/manifest/extra-vars.json new file mode 100644 index 00000000..bcbef138 --- /dev/null +++ b/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" +} diff --git a/curiosity_rover_ogma/manifest/project.ogma b/curiosity_rover_ogma/manifest/project.ogma new file mode 100644 index 00000000..ed06fdcd --- /dev/null +++ b/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" +} diff --git a/curiosity_rover_ogma/manifest/vars-db.json b/curiosity_rover_ogma/manifest/vars-db.json new file mode 100644 index 00000000..080b747d --- /dev/null +++ b/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" + } + ] +} From 2db6052bded23ddabecea67254ebbf3c1a5a11dc Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 24 Aug 2026 11:15:34 -0700 Subject: [PATCH 3/4] curiosity_rover_ogma: Add build scripts (#159). Add dockerfile that builds Ogma. Add build scripts that build both Ogma and the generated app. --- curiosity_rover_ogma/Dockerfile | 75 +++++++++++++++++++++++++++++++++ curiosity_rover_ogma/build.sh | 49 +++++++++++++++++++++ curiosity_rover_ogma/run.sh | 21 +++++++++ 3 files changed, 145 insertions(+) create mode 100644 curiosity_rover_ogma/Dockerfile create mode 100755 curiosity_rover_ogma/build.sh create mode 100755 curiosity_rover_ogma/run.sh diff --git a/curiosity_rover_ogma/Dockerfile b/curiosity_rover_ogma/Dockerfile new file mode 100644 index 00000000..681e1f23 --- /dev/null +++ b/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 / diff --git a/curiosity_rover_ogma/build.sh b/curiosity_rover_ogma/build.sh new file mode 100755 index 00000000..82e903fd --- /dev/null +++ b/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! #####" diff --git a/curiosity_rover_ogma/run.sh b/curiosity_rover_ogma/run.sh new file mode 100755 index 00000000..75ede6df --- /dev/null +++ b/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 From 24109c76877d33c349ce248ae440d1fd14b5b318 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Mon, 24 Aug 2026 11:20:59 -0700 Subject: [PATCH 4/4] curiosity_rover_ogma: Add README (#159). --- curiosity_rover_ogma/README.md | 112 +++++++++++++++++++++++++++++++++ 1 file changed, 112 insertions(+) create mode 100644 curiosity_rover_ogma/README.md diff --git a/curiosity_rover_ogma/README.md b/curiosity_rover_ogma/README.md new file mode 100644 index 00000000..0f6336c2 --- /dev/null +++ b/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.