From ec6cb87cf1479fc4bff8509ab076011cd72d2d4f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 22 Jan 2023 04:19:38 +0000 Subject: [PATCH 01/51] ogma-language-smv: Add not-equal operator to SMV grammar. Refs #71. Requirements that contain the not-equal binary operator in TL formulas fail to be parsed correctly by Ogma. This commit modifies the SMV grammar so that inequality is supported by the encoding of the language. --- ogma-language-smv/grammar/SMV.cf | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-language-smv/grammar/SMV.cf b/ogma-language-smv/grammar/SMV.cf index d043452d..fde05f0b 100644 --- a/ogma-language-smv/grammar/SMV.cf +++ b/ogma-language-smv/grammar/SMV.cf @@ -93,6 +93,7 @@ _ . Number ::= "" Number ""; OrdOpLT . OrdOp ::= "<"; OrdOpLE . OrdOp ::= "<="; OrdOpEQ . OrdOp ::= "="; +OrdOpNE . OrdOp ::= "!="; OrdOpGT . OrdOp ::= ">"; OrdOpGE . OrdOp ::= ">="; From 2ce4277c81d879afd1d5f6797c4baa0c91439ada Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Sun, 22 Jan 2023 04:19:50 +0000 Subject: [PATCH 02/51] ogma-core: Translate not-equal operator from SMV to Copilot. Refs #71. Requirements that contain the not-equal binary operator in TL formulas fail to be parsed correctly by Ogma. This commit adds the translation of SMV's inequality operator != into Copilot's /= operator. --- ogma-core/src/Language/Trans/SMV2Copilot.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-core/src/Language/Trans/SMV2Copilot.hs b/ogma-core/src/Language/Trans/SMV2Copilot.hs index 45ee30b2..b39f3d6a 100644 --- a/ogma-core/src/Language/Trans/SMV2Copilot.hs +++ b/ogma-core/src/Language/Trans/SMV2Copilot.hs @@ -134,6 +134,7 @@ ordOp2Copilot :: OrdOp -> String ordOp2Copilot OrdOpLT = "<" ordOp2Copilot OrdOpLE = "<=" ordOp2Copilot OrdOpEQ = "==" +ordOp2Copilot OrdOpNE = "/=" ordOp2Copilot OrdOpGT = ">" ordOp2Copilot OrdOpGE = ">=" From c35347acfb36d74a91f75a113c87e6a9888c8200 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 1 Feb 2023 13:49:25 +0000 Subject: [PATCH 03/51] ogma-language-cocospec: Add not-equal operator to CoCoSpec grammar. Refs #71. Requirements that contain the not-equal binary operator in TL formulas fail to be parsed correctly by Ogma. This commit modifies the CoCoSpec grammar so that inequality is supported by the encoding of the language. --- ogma-language-cocospec/grammar/CoCoSpec.cf | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-language-cocospec/grammar/CoCoSpec.cf b/ogma-language-cocospec/grammar/CoCoSpec.cf index 46f39eed..be383903 100644 --- a/ogma-language-cocospec/grammar/CoCoSpec.cf +++ b/ogma-language-cocospec/grammar/CoCoSpec.cf @@ -81,6 +81,7 @@ NumOp2Minus. NumOp2In ::= "-" ; NumOp2Mult . NumOp2In ::= "*" ; BoolNumOp2Eq . BoolNumOp ::= "=" ; +BoolNumOp2Ne . BoolNumOp ::= "<>" ; BoolNumOp2Le . BoolNumOp ::= "<=" ; BoolNumOp2Lt . BoolNumOp ::= "<" ; BoolNumOp2Gt . BoolNumOp ::= ">" ; From fbdfe779d60acf82eadba086b02834dccf8591dd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 1 Feb 2023 13:50:38 +0000 Subject: [PATCH 04/51] ogma-core: Translate not-equal operator from CoCoSpec to Copilot. Refs #71. Requirements that contain the not-equal binary operator in TL formulas fail to be parsed correctly by Ogma. This commit adds the translation of CoCoSpec's inequality operator <> into Copilot's /= operator. --- ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs b/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs index 3711f797..f0894b9f 100644 --- a/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs +++ b/ogma-core/src/Language/Trans/CoCoSpec2Copilot.hs @@ -113,6 +113,7 @@ numOpTwoIn2Copilot NumOp2Mult = "*" -- operator. opTwoNum2Copilot :: BoolNumOp -> String opTwoNum2Copilot BoolNumOp2Eq = "==" +opTwoNum2Copilot BoolNumOp2Ne = "/=" opTwoNum2Copilot BoolNumOp2Le = "<=" opTwoNum2Copilot BoolNumOp2Lt = "<" opTwoNum2Copilot BoolNumOp2Gt = ">=" From 950667844d0903505b62e7de85473c66a2b49521 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 1 Feb 2023 13:44:56 +0000 Subject: [PATCH 05/51] ogma-core: Hide (/=) from Prelude in generated Copilot code. Refs #71. Ogma translates FRET's not-equal operator as Copilot's (/=), which clashes with the Prelude's. This commit hides that import from the Prelude in generated Copilot code. --- ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs | 2 +- ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs b/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs index 61a379de..c082cc51 100644 --- a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs +++ b/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs @@ -107,7 +107,7 @@ fretComponentSpec2Copilot' prefs fretComponentSpec = , "import qualified Copilot.Library.MTL as MTL" , "import Language.Copilot (reify)" , "import Prelude hiding ((&&), (||), (++)," - ++ " (<=), (>=), (<), (>), (==), not)" + ++ " (<=), (>=), (<), (>), (==), (/=), not)" , "" ] diff --git a/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs b/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs index f99af9c0..1febbf99 100644 --- a/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs +++ b/ogma-core/src/Language/Trans/FRETReqsDB2Copilot.hs @@ -111,7 +111,7 @@ fret2CopilotModule' prefs smvSpec cocoSpec = unlines $ concat sections , "import qualified Copilot.Library.PTLTL as PTLTL" , "import Language.Copilot (reify)" , "import Prelude hiding ((&&), (||), (++), (<=), (>=)," - ++ " (<), (>), (==), not)" + ++ " (<), (>), (==), (/=), not)" , "" ] From 03539f89df0c59ea8e55daf878051103092fef1f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 1 Feb 2023 13:52:19 +0000 Subject: [PATCH 06/51] ogma-language-smv: Document changes in CHANGELOG. Refs #71. --- ogma-language-smv/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-language-smv/CHANGELOG.md b/ogma-language-smv/CHANGELOG.md index 2562a511..4e96a09f 100644 --- a/ogma-language-smv/CHANGELOG.md +++ b/ogma-language-smv/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-smv +## [1.X.Y] - 2023-02-01 + +* Support inequality operator (#71). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). * Specify upper bound constraint for Cabal. Refs #69. From eb0b032cbdcab839475ce208c1c9f37fdb2e82d1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 1 Feb 2023 13:52:41 +0000 Subject: [PATCH 07/51] ogma-language-cocospec: Document changes in CHANGELOG. Refs #71. --- ogma-language-cocospec/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-language-cocospec/CHANGELOG.md b/ogma-language-cocospec/CHANGELOG.md index 41f19dfa..485f69e4 100644 --- a/ogma-language-cocospec/CHANGELOG.md +++ b/ogma-language-cocospec/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-cocospec +## [1.X.Y] - 2023-02-01 + +* Support inequality operator (#71). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). * Specify upper bound constraint for Cabal. Refs #69. From 393cb1eda1034bbacfa0f3935bf3dc58c4d2173d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 1 Feb 2023 13:53:15 +0000 Subject: [PATCH 08/51] ogma-core: Document changes in CHANGELOG. Refs #71. --- ogma-core/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 3931e684..386c63fa 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-core +## [1.X.Y] - 2023-02-01 + +* Support inequality operator in SMV and CoCoSpec (#71). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). * Introduce new ROS2 backend (#56). From e43c183a8f3bfb53a773961e47319013bf696f3c Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 20 May 2022 09:53:35 -0400 Subject: [PATCH 09/51] ogma-core: Introduce command for FPrime monitoring package generation. Refs #77. This commit adds a new command the ogma's core that generates an FPrime monitoring component that exposes ports for input data, as well as one a command to execute the monitors when desired, reports any violations. --- ogma-core/ogma-core.cabal | 4 + ogma-core/src/Command/FPrimeApp.hs | 739 ++++++++++++++++++++ ogma-core/templates/fprime/CMakeLists.txt | 9 + ogma-core/templates/fprime/Dockerfile | 49 ++ ogma-core/templates/fprime/instance-copilot | 3 + 5 files changed, 804 insertions(+) create mode 100644 ogma-core/src/Command/FPrimeApp.hs create mode 100644 ogma-core/templates/fprime/CMakeLists.txt create mode 100644 ogma-core/templates/fprime/Dockerfile create mode 100644 ogma-core/templates/fprime/instance-copilot diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index df5f951e..85dfa7d4 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -63,12 +63,16 @@ data-files: templates/copilot-cfs/CMakeLists.txt templates/ros/CMakeLists.txt templates/ros/src/.keep templates/ros/package.xml + templates/fprime/CMakeLists.txt + templates/fprime/Dockerfile + templates/fprime/instance-copilot library exposed-modules: Command.CFSApp Command.CStructs2Copilot Command.CStructs2MsgHandlers + Command.FPrimeApp Command.FRETComponentSpec2Copilot Command.FRETReqsDB2Copilot Command.Result diff --git a/ogma-core/src/Command/FPrimeApp.hs b/ogma-core/src/Command/FPrimeApp.hs new file mode 100644 index 00000000..66d060f1 --- /dev/null +++ b/ogma-core/src/Command/FPrimeApp.hs @@ -0,0 +1,739 @@ +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY +-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A +-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE +-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF +-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN +-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR +-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR +-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, +-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING +-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES +-- IT "AS IS." +-- +-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS +-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN +-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, +-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S +-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE +-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY +-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY +-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS +-- AGREEMENT. +-- +-- | Create components that subscribe +-- to obtain data and call Copilot when new values arrive. + +{- HLINT ignore "Functor law" -} +module Command.FPrimeApp + ( fprimeApp + , ErrorCode + ) + where + +-- External imports +import qualified Control.Exception as E +import Control.Monad.Except ( ExceptT, liftEither, liftIO, runExceptT, + throwError ) +import Data.Aeson ( eitherDecode ) +import Data.Char ( toUpper ) +import Data.List ( find, intercalate, nub, sort ) +import Data.Maybe ( fromMaybe ) +import System.FilePath ( () ) + +-- External imports: auxiliary +import Data.ByteString.Extra as B ( safeReadFile ) +import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier ) +import System.Directory.Extra ( copyDirectoryRecursive ) + +-- Internal imports: auxiliary +import Command.Result ( Result (..) ) +import Data.Location ( Location (..) ) +import Language.FRETComponentSpec.AST ( FRETComponentSpec, + fretExternalVariableName, + fretExternalVariables, + fretRequirementName, fretRequirements ) + +-- Internal imports +import Paths_ogma_core ( getDataDir ) + +-- * FPrime component generation + +-- | Generate a new FPrime component connected to Copilot. +fprimeApp :: FilePath -- ^ Target directory where the component + -- should be created. + -> Maybe FilePath -- ^ FRET Component specification file. + -> Maybe FilePath -- ^ File containing a list of variables to make + -- available to Copilot. + -> Maybe FilePath -- ^ File containing a list of known variables + -- with their types and the message IDs they + -- can be obtained from. + -> Maybe FilePath -- ^ File containing a list of handlers used in the + -- Copilot specification. The handlers are assumed + -- to receive no arguments. + -> IO (Result ErrorCode) +fprimeApp targetDir fretCSFile varNameFile varDBFile handlersFile = + processResult $ do + cs <- parseOptionalFRETCS fretCSFile + vs <- parseOptionalVariablesFile varNameFile + rs <- parseOptionalRequirementsListFile handlersFile + varDB <- parseOptionalVarDBFile varDBFile + + liftEither $ checkArguments cs vs rs + + let varNames = fromMaybe (fretCSExtractExternalVariables cs) vs + monitors = fromMaybe (fretCSExtractHandlers cs) rs + + e <- liftIO $ fprimeApp' targetDir varNames varDB monitors + liftEither e + +-- | Generate a new FPrime component connected to Copilot, by copying the +-- template and filling additional necessary files. +fprimeApp' :: FilePath -- ^ Target directory where the component + -- should be created. + -> [String] -- ^ List of variable names (data sources). + -> [(String, String)] -- ^ List of variables with their types, and + -- the message IDs (topics) they can be + -- obtained from. + -> [String] -- ^ List of handlers associated to the + -- monitors (or requirements monitored). + -> IO (Either ErrorTriplet ()) +fprimeApp' targetDir varNames varDB monitors = + E.handle (return . Left . cannotCopyTemplate) $ do + -- Obtain template dir + dataDir <- getDataDir + let templateDir = dataDir "templates" "fprime" + + -- Expand template + copyDirectoryRecursive templateDir targetDir + + let f n o@(oVars) = + case variableMap varDB n of + Nothing -> o + Just vars -> (vars : oVars) + + -- This is a Data.List.unzip4 + let vars = foldr f [] varNames + + let fprimeFileName = + targetDir "Copilot.fpp" + fprimeFileContents = + unlines $ + componentInterface vars monitors + + writeFile fprimeFileName fprimeFileContents + + let fprimeFileName = + targetDir "Copilot.hpp" + fprimeFileContents = + unlines $ + componentHeader vars monitors + + writeFile fprimeFileName fprimeFileContents + + let fprimeFileName = + targetDir "Copilot.cpp" + fprimeFileContents = + unlines $ + componentImpl vars monitors + + writeFile fprimeFileName fprimeFileContents + + return $ Right () + +-- ** Argument processing + +-- | Process FRET component spec, if available, and return its abstract +-- representation. +parseOptionalFRETCS :: Maybe FilePath + -> ExceptT ErrorTriplet IO (Maybe FRETComponentSpec) +parseOptionalFRETCS Nothing = return Nothing +parseOptionalFRETCS (Just fp) = do + -- Throws an exception if the file cannot be read. + content <- liftIO $ B.safeReadFile fp + + let fretCS :: Either String FRETComponentSpec + fretCS = eitherDecode =<< content + + case fretCS of + Left e -> throwError $ cannotOpenFRETFile fp e + Right cs -> return $ Just cs + +-- | Process a variable selection file, if available, and return the variable +-- names. +parseOptionalVariablesFile :: Maybe FilePath + -> ExceptT ErrorTriplet IO (Maybe [String]) +parseOptionalVariablesFile Nothing = return Nothing +parseOptionalVariablesFile (Just fp) = do + -- Fail if the file cannot be opened. + varNamesE <- liftIO $ E.try $ lines <$> readFile fp + case varNamesE of + Left e -> throwError $ cannotOpenVarFile fp e + Right varNames -> return $ Just varNames + +-- | Process a requirements / handlers list file, if available, and return the +-- handler names. +parseOptionalRequirementsListFile :: Maybe FilePath + -> ExceptT ErrorTriplet IO (Maybe [String]) +parseOptionalRequirementsListFile Nothing = return Nothing +parseOptionalRequirementsListFile (Just fp) = do + -- Fail if the file cannot be opened. + handlerNamesE <- liftIO $ E.try $ lines <$> readFile fp + case handlerNamesE of + Left e -> throwError $ cannotOpenHandlersFile fp e + Right monitors -> return $ Just monitors + +-- | Process a variable database file, if available, and return the rows in it. +parseOptionalVarDBFile :: Maybe FilePath + -> ExceptT ErrorTriplet + IO + [(String, String)] +parseOptionalVarDBFile Nothing = return [] +parseOptionalVarDBFile (Just fp) = do + -- We first try to open the files we need to fill in details in the FPrime + -- component template. + -- + -- The variable DB is optional, so this check only fails if the filename + -- provided does not exist or if the file cannot be opened or parsed (wrong + -- format). + varDBE <- liftIO $ E.try $ fmap read <$> lines <$> readFile fp + case varDBE of + Left e -> throwError $ cannotOpenDB fp e + Right varDB -> return varDB + +-- | Check that the arguments provided are sufficient to operate. +-- +-- The FPrime backend provides several modes of operation, which are selected +-- by providing different arguments to the `ros` command. +-- +-- When a FRET component specification file is provided, the variables and +-- requirements defined in it are used unless variables or handlers files are +-- provided, in which case the latter take priority. +-- +-- If a FRET file is not provided, then the user must provide BOTH a variable +-- list, and a list of handlers. +checkArguments :: Maybe FRETComponentSpec + -> Maybe [String] + -> Maybe [String] + -> Either ErrorTriplet () +checkArguments Nothing Nothing Nothing = Left wrongArguments +checkArguments Nothing Nothing _ = Left wrongArguments +checkArguments Nothing _ Nothing = Left wrongArguments +checkArguments _ (Just []) _ = Left wrongArguments +checkArguments _ _ (Just []) = Left wrongArguments +checkArguments _ _ _ = Right () + +-- | Extract the variables from a FRET component specification, and sanitize +-- them to be used in FPrime. +fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String] +fretCSExtractExternalVariables Nothing = [] +fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier + $ map fretExternalVariableName + $ fretExternalVariables cs + +-- | Extract the requirements from a FRET component specification, and sanitize +-- them to match the names of the handlers used by Copilot. +fretCSExtractHandlers :: Maybe FRETComponentSpec -> [String] +fretCSExtractHandlers Nothing = [] +fretCSExtractHandlers (Just cs) = map handlerNameF + $ map fretRequirementName + $ fretRequirements cs + where + handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier + +-- | Return the variable information needed to generate declarations +-- and subscriptions for a given variable name and variable database. +variableMap :: [(String, String)] + -> String + -> Maybe VarDecl +variableMap varDB varName = + csvToVarMap <$> find (sameName varName) varDB + + where + + -- True if the given variable and db entry have the same name + sameName :: String + -> (String, String) + -> Bool + sameName n (vn, _) = n == vn + + -- Convert a DB row into Variable info needed to generate the FPrime file + csvToVarMap :: (String, String) + -> (VarDecl) + csvToVarMap (nm, ty) = (VarDecl nm ty) + +-- | The declaration of a variable in C, with a given type and name. +data VarDecl = VarDecl + { varDeclName :: String + , varDeclType :: String + } + +-- * FPrime component content + +-- | Return the contents of the FPrime component interface (.fpp) specification. +componentInterface :: [VarDecl] + -> [String] -- Monitors + -> [String] +componentInterface variables monitors = + [ "module Ref {" + , "" + ] + ++ typePorts ++ + [ "" + , " @ Monitoring component" + , " queued component Copilot {" + , "" + , " # ----------------------------------------------------------------------" + , " # General ports" + , " # ----------------------------------------------------------------------" + , "" + ] + ++ inputPorts ++ + [ "" + , " # ----------------------------------------------------------------------" + , " # Special ports" + , " # ----------------------------------------------------------------------" + , "" + , " @ Command receive" + , " command recv port cmdIn" + , "" + , " @ Command registration" + , " command reg port cmdRegOut" + , "" + , " @ Command response" + , " command resp port cmdResponseOut" + , "" + , " @ Event" + , " event port eventOut" + , "" + , " @ Parameter get" + , " param get port prmGetOut" + , "" + , " @ Parameter set" + , " param set port prmSetOut" + , "" + , " @ Telemetry" + , " telemetry port tlmOut" + , "" + , " @ Text event" + , " text event port textEventOut" + , "" + , " @ Time get" + , " time get port timeGetOut" + , "" + , " # ----------------------------------------------------------------------" + , " # Parameters" + , " # ----------------------------------------------------------------------" + , "" + , " # This section intentionally left blank" + , "" + , " # ----------------------------------------------------------------------" + , " # Events" + , " # ----------------------------------------------------------------------" + , "" + ] + ++ violationEvents ++ + [ "" + , " # ----------------------------------------------------------------------" + , " # Commands" + , " # ----------------------------------------------------------------------" + , "" + , " sync command CHECK_MONITORS()" + , "" + , " # ----------------------------------------------------------------------" + , " # Telemetry" + , " # ----------------------------------------------------------------------" + , "" + , " # This section intentionally left blank" + , "" + , " }" + , "" + , "}" + ] + where + + typePorts = nub $ sort $ map toTypePort variables + toTypePort varDecl = " port " + ++ fprimeVarDeclType varDecl + ++ "Value(value: " + ++ fprimeVarDeclType varDecl + ++ ")" + + inputPorts = map toInputPortDecl variables + toInputPortDecl varDecl = " async input port " + ++ varDeclName varDecl + ++ "In : " ++ fprimeVarDeclType varDecl + ++ "Value" + + fprimeVarDeclType varDecl = case varDeclType varDecl of + "uint8_t" -> "U8" + "uint16_t" -> "U16" + "uint32_t" -> "U32" + "uint64_t" -> "U64" + "int8_t" -> "I8" + "int16_t" -> "I16" + "int32_t" -> "I32" + "int64_t" -> "I64" + "float" -> "F32" + "double" -> "F64" + def -> def + + violationEvents = intercalate [""] + $ map violationEvent monitors + violationEvent monitor = + [ " @ " ++ monitor ++ " violation" + , " event " ++ ucMonitor ++ "_VIOLATION(" + , " " ++ replicate (length ucMonitor) ' ' ++ " ) \\" + , " severity activity high \\" + , " id 0 \\" + , " format \"" ++ monitor ++ " violation\"" + ] + where + ucMonitor = map toUpper monitor + +-- | Return the contents of the FPrime component header file. +componentHeader :: [VarDecl] + -> [String] -- Monitors + -> [String] +componentHeader variables _monitors = + [ "// ======================================================================" + , "// \\title Copilot.hpp" + , "// \\author root" + , "// \\brief hpp file for Copilot component implementation class" + , "// ======================================================================" + , "" + , "#ifndef Copilot_HPP" + , "#define Copilot_HPP" + , "" + , "#include \"Ref/Copilot/CopilotComponentAc.hpp\"" + , "" + , "namespace Ref {" + , "" + , " class Copilot :" + , " public CopilotComponentBase" + , " {" + , "" + , " public:" + , "" + , " // ----------------------------------------------------------------------" + , " // Construction, initialization, and destruction" + , " // ----------------------------------------------------------------------" + , "" + , " //! Construct object Copilot" + , " //!" + , " Copilot(" + , " const char *const compName /*!< The component name*/" + , " );" + , "" + , " //! Initialize object Copilot" + , " //!" + , " void init(" + , " const NATIVE_INT_TYPE queueDepth, /*!< The queue depth*/" + , " const NATIVE_INT_TYPE instance = 0 /*!< The instance number*/" + , " );" + , "" + , " //! Destroy object Copilot" + , " //!" + , " ~Copilot();" + , "" + , " PRIVATE:" + , "" + , " // ----------------------------------------------------------------------" + , " // Handler implementations for user-defined typed input ports" + , " // ----------------------------------------------------------------------" + , "" + ] + ++ handlers ++ + [ "" + , " PRIVATE:" + , "" + , " // ----------------------------------------------------------------------" + , " // Command handler implementations" + , " // ----------------------------------------------------------------------" + , "" + , " //! Implementation for CHECK_MONITORS command handler" + , " //! " + , " void CHECK_MONITORS_cmdHandler(" + , " const FwOpcodeType opCode, /*!< The opcode*/" + , " const U32 cmdSeq /*!< The command sequence number*/" + , " );" + , "" + , " };" + , "" + , "} // end namespace Ref" + , "" + , "#endif" + ] + where + handlers = intercalate [""] + $ map toInputHandler variables + toInputHandler nm = + [ " //! Handler implementation for " ++ varDeclName nm ++ "In" + , " //!" + , " void " ++ varDeclName nm ++ "In_handler(" + , " const NATIVE_INT_TYPE portNum, /*!< The port number*/" + , " " ++ portTy ++ " value" + , " );" + ] + where + portTy = varDeclType nm + + +-- | Return the contents of the main FPrime component. +componentImpl :: [VarDecl] + -> [String] -- Monitors + -> [String] +componentImpl variables monitors = + [ "// ======================================================================" + , "// \\title Copilot.cpp" + , "// \\author Ogma" + , "// \\brief cpp file for Copilot component implementation class" + , "// ======================================================================" + , "" + , "" + , "#include " + , "#include \"Fw/Types/BasicTypes.hpp\"" + , "" + , "#ifdef __cplusplus" + , "extern \"C\" {" + , "#endif" + , "" + , "#include \"copilot.h\"" + , "#include \"copilot_types.h\"" + , "" + , "#ifdef __cplusplus" + , "}" + , "#endif" + , "" + ] + ++ inputs + ++ monitorResults ++ + [ "" + , "namespace Ref {" + , "" + , " // ----------------------------------------------------------------------" + , " // Construction, initialization, and destruction" + , " // ----------------------------------------------------------------------" + , "" + , " Copilot ::" + , " Copilot(" + , " const char *const compName" + , " ) : CopilotComponentBase(compName)" + , " {" + , "" + , " }" + , "" + , " void Copilot ::" + , " init(" + , " const NATIVE_INT_TYPE queueDepth," + , " const NATIVE_INT_TYPE instance" + , " )" + , " {" + , " CopilotComponentBase::init(queueDepth, instance);" + , " }" + , "" + , " Copilot ::" + , " ~Copilot()" + , " {" + , "" + , " }" + , "" + , " // ----------------------------------------------------------------------" + , " // Handler implementations for user-defined typed input ports" + , " // ----------------------------------------------------------------------" + , "" + ] + ++ inputHandlers ++ + [ "" + , " // ----------------------------------------------------------------------" + , " // Command handler implementations" + , " // ----------------------------------------------------------------------" + , "" + , " void Copilot ::" + , " CHECK_MONITORS_cmdHandler(" + , " const FwOpcodeType opCode," + , " const U32 cmdSeq" + , " )" + , " {" + ] + ++ triggerResultReset ++ + [ " step();" + , " this->cmdResponse_out(opCode,cmdSeq,Fw::CmdResponse::OK);" + ] + ++ triggerChecks ++ + [ " }" + , "" + , "} // end namespace Ref" + , "" + ] + ++ triggers + + where + + inputs = variablesS + + monitorResults = intercalate [""] + $ map monitorResult monitors + monitorResult monitor = + [ "bool " ++ monitor ++ "_result;" + ] + + inputHandlers = intercalate [""] + $ map toInputHandler variables + toInputHandler nm = + [ " void Copilot :: " + , " " ++ varDeclName nm ++ "In_handler(" + , " const NATIVE_INT_TYPE portNum," + , " " ++ portTy ++ " value" + , " )" + , " {" + , " " ++ varDeclName nm ++ " = (" ++ ty ++ ") value;" + , " }" + ] + where + portTy = varDeclType nm + ty = varDeclType nm + + triggerResultReset = intercalate [""] + $ map monitorResultReset monitors + monitorResultReset monitor = + [ " " ++ monitor ++ "_result = false;" + ] + + triggerChecks = intercalate [""] + $ map triggerCheck monitors + triggerCheck monitor = + [ " if (" ++ monitor ++ "_result) {" + , " this->log_ACTIVITY_HI_" ++ ucMonitor ++ "_VIOLATION();" + , " }" + ] + where + ucMonitor = map toUpper monitor + + triggers :: [String] + triggers = intercalate [""] + $ map triggerImpl monitors + triggerImpl monitor = + [ "void " ++ monitor ++ "() {" + , " " ++ monitor ++ "_result = true;" + , "}" + ] + + variablesS :: [String] + variablesS = map toVarDecl variables + toVarDecl varDecl = + varDeclType varDecl ++ " " ++ varDeclName varDecl ++ ";" + +-- * Exception handlers + +-- | Exception handler to deal with the case in which the arguments +-- provided are incorrect. +wrongArguments :: ErrorTriplet +wrongArguments = + ErrorTriplet ecWrongArguments msg LocationNothing + where + msg = + "the arguments provided are insufficient: you must provide a FRET " + ++ "component specification file, or both a variables and a handlers " + ++ "file." + +-- | Exception handler to deal with the case in which the FRET CS cannot be +-- opened. +cannotOpenFRETFile :: FilePath -> String -> ErrorTriplet +cannotOpenFRETFile file _e = + ErrorTriplet ecCannotOpenFRETFile msg (LocationFile file) + where + msg = + "cannot open FRET component specification file " ++ file + +-- | Exception handler to deal with the case in which the variable DB cannot be +-- opened. +cannotOpenDB :: FilePath -> E.SomeException -> ErrorTriplet +cannotOpenDB file _e = + ErrorTriplet ecCannotOpenDBUser msg (LocationFile file) + where + msg = + "cannot open variable DB file " ++ file + +-- | Exception handler to deal with the case in which the variable file +-- provided by the user cannot be opened. +cannotOpenVarFile :: FilePath -> E.SomeException -> ErrorTriplet +cannotOpenVarFile file _e = + ErrorTriplet ecCannotOpenVarFile msg (LocationFile file) + where + msg = + "cannot open variable list file " ++ file + +-- | Exception handler to deal with the case in which the handlers file +-- provided by the user cannot be opened. +cannotOpenHandlersFile :: FilePath -> E.SomeException -> ErrorTriplet +cannotOpenHandlersFile file _e = + ErrorTriplet ecCannotOpenHandlersFile msg (LocationFile file) + where + msg = + "cannot open handler list file " ++ file + +-- | Exception handler to deal with the case of files that cannot be +-- copied/generated due lack of space or permissions or some I/O error. +cannotCopyTemplate :: E.SomeException -> ErrorTriplet +cannotCopyTemplate e = + ErrorTriplet ecCannotCopyTemplate msg LocationNothing + where + msg = + "FPrime component generation failed during copy/write operation. Check" + ++ " that there's free space in the disk and that you have the necessary" + ++ " permissions to write in the destination directory." + ++ show e + +-- | A triplet containing error information. +data ErrorTriplet = ErrorTriplet ErrorCode String Location + +-- | Process a computation that can fail with an error code, and turn it into a +-- computation that returns a 'Result'. +processResult :: Monad m => ExceptT ErrorTriplet m a -> m (Result ErrorCode) +processResult m = do + r <- runExceptT m + case r of + Left (ErrorTriplet errorCode msg location) + -> return $ Error errorCode msg location + _ -> return Success + +-- * Error codes + +-- | Encoding of reasons why the command can fail. +-- +-- The error codes used are 1 for user error, and 2 for internal bug. +type ErrorCode = Int + +-- | Error: wrong arguments provided. +ecWrongArguments :: ErrorCode +ecWrongArguments = 1 + +-- | Error: the FRET component specification provided by the user cannot be +-- opened. +ecCannotOpenFRETFile :: ErrorCode +ecCannotOpenFRETFile = 1 + +-- | Error: the variable DB provided by the user cannot be opened. +ecCannotOpenDBUser :: ErrorCode +ecCannotOpenDBUser = 1 + +-- | Error: the variable file provided by the user cannot be opened. +ecCannotOpenVarFile :: ErrorCode +ecCannotOpenVarFile = 1 + +-- | Error: the handlers file provided by the user cannot be opened. +ecCannotOpenHandlersFile :: ErrorCode +ecCannotOpenHandlersFile = 1 + +-- | Error: the files cannot be copied/generated due lack of space or +-- permissions or some I/O error. +ecCannotCopyTemplate :: ErrorCode +ecCannotCopyTemplate = 1 diff --git a/ogma-core/templates/fprime/CMakeLists.txt b/ogma-core/templates/fprime/CMakeLists.txt new file mode 100644 index 00000000..30c316f7 --- /dev/null +++ b/ogma-core/templates/fprime/CMakeLists.txt @@ -0,0 +1,9 @@ +# Register the standard build +set(SOURCE_FILES + "${CMAKE_CURRENT_LIST_DIR}/copilot.c" + "${CMAKE_CURRENT_LIST_DIR}/copilot.h" + "${CMAKE_CURRENT_LIST_DIR}/copilot_types.h" + "${CMAKE_CURRENT_LIST_DIR}/Copilot.cpp" + "${CMAKE_CURRENT_LIST_DIR}/Copilot.fpp" +) +register_fprime_module() diff --git a/ogma-core/templates/fprime/Dockerfile b/ogma-core/templates/fprime/Dockerfile new file mode 100644 index 00000000..04d9579c --- /dev/null +++ b/ogma-core/templates/fprime/Dockerfile @@ -0,0 +1,49 @@ +# This dockerfile compiles a monitoring application inside FPrime's Reference +# Application. +FROM ubuntu:focal + +# Avoid questions during package installation. +ENV DEBIAN_FRONTEND=noninteractive + +# Install FPrime dependencies and clone fprime from the repo. +RUN apt-get update +RUN apt-get install -y git cmake gcc python3 pip + +RUN git clone https://github.com/nasa/fprime +RUN pip install -r fprime/requirements.txt + +WORKDIR fprime/Ref + +# Add all the monitoring app files. +RUN mkdir Copilot +ADD CMakeLists.txt Copilot/ +ADD Copilot.fpp Copilot/ +ADD Copilot.cpp Copilot/ +ADD Copilot.hpp Copilot/ +ADD copilot.c Copilot/ +ADD copilot.h Copilot/ +ADD copilot_types.h Copilot/ + +# Enable Copilot app (add it after SignalGen). +RUN sed -i -e '/^add_fprime_subdirectory.*SignalGen.*/a add_fprime_subdirectory("${CMAKE_CURRENT_LIST_DIR}\/Copilot\/")' CMakeLists.txt + +RUN fprime-util generate + +# Update Ref deployment. + +## Define Component Instance. +## +## This command adds the contents of the given instance-copilot at the end of +## Queued component instances section, which is right before the Passive +## components section. +ADD instance-copilot . +RUN line=$(grep -n 'Passive component instances' Top/instances.fpp | tail -n1 | cut -d: -f1); line=$(($line - 2)); sed -i -e "${line}r instance-copilot" Top/instances.fpp +RUN rm instance-copilot + +## Update topology. +## +## This command adds the copilot monitoring node right after linuxTime in the +## topology. +RUN sed -i -e '/^ \+instance linuxTime/a\ \ \ \ instance copilotMonitor' Top/topology.fpp + +RUN fprime-util build --jobs "$(nproc || printf '%s\n' 1)" diff --git a/ogma-core/templates/fprime/instance-copilot b/ogma-core/templates/fprime/instance-copilot new file mode 100644 index 00000000..67fecc05 --- /dev/null +++ b/ogma-core/templates/fprime/instance-copilot @@ -0,0 +1,3 @@ + instance copilotMonitor: Ref.Copilot base id 0x2700 \ + queue size Default.queueSize + From e7a8e1edacc369f0e420db77a5c17215644bb34f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 20 May 2022 10:01:34 -0400 Subject: [PATCH 10/51] ogma-cli: Make new `fprime` command available via the CLI. Refs #77. Expose the new FPrime backend via the command-line interface. --- ogma-cli/ogma-cli.cabal | 1 + ogma-cli/src/CLI/CommandFPrimeApp.hs | 148 +++++++++++++++++++++++++++ ogma-cli/src/CLI/CommandTop.hs | 14 +++ 3 files changed, 163 insertions(+) create mode 100644 ogma-cli/src/CLI/CommandFPrimeApp.hs diff --git a/ogma-cli/ogma-cli.cabal b/ogma-cli/ogma-cli.cabal index c7fe0d57..f25e4f31 100644 --- a/ogma-cli/ogma-cli.cabal +++ b/ogma-cli/ogma-cli.cabal @@ -117,6 +117,7 @@ executable ogma CLI.CommandCFSApp CLI.CommandCStructs2Copilot CLI.CommandCStructs2MsgHandlers + CLI.CommandFPrimeApp CLI.CommandFretComponentSpec2Copilot CLI.CommandFretReqsDB2Copilot CLI.CommandROSApp diff --git a/ogma-cli/src/CLI/CommandFPrimeApp.hs b/ogma-cli/src/CLI/CommandFPrimeApp.hs new file mode 100644 index 00000000..e3f57883 --- /dev/null +++ b/ogma-cli/src/CLI/CommandFPrimeApp.hs @@ -0,0 +1,148 @@ +-- Copyright 2022 United States Government as represented by the Administrator +-- of the National Aeronautics and Space Administration. All Rights Reserved. +-- +-- Disclaimers +-- +-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY +-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT +-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO +-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A +-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE +-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF +-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN +-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR +-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR +-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER, +-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING +-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES +-- IT "AS IS." +-- +-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST +-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS +-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN +-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE, +-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S +-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE +-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY +-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY +-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS +-- AGREEMENT. +-- +-- | CLI interface to the FPrimeApp subcommand. +module CLI.CommandFPrimeApp + ( + -- * Direct command access + command + , CommandOpts + , ErrorCode + + -- * CLI + , commandDesc + , commandOptsParser + ) + where + +-- External imports +import Options.Applicative ( Parser, help, long, metavar, optional, showDefault, + strOption, value ) + +-- External imports: command results +import Command.Result ( Result ) + +-- External imports: actions or commands supported +import Command.FPrimeApp ( ErrorCode, fprimeApp ) + +-- * Command + +-- | Options needed to generate the FPrime component. +data CommandOpts = CommandOpts + { fprimeAppTarget :: String + , fprimeAppFRETFile :: Maybe String + , fprimeAppVarNames :: Maybe String + , fprimeAppVarDB :: Maybe String + , fprimeAppHandlers :: Maybe String + } + +-- | Create component that subscribe +-- to obtain necessary data from the bus and call Copilot when new data +-- arrives. +-- +-- This is just an uncurried version of "Command.fprimeApp". +command :: CommandOpts -> IO (Result ErrorCode) +command c = + fprimeApp + (fprimeAppTarget c) + (fprimeAppFRETFile c) + (fprimeAppVarNames c) + (fprimeAppVarDB c) + (fprimeAppHandlers c) + +-- * CLI + +-- | FPrime command description +commandDesc :: String +commandDesc = "Generate a complete F' monitoring component" + +-- | Subparser for the @fprime@ command, used to generate an FPrime component +-- connected to Copilot monitors. +commandOptsParser :: Parser CommandOpts +commandOptsParser = CommandOpts + <$> strOption + ( long "app-target-dir" + <> metavar "DIR" + <> showDefault + <> value "fprime" + <> help strFPrimeAppDirArgDesc + ) + <*> optional + ( strOption + ( long "fret-file-name" + <> metavar "FILENAME" + <> help strFPrimeAppFRETFileNameArgDesc + ) + ) + <*> optional + ( strOption + ( long "variable-file" + <> metavar "FILENAME" + <> help strFPrimeAppVarListArgDesc + ) + ) + <*> optional + ( strOption + ( long "variable-db" + <> metavar "FILENAME" + <> help strFPrimeAppVarDBArgDesc + ) + ) + <*> optional + ( strOption + ( long "handlers-file" + <> metavar "FILENAME" + <> help strFPrimeAppHandlerListArgDesc + ) + ) + +-- | Argument target directory to FPrime component generation command +strFPrimeAppDirArgDesc :: String +strFPrimeAppDirArgDesc = "Target directory" + +-- | Argument FRET CS to FPrime component generation command +strFPrimeAppFRETFileNameArgDesc :: String +strFPrimeAppFRETFileNameArgDesc = + "File containing FRET Component Specification" + +-- | Argument variable list to FPrime component generation command +strFPrimeAppVarListArgDesc :: String +strFPrimeAppVarListArgDesc = + "File containing list of F' variables to make accessible" + +-- | Argument variable database to FPrime component generation command +strFPrimeAppVarDBArgDesc :: String +strFPrimeAppVarDBArgDesc = + "File containing a DB of known F' variables" + +-- | Argument handler list to FPrime component generation command +strFPrimeAppHandlerListArgDesc :: String +strFPrimeAppHandlerListArgDesc = + "File containing list of Copilot handlers used in the specification" diff --git a/ogma-cli/src/CLI/CommandTop.hs b/ogma-cli/src/CLI/CommandTop.hs index f352b4ec..6da1b454 100644 --- a/ogma-cli/src/CLI/CommandTop.hs +++ b/ogma-cli/src/CLI/CommandTop.hs @@ -89,6 +89,7 @@ import Command.Result ( Result ) import qualified CLI.CommandCFSApp import qualified CLI.CommandCStructs2Copilot import qualified CLI.CommandCStructs2MsgHandlers +import qualified CLI.CommandFPrimeApp import qualified CLI.CommandFretComponentSpec2Copilot import qualified CLI.CommandFretReqsDB2Copilot import qualified CLI.CommandROSApp @@ -104,6 +105,7 @@ data CommandOpts = CommandOptsCFSApp CLI.CommandCFSApp.CommandOpts | CommandOptsCStructs2Copilot CLI.CommandCStructs2Copilot.CommandOpts | CommandOptsCStructs2MsgHandlers CLI.CommandCStructs2MsgHandlers.CommandOpts + | CommandOptsFPrimeApp CLI.CommandFPrimeApp.CommandOpts | CommandOptsFretComponentSpec2Copilot CLI.CommandFretComponentSpec2Copilot.CommandOpts | CommandOptsFretReqsDB2Copilot CLI.CommandFretReqsDB2Copilot.CommandOpts | CommandOptsROSApp CLI.CommandROSApp.CommandOpts @@ -121,6 +123,7 @@ commandOptsParser = subparser ( subcommandCStructs <> subcommandMsgHandlers <> subcommandCFSApp + <> subcommandFPrimeApp <> subcommandFretComponentSpec <> subcommandFretReqs <> subcommandROSApp @@ -187,6 +190,15 @@ subcommandROSApp = (CommandOptsROSApp <$> CLI.CommandROSApp.commandOptsParser) CLI.CommandROSApp.commandDesc +-- | Modifier for the FPrime app expansion subcommand, linking the subcommand +-- options and description to the command @fprime@ at top level. +subcommandFPrimeApp :: Mod CommandFields CommandOpts +subcommandFPrimeApp = + subcommand + "fprime" + (CommandOptsFPrimeApp <$> CLI.CommandFPrimeApp.commandOptsParser) + CLI.CommandFPrimeApp.commandDesc + -- * Command dispatcher -- | Command dispatcher that obtains the parameters from the command line and @@ -215,6 +227,8 @@ command (CommandOptsCStructs2Copilot c) = id <$> CLI.CommandCStructs2Copilot.command c command (CommandOptsCStructs2MsgHandlers c) = id <$> CLI.CommandCStructs2MsgHandlers.command c +command (CommandOptsFPrimeApp c) = + id <$> CLI.CommandFPrimeApp.command c command (CommandOptsFretComponentSpec2Copilot c) = id <$> CLI.CommandFretComponentSpec2Copilot.command c command (CommandOptsFretReqsDB2Copilot c) = From e59611a005a40be8f6c3de846aaca2234b192ee0 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 18 Jan 2023 10:39:02 -0800 Subject: [PATCH 11/51] ogma-cli: Document existence of `fprime` command in Main module. Refs #77. Mention the existence of the new FPrime backend in the top-level documentation of the main module. --- ogma-cli/src/Main.hs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/ogma-cli/src/Main.hs b/ogma-cli/src/Main.hs index bec47a9a..6535a987 100644 --- a/ogma-cli/src/Main.hs +++ b/ogma-cli/src/Main.hs @@ -53,6 +53,8 @@ -- * Generate Robot Operating System (ROS) applications for runtime monitoring -- using Copilot. -- +-- * Generate F' (FPrime) components for runtime monitoring using Copilot. +-- -- More information can be obtained by calling ogma with the argument @--help@. module Main ( main ) From bd179a70fc9a1b20ca9bfcc28ba54e19ebf18ed5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Wed, 18 Jan 2023 10:39:10 -0800 Subject: [PATCH 12/51] ogma-cli: Document existence of `fprime` command in Cabal file. Refs #77. Mention the existence of the FPrime backend in the documentation of the cabal file for the CLI, which will be used for hackage. --- ogma-cli/ogma-cli.cabal | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-cli/ogma-cli.cabal b/ogma-cli/ogma-cli.cabal index f25e4f31..0b7afeed 100644 --- a/ogma-cli/ogma-cli.cabal +++ b/ogma-cli/ogma-cli.cabal @@ -86,6 +86,7 @@ description: Ogma is a tool to facilitate the integration of safe runtim > structs Generate Copilot structs from C structs > handlers Generate message handlers from C structs > cfs Generate a complete CFS/Copilot application + > fprime Generate a complete F' monitoring component > fret-component-spec Generate a Copilot file from a FRET Component > Specification > fret-reqs-db Generate a Copilot file from a FRET Requirements From 287427936f9a58c4eeebd541804e22c0f28811c2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Fri, 20 May 2022 10:03:59 -0400 Subject: [PATCH 13/51] ogma-cli: Document `fprime` command in README. Refs #77. Add instructions of how the `fprime` command works. Add entry in list of features documenting the new F' (FPrime) support. Describe existing limitations for the command. --- ogma-cli/README.md | 119 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 119 insertions(+) diff --git a/ogma-cli/README.md b/ogma-cli/README.md index ffa09d29..e91d00a6 100644 --- a/ogma-cli/README.md +++ b/ogma-cli/README.md @@ -22,6 +22,9 @@ verification framework that generates hard real-time C99 code. - Generating [Robot Operating System](https://ros.org) applications that use Copilot for monitoring data published in different topics. +- Generating [F' (FPrime)](https://github.com/nasa/fprime/) components that use + Copilot for monitoring data published in different ports. +

