packages feed

ogma-language-cocospec (empty) → 1.0.6

raw patch · 9 files changed

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

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

Files

+ CHANGELOG.md view
@@ -0,0 +1,31 @@+# Revision history for ogma-language-cocospec++## [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.CoCoSpec -o src/ grammar/CoCoSpec.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/CoCoSpec.cf view
@@ -0,0 +1,93 @@+-- 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 CoCoSpec 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" ;+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 ::= "=" ;+BoolNumOp2Le . BoolNumOp ::= "<=" ;+BoolNumOp2Lt . BoolNumOp ::= "<" ;+BoolNumOp2Gt . BoolNumOp ::= ">" ;+BoolNumOp2Ge . BoolNumOp ::= ">=" ;++-- Basic types++BoolConstTrue.  BoolConst ::= "true" ;+BoolConstFalse. BoolConst ::= "false" ;+BoolConstFTP.   BoolConst ::= "FTP" ;
+ ogma-language-cocospec.cabal view
@@ -0,0 +1,112 @@+-- 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-cocospec+version:             1.0.6+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+                     grammar/CoCoSpec.cf+                     src/.keep+                     tests/cocospec_good+                     tests/cocospec_bad++synopsis:            Ogma: Runtime Monitor translator: CoCoSpec 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 CoCoSpec Boolean expressions, used by+                     the tool FRET to capture requirement specifications.++custom-setup+  setup-depends:+      base    >= 4.11.0.0 && < 5+    , Cabal   >= 2.0+    , process+    , BNFC    >= 2.9.1++library++  exposed-modules:+    -- Automatically generated+    Language.CoCoSpec.AbsCoCoSpec+    Language.CoCoSpec.LexCoCoSpec+    Language.CoCoSpec.ParCoCoSpec+    Language.CoCoSpec.PrintCoCoSpec++  autogen-modules:+    Language.CoCoSpec.AbsCoCoSpec+    Language.CoCoSpec.LexCoCoSpec+    Language.CoCoSpec.ParCoCoSpec+    Language.CoCoSpec.PrintCoCoSpec++  build-depends:+      base  >= 4.11.0.0 && < 5+    , array >= 0.5.2.0++  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+    , test-framework+    , test-framework-quickcheck2++    , ogma-language-cocospec++  hs-source-dirs:+    tests++  default-language:+    Haskell2010++  ghc-options:+    -Wall
+ src/.keep view
+ tests/Main.hs view
@@ -0,0 +1,69 @@+-- 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 CoCoSpec 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.CoCoSpec.ParCoCoSpec as CoCoSpec ( myLexer,+                                                             pBoolSpec )++-- | Run all unit tests for the CoCoSpec parser.+main :: IO ()+main =+  defaultMainWithOpts tests mempty++-- | All unit tests for the CoCoSpec parser.+tests :: [Test.Framework.Test]+tests =+  [ testProperty "Parse CoCoSpec (correct case)"   propParseCoCoSpecOk+  , testProperty "Parse CoCoSpec (incorrect case)" propParseCoCoSpecFail+  ]++-- | Test the CoCoSpec parser on a well-formed boolean specification.+propParseCoCoSpecOk :: Property+propParseCoCoSpecOk = monadicIO $ do+  content <- run $ readFile "tests/cocospec_good"+  let program = CoCoSpec.pBoolSpec $ CoCoSpec.myLexer content+  assert (isRight program)++-- | Test the CoCoSpec parser on an incorrect boolean specification.+propParseCoCoSpecFail :: Property+propParseCoCoSpecFail = monadicIO $ do+  content <- run $ readFile "tests/cocospec_bad"+  let program = CoCoSpec.pBoolSpec $ CoCoSpec.myLexer content+  assert (isLeft program)
+ tests/cocospec_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/cocospec_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 )) )))) ))))