diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -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. diff --git a/LICENSE.pdf b/LICENSE.pdf new file mode 100644 Binary files /dev/null and b/LICENSE.pdf differ diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -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 + } diff --git a/grammar/Lustre.cf b/grammar/Lustre.cf new file mode 100644 --- /dev/null +++ b/grammar/Lustre.cf @@ -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" ; diff --git a/ogma-language-lustre.cabal b/ogma-language-lustre.cabal new file mode 100644 --- /dev/null +++ b/ogma-language-lustre.cabal @@ -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 + , 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 diff --git a/src/.keep b/src/.keep new file mode 100644 --- /dev/null +++ b/src/.keep diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -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) diff --git a/tests/lustre_bad b/tests/lustre_bad new file mode 100644 --- /dev/null +++ b/tests/lustre_bad @@ -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 )) )))) )))) diff --git a/tests/lustre_good b/tests/lustre_good new file mode 100644 --- /dev/null +++ b/tests/lustre_good @@ -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 )) )))) ))))