Conversion of requirements into C code @@ -45,6 +48,7 @@ verification framework that generates hard real-time C99 code. - [cFS Application Generation](#cfs-application-generation) - [Struct Interface Generation](#struct-interface-generation) - [ROS Application Generation](#ros-application-generation) + - [F' Component Generation](#f-component-generation) - [Contributions](#contributions) - [Acknowledgements](#acknowledgements) - [License](#license) @@ -108,6 +112,7 @@ Available commands: structs Generate Copilot structs from C structs handlers Generate message handlers from C structs cfs Generate a complete cFS/Copilot application + fprime Generate a complete F' monitoring component fret-component-spec Generate a Copilot file from a FRET Component Specification fret-reqs-db Generate a Copilot file from a FRET Requirements @@ -442,6 +447,120 @@ be generated for any variables for which a DB entry cannot be found. At present, Ogma will proceed without warnings if a variable is mentioned in a requirement or variables file but a matching entry is not found in the variable DB. +## F' Component Generation + +F' (FPrime) is a component-based framework for spaceflight applications. + +Ogma is able to generate F' monitoring components that subscribe to obtain +the data needed by the monitors and report any violations. At present, support +for F' component generation is considered preliminary. + +F' components are generated using the Ogma command `fprime`, which receives +five main arguments: +- `--app-target-dir DIR`: location where the F' application files must be + stored. +- `--fret-file-name FILENAME`: a file containing a FRET component specification. +- `--variable-file FILENAME`: a file containing a list of variables that must +be made available to the monitor. +- `--variable-db FILENAME`: a file containing a database of known variables, +and their types. +- `--handlers FILENAME`: a file containing a list of handlers used in the + specification. + +Not all arguments are mandatory. You should always provide either a FRET +component specification, or both a variable file and a handlers file. If you +provide a variables file or a handler file _and_ a FRET component +specification, the variables/handlers file will always take precedence, and the +variables/requirements listed in the FRET component specification file will be +ignored. + +The following execution generates an initial F' component for runtime +monitoring using Copilot: +```sh +$ ogma fprime --fret-file-name Export.json --variable-db fprime-variable-db --app-target-dir fprime_demo +``` + +The component generated by Ogma contains the following files: +``` +fprime_demo/CMakeLists.txt +fprime_demo/Copilot.fpp +fprime_demo/Copilot.cpp +fprime_demo/Copilot.hpp +fprime_demo/Dockerfile +fprime_demo/inline-copilot +``` + +For completion, the following execution should compile the produced monitoring +component in a docker environment (assuming that the necessary `Export.json`, +`fprime-variable-db` files exist, they have consistent information, etc.) using +FPrime's Reference Application: + +```sh +$ ogma fprime --fret-file-name Export.json --variable-db fprime-variable-db --app-target-dir fprime_demo +$ ogma fret-component-spec --fret-file-name Export.json > Spec.hs +$ sed -i -e 's/compile "fret"/compile "copilot"/g' Spec.hs +$ cd fprime_demo/ +$ runhaskell ../Spec.hs +$ docker build -t fprime . +``` + +### File formats + +The format of the variables, variable DB, and handlers file are as follows. + +The variables file can contain a list of variables used in a specification, one +per line. For example, if we are working with a specification that uses three +boolean variables called `autopilot`, `sensorLimitsExceeded`, and `pullup`, we +can provide them to Ogma's `fprime` command in a file like the following: +```sh +$ cat variables +autopilot +sensorLimitsExceeded +pullup +``` + +The variables database file contains a list of known variables and their types. +It does not matter if there are variables that are not used for one particular +specification, FRET file, or requirement/monitor. The only thing that matters +is that the variables used, and their types, be listed in the file. Continuing +with the same example, we could have: + +```sh +$ cat fprime-variable-db +("temperature", "uint8_t") +("autopilot", "bool") +("sensorLimitsExceeded", "bool") +("pullup", "bool") +("current_consumption", "float") +``` + +In our example, we only care about the boolean variables; it is sufficient that +they be listed in the variable DB file. + +Finally, the handlers file is a list of monitor handlers that the generated +FPrime component should restrict to monitoring. They are listed one per line: +```sh +$ cat handlers +handlerpropREQ_001 +``` + +Note that the handler name must match the one used by Copilot. Ogma transforms +requirement names to ensure that they corresponding handlers are valid C +identifiers. For example, the Ogma-generated monitor for a FRET requirement +`REQ_001` would, upon violation, call a C handler `handlerpropREQ_001`. The +transformation only applies if you are working with FRET files and not directly +with other source languages. + +### Current limitations + +The user must place the code generated by Copilot monitors in three files, +`fprime_demo/src/copilot.h`, `fprime_demo/src/copilot_types.h` and +`fprime_demo/src/copilot.c`. No Copilot or C code for the monitors is generated +by default by the `fprime` command. + +The code generated by default assumes that handlers receive no arguments. The +user must modify the handlers accordingly if that is not the case. + ## Struct Interface Generation A lot of the information that must be monitored in real-world C applications is From 366ab47c067405796aad954499c146e2424ea2ba Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 09:51:12 -0700 Subject: [PATCH 14/51] ogma-core: Document changes in CHANGELOG. Refs #77. --- ogma-core/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 386c63fa..6a5bbe4e 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,8 +1,9 @@ # Revision history for ogma-core -## [1.X.Y] - 2023-02-01 +## [1.X.Y] - 2023-03-21 * Support inequality operator in SMV and CoCoSpec (#71). +* Introduce new F' (FPrime) backend (#77). ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 76fc7b0bce982619f30376ebf6ac6b4260e91224 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 15:48:58 -0700 Subject: [PATCH 15/51] ogma-cli: Document changes in CHANGELOG. Refs #77. --- ogma-cli/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index ec011f06..2966f938 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-cli +## [1.X.Y] - 2023-03-21 + +* Introduce new F' (FPrime) backend (#77). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). * Replace tabs in cabal file (#69). From 05854229620c0a2f287eaad4dcc6e26927a0bad1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:53:47 -0700 Subject: [PATCH 16/51] ogma-language-smv: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-language-smv/ogma-language-smv.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-language-smv/ogma-language-smv.cabal b/ogma-language-smv/ogma-language-smv.cabal index b7a728db..e859faa1 100644 --- a/ogma-language-smv/ogma-language-smv.cabal +++ b/ogma-language-smv/ogma-language-smv.cabal @@ -55,6 +55,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim This library contains a frontend to read SMV Boolean expressions, used by the tool FRET to capture requirement specifications. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + custom-setup setup-depends: base >= 4.11.0.0 && < 5 From 0deecb4d59f5f1efc132e6777a86bfcf6004d644 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:55:25 -0700 Subject: [PATCH 17/51] ogma-language-fret-reqs: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-language-fret-reqs/ogma-language-fret-reqs.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal b/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal index b68951df..e9e75777 100644 --- a/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal +++ b/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal @@ -52,6 +52,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim . This library contains a frontend to read FRET Component Requirement Databases. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + library exposed-modules: From 7abf3645109711ad3e35d47cc6b8adb701beb59f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:55:47 -0700 Subject: [PATCH 18/51] ogma-language-fret-cs: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-language-fret-cs/ogma-language-fret-cs.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-language-fret-cs/ogma-language-fret-cs.cabal b/ogma-language-fret-cs/ogma-language-fret-cs.cabal index e3429f53..a4b975cd 100644 --- a/ogma-language-fret-cs/ogma-language-fret-cs.cabal +++ b/ogma-language-fret-cs/ogma-language-fret-cs.cabal @@ -52,6 +52,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim . This library contains a frontend to read FRET Component Specifications. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + library exposed-modules: From e82ee0d1e00fcfcc9f29f5afaeb8ceef4f361b90 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:56:02 -0700 Subject: [PATCH 19/51] ogma-language-copilot: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-language-copilot/ogma-language-copilot.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-language-copilot/ogma-language-copilot.cabal b/ogma-language-copilot/ogma-language-copilot.cabal index f4230609..517573f5 100644 --- a/ogma-language-copilot/ogma-language-copilot.cabal +++ b/ogma-language-copilot/ogma-language-copilot.cabal @@ -51,6 +51,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim This library contains a frontend to read Copilot monitors, a definition of Copilot structs, and a backend to generate and pretty print Copilot code. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + library exposed-modules: From 8e8e5fd9309a4fe3cb01dcf7247f8fdd52a882c2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:56:20 -0700 Subject: [PATCH 20/51] ogma-language-cocospec: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-language-cocospec/ogma-language-cocospec.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-language-cocospec/ogma-language-cocospec.cabal b/ogma-language-cocospec/ogma-language-cocospec.cabal index 25c106f4..377c41bb 100644 --- a/ogma-language-cocospec/ogma-language-cocospec.cabal +++ b/ogma-language-cocospec/ogma-language-cocospec.cabal @@ -55,6 +55,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim This library contains a frontend to read CoCoSpec Boolean expressions, used by the tool FRET to capture requirement specifications. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + custom-setup setup-depends: base >= 4.11.0.0 && < 5 From d4da663312707c630bf3fad0e101df586bc83b59 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:56:37 -0700 Subject: [PATCH 21/51] ogma-language-c: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-language-c/ogma-language-c.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-language-c/ogma-language-c.cabal b/ogma-language-c/ogma-language-c.cabal index 412aaf80..0551c5f2 100644 --- a/ogma-language-c/ogma-language-c.cabal +++ b/ogma-language-c/ogma-language-c.cabal @@ -54,6 +54,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim . This library contains a frontend to read C header files. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + custom-setup setup-depends: base >= 4.11.0.0 && < 5 From 2eb67dc5a5b01f17a0df826c8bd7a82084036889 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:57:29 -0700 Subject: [PATCH 22/51] ogma-extra: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-extra/ogma-extra.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-extra/ogma-extra.cabal b/ogma-extra/ogma-extra.cabal index f096ab60..750ee599 100644 --- a/ogma-extra/ogma-extra.cabal +++ b/ogma-extra/ogma-extra.cabal @@ -52,6 +52,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim and modules that are used in several ogma packages and their testing facilities. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + library exposed-modules: From 227ef0e6cc447e408f848d850ca715766040fd51 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:57:40 -0700 Subject: [PATCH 23/51] ogma-core: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-core/ogma-core.cabal | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 85dfa7d4..05597d63 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -66,6 +66,14 @@ data-files: templates/copilot-cfs/CMakeLists.txt templates/fprime/CMakeLists.txt templates/fprime/Dockerfile templates/fprime/instance-copilot + +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + library exposed-modules: From ec61a14b539368a723d992e7f3205115757c0908 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 16:57:51 -0700 Subject: [PATCH 24/51] ogma-cli: Mark package as uncurated. Refs #74. Cabal packages in Ogma are not using the flag x-curation to indicate to package maintainers that our packages should not be modified by them. Because this is a NASA project, we want to make sure that users obtain exactly what we publish, unmodified by anyone external to our project. This commit sets modifies the cabal package to include x-curation: uncurated, signaling our preferences to the Hackage maintainers. --- ogma-cli/ogma-cli.cabal | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/ogma-cli/ogma-cli.cabal b/ogma-cli/ogma-cli.cabal index 0b7afeed..de68f4d0 100644 --- a/ogma-cli/ogma-cli.cabal +++ b/ogma-cli/ogma-cli.cabal @@ -109,6 +109,13 @@ description: Ogma is a tool to facilitate the integration of safe runtim . - , Dutle et al. 2020. +-- Ogma packages should be uncurated so that only the official maintainers make +-- changes. +-- +-- Because this is a NASA project, we want to make sure that users obtain +-- exactly what we publish, unmodified by anyone external to our project. +x-curation: uncurated + executable ogma main-is: From efb98eccf7f87e3948605e746d9ed2b90e758a2f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 25/51] ogma-language-smv: Document changes in CHANGELOG. Refs #74. --- ogma-language-smv/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-smv/CHANGELOG.md b/ogma-language-smv/CHANGELOG.md index 4e96a09f..75c81303 100644 --- a/ogma-language-smv/CHANGELOG.md +++ b/ogma-language-smv/CHANGELOG.md @@ -1,8 +1,9 @@ # Revision history for ogma-language-smv -## [1.X.Y] - 2023-02-01 +## [1.X.Y] - 2023-03-21 * Support inequality operator (#71). +* Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 825623d90e1440024a0cc8f41c0f70e004eae392 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 26/51] ogma-language-fret-reqs: Document changes in CHANGELOG. Refs #74. --- ogma-language-fret-reqs/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-language-fret-reqs/CHANGELOG.md b/ogma-language-fret-reqs/CHANGELOG.md index ebd4bda3..530998e8 100644 --- a/ogma-language-fret-reqs/CHANGELOG.md +++ b/ogma-language-fret-reqs/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-fret-reqs +## [1.X.Y] - 2023-03-21 + +* Mark package as uncurated (#74). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 3da2476aaf1247f39c3fe3d9404ededdbec0edf4 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 27/51] ogma-language-fret-cs: Document changes in CHANGELOG. Refs #74. --- ogma-language-fret-cs/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-language-fret-cs/CHANGELOG.md b/ogma-language-fret-cs/CHANGELOG.md index 026f0108..f7cd23bb 100644 --- a/ogma-language-fret-cs/CHANGELOG.md +++ b/ogma-language-fret-cs/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-fret-cs +## [1.X.Y] - 2023-03-21 + +* Mark package as uncurated (#74). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 471a99492dd9f309513cf33209746474291e56fd Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 28/51] ogma-language-copilot: Document changes in CHANGELOG. Refs #74. --- ogma-language-copilot/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-language-copilot/CHANGELOG.md b/ogma-language-copilot/CHANGELOG.md index 9dbd1724..f9c864ca 100644 --- a/ogma-language-copilot/CHANGELOG.md +++ b/ogma-language-copilot/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-copilot +## [1.X.Y] - 2023-03-21 + +* Mark package as uncurated (#74). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From b76c153fae02c3da20ce8e3ced5a4a6c974db535 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 29/51] ogma-language-cocospec: Document changes in CHANGELOG. Refs #74. --- ogma-language-cocospec/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-cocospec/CHANGELOG.md b/ogma-language-cocospec/CHANGELOG.md index 485f69e4..7a434463 100644 --- a/ogma-language-cocospec/CHANGELOG.md +++ b/ogma-language-cocospec/CHANGELOG.md @@ -1,8 +1,9 @@ # Revision history for ogma-language-cocospec -## [1.X.Y] - 2023-02-01 +## [1.X.Y] - 2023-03-21 * Support inequality operator (#71). +* Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From ffe45526c9772d9f30ef58277e4f9c5be45b7474 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 30/51] ogma-language-c: Document changes in CHANGELOG. Refs #74. --- ogma-language-c/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-language-c/CHANGELOG.md b/ogma-language-c/CHANGELOG.md index d876ebf2..48dce1b2 100644 --- a/ogma-language-c/CHANGELOG.md +++ b/ogma-language-c/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-c +## [1.X.Y] - 2023-03-21 + +* Mark package as uncurated (#74). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). * Specify upper bound constraint for Cabal. Refs #69. From be6d6d310832d7737872c4ac9f2ca96a066e1436 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 31/51] ogma-extra: Document changes in CHANGELOG. Refs #74. --- ogma-extra/CHANGELOG.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/ogma-extra/CHANGELOG.md b/ogma-extra/CHANGELOG.md index 4ec85ecb..7e7dbcfb 100644 --- a/ogma-extra/CHANGELOG.md +++ b/ogma-extra/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-extra +## [1.X.Y] - 2023-03-21 + +* Mark package as uncurated (#74). + ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 2285a33fe12529659e25e4fefc7e0738597cec7f Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 32/51] ogma-core: Document changes in CHANGELOG. Refs #74. --- ogma-core/CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 6a5bbe4e..5b0359c8 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -4,6 +4,7 @@ * Support inequality operator in SMV and CoCoSpec (#71). * Introduce new F' (FPrime) backend (#77). +* Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 97901f13abc59e71b10e89beed2365af84251991 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 17:04:33 -0700 Subject: [PATCH 33/51] ogma-cli: Document changes in CHANGELOG. Refs #74. --- ogma-cli/CHANGELOG.md | 1 + 1 file changed, 1 insertion(+) diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index 2966f938..e42be75b 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -3,6 +3,7 @@ ## [1.X.Y] - 2023-03-21 * Introduce new F' (FPrime) backend (#77). +* Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 * Version bump 1.0.7 (#69). From 921fec5f4a29c89106932e0c8b76babf82f6aae1 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 34/51] ogma-extra: Version bump (1.0.8). Refs #81. --- ogma-extra/ogma-extra.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ogma-extra/ogma-extra.cabal b/ogma-extra/ogma-extra.cabal index 750ee599..30ad92b9 100644 --- a/ogma-extra/ogma-extra.cabal +++ b/ogma-extra/ogma-extra.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-extra -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf From 3e3c372ca6ec3fa9800ac87e8cf42bb3eefe540d Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 35/51] ogma-language-c: Version bump (1.0.8). Refs #81. --- ogma-language-c/ogma-language-c.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ogma-language-c/ogma-language-c.cabal b/ogma-language-c/ogma-language-c.cabal index 0551c5f2..8b3f109a 100644 --- a/ogma-language-c/ogma-language-c.cabal +++ b/ogma-language-c/ogma-language-c.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Custom name: ogma-language-c -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf From 46a5055ab0498779c040e1035dbeb76e7855d931 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 36/51] ogma-language-cocospec: Version bump (1.0.8). Refs #81. --- ogma-language-cocospec/ogma-language-cocospec.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ogma-language-cocospec/ogma-language-cocospec.cabal b/ogma-language-cocospec/ogma-language-cocospec.cabal index 377c41bb..c0a6014a 100644 --- a/ogma-language-cocospec/ogma-language-cocospec.cabal +++ b/ogma-language-cocospec/ogma-language-cocospec.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Custom name: ogma-language-cocospec -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf From 3f05424b6b8121b63d7d75872377c384226abee7 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 37/51] ogma-language-copilot: Version bump (1.0.8). Refs #81. --- ogma-language-copilot/ogma-language-copilot.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ogma-language-copilot/ogma-language-copilot.cabal b/ogma-language-copilot/ogma-language-copilot.cabal index 517573f5..5aec5083 100644 --- a/ogma-language-copilot/ogma-language-copilot.cabal +++ b/ogma-language-copilot/ogma-language-copilot.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-language-copilot -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf From 4c704b278307b6c616039b93310c7f05f31c85e9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 38/51] ogma-language-smv: Version bump (1.0.8). Refs #81. --- ogma-language-smv/ogma-language-smv.cabal | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ogma-language-smv/ogma-language-smv.cabal b/ogma-language-smv/ogma-language-smv.cabal index e859faa1..e5bd6d75 100644 --- a/ogma-language-smv/ogma-language-smv.cabal +++ b/ogma-language-smv/ogma-language-smv.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Custom name: ogma-language-smv -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf From 0e0e5d5ae8c78a303a35599eb11928c866f9e8d5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 39/51] ogma-language-fret-cs: Version bump (1.0.8). Refs #81. We choose to bump the version constraints for all dependencies at once to keep them in sync, since it will be much easier than trying to track the version number of each dependency inside the Ogma project. --- ogma-language-fret-cs/ogma-language-fret-cs.cabal | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ogma-language-fret-cs/ogma-language-fret-cs.cabal b/ogma-language-fret-cs/ogma-language-fret-cs.cabal index a4b975cd..d16d6537 100644 --- a/ogma-language-fret-cs/ogma-language-fret-cs.cabal +++ b/ogma-language-fret-cs/ogma-language-fret-cs.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-language-fret-cs -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -68,8 +68,8 @@ library base >= 4.11.0.0 && < 5 , aeson >= 2.0.0.0 && < 2.2 - , ogma-language-cocospec >= 1.0.0 && < 1.1 - , ogma-language-smv >= 1.0.0 && < 1.1 + , ogma-language-cocospec >= 1.0.8 && < 1.1 + , ogma-language-smv >= 1.0.8 && < 1.1 hs-source-dirs: src @@ -95,7 +95,7 @@ test-suite unit-tests , test-framework , test-framework-quickcheck2 - , ogma-extra >= 1.0.0 && < 1.1 + , ogma-extra >= 1.0.8 && < 1.1 , ogma-language-fret-cs hs-source-dirs: From 62dfa00211b2a2b114f8dfdaefe01470598e6218 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 40/51] ogma-language-fret-reqs: Version bump (1.0.8). Refs #81. We choose to bump the version constraints for all dependencies at once to keep them in sync, since it will be much easier than trying to track the version number of each dependency inside the Ogma project. --- ogma-language-fret-reqs/ogma-language-fret-reqs.cabal | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal b/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal index e9e75777..7ebd9f20 100644 --- a/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal +++ b/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-language-fret-reqs -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -69,8 +69,8 @@ library , aeson >= 2.0.0.0 && < 2.2 , text - , ogma-language-cocospec >= 1.0.0 && < 1.1 - , ogma-language-smv >= 1.0.0 && < 1.1 + , ogma-language-cocospec >= 1.0.8 && < 1.1 + , ogma-language-smv >= 1.0.8 && < 1.1 hs-source-dirs: src @@ -96,7 +96,7 @@ test-suite unit-tests , test-framework , test-framework-quickcheck2 - , ogma-extra >= 1.0.0 && < 1.1 + , ogma-extra >= 1.0.8 && < 1.1 , ogma-language-fret-reqs hs-source-dirs: From e52c85feb03e1f97707713a83da85620f7a5a7e2 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 41/51] ogma-core: Version bump (1.0.8). Refs #81. We choose to bump the version constraints for all dependencies at once to keep them in sync, since it will be much easier than trying to track the version number of each dependency inside the Ogma project. In this case, the change is needed also because this version of ogma-core needs definitions that will be published in ogma-language-smv and ogma-language-cocospec. --- ogma-core/ogma-core.cabal | 16 ++++++++-------- 1 file changed, 8 insertions(+), 8 deletions(-) diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 05597d63..0762f6d0 100644 --- a/ogma-core/ogma-core.cabal +++ b/ogma-core/ogma-core.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-core -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -109,13 +109,13 @@ library , IfElse , mtl - , ogma-extra >= 1.0.0 && < 1.1 - , ogma-language-c >= 1.0.0 && < 1.1 - , ogma-language-cocospec >= 1.0.0 && < 1.1 - , ogma-language-copilot >= 1.0.0 && < 1.1 - , ogma-language-fret-cs >= 1.0.0 && < 1.1 - , ogma-language-fret-reqs >= 1.0.0 && < 1.1 - , ogma-language-smv >= 1.0.0 && < 1.1 + , 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 hs-source-dirs: src From 5d06181313ab42e4f1707083eafd27e8d63b89d6 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:36:12 -0700 Subject: [PATCH 42/51] ogma-cli: Version bump (1.0.8). Refs #81. --- ogma-cli/ogma-cli.cabal | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ogma-cli/ogma-cli.cabal b/ogma-cli/ogma-cli.cabal index de68f4d0..26c74f30 100644 --- a/ogma-cli/ogma-cli.cabal +++ b/ogma-cli/ogma-cli.cabal @@ -32,7 +32,7 @@ cabal-version: 2.0 build-type: Simple name: ogma-cli -version: 1.0.7 +version: 1.0.8 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -135,7 +135,7 @@ executable ogma build-depends: base >= 4.11.0.0 && < 5 , optparse-applicative - , ogma-core >= 1.0.7 && < 1.1 + , ogma-core >= 1.0.8 && < 1.1 hs-source-dirs: src From 26fb6d57f069401a4b20512f01ee232b2cb1a5b5 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 43/51] ogma-extra: Document changes in CHANGELOG. Refs #81. --- ogma-extra/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-extra/CHANGELOG.md b/ogma-extra/CHANGELOG.md index 7e7dbcfb..136412d9 100644 --- a/ogma-extra/CHANGELOG.md +++ b/ogma-extra/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-extra -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 From c47c1032659b97618ce507a97a34e1d62ce707bb Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 44/51] ogma-language-c: Document changes in CHANGELOG. Refs #81. --- ogma-language-c/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-c/CHANGELOG.md b/ogma-language-c/CHANGELOG.md index 48dce1b2..f48f4042 100644 --- a/ogma-language-c/CHANGELOG.md +++ b/ogma-language-c/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-language-c -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 From ffafc604318a61551a5c3098dde9b69bb48d8217 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 45/51] ogma-language-cocospec: Document changes in CHANGELOG. Refs #81. --- ogma-language-cocospec/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-cocospec/CHANGELOG.md b/ogma-language-cocospec/CHANGELOG.md index 7a434463..07db6959 100644 --- a/ogma-language-cocospec/CHANGELOG.md +++ b/ogma-language-cocospec/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-language-cocospec -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Support inequality operator (#71). * Mark package as uncurated (#74). From 7ff1e01b3e5fbd29e39d6525f1192f9c90241a81 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 46/51] ogma-language-copilot: Document changes in CHANGELOG. Refs #81. --- ogma-language-copilot/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-copilot/CHANGELOG.md b/ogma-language-copilot/CHANGELOG.md index f9c864ca..64e8f7a3 100644 --- a/ogma-language-copilot/CHANGELOG.md +++ b/ogma-language-copilot/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-language-copilot -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 From dd2004e01dffbe994dd90f9bed842dcb6b5f2571 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 47/51] ogma-language-smv: Document changes in CHANGELOG. Refs #81. --- ogma-language-smv/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-smv/CHANGELOG.md b/ogma-language-smv/CHANGELOG.md index 75c81303..bdf95021 100644 --- a/ogma-language-smv/CHANGELOG.md +++ b/ogma-language-smv/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-language-smv -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Support inequality operator (#71). * Mark package as uncurated (#74). From 46198a24c60b6dbe42beb9b181bd490b0145e0e3 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 48/51] ogma-language-fret-cs: Document changes in CHANGELOG. Refs #81. --- ogma-language-fret-cs/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-fret-cs/CHANGELOG.md b/ogma-language-fret-cs/CHANGELOG.md index f7cd23bb..727bff82 100644 --- a/ogma-language-fret-cs/CHANGELOG.md +++ b/ogma-language-fret-cs/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-language-fret-cs -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 From c9985b5fa55bab43bd30174aa45927fd0c39318e Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 49/51] ogma-language-fret-reqs: Document changes in CHANGELOG. Refs #81. --- ogma-language-fret-reqs/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-language-fret-reqs/CHANGELOG.md b/ogma-language-fret-reqs/CHANGELOG.md index 530998e8..747036e7 100644 --- a/ogma-language-fret-reqs/CHANGELOG.md +++ b/ogma-language-fret-reqs/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-language-fret-reqs -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Mark package as uncurated (#74). ## [1.0.7] - 2023-01-21 From 9c562d791feb24bad6dcc3cb73b77f6516135af9 Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 50/51] ogma-core: Document changes in CHANGELOG. Refs #81. --- ogma-core/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index 5b0359c8..578ecb68 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-core -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Support inequality operator in SMV and CoCoSpec (#71). * Introduce new F' (FPrime) backend (#77). * Mark package as uncurated (#74). From b1396353c8698ae00e503023368a5980e8285b3a Mon Sep 17 00:00:00 2001 From: Ivan Perez Date: Tue, 21 Mar 2023 18:38:10 -0700 Subject: [PATCH 51/51] ogma-cli: Document changes in CHANGELOG. Refs #81. --- ogma-cli/CHANGELOG.md | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index e42be75b..e9e3cde9 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -1,7 +1,8 @@ # Revision history for ogma-cli -## [1.X.Y] - 2023-03-21 +## [1.0.8] - 2023-03-21 +* Version bump 1.0.8 (#81). * Introduce new F' (FPrime) backend (#77). * Mark package as uncurated (#74).