ogma-core 1.0.8 → 1.0.9

raw patch · 8 files changed

+44/−12 lines, 8 filesdep ~ogma-extradep ~ogma-language-cdep ~ogma-language-cocospec

Dependency ranges changed: ogma-extra, ogma-language-c, ogma-language-cocospec, ogma-language-copilot, ogma-language-fret-cs, ogma-language-fret-reqs, ogma-language-smv

Files

• CHANGELOG.md +6/−0
• ogma-core.cabal +8/−8
• src/Command/FRETComponentSpec2Copilot.hs +2/−0
• src/Command/FRETReqsDB2Copilot.hs +2/−0
• src/Language/Trans/CoCoSpec2Copilot.hs +2/−0
• src/Language/Trans/FRETComponentSpec2Copilot.hs +10/−1
• src/Language/Trans/FRETReqsDB2Copilot.hs +12/−3
• tests/Main.hs +2/−0

@@ -1,5 +1,11 @@ # Revision history for ogma-core +## [1.0.9] - 2023-05-21++* Version bump 1.0.9 (#93).+* Allow customizing the names of the C files generated by Copilot (#80).+* Translate ZtoPre and YtoPre to Copilot (#86).+ ## [1.0.8] - 2023-03-21  * Version bump 1.0.8 (#81).

@@ -32,7 +32,7 @@ build-type:          Simple  name:                ogma-core-version:             1.0.8+version:             1.0.9 homepage:            http://nasa.gov license:             OtherLicense license-file:        LICENSE.pdf@@ -109,13 +109,13 @@     , IfElse     , mtl -    , ogma-extra              >= 1.0.8 && < 1.1-    , ogma-language-c         >= 1.0.8 && < 1.1-    , ogma-language-cocospec  >= 1.0.8 && < 1.1-    , ogma-language-copilot   >= 1.0.8 && < 1.1-    , ogma-language-fret-cs   >= 1.0.8 && < 1.1-    , ogma-language-fret-reqs >= 1.0.8 && < 1.1-    , ogma-language-smv       >= 1.0.8 && < 1.1+    , ogma-extra              >= 1.0.9 && < 1.1+    , ogma-language-c         >= 1.0.9 && < 1.1+    , ogma-language-cocospec  >= 1.0.9 && < 1.1+    , ogma-language-copilot   >= 1.0.9 && < 1.1+    , ogma-language-fret-cs   >= 1.0.9 && < 1.1+    , ogma-language-fret-reqs >= 1.0.9 && < 1.1+    , ogma-language-smv       >= 1.0.9 && < 1.1    hs-source-dirs:     src

@@ -94,6 +94,7 @@   { fretCS2CopilotUseCoCoSpec :: Bool   , fretCS2CopilotIntType     :: String   , fretCS2CopilotRealType    :: String+  , fretCS2CopilotFilename    :: String   }  -- | Parse a JSON file containing a FRET component specification.@@ -130,6 +131,7 @@       (fretCS2CopilotUseCoCoSpec options)       (fretCS2CopilotIntType options)       (fretCS2CopilotRealType options)+      (fretCS2CopilotFilename options)  -- * Result 

@@ -93,6 +93,7 @@ -- to Copilot code. data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions   { fretReqsDB2CopilotUseCoCoSpec :: Bool+  , fretReqsDB2CopilotFilename    :: String   }  -- | Parse a JSON file containing a FRET requirement database.@@ -127,6 +128,7 @@ fretReqsDB2CopilotOptions options =   T.FRETReqsDB2CopilotOptions       (fretReqsDB2CopilotUseCoCoSpec options)+      (fretReqsDB2CopilotFilename options)  -- * Result 

@@ -130,6 +130,8 @@ -- operator. opOnePre2Copilot :: Op1Pre -> String opOnePre2Copilot Op1Pre    = "pre"+opOnePre2Copilot Op1YtoPre = "pre"+opOnePre2Copilot Op1ZtoPre = "tpre" opOnePre2Copilot Op1Once   = "PTLTL.eventuallyPrev" opOnePre2Copilot Op1Hist   = "PTLTL.alwaysBeen" opOnePre2Copilot Op1Y      = "PTLTL.previous"

@@ -57,6 +57,7 @@   { fretCS2CopilotUseCoCoSpec :: Bool   , fretCS2CopilotIntType     :: String   , fretCS2CopilotRealType    :: String+  , fretCS2CopilotFilename    :: String   }  -- | Transform a FRET TL specification into a Copilot specification.@@ -86,6 +87,7 @@       , pure clock       , pure ftp       , pure pre+      , pure tpre       , pure spec       , pure main'       ]@@ -222,6 +224,12 @@           , "pre = ([False] ++)"           ] +    -- Auxiliary streams: tpre+    tpre = [ ""+           , "tpre :: Stream Bool -> Stream Bool"+           , "tpre = ([True] ++)"+           ]+     -- Main specification     spec :: [String]     spec = [ ""@@ -249,7 +257,8 @@     main' :: [String]     main' = [ ""             , "main :: IO ()"-            , "main = reify spec >>= compile \"fret\""+            , "main = reify spec >>= compile \""+                 ++ fretCS2CopilotFilename prefs ++ "\""             ]  -- | Return the corresponding type in Copilot matching a given FRET type.

@@ -62,6 +62,7 @@ -- to Copilot code. data FRETReqsDB2CopilotOptions = FRETReqsDB2CopilotOptions   { fretReqsDB2CopilotUseCoCoSpec :: Bool+  , fretReqsDB2CopilotFilename    :: String   }  -- | Return a string with the contents of the Copilot module that implements a@@ -93,10 +94,12 @@                               else SMV.boolSpecNames smvSpec      sections | fretReqsDB2CopilotUseCoCoSpec prefs-             = [ imports, propDef, externs, clock, ftp, undef, spec, main' ]+             = [ imports, propDef, externs, clock, ftp, undef, tpre, spec+               , main'+               ]               | otherwise-             = [ imports, propDef, externs, clock, ftp, spec, main' ]+             = [ imports, propDef, externs, clock, ftp, tpre, spec, main' ]      imports :: [String]     imports =@@ -144,6 +147,11 @@                , "pre = undefined"                ] +    tpre     = [ ""+               , "tpre :: Stream Bool -> Stream Bool"+               , "tpre = ([True] ++)"+               ]+     spec     = [ ""                , "-- | Complete specification. Calls the C function void handler(); when"                , "-- the property is violated."@@ -155,5 +163,6 @@      main'    = [ ""                , "main :: IO ()"-               , "main = reify spec >>= compile \"fret\""+               , "main = reify spec >>= compile \""+                    ++ fretReqsDB2CopilotFilename prefs ++ "\""                ]

@@ -110,6 +110,7 @@                  { fretCS2CopilotUseCoCoSpec = False                  , fretCS2CopilotIntType     = "Int64"                  , fretCS2CopilotRealType    = "Float"+                 , fretCS2CopilotFilename    = "fret"                  }     result <- fretComponentSpec2Copilot file opts @@ -139,6 +140,7 @@ testFretReqsDBCoCoSpec2Copilot file success = do     let opts = FRETReqsDB2CopilotOptions                  { fretReqsDB2CopilotUseCoCoSpec = True+                 , fretReqsDB2CopilotFilename    = "fret"                  }     result <- fretReqsDB2Copilot file opts