diff --git a/ogma-cli/CHANGELOG.md b/ogma-cli/CHANGELOG.md index cc5b594..3f62cd5 100644 --- a/ogma-cli/CHANGELOG.md +++ b/ogma-cli/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for ogma-cli +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Re-structure README around on backends (#75). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-cli/README.md b/ogma-cli/README.md index 1c89919..b008a05 100644 --- a/ogma-cli/README.md +++ b/ogma-cli/README.md @@ -7,31 +7,20 @@ verification framework that generates hard real-time C99 code. # Features -- Translating requirements defined in [NASA's requirements elicitation tool - FRET](https://github.com/NASA-SW-VnV/fret) into corresponding monitors in - Copilot. +- Generating [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) runtime + monitoring applications that monitor data received from the message bus. -- Generating [NASA Core Flight System](https://cfs.gsfc.nasa.gov/) applications - that use Copilot for monitoring data received from the message bus. +- Generating [Robot Operating System](https://ros.org) runtime monitoring + applications. + +- Generating [F' (FPrime)](https://github.com/nasa/fprime/) runtime monitoring + components. - Generating message handlers for NASA Core Flight System applications to make external data in structs available to a Copilot monitor. - Generating the glue code necessary to work with C structs in Copilot. -- 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 -
- Conversion of FRET requirements into C code. -

-

Monitoring within simulation video
@@ -44,7 +33,6 @@ verification framework that generates hard real-time C99 code. - [Pre-requisites](#pre-requisites) - [Compilation](#compilation) - [Usage](#usage) - - [Language Transformations: FRET](#language-transformations-fret) - [cFS Application Generation](#cfs-application-generation) - [ROS Application Generation](#ros-application-generation) - [F' Component Generation](#f-component-generation) @@ -98,215 +86,8 @@ After that, the `ogma` executable will be placed in the directory # Usage [(Back to top)](#table-of-contents) -The main invocation of `ogma` with `--help` lists sub-commands available: -```sh -$ ogma --help -ogma - an anything-to-Copilot application generator - -Usage: ogma COMMAND - Generate complete or partial Copilot applications from multiple languages - -Available options: - -h,--help Show this help text - -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 - Database - ros Generate a ROS 2 monitoring package -``` - -## Language transformations: FRET -[(Back to top)](#table-of-contents) - -[FRET](https://github.com/NASA-SW-VnV/fret) is a requirements elicitation tool -created by NASA Ames Research Center. Requirements can be specified in -structured natural language called FRETish, and the tool helps users understand -them, validate them, and formalize them. For instructions on how to specify, -analyze and export FRET requirements, see [the FRET -manual](https://github.com/NASA-SW-VnV/fret/blob/master/fret-electron/docs/_media/userManual.md). - -

- -
-Screenshot of requirement specified inside NASA's requirements elicitation tool FRET. -

- -Ogma can convert specifications generated by FRET into Copilot monitors. -Specifically, the commands `fret-component-spec` and `fret-reqs-db` allow users -to interact with the different kinds of files produced by FRET. - -FRET files include properties encoded using Temporal Logic, both in -[SMV](http://www.cs.cmu.edu/~modelcheck/smv.html) and in -[CoCoSpec](https://link.springer.com/chapter/10.1007%2F978-3-319-41591-8_24), -the latter of which is an extension of Lustre. Ogma uses the SMV expressions by -default, but the CLI flag `--cocospec` can be used to select the CoCoSpec -variant of requirements instead. - -As an example, from the following FRET requirement: -``` -test_component shall satisfy (input_signal <= 5) -``` - -Ogma generates the following Copilot specification: - -```haskell -import Copilot.Compile.C99 -import Copilot.Language hiding (prop) -import Copilot.Language.Prelude -import Copilot.Library.LTL (next) -import Copilot.Library.MTL hiding (since, alwaysBeen, trigger) -import Copilot.Library.PTLTL (since, previous, alwaysBeen) -import Language.Copilot (reify) -import Prelude hiding ((&&), (||), (++), not, (<=), (>=), (<), (>)) - -input_signal :: Stream Double -input_signal = extern "input_signal" Nothing - --- | propTestCopilot_001 --- @ --- test_component shall satisfy (input_signal <= 5) --- @ -propTestCopilot_001 :: Stream Bool -propTestCopilot_001 = ( alwaysBeen (( ( ( input_signal <= 5 ) ) )) ) - --- | Complete specification. Calls the C function void handler(); when --- the property is violated. -spec :: Spec -spec = do - trigger "handlerpropTestCopilot_001" (not propTestCopilot_001) [] - -main :: IO () -main = reify spec >>= compile "fret" -``` - -This program can be compiled using Copilot to generate a `fret.c` file that -includes a hard real-time C99 implementation of the monitor. The specification -generated by FRET for the FRETish requirement shown above is included with the -Ogma distribution, and can be tested with: - -```sh -$ ogma fret-component-spec --cocospec --fret-file-name examples/fret-reqs-small.json > FretCopilot.hs -$ runhaskell FretCopilot.hs -``` - -The first step executes `ogma`, generating a Copilot monitor in a file called -`FretCopilot.hs`. The second step executes the Copilot compiler, generating a C -implementation `fret.c` and C header file `fret.h`. - -The resulting `fret.c` file can be tested with the main provided in -`examples/fret-reqs-small-main.c`, which defines a handler for Copilot to call -when the property monitored is violated, and a main function that steps through -the execution, providing new data for the Copilot monitor: - -```c -#include - -double input_signal; // Input data made available for the monitor -void step(void); // Copilot monitor's main entry point - -void handlerpropTestCopilot_001(void) { - printf("Monitor condition violated\n"); -} - -int main (int argc, char** argv) { - int i = 0; - - input_signal = 0; - - for (i=0; i<10; i++) { - printf("Running step %d\n", i); - input_signal += 1; - step(); - } - return 0; -} -``` - -To compile both files, run `gcc examples/fret-reqs-small-main.c fret.c -o -main`. Executing the resulting `main` shows that the condition is violated -after a number of steps: -``` -Running step 0 -Running step 1 -Running step 2 -Running step 3 -Running step 4 -Running step 5 -Monitor condition violated -Running step 6 -Monitor condition violated -Running step 7 -Monitor condition violated -Running step 8 -Monitor condition violated -Running step 9 -Monitor condition violated -``` - -Take a peek inside the intermediate files `FretCopilot.hs`, `fret.c` and -`fret.h` to see what is being generated by Ogma and by Copilot. - -The generated C code can be integrated as part of a larger application. For -example, the following shows a Copilot monitor generated from a FRET file -integrated in an X-Plane widget that presents information to users during a -flight in the X-Plane simulator. - -

- -
-Screenshot of Copilot monitor generated by Ogma from FRET requirement, -integrated into the X-Plane flight simulator. The widget on the right side of -the screen presents information received and returned by the monitor, with a -red/fire icon to signal that the monitor has been triggered (i.e., that the -property has been violated). -

- -**Numeric Representations** - -FRET Component Specifications use the types `real` and `int` to represent -different numeric variables. Copilot distinguishes between different numeric -representations and supports multiple precisions, and so does the final C -code generated from the Copilot specification. - -To help users generate code that works as part of a larger system without -modifications, Ogma includes two additional flags to map the types `real` and -`int` to specific Copilot (Haskell) types. For example, the following command -would generate a Copilot specification for a hypothetical -`numeric-example.json` FRET CS file while mapping all real variables to the -type `Double` and all integer variables to the type `Int32`: - -``` -$ ogma fret-component-spec --fret-file-name numeric-example.json --map-int-to Int32 --map-real-to Double -``` - -In the name of flexibility, Ogma does not sanitize the values of these -variables and copies the types passed to these options verbatim to the -generated Copilot code. It is the user's responsibility to ensure the types -passed are valid Haskell types within the scope of the module generated. -Note that Copilot supports only a limited subset of numeric types, which -must be instances of the type class -[`Typed`](https://hackage.haskell.org/package/copilot-core/docs/Copilot-Core-Type.html#t:Typed). - -**Name customization** - -All FRET-related commands allow for customization of the target C filenames via -an argument `--target-file-name`. For example, the following execution causes -the C files produced by Copilot to be called `monitor.c`, `monitor.h` and -`monitor_types.h`, as opposed to the default names `fret.c`, `fret.h` and -`fret_types.h`, respectively: - -```sh -$ ogma fret-component-spec --cocospec --fret-file-name examples/fret-reqs-small.json --target-file-name monitor > FretCopilot.hs -$ runhaskell FretCopilot.hs -$ ls monitor* -monitor.c monitor.h monitor_types.h -``` +The main invocation of `ogma` with `--help` lists sub-commands available. More +details are provided in the following sections. ## cFS Application Generation @@ -415,10 +196,9 @@ the data needed by the monitors and report any violations. At present, support for ROS app generation is considered preliminary. ROS applications are generated using the Ogma command `ros`, which receives -five main arguments: +four main arguments: - `--app-target-dir DIR`: location where the ROS 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, @@ -426,17 +206,10 @@ and the topic they are included with. - `--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 ROS application for runtime monitoring using Copilot: ```sh -$ ogma ros --fret-file-name Export.json --variable-file variables --variable-db ros-variable-db --app-target-dir ros_demo +$ ogma ros --handlers filename --variable-file variables --variable-db ros-variable-db --app-target-dir ros_demo ``` The application generated by Ogma contains the following files: @@ -475,7 +248,6 @@ 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, @@ -483,17 +255,10 @@ 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 +$ ogma fprime --handlers filename --variable-file filename --variable-db fprime-variable-db --app-target-dir fprime_demo ``` The component generated by Ogma contains the following files: @@ -506,19 +271,6 @@ 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 --target-file-name copilot > 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. @@ -536,8 +288,8 @@ 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 +specification, or property/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 @@ -559,13 +311,6 @@ $ 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, @@ -632,12 +377,9 @@ changes. Ogma has been created by Ivan Perez and Alwyn Goodloe. -The Ogma team would like to thank Dimitra Giannakopoulou, Anastasia Mavridou, -and Thomas Pressburger, from the FRET Team at NASA Ames, for the continued -input during the development of Ogma. - -We would also like to thank Cesar Munoz and Swee Balachandran, for their help -with the cFS backend. +The Ogma team would like to thank Swee Balachandran, Dimitra Giannakopoulou, +Anastasia Mavridou, Cesar Munoz and Thomas Pressburger, for the input during +the development of Ogma. X-Plane images obtained via the X-Plane 10 (Pro) flight simulator. Re-shared with permission. diff --git a/ogma-cli/ogma-cli.cabal b/ogma-cli/ogma-cli.cabal index 140ac61..9fded44 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -141,7 +141,7 @@ executable ogma build-depends: base >= 4.11.0.0 && < 5 , optparse-applicative - , ogma-core >= 1.1.0 && < 1.2 + , ogma-core >= 1.2.0 && < 1.3 hs-source-dirs: src diff --git a/ogma-core/CHANGELOG.md b/ogma-core/CHANGELOG.md index f7ec75f..030a87c 100644 --- a/ogma-core/CHANGELOG.md +++ b/ogma-core/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for ogma-core +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Generalize JSON parser (#115). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-core/ogma-core.cabal b/ogma-core/ogma-core.cabal index 87c37bc..5dc9ac1 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -92,8 +92,8 @@ library Language.Trans.CStruct2CopilotStruct Language.Trans.CStructs2Copilot Language.Trans.CStructs2MsgHandlers - Language.Trans.FRETComponentSpec2Copilot Language.Trans.FRETReqsDB2Copilot + Language.Trans.Spec2Copilot Language.Trans.SMV2Copilot other-modules: @@ -105,17 +105,19 @@ library build-depends: base >= 4.11.0.0 && < 5 , aeson >= 2.0.0.0 && < 2.2 + , bytestring , filepath , IfElse , mtl - , ogma-extra >= 1.1.0 && < 1.2 - , ogma-language-c >= 1.1.0 && < 1.2 - , ogma-language-cocospec >= 1.1.0 && < 1.2 - , ogma-language-copilot >= 1.1.0 && < 1.2 - , ogma-language-fret-cs >= 1.1.0 && < 1.2 - , ogma-language-fret-reqs >= 1.1.0 && < 1.2 - , ogma-language-smv >= 1.1.0 && < 1.2 + , ogma-extra >= 1.2.0 && < 1.3 + , ogma-language-c >= 1.2.0 && < 1.3 + , ogma-language-cocospec >= 1.2.0 && < 1.3 + , ogma-language-copilot >= 1.2.0 && < 1.3 + , ogma-language-fret-reqs >= 1.2.0 && < 1.3 + , ogma-language-jsonspec >= 1.2.0 && < 1.3 + , ogma-language-smv >= 1.2.0 && < 1.3 + , ogma-spec >= 1.2.0 && < 1.3 hs-source-dirs: src diff --git a/ogma-core/src/Command/FPrimeApp.hs b/ogma-core/src/Command/FPrimeApp.hs index 66d060f..da60c15 100644 --- a/ogma-core/src/Command/FPrimeApp.hs +++ b/ogma-core/src/Command/FPrimeApp.hs @@ -53,13 +53,14 @@ import Data.ByteString.Extra as B ( safeReadFile ) import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier ) import System.Directory.Extra ( copyDirectoryRecursive ) +-- External imports: ogma +import Data.OgmaSpec (Spec, externalVariableName, externalVariables, + requirementName, requirements) +import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) + -- 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 ) @@ -153,14 +154,13 @@ fprimeApp' targetDir varNames varDB monitors = -- | Process FRET component spec, if available, and return its abstract -- representation. parseOptionalFRETCS :: Maybe FilePath - -> ExceptT ErrorTriplet IO (Maybe FRETComponentSpec) + -> ExceptT ErrorTriplet IO (Maybe (Spec String)) 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 + let fretCS :: Either String (Spec String) + fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content case fretCS of Left e -> throwError $ cannotOpenFRETFile fp e @@ -219,7 +219,7 @@ parseOptionalVarDBFile (Just fp) = do -- -- If a FRET file is not provided, then the user must provide BOTH a variable -- list, and a list of handlers. -checkArguments :: Maybe FRETComponentSpec +checkArguments :: Maybe (Spec a) -> Maybe [String] -> Maybe [String] -> Either ErrorTriplet () @@ -232,19 +232,19 @@ checkArguments _ _ _ = Right () -- | Extract the variables from a FRET component specification, and sanitize -- them to be used in FPrime. -fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String] +fretCSExtractExternalVariables :: Maybe (Spec a) -> [String] fretCSExtractExternalVariables Nothing = [] fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier - $ map fretExternalVariableName - $ fretExternalVariables cs + $ map externalVariableName + $ externalVariables 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 :: Maybe (Spec a) -> [String] fretCSExtractHandlers Nothing = [] fretCSExtractHandlers (Just cs) = map handlerNameF - $ map fretRequirementName - $ fretRequirements cs + $ map requirementName + $ requirements cs where handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier @@ -737,3 +737,19 @@ ecCannotOpenHandlersFile = 1 -- permissions or some I/O error. ecCannotCopyTemplate :: ErrorCode ecCannotCopyTemplate = 1 + +-- | JSONPath selectors for a FRET file +fretFormat :: JSONFormat +fretFormat = JSONFormat + { specInternalVars = "..Internal_variables[*]" + , specInternalVarId = ".name" + , specInternalVarExpr = ".assignmentCopilot" + , specInternalVarType = ".type" + , specExternalVars = "..Other_variables[*]" + , specExternalVarId = ".name" + , specExternalVarType = ".type" + , specRequirements = "..Requirements[*]" + , specRequirementId = ".name" + , specRequirementDesc = ".fretish" + , specRequirementExpr = ".ptLTL" + } diff --git a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs b/ogma-core/src/Command/FRETComponentSpec2Copilot.hs index b0ee34a..697f427 100644 --- a/ogma-core/src/Command/FRETComponentSpec2Copilot.hs +++ b/ogma-core/src/Command/FRETComponentSpec2Copilot.hs @@ -1,3 +1,4 @@ +{-# LANGUAGE ExistentialQuantification #-} -- Copyright 2020 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- @@ -41,7 +42,8 @@ module Command.FRETComponentSpec2Copilot -- External imports import Control.Monad.IfElse ( awhen ) -import Data.Aeson ( eitherDecode ) +import Data.Aeson ( eitherDecode, decode ) +import Data.ByteString.Lazy (fromStrict) -- External imports: auxiliary import Data.ByteString.Extra as B ( safeReadFile ) @@ -50,12 +52,22 @@ import Data.ByteString.Extra as B ( safeReadFile ) import Command.Result ( Result (..) ) import Data.Location ( Location (..) ) --- Internal imports -import Language.FRETComponentSpec.AST ( FRETComponentSpec ) -import qualified Language.Trans.FRETComponentSpec2Copilot as T - ( fretComponentSpec2Copilot - , FRETComponentSpec2CopilotOptions(FRETComponentSpec2CopilotOptions) - ) +-- Internal imports: language ASTs, transformers +import Data.OgmaSpec (Spec) + +import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec +import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, + pBoolSpec ) + +import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) + +import qualified Language.SMV.AbsSMV as SMV +import qualified Language.SMV.ParSMV as SMV (myLexer, pBoolSpec) +import Language.SMV.Substitution (substituteBoolExpr) + +import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec (boolSpec2Copilot) +import Language.Trans.SMV2Copilot as SMV (boolSpec2Copilot) +import Language.Trans.Spec2Copilot (spec2Copilot, specAnalyze) -- | Print the contents of a Copilot module that implements the Past-time TL -- formula in a FRET file. @@ -72,15 +84,9 @@ fretComponentSpec2Copilot :: FilePath -- ^ Path to a file containing a FRET -> IO (Result ErrorCode) fretComponentSpec2Copilot fp options = do - -- All of the following operations use Either to return error messages. The - -- use of the monadic bind to pass arguments from one function to the next - -- will cause the program to stop at the earliest error. - fret <- parseFretComponentSpec fp + let functions = fretExprPair (fretCS2CopilotUseCoCoSpec options) - -- Extract internal command options from external command options - let internalOptions = fretComponentSpec2CopilotOptions options - - let copilot = T.fretComponentSpec2Copilot internalOptions =<< fret + copilot <- fretComponentSpec2Copilot' fp options functions let (mOutput, result) = fretComponentSpec2CopilotResult options fp copilot @@ -88,6 +94,34 @@ fretComponentSpec2Copilot fp options = do awhen mOutput putStrLn return result +-- | Print the contents of a Copilot module that implements the Past-time TL +-- formula in a FRET file, using a subexpression handler. +-- +-- PRE: The file given is readable, contains a valid FRET file with a PT +-- formula in the @ptExpanded@ key, the formula does not use any identifiers +-- that exist in Copilot, or any of @prop@, @clock@, @ftp@. All identifiers +-- used are valid C99 identifiers. +fretComponentSpec2Copilot' :: FilePath + -> FRETComponentSpec2CopilotOptions + -> FRETExprPair + -> IO (Either String String) +fretComponentSpec2Copilot' fp options (FRETExprPair parse replace print) = do + let name = fretCS2CopilotFilename options + useCoCoSpec = fretCS2CopilotUseCoCoSpec options + typeMaps = fretTypeToCopilotTypeMapping options + + -- All of the following operations use Either to return error messages. The + -- use of the monadic bind to pass arguments from one function to the next + -- will cause the program to stop at the earliest error. + content <- B.safeReadFile fp + res <- case content of + Left s -> return $ Left s + Right b -> return $ parseJSONSpec parse (fretFormat useCoCoSpec) =<< eitherDecode b + + let copilot = spec2Copilot name typeMaps replace print =<< specAnalyze =<< res + + return copilot + -- | Options used to customize the conversion of FRET Component Specifications -- to Copilot code. data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions @@ -97,17 +131,6 @@ data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions , fretCS2CopilotFilename :: String } --- | Parse a JSON file containing a FRET component specification. --- --- Returns a 'Left' with an error message if the file does not have the correct --- format. --- --- Throws an exception if the file cannot be read. -parseFretComponentSpec :: FilePath -> IO (Either String FRETComponentSpec) -parseFretComponentSpec fp = do - content <- B.safeReadFile fp - return $ eitherDecode =<< content - -- * Error codes -- | Encoding of reasons why the command can fail. @@ -120,19 +143,6 @@ type ErrorCode = Int ecFretCSError :: ErrorCode ecFretCSError = 1 --- * Input arguments - --- | Convert command input argument options to internal transformation function --- input arguments. -fretComponentSpec2CopilotOptions :: FRETComponentSpec2CopilotOptions - -> T.FRETComponentSpec2CopilotOptions -fretComponentSpec2CopilotOptions options = - T.FRETComponentSpec2CopilotOptions - (fretCS2CopilotUseCoCoSpec options) - (fretCS2CopilotIntType options) - (fretCS2CopilotRealType options) - (fretCS2CopilotFilename options) - -- * Result -- | Process the result of the transformation function. @@ -143,3 +153,52 @@ fretComponentSpec2CopilotResult :: FRETComponentSpec2CopilotOptions fretComponentSpec2CopilotResult options fp result = case result of Left msg -> (Nothing, Error ecFretCSError msg (LocationFile fp)) Right t -> (Just t, Success) + +-- * Parser + +-- | JSONPath selectors for a FRET file +fretFormat :: Bool -> JSONFormat +fretFormat useCoCoSpec = JSONFormat + { specInternalVars = "..Internal_variables[*]" + , specInternalVarId = ".name" + , specInternalVarExpr = ".assignmentCopilot" + , specInternalVarType = ".type" + , specExternalVars = "..Other_variables[*]" + , specExternalVarId = ".name" + , specExternalVarType = ".type" + , specRequirements = "..Requirements[*]" + , specRequirementId = ".name" + , specRequirementDesc = ".fretish" + , specRequirementExpr = if useCoCoSpec then ".CoCoSpecCode" else ".ptLTL" + } + +-- * Mapping of types from FRET to Copilot +fretTypeToCopilotTypeMapping :: FRETComponentSpec2CopilotOptions + -> [(String, String)] +fretTypeToCopilotTypeMapping options = + [ ("bool", "Bool") + , ("int", fretCS2CopilotIntType options) + , ("integer", fretCS2CopilotIntType options) + , ("real", fretCS2CopilotRealType options) + , ("string", "String") + ] + +-- * Handler for boolean expressions + +-- | Handler for boolean expressions that knows how to parse them, replace +-- variables in them, and convert them to Copilot. +data FRETExprPair = forall a . FRETExprPair + { exprParse :: String -> Either String a + , exprReplace :: [(String, String)] -> a -> a + , exprPrint :: a -> String + } + +-- | Return a handler depending on whether it should be for CoCoSpec boolean +-- expressions or for SMV boolean expressions. +fretExprPair :: Bool -> FRETExprPair +fretExprPair True = FRETExprPair (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) + (\_ -> id) + (CoCoSpec.boolSpec2Copilot) +fretExprPair False = FRETExprPair (SMV.pBoolSpec . SMV.myLexer) + (substituteBoolExpr) + (SMV.boolSpec2Copilot) diff --git a/ogma-core/src/Command/ROSApp.hs b/ogma-core/src/Command/ROSApp.hs index 306ffff..d3e2f79 100644 --- a/ogma-core/src/Command/ROSApp.hs +++ b/ogma-core/src/Command/ROSApp.hs @@ -56,13 +56,14 @@ import Data.ByteString.Extra as B (safeReadFile) import Data.String.Extra (sanitizeLCIdentifier, sanitizeUCIdentifier) import System.Directory.Extra (copyDirectoryRecursive) +-- External imports: ogma +import Data.OgmaSpec (Spec, externalVariableName, externalVariables, + requirementName, requirements) +import Language.JSONSpec.Parser (JSONFormat (..), parseJSONSpec) + -- 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 ) @@ -157,14 +158,13 @@ rosApp' targetDir varNames varDB monitors = -- | Process FRET component spec, if available, and return its abstract -- representation. parseOptionalFRETCS :: Maybe FilePath - -> ExceptT ErrorTriplet IO (Maybe FRETComponentSpec) + -> ExceptT ErrorTriplet IO (Maybe (Spec String)) 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 + let fretCS :: Either String (Spec String) + fretCS = parseJSONSpec return fretFormat =<< eitherDecode =<< content case fretCS of Left e -> throwError $ cannotOpenFRETFile fp e @@ -223,7 +223,7 @@ parseOptionalVarDBFile (Just fp) = do -- -- If a FRET file is not provided, then the user must provide BOTH a variable -- list, and a list of handlers. -checkArguments :: Maybe FRETComponentSpec +checkArguments :: Maybe (Spec String) -> Maybe [String] -> Maybe [String] -> Either ErrorTriplet () @@ -236,19 +236,19 @@ checkArguments _ _ _ = Right () -- | Extract the variables from a FRET component specification, and sanitize -- them to be used in ROS. -fretCSExtractExternalVariables :: Maybe FRETComponentSpec -> [String] +fretCSExtractExternalVariables :: Maybe (Spec String) -> [String] fretCSExtractExternalVariables Nothing = [] fretCSExtractExternalVariables (Just cs) = map sanitizeLCIdentifier - $ map fretExternalVariableName - $ fretExternalVariables cs + $ map externalVariableName + $ externalVariables 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 :: Maybe (Spec String) -> [String] fretCSExtractHandlers Nothing = [] fretCSExtractHandlers (Just cs) = map handlerNameF - $ map fretRequirementName - $ fretRequirements cs + $ map requirementName + $ requirements cs where handlerNameF = ("handlerprop" ++) . sanitizeUCIdentifier @@ -712,3 +712,19 @@ ecCannotOpenHandlersFile = 1 -- permissions or some I/O error. ecCannotCopyTemplate :: ErrorCode ecCannotCopyTemplate = 1 + +-- | JSONPath selectors for a FRET file +fretFormat :: JSONFormat +fretFormat = JSONFormat + { specInternalVars = "..Internal_variables[*]" + , specInternalVarId = ".name" + , specInternalVarExpr = ".assignmentCopilot" + , specInternalVarType = ".type" + , specExternalVars = "..Other_variables[*]" + , specExternalVarId = ".name" + , specExternalVarType = ".type" + , specRequirements = "..Requirements[*]" + , specRequirementId = ".name" + , specRequirementDesc = ".fretish" + , specRequirementExpr = ".ptLTL" + } diff --git a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs b/ogma-core/src/Language/Trans/Spec2Copilot.hs similarity index 50% rename from ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs rename to ogma-core/src/Language/Trans/Spec2Copilot.hs index d262997..a23e69b 100644 --- a/ogma-core/src/Language/Trans/FRETComponentSpec2Copilot.hs +++ b/ogma-core/src/Language/Trans/Spec2Copilot.hs @@ -1,4 +1,4 @@ --- Copyright 2020 United States Government as represented by the Administrator +-- Copyright 2024 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- -- Disclaimers @@ -27,69 +27,48 @@ -- 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. --- -{-# LANGUAGE OverloadedStrings #-} --- | Transform a FRET Component Specification into a Copilot specification. +-- | Transform an Ogma specification into a standalone Copilot specification. -- -- Normally, this module would be implemented as a conversion between ASTs, but -- we want to add comments to the generated code, which are not representable -- in the abstract syntax tree. -module Language.Trans.FRETComponentSpec2Copilot where +module Language.Trans.Spec2Copilot where -- External imports -import Data.List ( intersect, union ) +import Data.List ( intersect, lookup, union ) import Data.Maybe ( fromMaybe ) -- External imports: auxiliary import Data.String.Extra ( sanitizeLCIdentifier, sanitizeUCIdentifier ) --- Internal imports: language ASTs, transformers -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, - pBoolSpec ) -import Language.FRETComponentSpec.AST as FRET -import qualified Language.Trans.CoCoSpec2Copilot as CoCoSpec ( boolSpec2Copilot ) -import Language.Trans.SMV2Copilot as SMV ( boolSpec2Copilot ) - --- | Options used to customize the conversion of FRET Component Specifications --- to Copilot code. -data FRETComponentSpec2CopilotOptions = FRETComponentSpec2CopilotOptions - { fretCS2CopilotUseCoCoSpec :: Bool - , fretCS2CopilotIntType :: String - , fretCS2CopilotRealType :: String - , fretCS2CopilotFilename :: String - } - --- | Transform a FRET TL specification into a Copilot specification. --- --- This function may fail with a 'Left' value if the resulting Copilot --- specification would contain name clashes or other errors. -fretComponentSpec2Copilot :: FRETComponentSpec2CopilotOptions - -> FRETComponentSpec - -> Either String String -fretComponentSpec2Copilot prefs parseResult = - fretComponentSpec2Copilot' prefs =<< fret2CopilotAnalyze parseResult - --- | For a given FRET file, return the corresponding Copilot file, or an error +-- External imports: ogma-spec +import Data.OgmaSpec (ExternalVariableDef (..), InternalVariableDef (..), + Requirement (..), Spec (..)) + +-- | For a given spec, return the corresponding Copilot file, or an error -- message if such file cannot be generated. -- -- PRE: there are no name clashes between the variables and names used in the --- FRET specification and any definitions in Haskell's Prelude or in Copilot. -fretComponentSpec2Copilot' :: FRETComponentSpec2CopilotOptions - -> FRETComponentSpec - -> Either String String -fretComponentSpec2Copilot' prefs fretComponentSpec = - unlines . concat <$> sequence - [ pure imports - , pure externs +-- specification and any definitions in Haskell's Prelude or in Copilot. +spec2Copilot :: String -- Spec / target file name + -> [(String, String)] -- Type substitution table + -> ([(String, String)] -> a -> a) -- Expr subsitution function + -> (a -> String) -- Expr show function + -> Spec a -- Specification + -> Either String String +spec2Copilot specName typeMaps exprTransform showExpr spec = + pure $ unlines $ concat + [ imports + , externs , internals , reqs - , pure clock - , pure ftp - , pure pre - , pure tpre - , pure spec - , pure main' + , clock + , ftp + , pre + , tpre + , copilotSpec + , main' ] where @@ -115,90 +94,75 @@ fretComponentSpec2Copilot' prefs fretComponentSpec = -- Extern streams externs = concatMap externVarToDecl - (FRET.fretExternalVariables fretComponentSpec) + (externalVariables spec) where - externVarToDecl i = [ FRET.fretExternalVariableName i + externVarToDecl i = [ propName ++ " :: Stream " ++ "(" - ++ fretTypeToCopilotType - prefs - (FRET.fretExternalVariableType i) + ++ safeMap typeMaps (externalVariableType i) ++ ")" - , FRET.fretExternalVariableName i + , propName ++ " = " ++ "extern" ++ " " - ++ show (FRET.fretExternalVariableName i) + ++ show (externalVariableName i) ++ " " ++ "Nothing" , "" ] + where + propName = safeMap nameSubstitutions (externalVariableName i) -- Internal stream definitions - internals = concat - <$> mapM internalVarToDecl - (FRET.fretInternalVariables fretComponentSpec) + internals = concatMap internalVarToDecl + (internalVariables spec) where - internalVarToDecl i = fmap (\implem -> - [ FRET.fretInternalVariableName i + internalVarToDecl i = (\implem -> + [ propName ++ " :: Stream " ++ "(" - ++ fretTypeToCopilotType - prefs - (FRET.fretInternalVariableType i) + ++ safeMap typeMaps (internalVariableType i) ++ ")" - , FRET.fretInternalVariableName i + , propName ++ " = " ++ implem , "" ]) implementation where - implementation = if null (FRET.fretInternalVariableCopilot i) - then CoCoSpec.boolSpec2Copilot - <$> CoCoSpec.pBoolSpec - ( CoCoSpec.myLexer - $ FRET.fretInternalVariableLustre i - ) - else pure (FRET.fretInternalVariableCopilot i) + propName = safeMap nameSubstitutions (internalVariableName i) + implementation = (internalVariableExpr i) -- Encoding of requirements as boolean streams - reqs :: Either String [String] - reqs = concat <$> mapM reqToDecl (FRET.fretRequirements fretComponentSpec) + reqs :: [String] + reqs = concatMap reqToDecl (requirements spec) where - reqToDecl i = sequence - [ pure reqComment, pure reqSignature, reqBody, pure "" ] + reqToDecl i = [ reqComment, reqSignature + , reqBody nameSubstitutions + , "" + ] where + reqName = safeMap nameSubstitutions (requirementName i) + -- Definition comment, which includes the requirement for -- traceability purposes. - reqComment = "-- | " ++ FRET.fretRequirementName i ++ "\n" ++ + reqComment = "-- | " ++ requirementName i ++ "\n" ++ "-- @" ++ "\n" ++ - "-- " ++ FRET.fretRequirementFretish i ++ "\n" ++ + "-- " ++ requirementDescription i ++ "\n" ++ "-- @" -- Definition type signature. - reqSignature = FRET.fretRequirementName i + reqSignature = reqName ++ " :: " ++ "Stream" ++ " " ++ "Bool" - -- Definition implementation, either in SMV or in CoCoSpec - reqBody = if fretCS2CopilotUseCoCoSpec prefs - then reqBodyCoCo - else reqBodyPT + -- Definition implementation. We use an auxiliary function to + -- transform the implementation into Copilot, applying a + -- substitution. + reqBody subs = reqName ++ " = " ++ + (showExpr (exprTransform subs (requirementExpr i))) - reqBodyPT = fmap (\e -> FRET.fretRequirementName i ++ " = " - ++ SMV.boolSpec2Copilot e - ) - (fromMaybe (Left $ "No requirement for " ++ show i) - (FRET.fretRequirementPTExpanded i)) - - reqBodyCoCo = fmap - (\e -> FRET.fretRequirementName i ++ " = " - ++ CoCoSpec.boolSpec2Copilot e - ) - (fromMaybe (Left $ "No requirement for " ++ show i) - (FRET.fretRequirementCoCoSpec i)) -- Auxiliary streams: clock clock :: [String] @@ -231,55 +195,62 @@ fretComponentSpec2Copilot' prefs fretComponentSpec = ] -- Main specification - spec :: [String] - spec = [ "" - , "-- | Complete specification. Calls the C function void " - ++ " handler(); when" - , "-- the property is violated." - , "spec :: Spec" - , "spec = do" - ] - ++ triggers - ++ [ "" ] + copilotSpec :: [String] + copilotSpec = [ "" + , "-- | Complete specification. Calls the C function void " + ++ " handler(); when" + , "-- the property is violated." + , "spec :: Spec" + , "spec = do" + ] + ++ triggers + ++ [ "" ] where triggers :: [String] - triggers = fmap reqTrigger (FRET.fretRequirements fretComponentSpec) + triggers = fmap reqTrigger (requirements spec) - reqTrigger :: FRETRequirement -> String + reqTrigger :: Requirement a -> String reqTrigger r = " trigger " ++ show handlerName ++ " (not " ++ propName ++ ") " ++ "[]" where - handlerName = "handler" ++ FRET.fretRequirementName r - propName = FRET.fretRequirementName r + handlerName = "handler" ++ requirementName r + propName = requirementName r -- Main program that compiles specification to C in two files (code and -- header). main' :: [String] main' = [ "" , "main :: IO ()" - , "main = reify spec >>= compile \"" - ++ fretCS2CopilotFilename prefs ++ "\"" + , "main = reify spec >>= compile \"" ++ specName ++ "\"" ] --- | Return the corresponding type in Copilot matching a given FRET type. -fretTypeToCopilotType :: FRETComponentSpec2CopilotOptions -> String -> String -fretTypeToCopilotType _options "bool" = "Bool" -fretTypeToCopilotType options "int" = fretCS2CopilotIntType options -fretTypeToCopilotType options "integer" = fretCS2CopilotIntType options -fretTypeToCopilotType options "real" = fretCS2CopilotRealType options -fretTypeToCopilotType _options "string" = "String" -fretTypeToCopilotType _options x = x - --- | Analyze a FRET-Copilot file and determine if there will be any name --- clashes after the conversion to Copilot. --- --- This function does not compare against Haskell's prelude or Copilot's --- modules. It simply makes simple conversions to comply with Copilot/Haskell's --- grammar (e.g., variable/function names start with lowercase) and determines --- if the conversion would make two definitions in the given specification --- produce name clashes between them. -fret2CopilotAnalyze :: FRETComponentSpec -> Either String FRETComponentSpec -fret2CopilotAnalyze fretComponentSpec + -- Map from a variable name to its desired identifier in the code + -- generated. + internalVariableMap = + map (\x -> (x, sanitizeLCIdentifier x)) internalVariableNames + + externalVariableMap = + map (\x -> (x, sanitizeLCIdentifier x)) externalVariableNames + + requirementNameMap = + map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames + + nameSubstitutions = internalVariableMap + ++ externalVariableMap + ++ requirementNameMap + + -- Variable/requirement names used in the component spec. + internalVariableNames = map internalVariableName + $ internalVariables spec + + externalVariableNames = map externalVariableName + $ externalVariables spec + + requirementNames = map requirementName + $ requirements spec + +specAnalyze :: Spec a -> Either String (Spec a) +specAnalyze spec | not (null evnClash) = Left $ "Name clash detected: " ++ show evnClash @@ -290,7 +261,7 @@ fret2CopilotAnalyze fretComponentSpec = Left $ "Name clash detected: " ++ show reqClash | otherwise - = Right $ foldr applySubstitution fretComponentSpec nameSubstitutions + = Right spec where @@ -321,16 +292,21 @@ fret2CopilotAnalyze fretComponentSpec requirementNameMap = map (\x -> (x, "prop" ++ sanitizeUCIdentifier x)) requirementNames - nameSubstitutions = internalVariableMap - ++ externalVariableMap - ++ requirementNameMap - -- Variable/requirement names used in the component spec. - internalVariableNames = map fretInternalVariableName - $ fretInternalVariables fretComponentSpec + internalVariableNames = map internalVariableName + $ internalVariables spec + + externalVariableNames = map externalVariableName + $ externalVariables spec - externalVariableNames = map fretExternalVariableName - $ fretExternalVariables fretComponentSpec + requirementNames = map requirementName + $ requirements spec - requirementNames = map fretRequirementName - $ fretRequirements fretComponentSpec +-- * Auxiliary + +-- | Substitute a string based on a given substitution table. +-- +-- This function leaves the key unchanged if it cannot be found in the +-- substitution table. +safeMap :: [(String, String)] -> String -> String +safeMap ls k = fromMaybe k $ lookup k ls diff --git a/ogma-extra/CHANGELOG.md b/ogma-extra/CHANGELOG.md index c1f44fa..670eefb 100644 --- a/ogma-extra/CHANGELOG.md +++ b/ogma-extra/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-extra +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-extra/ogma-extra.cabal b/ogma-extra/ogma-extra.cabal index 43e3880..1fe3fbf 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-c/CHANGELOG.md b/ogma-language-c/CHANGELOG.md index d08b0f8..e28e58c 100644 --- a/ogma-language-c/CHANGELOG.md +++ b/ogma-language-c/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-c +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-language-c/ogma-language-c.cabal b/ogma-language-c/ogma-language-c.cabal index 2185536..da9ad09 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-cocospec/CHANGELOG.md b/ogma-language-cocospec/CHANGELOG.md index f94d8f9..c96569d 100644 --- a/ogma-language-cocospec/CHANGELOG.md +++ b/ogma-language-cocospec/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-cocospec +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-language-cocospec/ogma-language-cocospec.cabal b/ogma-language-cocospec/ogma-language-cocospec.cabal index fa3b8ac..22ec6fa 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-copilot/CHANGELOG.md b/ogma-language-copilot/CHANGELOG.md index bfb6a6a..fff3d19 100644 --- a/ogma-language-copilot/CHANGELOG.md +++ b/ogma-language-copilot/CHANGELOG.md @@ -1,5 +1,9 @@ # Revision history for ogma-language-copilot +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-language-copilot/ogma-language-copilot.cabal b/ogma-language-copilot/ogma-language-copilot.cabal index ea1eba5..4a69a7e 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf diff --git a/ogma-language-fret-cs/CHANGELOG.md b/ogma-language-fret-cs/CHANGELOG.md deleted file mode 100644 index 38a32f2..0000000 --- a/ogma-language-fret-cs/CHANGELOG.md +++ /dev/null @@ -1,57 +0,0 @@ -# Revision history for ogma-language-fret-cs - -## [1.1.0] - 2023-11-21 - -* Version bump 1.1.0 (#112). - -## [1.0.11] - 2023-09-21 - -* Version bump 1.0.11 (#103). - -## [1.0.10] - 2023-07-21 - -* Version bump 1.0.10 (#98). -* Improve parsing error messages (#96). - -## [1.0.9] - 2023-05-21 - -* Version bump 1.0.9 (#93). - -## [1.0.8] - 2023-03-21 - -* Version bump 1.0.8 (#81). -* Mark package as uncurated (#74). - -## [1.0.7] - 2023-01-21 -* Version bump 1.0.7 (#69). - -## [1.0.6] - 2022-11-21 - -* Version bump 1.0.6 (#64). -* Update license in cabal file to OtherLicense (#62). - -## [1.0.5] - 2022-09-21 - -* Version bump 1.0.5 (#60). -* Bump version bounds of Aeson; adjust code to work with Aeson 2 (#55). -* Support floating point numbers in SMV expressions (#58). - -## [1.0.4] - 2022-07-21 - -* Version bump 1.0.4 (#53). - -## [1.0.3] - 2022-05-21 - -* Version bump 1.0.3 (#49). - -## [1.0.2] - 2022-03-21 - -* Version bump 1.0.2 (#43). - -## [1.0.1] - 2022-01-21 - -* Version bump 1.0.1 (#39). - -## [1.0.0] - 2021-11-22 - -* Initial release. diff --git a/ogma-language-fret-cs/src/Language/FRETComponentSpec/AST.hs b/ogma-language-fret-cs/src/Language/FRETComponentSpec/AST.hs deleted file mode 100644 index bafa44b..0000000 --- a/ogma-language-fret-cs/src/Language/FRETComponentSpec/AST.hs +++ /dev/null @@ -1,262 +0,0 @@ --- Copyright 2020 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. --- -{-# LANGUAGE OverloadedStrings #-} -{- HLINT ignore "Functor law" -} - --- | Representation and parser of FRET Component Specifications. --- --- FRET files are JSON files, implemented in Haskell using type classes, so the --- parser is defined in the same module as the AST to avoid having orphan --- instances. -module Language.FRETComponentSpec.AST where - --- External imports -import Data.Aeson ( FromJSON (..), Value (Object), (.:) ) -import Data.Aeson.Types ( prependFailure, typeMismatch ) -import Data.Aeson.Key ( toString ) -import qualified Data.Aeson.KeyMap as M - --- Internal imports -import qualified Language.CoCoSpec.AbsCoCoSpec as CoCoSpec -import qualified Language.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer, - pBoolSpec ) - -import qualified Language.SMV.AbsSMV as SMV -import qualified Language.SMV.ParSMV as SMV ( myLexer, pBoolSpec ) - --- | Abstract representation of a FRET file. -data FRETComponentSpec = FRETComponentSpec - { fretName :: String - , fretInternalVariables :: [ FRETInternalVariableDef ] - , fretExternalVariables :: [ FRETExternalVariableDef ] - , fretRequirements :: [ FRETRequirement ] - } - deriving (Show) - --- | Instance to parse FRET semantics keys in JSON format. -instance FromJSON FRETComponentSpec where - parseJSON (Object v) - | (specName, Object specValues) <- head (M.toList v) - = FRETComponentSpec (toString specName) - <$> specValues .: "Internal_variables" - <*> specValues .: "Other_variables" - <*> specValues .: "Requirements" - - | (specName, specValues) <- head (M.toList v) - = prependFailure "parsing FRET Component Specification failed, " - (typeMismatch "Object" specValues) - - parseJSON invalid = - prependFailure "parsing FRET Component Specification failed, " - (typeMismatch "Object" invalid) - --- | Internal variable definition, with a given name, its type and either a --- Lustre or a Copilot expression. -data FRETInternalVariableDef = FRETInternalVariableDef - { fretInternalVariableName :: String - , fretInternalVariableType :: String - , fretInternalVariableLustre :: String - , fretInternalVariableCopilot :: String - } - deriving (Show) - -instance FromJSON FRETInternalVariableDef where - parseJSON (Object v) = FRETInternalVariableDef - <$> v .: "name" - <*> v .: "type" - <*> v .: "assignmentLustre" - <*> v .: "assignmentCopilot" - - parseJSON invalid = - prependFailure "parsing FRET Internal Variable definition failed, " - (typeMismatch "Object" invalid) - --- | External variable definition, with a given name and type. --- --- The value of external variables is assigned outside Copilot, so they have no --- defining expression in this type.. -data FRETExternalVariableDef = FRETExternalVariableDef - { fretExternalVariableName :: String - , fretExternalVariableType :: String - } - deriving (Show) - -instance FromJSON FRETExternalVariableDef where - parseJSON (Object v) = FRETExternalVariableDef - <$> v .: "name" - <*> v .: "type" - - parseJSON invalid = - prependFailure "parsing FRET External Variable failed, " - (typeMismatch "Object" invalid) - --- | Requirement with a given name and a CoCoSpec expression. -data FRETRequirement = FRETRequirement - { fretRequirementName :: String - , fretRequirementCoCoSpec :: Maybe (Either String CoCoSpec.BoolSpec) - , fretRequirementPTExpanded :: Maybe (Either String SMV.BoolSpec) - , fretRequirementFretish :: String - } - deriving (Show) - -instance FromJSON FRETRequirement where - parseJSON (Object v) = do - n <- v .: "name" - - coco <- fmap (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) - <$> v .: "CoCoSpecCode" - coco' <- - case coco of - Nothing -> fail $ noField "CoCoSpecCode" n - Just (Left s) -> fail $ noParse "CoCoSpecCode" n s - Just (Right _) -> return coco - - ptltl <- fmap (SMV.pBoolSpec . SMV.myLexer) <$> v .: "ptLTL" - ptltl' <- - case ptltl of - Nothing -> fail $ noField "ptLTL" n - Just (Left s) -> fail $ noParse "ptLTL" n s - Just (Right _) -> return ptltl - - fretish <- v .: "fretish" - - return $ FRETRequirement n coco' ptltl' fretish - - where - - noField field req = concat - [ "error: requirement ", show req , " does not have a ", field - , " field" - ] - - noParse field req err = concat - [ "error: parsing of ", field, " field of requirement ", show req - , " failed with ", err - ] - - - parseJSON invalid = - prependFailure "parsing FRET Requirement failed, " - (typeMismatch "Object" invalid) - --- | Apply a variable subsitution to variables and requirements in a FRET --- file. -applySubstitution :: (String, String) -> FRETComponentSpec -> FRETComponentSpec -applySubstitution sub file = - FRETComponentSpec tlName - tlInternalVariables - tlExternalVariables - tlReqs - where - - -- Result component spec fields - tlName = fretName file - tlInternalVariables = map internalVarMapF $ fretInternalVariables file - tlExternalVariables = map externalVarMapF $ fretExternalVariables file - tlReqs = map reqMapF $ fretRequirements file - - -- Mapping function for fields with names to substitute - internalVarMapF x = x { fretInternalVariableName = - subsName sub (fretInternalVariableName x) } - - externalVarMapF x = x { fretExternalVariableName = - subsName sub (fretExternalVariableName x)} - - reqMapF x = x { fretRequirementName = - subsName sub (fretRequirementName x) - - , fretRequirementPTExpanded = - fmap (fmap (subBS sub)) (fretRequirementPTExpanded x) - } - - -- Substitute name x if it matches the old name oName - subsName (oName, nName) x = if x == oName then nName else x - - -- Substitute a name in all identifiers in a boolean expression - subBS sub' = mapBoolSpecIdent (subsName sub') - - -- Traverse a boolean expression applying a function to all identifiers - mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec - mapBoolSpecIdent f boolSpec = - case boolSpec of - SMV.BoolSpecSignal (SMV.Ident i) -> SMV.BoolSpecSignal (SMV.Ident (f i)) - - SMV.BoolSpecConst bc -> SMV.BoolSpecConst bc - - SMV.BoolSpecNum e -> SMV.BoolSpecNum (mapNumExprIdent f e) - - SMV.BoolSpecCmp spec1 op2 spec2 -> SMV.BoolSpecCmp - (mapBoolSpecIdent f spec1) op2 - (mapBoolSpecIdent f spec2) - - SMV.BoolSpecNeg spec -> SMV.BoolSpecNeg (mapBoolSpecIdent f spec) - - SMV.BoolSpecAnd spec1 spec2 -> SMV.BoolSpecAnd - (mapBoolSpecIdent f spec1) - (mapBoolSpecIdent f spec2) - - SMV.BoolSpecOr spec1 spec2 -> SMV.BoolSpecOr - (mapBoolSpecIdent f spec1) - (mapBoolSpecIdent f spec2) - - SMV.BoolSpecXor spec1 spec2 -> SMV.BoolSpecXor - (mapBoolSpecIdent f spec1) - (mapBoolSpecIdent f spec2) - - SMV.BoolSpecImplies spec1 spec2 -> SMV.BoolSpecImplies - (mapBoolSpecIdent f spec1) - (mapBoolSpecIdent f spec2) - - SMV.BoolSpecEquivs spec1 spec2 -> SMV.BoolSpecEquivs - (mapBoolSpecIdent f spec1) - (mapBoolSpecIdent f spec2) - - SMV.BoolSpecOp1 op spec -> SMV.BoolSpecOp1 op (mapBoolSpecIdent f spec) - - SMV.BoolSpecOp2 spec1 op2 spec2 -> SMV.BoolSpecOp2 - (mapBoolSpecIdent f spec1) op2 - (mapBoolSpecIdent f spec2) - - -- Traverse a numeric expression applying a function to all identifiers - mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr - mapNumExprIdent f numExpr = - case numExpr of - SMV.NumId (SMV.Ident i) -> SMV.NumId (SMV.Ident (f i)) - SMV.NumConstI c -> SMV.NumConstI c - SMV.NumConstD c -> SMV.NumConstD c - SMV.NumAdd expr1 op expr2 -> SMV.NumAdd - (mapNumExprIdent f expr1) - op - (mapNumExprIdent f expr2) - SMV.NumMult expr1 op expr2 -> SMV.NumMult - (mapNumExprIdent f expr1) - op - (mapNumExprIdent f expr2) diff --git a/ogma-language-fret-cs/tests/Main.hs b/ogma-language-fret-cs/tests/Main.hs deleted file mode 100644 index d139a36..0000000 --- a/ogma-language-fret-cs/tests/Main.hs +++ /dev/null @@ -1,81 +0,0 @@ --- Copyright 2020 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. --- --- | Test FRETCS language library. -module Main where - --- External imports -import Data.Aeson ( eitherDecode ) -import Data.Either ( isLeft, isRight ) -import Test.Framework ( Test, defaultMainWithOpts ) -import Test.Framework.Providers.QuickCheck2 ( testProperty ) -import Test.QuickCheck ( Property ) -import Test.QuickCheck.Monadic ( assert, monadicIO, run ) - --- External imports: auxiliary -import Data.ByteString.Extra as B ( safeReadFile ) - --- Internal imports -import Language.FRETComponentSpec.AST ( FRETComponentSpec ) - --- | Run all unit tests for the FRETCS parser. -main :: IO () -main = - defaultMainWithOpts tests mempty - --- | All unit tests for the FRETCS parser. -tests :: [Test.Framework.Test] -tests = - [ testProperty "Parse FRETCS (correct case)" propParseFRETCSOk - , testProperty "Parse FRETCS (incorrect case)" propParseFRETCSFail - ] - --- | Test the FRETCS parser on a well-formed boolean specification. -propParseFRETCSOk :: Property -propParseFRETCSOk = monadicIO $ do - content <- run $ parseFretComponentSpec "tests/fret_good.json" - assert (isRight content) - --- | Test the FRETCS parser on an incorrect boolean specification. -propParseFRETCSFail :: Property -propParseFRETCSFail = monadicIO $ do - componentSpec <- run $ parseFretComponentSpec "tests/fret_bad.json" - assert (isLeft componentSpec) - --- | Parse a JSON file containing a FRET component specification. --- --- Returns a 'Left' with an error message if the file does not have the correct --- format. --- --- Throws an exception if the file cannot be read. -parseFretComponentSpec :: FilePath -> IO (Either String FRETComponentSpec) -parseFretComponentSpec fp = do - componentSpec <- B.safeReadFile fp - return $ eitherDecode =<< componentSpec diff --git a/ogma-language-fret-cs/tests/fret_bad.json b/ogma-language-fret-cs/tests/fret_bad.json deleted file mode 100644 index 75e6ffa..0000000 --- a/ogma-language-fret-cs/tests/fret_bad.json +++ /dev/null @@ -1,21 +0,0 @@ -{ - "RTSASpec": { - "Middle_variables": [], - "Other_variables": [ - {"name":"param_is_short", "type":"bool"}, - {"name":"param_value_short", "type":"real"}, - {"name":"param_value_long", "type":"real"}, - {"name":"upper_param_limit", "type":"real"}, - {"name":"lower_param_limit", "type":"real"}, - {"name":"envelope_issue", "type":"bool"} - ], - "Requirements": [ - { - "name": "behnazOne", - "CoCoSpecCode": "", - "ptltl": "((H ((((! flight_mode) & (Y flight_mode)) & (Y TRUE)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))) & (((! ((! flight_mode) & (Y flight_mode))) S ((! ((! flight_mode) & (Y flight_mode))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))", - "fretish": "Meaning not specified" - } - ] - } -} diff --git a/ogma-language-fret-cs/tests/fret_good.json b/ogma-language-fret-cs/tests/fret_good.json deleted file mode 100644 index 5ab0fef..0000000 --- a/ogma-language-fret-cs/tests/fret_good.json +++ /dev/null @@ -1,21 +0,0 @@ -{ - "RTSASpec": { - "Internal_variables": [], - "Other_variables": [ - {"name":"param_is_short", "type":"bool"}, - {"name":"param_value_short", "type":"real"}, - {"name":"param_value_long", "type":"real"}, - {"name":"upper_param_limit", "type":"real"}, - {"name":"lower_param_limit", "type":"real"}, - {"name":"envelope_issue", "type":"bool"} - ], - "Requirements": [ - { - "name": "behnazOne", - "CoCoSpecCode": "true", - "ptLTL": "((H ((((! flight_mode) & (Y flight_mode)) & (Y TRUE)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))) & (((! ((! flight_mode) & (Y flight_mode))) S ((! ((! flight_mode) & (Y flight_mode))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))))) & (! (( replanning_mode ))))) -> (O[<10] ((flight_mode & ((! (Y TRUE)) | (Y (! flight_mode)))) | (( replanning_mode ))))) & (flight_mode & ((! (Y TRUE)) | (Y (! flight_mode))))))))", - "fretish": "Meaning not specified" - } - ] - } -} diff --git a/ogma-language-fret-reqs/CHANGELOG.md b/ogma-language-fret-reqs/CHANGELOG.md index 31ca4fd..a73896d 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.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal b/ogma-language-fret-reqs/ogma-language-fret-reqs.cabal index 4e5f1e5..b3d3656 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.1.0 +version: 1.2.0 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.1.0 && < 1.2 - , ogma-language-smv >= 1.1.0 && < 1.2 + , ogma-language-cocospec >= 1.2.0 && < 1.3 + , ogma-language-smv >= 1.2.0 && < 1.3 hs-source-dirs: src diff --git a/ogma-language-jsonspec/CHANGELOG.md b/ogma-language-jsonspec/CHANGELOG.md new file mode 100644 index 0000000..39d46ef --- /dev/null +++ b/ogma-language-jsonspec/CHANGELOG.md @@ -0,0 +1,6 @@ +# Revision history for ogma-language-jsonspec + +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Initial release (#115). diff --git a/ogma-language-fret-cs/LICENSE.pdf b/ogma-language-jsonspec/LICENSE.pdf similarity index 100% rename from ogma-language-fret-cs/LICENSE.pdf rename to ogma-language-jsonspec/LICENSE.pdf diff --git a/ogma-language-fret-cs/Setup.hs b/ogma-language-jsonspec/Setup.hs similarity index 100% rename from ogma-language-fret-cs/Setup.hs rename to ogma-language-jsonspec/Setup.hs diff --git a/ogma-language-fret-cs/ogma-language-fret-cs.cabal b/ogma-language-jsonspec/ogma-language-jsonspec.cabal similarity index 75% rename from ogma-language-fret-cs/ogma-language-fret-cs.cabal rename to ogma-language-jsonspec/ogma-language-jsonspec.cabal index ba2fd46..63b68de 100644 --- a/ogma-language-fret-cs/ogma-language-fret-cs.cabal +++ b/ogma-language-jsonspec/ogma-language-jsonspec.cabal @@ -1,4 +1,4 @@ --- Copyright 2020 United States Government as represented by the Administrator +-- Copyright 2024 United States Government as represented by the Administrator -- of the National Aeronautics and Space Administration. All Rights Reserved. -- -- Disclaimers @@ -31,8 +31,8 @@ cabal-version: 2.0 build-type: Simple -name: ogma-language-fret-cs -version: 1.1.0 +name: ogma-language-jsonspec +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -40,17 +40,15 @@ author: Ivan Perez, Alwyn Goodloe maintainer: ivan.perezdominguez@nasa.gov category: Aerospace extra-source-files: CHANGELOG.md - tests/fret_good.json - tests/fret_bad.json -synopsis: Ogma: Runtime Monitor translator: FRET Component Specification Frontend +synopsis: Ogma: Runtime Monitor translator: JSON Frontend description: Ogma is a tool to facilitate the integration of safe runtime monitors into other systems. Ogma extends , a high-level runtime verification framework that generates hard real-time C99 code. . - This library contains a frontend to read FRET Component Specifications. + This library contains a frontend to read specifications from JSON files. -- Ogma packages should be uncurated so that only the official maintainers make -- changes. @@ -62,14 +60,17 @@ x-curation: uncurated library exposed-modules: - Language.FRETComponentSpec.AST + Language.JSONSpec.Parser build-depends: base >= 4.11.0.0 && < 5 , aeson >= 2.0.0.0 && < 2.2 + , jsonpath >= 0.3 && < 0.4 + , text + , megaparsec + , bytestring - , ogma-language-cocospec >= 1.1.0 && < 1.2 - , ogma-language-smv >= 1.1.0 && < 1.2 + , ogma-spec >= 1.2.0 && < 1.3 hs-source-dirs: src @@ -79,30 +80,3 @@ library ghc-options: -Wall - -test-suite unit-tests - type: - exitcode-stdio-1.0 - - main-is: - Main.hs - - build-depends: - base >= 4.11.0.0 && < 5 - - , aeson >= 2.0.0.0 && < 2.2 - , QuickCheck - , test-framework - , test-framework-quickcheck2 - - , ogma-extra >= 1.1.0 && < 1.2 - , ogma-language-fret-cs - - hs-source-dirs: - tests - - default-language: - Haskell2010 - - ghc-options: - -Wall diff --git a/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs new file mode 100644 index 0000000..4d079da --- /dev/null +++ b/ogma-language-jsonspec/src/Language/JSONSpec/Parser.hs @@ -0,0 +1,194 @@ +-- Copyright 2024 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. +-- + +-- | Parser for Ogma specs stored in JSON files. +module Language.JSONSpec.Parser where + +-- External imports +import Data.Aeson (FromJSON (..), Value (..), decode, (.:)) +import Data.Aeson.Key (toString) +import qualified Data.Aeson.KeyMap as M +import Data.Aeson.Types (prependFailure, typeMismatch) +import Data.Bifunctor (first) +import Data.ByteString.Lazy (fromStrict) +import Data.JSONPath.Execute +import Data.JSONPath.Parser +import Data.JSONPath.Types +import Data.Text (pack, unpack) +import qualified Data.Text as T +import qualified Data.Text.Encoding as T +import qualified Data.Text.IO as T +import Text.Megaparsec (eof, errorBundlePretty, parse) + +-- External imports: ogma-spec +import Data.OgmaSpec + +data JSONFormat = JSONFormat + { specInternalVars :: String + , specInternalVarId :: String + , specInternalVarExpr :: String + , specInternalVarType :: String + , specExternalVars :: String + , specExternalVarId :: String + , specExternalVarType :: String + , specRequirements :: String + , specRequirementId :: String + , specRequirementDesc :: String + , specRequirementExpr :: String + } + +data JSONFormatInternal = JSONFormatInternal + { jfiInternalVars :: [JSONPathElement] + , jfiInternalVarId :: [JSONPathElement] + , jfiInternalVarExpr :: [JSONPathElement] + , jfiInternalVarType :: [JSONPathElement] + , jfiExternalVars :: [JSONPathElement] + , jfiExternalVarId :: [JSONPathElement] + , jfiExternalVarType :: [JSONPathElement] + , jfiRequirements :: [JSONPathElement] + , jfiRequirementId :: [JSONPathElement] + , jfiRequirementDesc :: [JSONPathElement] + , jfiRequirementExpr :: [JSONPathElement] + } + +parseJSONFormat :: JSONFormat -> Either String JSONFormatInternal +parseJSONFormat jsonFormat = do + jfi2 <- showErrors $ parseJSONPath (pack (specInternalVars jsonFormat)) + jfi3 <- showErrors $ parseJSONPath (pack (specInternalVarId jsonFormat)) + jfi4 <- showErrors $ parseJSONPath (pack (specInternalVarExpr jsonFormat)) + jfi5 <- showErrors $ parseJSONPath (pack (specInternalVarType jsonFormat)) + jfi6 <- showErrors $ parseJSONPath (pack (specExternalVars jsonFormat)) + jfi7 <- showErrors $ parseJSONPath (pack (specExternalVarId jsonFormat)) + jfi8 <- showErrors $ parseJSONPath (pack (specExternalVarType jsonFormat)) + jfi9 <- showErrors $ parseJSONPath (pack (specRequirements jsonFormat)) + jfi10 <- showErrors $ parseJSONPath (pack (specRequirementId jsonFormat)) + jfi11 <- showErrors $ parseJSONPath (pack (specRequirementDesc jsonFormat)) + jfi12 <- showErrors $ parseJSONPath (pack (specRequirementExpr jsonFormat)) + return $ JSONFormatInternal + { jfiInternalVars = jfi2 + , jfiInternalVarId = jfi3 + , jfiInternalVarExpr = jfi4 + , jfiInternalVarType = jfi5 + , jfiExternalVars = jfi6 + , jfiExternalVarId = jfi7 + , jfiExternalVarType = jfi8 + , jfiRequirements = jfi9 + , jfiRequirementId = jfi10 + , jfiRequirementDesc = jfi11 + , jfiRequirementExpr = jfi12 + } + +parseJSONSpec :: (String -> Either String a) -> JSONFormat -> Value -> Either String (Spec a) +parseJSONSpec parseExpr jsonFormat value = do + jsonFormatInternal <- parseJSONFormat jsonFormat + + let values :: [Value] + values = executeJSONPath (jfiInternalVars jsonFormatInternal) value + + internalVarDef :: Value -> Either String InternalVariableDef + internalVarDef value = do + let msg = "internal variable name" + varId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarId jsonFormatInternal) value)) + + let msg = "internal variable type" + varType <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarType jsonFormatInternal) value)) + + let msg = "internal variable expr" + varExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiInternalVarExpr jsonFormatInternal) value)) + + return $ InternalVariableDef + { internalVariableName = varId + , internalVariableType = varType + , internalVariableExpr = varExpr + } + + internalVariableDefs <- mapM internalVarDef values + + let values :: [Value] + values = executeJSONPath (jfiExternalVars jsonFormatInternal) value + + externalVarDef :: Value -> Either String ExternalVariableDef + externalVarDef value = do + + let msg = "external variable name" + varId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiExternalVarId jsonFormatInternal) value)) + + let msg = "external variable type" + varType <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiExternalVarType jsonFormatInternal) value)) + + return $ ExternalVariableDef + { externalVariableName = varId + , externalVariableType = varType + } + + externalVariableDefs <- mapM externalVarDef values + + let values :: [Value] + values = executeJSONPath (jfiRequirements jsonFormatInternal) value + + -- requirementDef :: Value -> Either String (Requirement a) + requirementDef value = do + let msg = "Requirement name" + reqId <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementId jsonFormatInternal) value)) + + let msg = "Requirement expression" + reqExpr <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementExpr jsonFormatInternal) value)) + reqExpr' <- parseExpr reqExpr + + let msg = "Requirement description" + reqDesc <- valueToString msg =<< (listToEither msg (executeJSONPath (jfiRequirementDesc jsonFormatInternal) value)) + + return $ Requirement + { requirementName = reqId + , requirementExpr = reqExpr' + , requirementDescription = reqDesc + } + + requirements <- mapM requirementDef values + + return $ Spec internalVariableDefs externalVariableDefs requirements + +valueToString :: String -> Value -> Either String String +valueToString msg (String x) = Right $ unpack x +valueToString msg _ = Left $ "The JSON value provided for " ++ msg ++ " does not contain a string" + +listToEither :: String -> [a] -> Either String a +listToEither _ [x] = Right x +listToEither msg [] = Left $ "Failed to find a value for " ++ msg +listToEither msg _ = Left $ "Unexpectedly found multiple values for " ++ msg + +-- | Parse a JSONPath expression, returning its element components. +parseJSONPath :: T.Text -> Either String [JSONPathElement] +parseJSONPath = first errorBundlePretty . parse (jsonPath eof) "" + +showErrors :: Show a => Either a b -> Either String b +showErrors (Left s) = Left (show s) +showErrors (Right x) = Right x diff --git a/ogma-language-smv/CHANGELOG.md b/ogma-language-smv/CHANGELOG.md index dc888eb..79e7a1d 100644 --- a/ogma-language-smv/CHANGELOG.md +++ b/ogma-language-smv/CHANGELOG.md @@ -1,5 +1,10 @@ # Revision history for ogma-language-smv +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Introduce identifier substitution functions (#115). + ## [1.1.0] - 2023-11-21 * Version bump 1.1.0 (#112). diff --git a/ogma-language-smv/ogma-language-smv.cabal b/ogma-language-smv/ogma-language-smv.cabal index 68ef21d..0d79b00 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.1.0 +version: 1.2.0 homepage: http://nasa.gov license: OtherLicense license-file: LICENSE.pdf @@ -77,6 +77,7 @@ library Language.SMV.LexSMV Language.SMV.ParSMV Language.SMV.PrintSMV + Language.SMV.Substitution autogen-modules: Language.SMV.AbsSMV diff --git a/ogma-language-smv/src/Language/SMV/Substitution.hs b/ogma-language-smv/src/Language/SMV/Substitution.hs new file mode 100644 index 0000000..f22c474 --- /dev/null +++ b/ogma-language-smv/src/Language/SMV/Substitution.hs @@ -0,0 +1,69 @@ +module Language.SMV.Substitution where + +import qualified Language.SMV.AbsSMV as SMV + +substituteBoolExpr subs e = foldr subBS e subs + +-- Substitute name x if it matches the old name oName +subsName (oName, nName) x = if x == oName then nName else x + +-- Substitute a name in all identifiers in a boolean expression +subBS sub' = mapBoolSpecIdent (subsName sub') + +-- Traverse a boolean expression applying a function to all identifiers +mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec +mapBoolSpecIdent f boolSpec = + case boolSpec of + SMV.BoolSpecSignal (SMV.Ident i) -> SMV.BoolSpecSignal (SMV.Ident (f i)) + + SMV.BoolSpecConst bc -> SMV.BoolSpecConst bc + + SMV.BoolSpecNum e -> SMV.BoolSpecNum (mapNumExprIdent f e) + + SMV.BoolSpecCmp spec1 op2 spec2 -> SMV.BoolSpecCmp + (mapBoolSpecIdent f spec1) op2 + (mapBoolSpecIdent f spec2) + + SMV.BoolSpecNeg spec -> SMV.BoolSpecNeg (mapBoolSpecIdent f spec) + + SMV.BoolSpecAnd spec1 spec2 -> SMV.BoolSpecAnd + (mapBoolSpecIdent f spec1) + (mapBoolSpecIdent f spec2) + + SMV.BoolSpecOr spec1 spec2 -> SMV.BoolSpecOr + (mapBoolSpecIdent f spec1) + (mapBoolSpecIdent f spec2) + + SMV.BoolSpecXor spec1 spec2 -> SMV.BoolSpecXor + (mapBoolSpecIdent f spec1) + (mapBoolSpecIdent f spec2) + + SMV.BoolSpecImplies spec1 spec2 -> SMV.BoolSpecImplies + (mapBoolSpecIdent f spec1) + (mapBoolSpecIdent f spec2) + + SMV.BoolSpecEquivs spec1 spec2 -> SMV.BoolSpecEquivs + (mapBoolSpecIdent f spec1) + (mapBoolSpecIdent f spec2) + + SMV.BoolSpecOp1 op spec -> SMV.BoolSpecOp1 op (mapBoolSpecIdent f spec) + + SMV.BoolSpecOp2 spec1 op2 spec2 -> SMV.BoolSpecOp2 + (mapBoolSpecIdent f spec1) op2 + (mapBoolSpecIdent f spec2) + +-- Traverse a numeric expression applying a function to all identifiers +mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr +mapNumExprIdent f numExpr = + case numExpr of + SMV.NumId (SMV.Ident i) -> SMV.NumId (SMV.Ident (f i)) + SMV.NumConstI c -> SMV.NumConstI c + SMV.NumConstD c -> SMV.NumConstD c + SMV.NumAdd expr1 op expr2 -> SMV.NumAdd + (mapNumExprIdent f expr1) + op + (mapNumExprIdent f expr2) + SMV.NumMult expr1 op expr2 -> SMV.NumMult + (mapNumExprIdent f expr1) + op + (mapNumExprIdent f expr2) diff --git a/ogma-spec/CHANGELOG.md b/ogma-spec/CHANGELOG.md new file mode 100644 index 0000000..f99dee3 --- /dev/null +++ b/ogma-spec/CHANGELOG.md @@ -0,0 +1,6 @@ +# Revision history for ogma-spec + +## [1.2.0] - 2024-01-21 + +* Version bump 1.2.0 (#117). +* Initial release (#115). diff --git a/ogma-spec/LICENSE.pdf b/ogma-spec/LICENSE.pdf new file mode 100644 index 0000000..d4333fb Binary files /dev/null and b/ogma-spec/LICENSE.pdf differ diff --git a/ogma-spec/Setup.hs b/ogma-spec/Setup.hs new file mode 100644 index 0000000..9a994af --- /dev/null +++ b/ogma-spec/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ogma-spec/ogma-spec.cabal b/ogma-spec/ogma-spec.cabal new file mode 100644 index 0000000..8151465 --- /dev/null +++ b/ogma-spec/ogma-spec.cabal @@ -0,0 +1,75 @@ +-- Copyright 2024 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. + +cabal-version: 2.0 +build-type: Simple + +name: ogma-spec +version: 1.2.0 +homepage: http://nasa.gov +license: OtherLicense +license-file: LICENSE.pdf +author: Ivan Perez, Alwyn Goodloe +maintainer: ivan.perezdominguez@nasa.gov +category: Aerospace +extra-source-files: CHANGELOG.md + +synopsis: Ogma: Runtime Monitor translator: JSON Frontend + +description: Ogma is a tool to facilitate the integration of safe runtime monitors into + other systems. Ogma extends + , a high-level runtime + verification framework that generates hard real-time C99 code. + . + This library contains an abstract representation of an Ogma specification. + +-- 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: + Data.OgmaSpec + + build-depends: + base >= 4.11.0.0 && < 5 + + hs-source-dirs: + src + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/ogma-spec/src/Data/OgmaSpec.hs b/ogma-spec/src/Data/OgmaSpec.hs new file mode 100644 index 0000000..e7ef13b --- /dev/null +++ b/ogma-spec/src/Data/OgmaSpec.hs @@ -0,0 +1,67 @@ +-- Copyright 2024 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. +-- +-- | Abstract representation of an Ogma specification. +module Data.OgmaSpec where + +-- | Abstract representation of an Ogma specification. +data Spec a = Spec + { internalVariables :: [ InternalVariableDef ] + , externalVariables :: [ ExternalVariableDef ] + , requirements :: [ Requirement a ] + } + deriving (Show) + +-- | Internal variable definition, with a given name, its type and definining +-- expression. +data InternalVariableDef = InternalVariableDef + { internalVariableName :: String + , internalVariableType :: String + , internalVariableExpr :: String + } + deriving (Show) + +-- | External variable definition, with a given name and type. +-- +-- The value of external variables is assigned outside Copilot, so they have no +-- defining expression in this type. +data ExternalVariableDef = ExternalVariableDef + { externalVariableName :: String + , externalVariableType :: String + } + deriving (Show) + +-- | Requirement with a given name and a boolean expression. +data Requirement a = Requirement + { requirementName :: String + , requirementExpr :: a + , requirementDescription :: String + } + deriving (Show)