diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,32 @@ +# Revision history for ogma-language-smv + +## [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). +* 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/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.SMV -o src/ grammar/SMV.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/SMV.cf b/grammar/SMV.cf new file mode 100644 --- /dev/null +++ b/grammar/SMV.cf @@ -0,0 +1,111 @@ +-- 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. + +-- This is a simplified grammar of SMV temporal logic expressions, extended +-- with the tags that FRET uses around names. +-- +-- The format of FRET files itself uses JSON, so this grammar applies +-- only to specific fields in those files. + +entrypoints BoolSpec; + +BoolSpecSignal. BoolSpec9 ::= Ident; +BoolSpecConst. BoolSpec9 ::= BoolConst ; +BoolSpecNum. BoolSpec9 ::= NumExpr; +BoolSpecCmp. BoolSpec8 ::= BoolSpec8 OrdOp BoolSpec9; +BoolSpecNeg. BoolSpec7 ::= "!" BoolSpec8; +BoolSpecAnd. BoolSpec6 ::= BoolSpec6 "&" BoolSpec7; +BoolSpecOr. BoolSpec5 ::= BoolSpec5 "|" BoolSpec6; +BoolSpecXor. BoolSpec4 ::= BoolSpec4 "xor" BoolSpec5; +BoolSpecImplies. BoolSpec3 ::= BoolSpec3 "->" BoolSpec4; +BoolSpecEquivs. BoolSpec2 ::= BoolSpec2 "<->" BoolSpec3; +BoolSpecOp1. BoolSpec1 ::= OpOne BoolSpec2; +BoolSpecOp2. BoolSpec ::= BoolSpec OpTwo BoolSpec1; + +_ . BoolSpec9 ::= "(" BoolSpec ")"; +_ . BoolSpec9 ::= "" BoolSpec ""; +_ . BoolSpec9 ::= "" BoolSpec ""; +_ . BoolSpec8 ::= BoolSpec9 ; +_ . BoolSpec7 ::= BoolSpec8 ; +_ . BoolSpec6 ::= BoolSpec7 ; +_ . BoolSpec5 ::= BoolSpec6 ; +_ . BoolSpec4 ::= BoolSpec5 ; +_ . BoolSpec3 ::= BoolSpec4 ; +_ . BoolSpec2 ::= BoolSpec3 ; +_ . BoolSpec1 ::= BoolSpec2 ; +_ . BoolSpec ::= BoolSpec1 ; + +NumId . NumExpr2 ::= Ident ; +NumConstI . NumExpr2 ::= Integer ; +NumConstD . NumExpr2 ::= Double; +NumAdd . NumExpr1 ::= NumExpr1 AdditiveOp NumExpr2; +NumMult . NumExpr ::= NumExpr MultOp NumExpr1; + +_ . NumExpr2 ::= "(" NumExpr ")" ; +_ . NumExpr1 ::= NumExpr2 ; +_ . NumExpr ::= NumExpr1; + +OpPlus . AdditiveOp ::= "+" ; +OpMinus . AdditiveOp ::= "-" ; + +OpTimes . MultOp ::= "*" ; +OpDiv . MultOp ::= "/" ; + +BoolConstTrue. BoolConst ::= "TRUE"; +BoolConstFalse. BoolConst ::= "FALSE"; +BoolConstFTP. BoolConst ::= "FTP"; +BoolConstLAST. BoolConst ::= "LAST"; + +Op1Alone . OpOne ::= Op1Name; +Op1MTL. OpOne ::= Op1Name "[" OrdOp Number "]"; + +NumberInt . Number ::= Integer; +_ . Number ::= "" Number ""; +_ . Number ::= "" Number ""; + +OrdOpLT . OrdOp ::= "<"; +OrdOpLE . OrdOp ::= "<="; +OrdOpEQ . OrdOp ::= "="; +OrdOpGT . OrdOp ::= ">"; +OrdOpGE . OrdOp ::= ">="; + +Op1Pre. Op1Name ::= "pre"; +Op1X. Op1Name ::= "X"; +Op1G. Op1Name ::= "G"; +Op1F. Op1Name ::= "F"; +Op1Y. Op1Name ::= "Y"; +Op1Z. Op1Name ::= "Z"; +Op1Hist. Op1Name ::= "H"; +Op1O. Op1Name ::= "O"; + +Op2S. OpTwo ::= "S"; +Op2T. OpTwo ::= "T"; +Op2V. OpTwo ::= "V"; +Op2U. OpTwo ::= "U"; diff --git a/ogma-language-smv.cabal b/ogma-language-smv.cabal new file mode 100644 --- /dev/null +++ b/ogma-language-smv.cabal @@ -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-smv +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/SMV.cf + src/.keep + tests/smv_good + tests/smv_bad + +synopsis: Ogma: Runtime Monitor translator: SMV 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 SMV 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.SMV.AbsSMV + Language.SMV.LexSMV + Language.SMV.ParSMV + Language.SMV.PrintSMV + + autogen-modules: + Language.SMV.AbsSMV + Language.SMV.LexSMV + Language.SMV.ParSMV + Language.SMV.PrintSMV + + 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-smv + + 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 SMV 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.SMV.ParSMV as SMV ( myLexer, pBoolSpec ) + +-- | Run all unit tests for the SMV parser. +main :: IO () +main = + defaultMainWithOpts tests mempty + +-- | All unit tests for the SMV parser. +tests :: [Test.Framework.Test] +tests = + [ testProperty "Parse SMV (correct case)" propParseSMVOk + , testProperty "Parse SMV (incorrect case)" propParseSMVFail + ] + +-- | Test the SMV parser on a well-formed boolean specification. +propParseSMVOk :: Property +propParseSMVOk = monadicIO $ do + content <- run $ readFile "tests/smv_good" + let program = SMV.pBoolSpec $ SMV.myLexer content + assert (isRight program) + +-- | Test the SMV parser on an incorrect boolean specification. +propParseSMVFail :: Property +propParseSMVFail = monadicIO $ do + content <- run $ readFile "tests/smv_bad" + let program = SMV.pBoolSpec $ SMV.myLexer content + assert (isLeft program) diff --git a/tests/smv_bad b/tests/smv_bad new file mode 100644 --- /dev/null +++ b/tests/smv_bad @@ -0,0 +1,1 @@ +((D ((((! 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)))))))) diff --git a/tests/smv_good b/tests/smv_good new file mode 100644 --- /dev/null +++ b/tests/smv_good @@ -0,0 +1,1 @@ +((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))))))))