ogma-core: Including missing operator notPreviousNot in generated spec

[ivanperez-keera]

Description

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.

Type

• Bug: Ogma produces invalid code.

Additional context

None.

Requester

• Ivan Perez.

Method to check presence of bug

Compiling the following spec produces an invalid Copilot module:

{
  "test_componentSpec": {
    "Functions": [
    ],
    "Internal_variables": [
    ],
    "Other_variables": [
    ],
    "Requirements": [
      {
        "CoCoSpecCode": "true",
        "fretish": "unimportant",
        "name": "testCopilot-001",
        "ptLTL": "Z TRUE"
      }
    ]
  }
}

Monitor.hs:17:24: error:
    Variable not in scope: notPreviousNot :: Stream Bool -> Stream Bool
   |
17 | propTestCopilot_001 = (notPreviousNot true)

Expected result

The execution above should produce a Copilot specification that can be compiled and where notPreviousNot has been defined.

Desired result

The execution above should produce a Copilot specification that can be compiled and where notPreviousNot has been defined.

Proposed solution

Add a definition for notPreviousNot to the generated Copilot spec.

Further notes

None.

[ivanperez-keera]

Change Manager: Confirmed that the issue exists.

[ivanperez-keera]

Technical Lead: Confirmed that the issue should be addressed.

[ivanperez-keera]

Technical Lead: Issue scheduled for fixing in Ogma 1.5.

Fix assigned to: @ivanperez-keera .

[ivanperez-keera]

Implementor: Solution implemented, review requested.

[ivanperez-keera]

Change Manager: Verified that:

• Solution is implemented:
  • The code proposed compiles and passes all tests. Details:
    • Build logs:
      • https://github.com/nasa/ogma/actions/runs/11966197649/job/33361417813
      • https://github.com/nasa/ogma/actions/runs/11966197650/job/33361417794
    • Build log archives:
      • logs_31199025145.zip
      • logs_31199025147.zip
  • 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]

Change Manager: Implementation ready to be merged.