ogma-language-lustre (empty) → 1.7.0

raw patch · 9 files changed

+415/−0 lines, 9 filesdep +QuickCheckdep +arraydep +basebuild-type:Customsetup-changedbinary-added

Dependencies added: QuickCheck, array, base, ogma-language-lustre, test-framework, test-framework-quickcheck2

Files

CHANGELOG.md +94/−0
LICENSE.pdf binary
Setup.hs +27/−0
grammar/Lustre.cf +96/−0
ogma-language-lustre.cabal +128/−0
src/.keep +0/−0
tests/Main.hs +68/−0
tests/lustre_bad +1/−0
tests/lustre_good +1/−0

+ CHANGELOG.md view

@@ -0,0 +1,94 @@+# Revision history for ogma-language-lustre++## [1.7.0] - 2025-03-21++* Version bump 1.7.0 (#269).+* Remove references to old design of Ogma from documentation (#220).+* Bump upper version constraint on Cabal (#213).+* Remove extraneous EOL character (#224).+* Specify tools needed using build-tool-depends (#149).+* Introduce package to process Lustre expressions (#267).++## [1.6.0] - 2025-01-21++* Version bump 1.6.0 (#208).+* Add repository information to cabal package (#148).+* Add version bounds to all dependencies (#119).++## [1.5.0] - 2024-11-21++* Version bump 1.5.0 (#178).++## [1.4.1] - 2024-09-21++* Version bump 1.4.1 (#155).+* Replace homepage (#147).++## [1.4.0] - 2024-05-21++* Version bump 1.4.0 (#145).++## [1.3.0] - 2024-03-21++* Version bump 1.3.0 (#133).++## [1.2.0] - 2024-01-21++* Version bump 1.2.0 (#117).++## [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).++## [1.0.9] - 2023-05-21++* Version bump 1.0.9 (#93).+* Add unary operators ZtoPre, YtoPre (#86).++## [1.0.8] - 2023-03-21++* Version bump 1.0.8 (#81).+* Support inequality operator (#71).+* 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.++## [1.0.6] - 2022-11-21++* Version bump 1.0.6 (#64).+* Update license in cabal file to OtherLicense (#62).+* Add empty file to keep directory structure in distributable package (#65).++## [1.0.5] - 2022-09-21++* Version bump 1.0.5 (#60).++## [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.

+ LICENSE.pdf view

binary file changed (absent → 117991 bytes)

+ Setup.hs view

@@ -0,0 +1,27 @@+-- | Custom Setup that runs bnfc to generate the language sub-libraries+-- for the parsers included in Ogma.+module Main (main) where++import Distribution.Simple         ( defaultMainWithHooks, hookedPrograms,+                                     postConf, preBuild, simpleUserHooks )+import Distribution.Simple.Program ( Program (..), findProgramVersion,+                                     simpleProgram )+import System.Process              ( system )++-- | Run BNFC on the grammar before the actual build step.+--+-- All options for bnfc are hard-coded here. There is an open bug in Cabal's+-- github repo about supporting BNFC.+main :: IO ()+main = defaultMainWithHooks $ simpleUserHooks+  { hookedPrograms = [ bnfcProgram ]+  , postConf       = \args flags packageDesc localBuildInfo -> do+      _ <- system "bnfc --haskell -p Language.Lustre -o src/ grammar/Lustre.cf"+      postConf simpleUserHooks args flags packageDesc localBuildInfo+  }++-- | TODO: This should be in Cabal.Distribution.Simple.Program.Builtin.+bnfcProgram :: Program+bnfcProgram = (simpleProgram "bnfc")+  { programFindVersion = findProgramVersion "--version" id+  }

+ grammar/Lustre.cf view

