Skip to content

ogma-cli: Add new diagram command. Refs #194. #195

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 7 commits into from
Jan 12, 2025

Conversation

ivanperez-keera
Copy link
Member

Add new command to transform diagrams into Copilot monitors, as prescribed in the solution proposed for #194.

…nasa#194.

We have determined that supporting transforming diagrams into monitors
would generally be useful for Ogma and related projects. A way to
support providing input files using diagrammatic formats should be
added.

This commit adds a new command at core level capable of transforming
diagrams in mermaid or DOT / Graphviz into standalone monitors.
Properties can be specified as boolean expressions in SMV, CoCoSpec, as
literal integers, or as literal expressions. The latter are copied
verbatim to the output Copilot module.
We have determined that supporting transforming diagrams into monitors
would generally be useful for Ogma and related projects. A way to
support providing input files using diagrammatic formats should be
added.

A prior commit has added a command at ogma-core level to transform
diagrams into standalone monitors.

This commit exposes the command from ogma-core to the user in the
command-line interface.
We have determined that supporting transforming diagrams into monitors
would generally be useful for Ogma and related projects. A way to
support providing input files using diagrammatic formats should be
added.

Prior commits have introduced a new command to transform different
kinds of graphical notations and property formats into monitors.

This commit adds several sample diagrams that users can follow to
understand the format supported by Ogma.
We have determined that supporting transforming diagrams into monitors
would generally be useful for Ogma and related projects. A way to
support providing input files using diagrammatic formats should be
added.

Prior commits have introduced a new command to transform different
kinds of graphical notations and property formats into monitors.

This commit updates the package description in the cabal file to
document that capability.
We have determined that supporting transforming diagrams into monitors
would generally be useful for Ogma and related projects. A way to
support providing input files using diagrammatic formats should be
added.

Prior commits have introduced a new command to transform different
kinds of graphical notations and property formats into monitors.

This commit updates the README to document that capability and
explain how to use it.
@ivanperez-keera
Copy link
Member Author

Change Manager: For consistency, the CHANGELOG entry in ogma-core and the summary line in the only commit related to ogma-core should match.

@ivanperez-keera
Copy link
Member Author

Implementor: Fix implemented, review requested.

@ivanperez-keera
Copy link
Member Author

Change Manager: Verified that:

  • Solution is implemented:
    • The code proposed compiles and passes all tests. Details:
    • The solution proposed produces the expected result. Details:
      The following Dockerfile uses the new command to transform 6 diagrams with different formats and different property formats into monitors, and checks that the resulting Copilot code compiles correctly, after which it prints the message "Success":
      FROM ubuntu:trusty
      
      RUN apt-get update
      
      RUN apt-get install --yes software-properties-common
      RUN add-apt-repository ppa:hvr/ghc
      RUN apt-get update
      
      RUN apt-get install --yes ghc-8.6.5 cabal-install-2.4
      RUN apt-get install --yes libz-dev
      
      ENV PATH=/opt/ghc/8.6.5/bin:/opt/cabal/2.4/bin:$PWD/.cabal-sandbox/bin:$PATH
      
      RUN cabal update
      RUN cabal v1-sandbox init
      RUN cabal v1-install alex happy --constraint='happy < 2.0'
      RUN apt-get install --yes git
      
      CMD git clone $REPO && \
          cd $NAME && \
          git checkout $COMMIT && \
          cd .. && \
          cabal v1-install copilot-4.2 $NAME/$PAT**/ --enable-tests && \
          ogma diagram --target-dir graphviz-smv-monitor     --file-name $NAME/ogma-cli/examples/diagram-smv.dot     -f dot --prop-format smv \
          ogma diagram --target-dir graphviz-copilot-monitor --file-name $NAME/ogma-cli/examples/diagram-copilot.dot -f dot --prop-format literal \
          ogma diagram --target-dir graphviz-inputs-monitor  --file-name $NAME/ogma-cli/examples/diagram-inputs.dot  -f dot --prop-format inputs \
          ogma diagram --target-dir mermaid-smv-monitor      --file-name $NAME/ogma-cli/examples/mermaid-smv.txt     -f mermaid --prop-format smv \
          ogma diagram --target-dir mermaid-copilot-monitor  --file-name $NAME/ogma-cli/examples/mermaid-copilot.txt -f mermaid --prop-format literal \
          ogma diagram --target-dir mermaid-inputs-monitor   --file-name $NAME/ogma-cli/examples/mermaid-inputs.txt  -f mermaid --prop-format inputs \
          cabal v1-exec -- runhaskell graphviz-smv-monitor/Copilot.hs && \
          cabal v1-exec -- runhaskell graphviz-copilot-monitor/Copilot.hs && \
          cabal v1-exec -- runhaskell graphviz-inputs-monitor/Copilot.hs && \
          cabal v1-exec -- runhaskell mermaid-smv-monitor/Copilot.hs && \
          cabal v1-exec -- runhaskell mermaid-copilot-monitor/Copilot.hs && \
          cabal v1-exec -- runhaskell mermaid-inputs-monitor/Copilot.hs && \
          echo "Success"
      Command (substitute variables based on new path after merge):
      $ docker run -e "REPO=https://github.com/ivanperez-keera/ogma" -e "NAME=ogma" -e "PAT=ogma"  -e "COMMIT=923b173f936be45b9f3fb14ed8a70ce75cda9272" -it ogma-verify-194
      
  • Implementation is documented. Details:
    All new modules and top-level definitions include documentation. The README and cabal file for ogma-cli are updated to document the new functionality.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    New examples are introduced to demonstrate new capabilities.
  • Required version bumps are evaluated. Details:
    Bump not required (API is backwards compatible and dependencies are extended).

@ivanperez-keera ivanperez-keera merged commit 7a74fd5 into nasa:develop Jan 12, 2025
2 checks passed
@ivanperez-keera ivanperez-keera deleted the develop-diagrams branch January 12, 2025 18:44
@ivanperez-keera ivanperez-keera changed the title ogma-cli: Add new diagram command ogma-cli: Add new diagram command. Refs #194. Jan 19, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant