ogma

# OGMA

Ogma is a tool to facilitate the integration of safe runtime monitors into
other systems. Ogma extends
[Copilot](https://github.com/Copilot-Language/copilot), a high-level runtime
verification framework that generates hard real-time C99 code.

# Features

- Generating [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) runtime
  monitoring applications that monitor data received from the message bus.

- Generating [Robot Operating System](https://ros.org) runtime monitoring
  applications.

- Generating [F' (F Prime)](https://github.com/nasa/fprime/) runtime monitoring
  components.

- Generating message handlers for NASA Core Flight System applications to make
  external data in structs available to a Copilot monitor.

- Generating monitors from diagrams in diagrammatic formats (e.g.,
  DOT/Graphviz, mermaid).

- Generating the glue code necessary to work with C structs in Copilot.

<p align="center">
  <img src="https://raw.githubusercontent.com/nasa/ogma/gh-pages/images/simulator.gif" alt="Monitoring within simulation video">
  <br />
  <i>Integration of monitors into larger applications (e.g., simulators).</i>
</p>

<p align="center">
  <img src="https://raw.githubusercontent.com/nasa/ogma/gh-pages/images/ros.gif" alt="Monitoring within ROS simulation video">
  <br />
  <i>Integration of monitors into robotics applications.</i>
</p>

## Table of Contents

- [Installation](#installation)
  - [Linux installation](#linux-installation)
  - [Mac installation](#mac-installation)
  - [Troubleshooting](#troubleshooting)
- [Usage](#usage)
  - [cFS Application Generation](#cfs-application-generation)
  - [ROS Application Generation](#ros-application-generation)
  - [F' Component Generation](#f-component-generation)
  - [Generating Monitors from Diagrams](#generating-monitors-from-diagrams)
  - [Struct Interface Generation](#struct-interface-generation)
- [Contributions](#contributions)
- [Acknowledgements](#acknowledgements)
- [License](#license)

# Installation
<sup>[(Back to top)](#table-of-contents)</sup>

## Linux Installation
<sup>[(Back to top)](#table-of-contents)</sup>

### Ubuntu 25.10 / Debian Forky or newer

On Ubuntu 25.10 / Debian Forky or newer, Ogma can be installed directly from
the package repositories with:

```sh
$ sudo apt-get install ogma
```

To test that Ogma is available, execute the following to print the list of
commands supported:

```sh
$ ogma --help
```

### Other Linux distributions

On other Linux distributions or older Debian-based distributions, to use Ogma
you must compile it from source, for which you need a number of pre-requisites,
such as a Haskell compiler (GHC) and the package manager Cabal
(`cabal-install`), the libraries `bz2` and `expat`, and the theorem prover
`z3`. At this time, we recommend GHC 8.6 and a version of `cabal-install`
between 2.4 and 3.2. (Ogma has been tested with GHC versions up to 9.2 and
cabal-install versions up to 3.6, although the installation steps may vary
slightly depending