Merge branch 'release-1.6.0'. Refs #208.

ogma-cli/CHANGELOG.md

@@ -1,5 +1,17 @@
 # Revision history for ogma-cli
 
+## [1.6.0] - 2025-01-21
+
+* Version bump 1.6.0 (#208).
+* Update contribution guidelines (#161).
+* Provide ability to customize template in fprime command (#185).
+* Provide ability to customize template in standalone command (#189).
+* Add repository information to cabal package (#148).
+* Add version bounds to all dependencies (#119).
+* Introduce new diagram command (#194).
+* Provide ability to preprocess properties via external command (#197).
+* Extend support for file, property formats across backends (#204).
+
 ## [1.5.0] - 2024-11-21
 
 * Version bump 1.5.0 (#178).

ogma-cli/README.md

@@ -19,6 +19,9 @@ verification framework that generates hard real-time C99 code.
 - 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">
@@ -42,6 +45,7 @@ verification framework that generates hard real-time C99 code.
   - [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)
@@ -401,6 +405,7 @@ F' components are generated using the Ogma command `fprime`, which receives
 five main arguments:
 - `--app-target-dir DIR`: location where the F' application files must be
   stored.
+- `--app-template-dir DIR`: directory holding F' component source template.
 - `--variable-file FILENAME`: a file containing a list of variables that must
 be made available to the monitor.
 - `--variable-db FILENAME`: a file containing a database of known variables,
@@ -464,6 +469,67 @@ $ cat handlers
 handlerpropREQ_001
 ```
 
+### Template Customization
+
+By default, Ogma uses a pre-defined template to generate the F' monitoring
+component. It's possible to customize the output by providing a directory with
+a set of files with an F' component template, which Ogma will use instead.
+
+To choose this feature, one must call Ogma's `fprime` command with the argument
+`--app-template-dir DIR`, where `DIR` is the path to a directory containing an
+F' component specification template. For example, assuming that the directory
+`my_template` contains a custom F' component template, one can execute:
+
+```
+$ ogma fprime --app-template-dir my_template/ --handlers filename --variable-file variables --variable-db fprime-variable-db --app-target-dir fprime_demo
+```
+
+Ogma will copy the files in that directory to the target path, filling in
+several holes with specific information. For the component interface, the
+variables are:
+
+- {{{ifaceTypePorts}}}: Contain the type declarations for the types used by the
+  ports.
+
+- {{{ifaceInputPorts}}}: Contains the declarations of the `async input` port,
+  to provide information needed by the monitors.
+
+- {{{ifaceViolationEvents}}}: Contains the output port declarations, used to
+  emit property violations.
+
+For the monitor's header file, the variables are:
+
+- {{{hdrHandlers}}}: Contains the declarations of operations to execute when
+  new information is received in an input port, prior to re-evaluating the
+  monitors.
+
+For the monitor's implementation, the variables are:
+
+- {{{implInputs}}}: Contains the declarations of the variables with inputs
+  needed by the monitor.
+
+- {{{implMonitorResults}}}: Contains the declarations of boolean variables,
+  each holding the result of the evaluation of one of the monitors.
+
+- {{{implInputHandlers}}}: Contains the implementations of operations to
+  execute when new information is received in an input port, prior to
+  re-evaluating the monitors.
+
+- {{{implTriggerResultReset}}}: Contains instructions that reset the status of
+  the monitors.
+
+- {{{implTriggerChecks}}}: Contains instructions that check whether any monitor
+  has resulted in a violation and, if so, sends an event via the corresponding
+  port.
+
+- {{{implTriggers}}}: Contains the implementations of the functions that set
+  the result of a monitor evaluation to true when the Copilot implementation
+  finds a violation.
+
+We understand that this level of customization may be insufficient for your
+application. If that is the case, feel free to reach out to our team to discuss
+how we could make the template expansion system more versatile.
+
 ### Current limitations
 
 The user must place the code generated by Copilot monitors in three files,
@@ -474,6 +540,128 @@ by default by the `fprime` command.
 The code generated by default assumes that handlers receive no arguments. The
 user must modify the handlers accordingly if that is not the case.
 
+## Generating Monitors from Diagrams
+
+Apart from the backends mentioned before, Ogma includes a command to
+transform diagrams into monitors.
+
+> [!NOTE]
+> The interface for this command is preliminary. At present, this command
+> generates a standalone monitor from a state machine diagram in either
+> [mermaid](https://github.com/mermaid-js/mermaid) or
+> [DOT](https://www.graphviz.org/documentation/). If you are interested in
+> other formats and kinds of diagrams being supported, please open a discussion
+> in the Discussions tab.
+>
+> Until this capability is integrated into other backends, to generate monitors
+> from diagrams for cFS, ROS or F', use the `diagram` command, and then use the
+> command for your target platform with the argument `--variable-file`.
+
+There command `diagram` provides the ability to convert a diagram into a
+standalone monitor. The command supports the following arguments:
+
+- `--target-dir DIR`: Use this argument to provide a target directory for the
+files generated.
+- `--template-dir DIR`: Use this command to provide a custom template for the
+  code being generated. See the files under `ogma-core/templates/diagram/`, as
+well as other commands supporting template customization, to understand how to
+customize the template.
+- `--file-name FILENAME`: File with the diagram being transformed.
+- `-f,--input-format FORMAT_NAME`: Name of the input format. See below for
+  details.
+- `-p,--prop-format FORMAT_NAME`: Format for the boolean properties or
+  transition conditions in the diagram. See below for details.
+- `--target-file-name FILENAME`: Filename prefix for monitoring files in target
+  language (default: "monitor").
+- `--mode MODE`: Mode of operation (see below for details).
+- `--state-var NAME`: Name of the state variable in C (default: "state").
+- `--input-var NAME`: Name of the input variable in C, if applicable (default:
+  "input").
+
+### Input Formats
+
+At present, this command supports diagrams in
+[mermaid](https://github.com/mermaid-js/mermaid) or
+[DOT](https://www.graphviz.org/documentation/) (Graphviz). Below is an example
+of the specific format of mermaid diagram supported:
+
+```
+graph TD;
+    0-->|input > 180|1;
+    1-->|input <= 180|0;
+    0-->|input < 120|2;
+    2-->|input >= 120|0;
+```
+
+which represents the following state machine:
+
+```mermaid
+graph TD;
+    0-->|input > 180|1;
+    1-->|input <= 180|0;
+    0-->|input < 120|2;
+    2-->|input >= 120|0;
+```
+
+Each transition in the diagram takes the shape
+`Origin-->|Condition|Destination;`, where `Origin` and `Destination` are
+non-negative numbers denoting states, and `Condition` is a transition condition
+as described below under [Property Formats](#property-formats).
+
+An example of the same diagram in DOT / Graphviz follows:
+```
+digraph g{
+   rankdir="LR";
+   edge[splines="curved"]
+   0 -> 1 [label = "input > 180"];
+   1 -> 0 [label = "input <= 180"];
+   0 -> 2 [label = "input < 120"];
+   2 -> 0 [label = "input >= 120"];
+}
+```
+
+To specify the name of a specific format, use the argument `--input-format`
+followed by one of `mermaid`, `dot`, or `graphviz` (same as `dot`).
+
+### Property Formats
+
+Ogma supports transition conditions specified in multiple languages, such as:
+
+- `inputs`: The transition conditions are values of an external input variable.
+  Use the additional argument `--input-var NAME` to customize the name of such
+variable.
+
+- `literal`: The expressions should be passed literally to the target file. If
+  your monitoring language is Copilot, then the expressions should be boolean
+Copilot streams.
+
+- `smv`: The expressions are boolean SMV expressions.
+
+Use the argument `--prop-format` to customize the name of the format being
+used.
+
+### Modes of Operation
+
+The generated monitoring code can operate in one of several ways, which
+can be customized via the argument `--mode`:
+
+- `check`: Check if a system is following a state machine faithfully. It
+  triggers a violation if the system transitions into a state that does
+  not match the expected state.
+
+- `calculate`: Compute the next expected state of the state machine. Under this
+  mode the monitor always fires, and it provides as an argument the new state
+that the state machine is in.
+
+- `safeguard`: Check whether transitioning to a given state would be safe. Under
+  this mode, the monitor always fires, and it provides as arguments booleans
+indicating whether transitioning to each state would be allowed or note.  For
+example, for the diagram above, the arguments passed to the external handler
+would be three booleans, indicating, respectively, if transitioning to state 0
+would be legal, if transitioning to state 1 would be legal, and if
+transitioning to state 2 would be legal. In this mode, the machine uses the
+externally provided state to determine which state it's actually in.
+
 ## Struct Interface Generation
 
 A lot of the information that must be monitored in real-world C applications is
@@ -517,13 +705,34 @@ individual `x` and `y` fields of a `Point` in a stream.
 # Contributions
 <sup>[(Back to top)](#table-of-contents)</sup>
 
-The best way to contribute to Ogma is to report any issues you find via the
-issue tracker, and to use Ogma to build applications or in your own research
-and let us know about your results.
-
-We kindly ask users not to send PRs to this project. Instead, please document
-the bugs you find or other suggestions as issues and we will make the necessary
-changes.
+We'd love to receive your contributions, be it code fixes, new features, bug
+reports, discussions, or anything else that can help the Ogma project.
+
+If you have any comments, questions, ideas, or other topics that you think may
+be of interest, start a new discussion
+[here](https://github.com/nasa/ogma/discussions).
+
+If you would like to contribute a fix for an issue, please comment on the issue
+indicating that you want to fix it so that we can assign it to you and track
+the status on our end. If the issue does not exist, create it first or ask that
+an existing discussion be promoted to an issue.
+
+If you are unsure about whether your submission should be filed as an issue or
+as a discussion, file it as a discussion. We can always move it later.
+
+To facilitate merging any pull requests that you send, please:
+- Reference the issue you are addressing with the text `Refs #<ISSUENUMBER>.`
+  at the end of the subject line of each commit message, in *every commit*.
+  Replace `<ISSUENUMBER>` with the number of the specific issue that your pull
+  request is addressing.
+- Describe what each commit does individually *in the commit's message*. It's
+  best to err on the side of being more descriptive than less.
+- Update the CHANGELOGs in the *last commit(s)*.
+
+You can take a look at the repository's [commit
+history](https://github.com/nasa/ogma/commits/develop/) to better
+understand the process we follow. Click on each commit to see how we write
+commit messages.
 
 # Acknowledgements
 <sup>[(Back to top)](#table-of-contents)</sup>

ogma-cli/examples/diagram-copilot.dot

@@ -0,0 +1,8 @@
+digraph g{
+   rankdir="LR";
+   edge[splines="curved"]
+   0 -> 1 [label = "input > 180"];
+   1 -> 0 [label = "input <= 180"];
+   0 -> 2 [label = "input < 120"];
+   2 -> 0 [label = "input >= 120"];
+}

ogma-cli/examples/diagram-inputs.dot

@@ -0,0 +1,8 @@
+digraph g{
+   rankdir="LR";
+   edge[splines="curved"]
+   0 -> 1 [label = "10"];
+   1 -> 0 [label = "0"];
+   0 -> 2 [label = "20"];
+   2 -> 0 [label = "0"];
+}

ogma-cli/examples/diagram-smv.dot

@@ -0,0 +1,8 @@
+digraph g{
+   rankdir="LR";
+   edge[splines="curved"]
+   0 -> 1 [label = "input > 180"];
+   1 -> 0 [label = "input <= 180"];
+   0 -> 2 [label = "input < 120"];
+   2 -> 0 [label = "input >= 120"];
+}

ogma-cli/examples/mermaid-copilot.txt

@@ -0,0 +1,6 @@
+graph TD;
+    1-->|input > 10|2;
+    2-->|input > 20|3;
+    3-->|input > 30|3;
+    3-->|input > 40|4;
+    4-->|true|4;

ogma-cli/examples/mermaid-inputs.txt

@@ -0,0 +1,6 @@
+graph TD;
+    1-->|2|2;
+    2-->|2|3;
+    3-->|2|3;
+    3-->|1|4;
+    4-->|3|4;

ogma-cli/examples/mermaid-smv.txt

@@ -0,0 +1,6 @@
+graph TD;
+    1-->|input > 10|2;
+    2-->|input > 20|3;
+    3-->|input > 30|3;
+    3-->|input > 40|4;
+    4-->|TRUE|4;