@@ -0,0 +1,96 @@+-- 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.+--+-- Simplified grammar of Lustre boolean expressions.++entrypoints BoolSpec;++-- Boolean Expressions++_          .    BoolSpec ::= BoolSpec ";" ;+BoolSpecPar.    BoolSpec ::= "(" BoolSpec ")" ;+BoolSpecConstI. BoolSpec ::= Integer ;+BoolSpecConstD. BoolSpec ::= Double ;+BoolSpecConstB. BoolSpec ::= BoolConst ;+BoolSpecSignal. BoolSpec ::= Ident ;+BoolSpecOp1Pre. BoolSpec ::= Op1Pre BoolSpec ;+BoolSpecOp2In.  BoolSpec ::= BoolSpec Op2In BoolSpec ;+BoolSpecOp2Pre. BoolSpec ::= Op2Pre "(" BoolSpec "," BoolSpec ")" ;+BoolSpecOp2OT.  BoolSpec ::= "OT" "(" NumExpr "," NumExpr "," BoolSpec ")" ;+BoolSpecOp2HT.  BoolSpec ::= "HT" "(" NumExpr "," NumExpr "," BoolSpec ")" ;+BoolSpecOp2ST.  BoolSpec ::= "ST" "(" NumExpr "," NumExpr "," BoolSpec "," BoolSpec ")" ;++-- Boolean Operators++Op1Once.   Op1Pre ::= "O"      ;+Op1Pre.    Op1Pre ::= "pre"    ;+Op1YtoPre. Op1Pre ::= "YtoPre" ;+Op1ZtoPre. Op1Pre ::= "ZtoPre" ;+Op1Hist.   Op1Pre ::= "H"      ;+Op1Y.      Op1Pre ::= "Y"      ;+Op1Not.    Op1Pre ::= "not"    ;+Op1Bang.   Op1Pre ::= "!"      ;++Op2And.     Op2In ::= "and"     ;+Op2Amp.     Op2In ::= "&"       ;+Op2Or.      Op2In ::= "or"      ;+Op2Impl.    Op2In ::= "=>"      ;+Op2NumOp  . Op2In ::= NumOp2In  ;+Op2NumCmp . Op2In ::= BoolNumOp ;+Op2InPre.   Op2In ::= "->"      ;++Op2SI.   Op2Pre ::= "SI" ;+Op2OT.   Op2Pre ::= "OT" ;++-- Numeric Expressions++NumExprNum.   NumExpr ::= Integer                  ;+NumExprId.    NumExpr ::= Ident                    ;+NumExprPar.   NumExpr ::= "(" NumExpr ")"          ;+NumExprOp2In. NumExpr ::= NumExpr NumOp2In NumExpr ;++-- Numeric Operators++NumOp2Plus.  NumOp2In ::= "+" ;+NumOp2Minus. NumOp2In ::= "-" ;+NumOp2Mult . NumOp2In ::= "*" ;++BoolNumOp2Eq . BoolNumOp ::= "=" ;+BoolNumOp2Ne . BoolNumOp ::= "<>" ;+BoolNumOp2Le . BoolNumOp ::= "<=" ;+BoolNumOp2Lt . BoolNumOp ::= "<" ;+BoolNumOp2Gt . BoolNumOp ::= ">" ;+BoolNumOp2Ge . BoolNumOp ::= ">=" ;++-- Basic types++BoolConstTrue.  BoolConst ::= "true" ;+BoolConstFalse. BoolConst ::= "false" ;+BoolConstFTP.   BoolConst ::= "FTP" ;

+ ogma-language-lustre.cabal view

