Skip to content

Commit

Permalink
ogma-core: Add import of Copilot's MTL module to Reqs DB translation.…
Browse files Browse the repository at this point in the history
… Refs nasa#101.

The translation of FRET Requirement DBs to Copilot may produce specs that use
operators from the MTL module. However, that module is not being imported.

This commit modifies the translator from FRET Requirement DBs to Copilot so
that the MTL module is imported qualified.
  • Loading branch information
ivanperez-keera committed Sep 22, 2023
1 parent 928b42f commit 9735e6e
Showing 1 changed file with 1 addition and 0 deletions.
1 change: 1 addition & 0 deletions ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs
Original file line number Diff line number Diff line change
Expand Up @@ -112,6 +112,7 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections
, "import Copilot.Library.PTLTL (since, previous,"
++ " alwaysBeen)"
, "import qualified Copilot.Library.PTLTL as PTLTL"
, "import qualified Copilot.Library.MTL as MTL"
, "import Language.Copilot (reify)"
, "import Prelude hiding ((&&), (||), (++), (<=), (>=),"
++ " (<), (>), (==), (/=), not)"
Expand Down

0 comments on commit 9735e6e

Please sign in to comment.