Skip to content
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

ogma-core: Add missing notPreviousNot to generated spec. Refs #168. #169

Merged
merged 2 commits into from
Nov 22, 2024

Conversation

ivanperez-keera
Copy link
Member

Modify Copilot spec generator to include a definition for notPreviousNot, as prescribed in the solution proposed for #168.

When an input spec uses the Z SMV operator, the produced Copilot spec
refers to a function notPreviousNot that is not defined. This function
should be included in the generated spec.

This commit makes the Copilot generator include a default definition for
notPreviousNot.
@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 checks that a spec containing a Z operator, which is mapped to notPreviousNot, is translated into a Copilot spec that can be compiled, after which it prints the message "Success":
      --- Dockerfile
      FROM ubuntu:trusty
      
      ENV DEBIAN_FRONTEND=noninteractive
      
      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
      RUN apt-get install --yes git
      
      ADD zspec.json /tmp/zspec.json
      
      SHELL ["/bin/bash", "-c"]
      CMD git clone $REPO \
          && cd $NAME \
          && git checkout $COMMIT \
          && cd .. \
          && cabal v1-sandbox init \
          && cabal v1-install $NAME/$PAT**/ copilot-4.1 --constraint="aeson>=2.0.3.0" \
          && ./.cabal-sandbox/bin/ogma fret-component-spec --fret-file-name /tmp/zspec.json > Spec.hs \
          && cabal v1-exec -- runhaskell Spec.hs \
          && echo "Success"
      
      --- zspec.json
      {
        "test_componentSpec": {
          "Functions": [
          ],
          "Internal_variables": [
          ],
          "Other_variables": [
          ],
          "Requirements": [
            {
              "CoCoSpecCode": "true",
              "fretish": "unimportant",
              "name": "testCopilot-001",
              "ptLTL": "Z TRUE"
            }
          ]
        }
      }
      
      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=090d256846fb69b12fb47acf1e6dfba286e51952" -it ogma-verify-168
      
  • Implementation is documented. Details:
    No updates needed. Change is internal to module.
  • Change history is clear.
  • Commit messages are clear.
  • Changelogs are updated.
  • Examples are updated. Details:
    No updates needed. Change is internal to module.
  • Required version bumps are evaluated. Details:
    No updates needed. Change is bug fix.

@ivanperez-keera ivanperez-keera merged commit 4f0f145 into nasa:develop Nov 22, 2024
2 checks passed
@ivanperez-keera ivanperez-keera deleted the develop-notPreviousNot branch November 22, 2024 15:00
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