@@ -0,0 +1,128 @@+-- 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.++cabal-version:       2.0+build-type:          Custom+name:                ogma-language-lustre+version:             1.7.0+homepage:            https://github.com/nasa/ogma+bug-reports:         https://github.com/nasa/ogma/issues+license:             OtherLicense+license-file:        LICENSE.pdf+author:              Ivan Perez, Alwyn Goodloe+maintainer:          ivan.perezdominguez@nasa.gov+category:            Aerospace+extra-source-files:  CHANGELOG.md+                     grammar/Lustre.cf+                     src/.keep+                     tests/lustre_good+                     tests/lustre_bad++synopsis:            Ogma: Runtime Monitor translator: Lustre Language Frontend++description:         Ogma is a tool to facilitate the integration of safe runtime monitors into+                     other systems. Ogma extends+                     <https://github.com/Copilot-Language/copilot Copilot>, a high-level runtime+                     verification framework that generates hard real-time C99 code.+                     .+                     This library contains a frontend to read Lustre Boolean expressions,+                     extended with several operators related to temporal logic.++-- 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++source-repository head+  type:     git+  location: git@github.com:nasa/ogma.git+  subdir:   ogma-language-lustre++custom-setup+  setup-depends:+      base    >= 4.11.0.0 && < 5+    , Cabal   >= 2.0 && < 3.15+    , process >= 1.6      && < 1.7++library++  exposed-modules:+    -- Automatically generated+    Language.Lustre.AbsLustre+    Language.Lustre.LexLustre+    Language.Lustre.ParLustre+    Language.Lustre.PrintLustre++  autogen-modules:+    Language.Lustre.AbsLustre+    Language.Lustre.LexLustre+    Language.Lustre.ParLustre+    Language.Lustre.PrintLustre++  build-depends:+      base  >= 4.11.0.0 && < 5+    , array >= 0.5.2.0  && < 0.6++  build-tool-depends:+      alex:alex   >= 3+    , BNFC:bnfc   >= 2.9.4+    , happy:happy >= 1.19++  hs-source-dirs:+    src++  default-language:+    Haskell2010++test-suite unit-tests+  type:+    exitcode-stdio-1.0++  main-is:+    Main.hs++  build-depends:+      base                       >= 4.11.0.0 && < 5+    , QuickCheck                 >= 2.8.2    && < 2.16+    , test-framework             >= 0.8.2    && < 0.9+    , test-framework-quickcheck2 >= 0.3.0.4  && < 0.4++    , ogma-language-lustre++  hs-source-dirs:+    tests++  default-language:+    Haskell2010++  ghc-options:+    -Wall

+ src/.keep view

+ tests/Main.hs view

@@ -0,0 +1,68 @@+-- 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 Lustre language library.+module Main where++-- External imports+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 )++-- Internal imports+import qualified Language.Lustre.ParLustre as Lustre ( myLexer, pBoolSpec )++-- | Run all unit tests for the Lustre parser.+main :: IO ()+main =+  defaultMainWithOpts tests mempty++-- | All unit tests for the Lustre parser.+tests :: [Test.Framework.Test]+tests =+  [ testProperty "Parse Lustre (correct case)"   propParseLustreOk+  , testProperty "Parse Lustre (incorrect case)" propParseLustreFail+  ]++-- | Test the Lustre parser on a well-formed boolean specification.+propParseLustreOk :: Property+propParseLustreOk = monadicIO $ do+  content <- run $ readFile "tests/lustre_good"+  let program = Lustre.pBoolSpec $ Lustre.myLexer content+  assert (isRight program)++-- | Test the Lustre parser on an incorrect boolean specification.+propParseLustreFail :: Property+propParseLustreFail = monadicIO $ do+  content <- run $ readFile "tests/lustre_bad"+  let program = Lustre.pBoolSpec $ Lustre.myLexer content+  assert (isLeft program)

+ tests/lustre_bad view

@@ -0,0 +1,1 @@+((D(((( not flight_mode) and (pre (flight_mode))) and ( not FTP)) => (pre (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))) and ((SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ( not (( not flight_mode) and (pre (flight_mode)))) )) => (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))

+ tests/lustre_good view

@@ -0,0 +1,1 @@+((H(((( not flight_mode) and (pre (flight_mode))) and ( not FTP)) => (pre (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))) and ((SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ( not (( not flight_mode) and (pre (flight_mode)))) )) => (SI( (flight_mode and (FTP or (pre ( not flight_mode)))), ((OT(10,10,( ( (conflict_detected) and ( ( Y ( not (conflict_detected) ) ) or ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) ) ) and ( not (( replanning_mode )) ) ))) => (OT(10-1,0,( ( flight_mode and ( FTP or ( Y not flight_mode ) ) ) or (( replanning_mode )) )))) ))))