Skip to content

Commit

Permalink
Merge branch 'develop-prop-name' into develop. Close #130.
Browse files Browse the repository at this point in the history
**Description**

The Spec to Copilot translator and the FPrime and ROS translators
generate handler names in slightly different ways. The latter adds an
extra `prop` to handler names, which means that the combination of both
requires a manual edit before they can be integrated.

**Type**

- Bug: backend generates incompatible code.

**Additional context**

None.

**Requester**

- Tage Andersen and Elias Evjen Hartmark (NMBU, Norway)

**Method to check presence of bug**

The following Dockerfile compiles a spec with the ROS and Copilot
standalone backends and uses the ROS tools to build the monitoring
application:

```
--- Dockerfile-verify-130
FROM ubuntu:focal

ENV DEBIAN_FRONTEND=noninteractive

RUN apt-get update
SHELL ["/bin/bash", "-c"]

RUN apt-get install --yes software-properties-common
RUN add-apt-repository universe
RUN apt-get update
RUN apt-get install curl -y
RUN curl -sSL https://raw.githubusercontent.com/ros/rosdistro/master/ros.key -o /usr/share/keyrings/ros-archive-keyring.gpg
RUN echo "deb [arch=$(dpkg --print-architecture) signed-by=/usr/share/keyrings/ros-archive-keyring.gpg] http://packages.ros.org/ros2/ubuntu $(source /etc/os-release && echo $UBUNTU_CODENAME) main" | tee /etc/apt/sources.list.d/ros2.list
RUN apt-get update
RUN apt-get upgrade -y
RUN apt-get install -y ros-foxy-ros-base python3-argcomplete
RUN apt-get install -y ros-dev-tools

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 cabal v1-install copilot-3.19
RUN apt-get install --yes git

ADD reqs.json /tmp/reqs.json
ADD variable-db /tmp/variable-db

CMD git clone $REPO && \
    cd $NAME && \
    git checkout $COMMIT && \
    cd .. && \
    cabal v1-install --force-reinstall $NAME/$PAT**/ && \
    ogma ros --fret-file-name /tmp/reqs.json --variable-db /tmp/variable-db && \
    ogma fret-component-spec --fret-file-name /tmp/reqs.json --target-file-name monitor > CS.hs && \
    cabal v1-exec -- runhaskell CS.hs && \
    mv monitor* ros/src/ && \
    cd ros/ && \
    source /opt/ros/foxy/setup.bash && \
    colcon build && \
    echo "Success"

--- reqs.json
{
  "test_componentSpec": {
    "Functions": [
    ],
    "Internal_variables": [
    ],
    "Other_variables": [
      {
        "name": "a",
        "type": "bool"
      }
    ],
    "Requirements": [
      {
        "CoCoSpecCode": "true",
        "fretish": "unimportant",
        "name": "testCopilot",
        "ptLTL": "a"
      }
    ]
  }
}

--- variables-db
("a","bool","/a","Bool")
```

Command (substitute variables based on new path after merge):

```sh
$ docker run -e "REPO=https://github.com/NASA/ogma" -e "NAME=ogma" -e PAT="ogma-" -e "COMMIT=<HASH>" -it ogma-verify-130
```

**Expected result**

Compiling the spec above using both the Copilot and the ROS backends
should produce a ROS app that includes the monitors and compiles
correctly without edits.

**Solution implemented**

Modify FPrime and ROS app generators to not include the extra `"prop"`
in handler names.

**Further notes**

None.
  • Loading branch information
ivanperez-keera committed Mar 14, 2024
2 parents 6737b53 + 8082ff8 commit dc83040
Show file tree
Hide file tree
Showing 3 changed files with 4 additions and 3 deletions.
3 changes: 2 additions & 1 deletion ogma-core/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,11 +1,12 @@
# Revision history for ogma-core

## [1.X.Y] - 2024-03-13
## [1.X.Y] - 2024-03-14

* Fix missing stream name substitution (#120).
* Use generalized JSON parser for DB Spec (#122).
* Fix translation of equivalence boolean operator from SMV (#126).
* Sanitize handler names (#127).
* Use same handler name in FPrime/ROS and Copilot (#130).

## [1.2.0] - 2024-01-21

Expand Down
2 changes: 1 addition & 1 deletion ogma-core/src/Command/FPrimeApp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -246,7 +246,7 @@ fretCSExtractHandlers (Just cs) = map handlerNameF
$ map requirementName
$ requirements cs
where
handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
handlerNameF = ("handler" ++) . sanitizeUCIdentifier

-- | Return the variable information needed to generate declarations
-- and subscriptions for a given variable name and variable database.
Expand Down
2 changes: 1 addition & 1 deletion ogma-core/src/Command/ROSApp.hs
Original file line number Diff line number Diff line change
Expand Up @@ -250,7 +250,7 @@ fretCSExtractHandlers (Just cs) = map handlerNameF
$ map requirementName
$ requirements cs
where
handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier
handlerNameF = ("handler" ++) . sanitizeUCIdentifier

-- | Return the variable information needed to generate declarations
-- and subscriptions for a given variable name and variable database.
Expand Down

0 comments on commit dc83040

Please sign in to comment.