diff --git a/CHANGELOG.md b/CHANGELOG.md new file mode 100644 --- /dev/null +++ b/CHANGELOG.md @@ -0,0 +1,31 @@ +# Revision history for ogma-language-fret-reqs + +## [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 (#55). + +## [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,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/ogma-language-fret-reqs.cabal b/ogma-language-fret-reqs.cabal new file mode 100644 --- /dev/null +++ b/ogma-language-fret-reqs.cabal @@ -0,0 +1,102 @@ +-- 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: Simple + +name: ogma-language-fret-reqs +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 + tests/fret_good.json + tests/fret_bad.json + +synopsis: Ogma: Runtime Monitor translator: FRET Component Requirement DB 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 Requirement Databases. + +library + + exposed-modules: + Language.FRETReqsDB.AST + + build-depends: + base >= 4.11.0.0 && < 5 + , aeson >= 2.0.0.0 && < 2.2 + , text + + , ogma-language-cocospec >= 1.0.0 && < 1.1 + , ogma-language-smv >= 1.0.0 && < 1.1 + + hs-source-dirs: + src + + default-language: + Haskell2010 + + 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.0.0 && < 1.1 + , ogma-language-fret-reqs + + hs-source-dirs: + tests + + default-language: + Haskell2010 + + ghc-options: + -Wall diff --git a/src/Language/FRETReqsDB/AST.hs b/src/Language/FRETReqsDB/AST.hs new file mode 100644 --- /dev/null +++ b/src/Language/FRETReqsDB/AST.hs @@ -0,0 +1,104 @@ +-- 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 DeriveGeneric #-} +{-# LANGUAGE OverloadedStrings #-} +{- HLINT ignore "Functor law" -} + +-- | Implementation of a (partial) FRET requirements database parser and a +-- datatype representing FRET Requirements DB files. +-- +-- FRET files are JSON files, which is implemented using type classes, so the +-- parser is defined in the same module as the AST to avoid having orphan +-- instances. +-- +module Language.FRETReqsDB.AST where + +-- External imports +import Data.Aeson ( FromJSON (..), Value (Object), withObject, + (.:) ) +import Data.Aeson.Types ( prependFailure, typeMismatch ) +import qualified Data.Text as T +import GHC.Generics ( Generic ) + +-- 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 ) + +-- * FRETReqsDB file format + +-- | Datatype representing FRETReqsDB files. +-- +-- Only the fields we are interested in are supported. +data FRETReqsDB = FRETReqsDB + { reqid :: T.Text + , parent_reqid :: T.Text + , project :: T.Text + , rationale :: T.Text + , fulltext :: T.Text + , semantics :: FRETSemantics + } + deriving (Generic, Show) + +-- | Instance to parse FRETReqsDB files in JSON format. +instance FromJSON FRETReqsDB where + parseJSON (Object v) = FRETReqsDB + <$> v .: "reqid" + <*> v .: "parent_reqid" + <*> v .: "project" + <*> v .: "rationale" + <*> v .: "fulltext" + <*> v .: "semantics" + + parseJSON invalid = + prependFailure "parsing FRET Requirement Database failed, " + (typeMismatch "Object" invalid) + +-- | Datatype representing the semantics key of a FRET file. +-- +-- Only the fields we are interested in are supported. +data FRETSemantics = FRETSemantics + { semanticsType :: T.Text + , semanticsFretish :: Either String SMV.BoolSpec + , semanticsCoCoSpec :: Either String CoCoSpec.BoolSpec + } + deriving (Generic, Show) + +-- | Instance to parse FRET semantics keys in JSON format. +instance FromJSON FRETSemantics where + parseJSON = withObject "semantics" $ \v -> FRETSemantics + <$> v .: "type" + <*> (SMV.pBoolSpec <$> SMV.myLexer <$> T.unpack <$> v .: "ptExpanded") + <*> (CoCoSpec.pBoolSpec + <$> CoCoSpec.myLexer <$> T.unpack <$> v .: "CoCoSpecCode") diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -0,0 +1,83 @@ +-- 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 FRETReqsDB 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.FRETReqsDB.AST ( FRETReqsDB ) + +-- | Run all unit tests for the FRETReqsDB parser. +main :: IO () +main = + defaultMainWithOpts tests mempty + +-- | All unit tests for the FRETReqsDB parser. +tests :: [Test.Framework.Test] +tests = + [ testProperty "Parse FRETReqsDB (correct case)" propParseFRETReqsDBOk + -- , testProperty "Parse FRETReqsDB (incorrect case)" propParseFRETReqsDBFail + ] + +-- | Test the FRETReqsDB parser on a well-formed boolean specification. +propParseFRETReqsDBOk :: Property +propParseFRETReqsDBOk = monadicIO $ do + content <- run $ parseFretReqsDB "tests/fret_good.json" + assert (isRight content) + +-- | Test the FRETReqsDB parser on an incorrect boolean specification. +propParseFRETReqsDBFail :: Property +propParseFRETReqsDBFail = monadicIO $ do + componentSpec <- run $ parseFretReqsDB "tests/fret_bad.json" + assert (isLeft componentSpec) + +-- | Parse a JSON file containing a FRET Requirements Database. +-- +-- 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. +parseFretReqsDB :: FilePath -> IO (Either String FRETReqsDB) +parseFretReqsDB fp = do + reqsDB <- B.safeReadFile fp + let e = eitherDecode =<< reqsDB + print e + return e diff --git a/tests/fret_bad.json b/tests/fret_bad.json new file mode 100644 --- /dev/null +++ b/tests/fret_bad.json @@ -0,0 +1,64 @@ +{ + "noreqid": "test_req1", + "parent_reqid": "", + "project": "Test", + "rationale": "", + "fulltext": "during flight_mode when conflict_detected planner_module shall within 10 seconds satisfy (replanning_mode).", + "semantics": { + "type": "nasa", + "scope": { + "type": "in" + }, + "condition": "regular", + "timing": "within", + "response": "satisfaction", + "variables": { + "regular": [ + "conflict_detected", + "replanning_mode" + ], + "modes": [ + "flight_mode" + ] + }, + "scope_mode": "flight_mode", + "scopeTextRange": [ + 0, + 17 + ], + "regular_condition": "(conflict_detected)", + "qualifier_word": "when", + "pre_condition": "(conflict_detected)", + "conditionTextRange": [ + 19, + 40 + ], + "component_name": "planner_module", + "componentTextRange": [ + 42, + 55 + ], + "duration": [ + "10" + ], + "timingTextRange": [ + 63, + 79 + ], + "post_condition": "(( replanning_mode ))", + "responseTextRange": [ + 81, + 105 + ], + "ft": "((LAST V ((! (Fin_flight_mode & (! LAST))) | (X (((Lin_flight_mode | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (Lin_flight_mode | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))) & (! (Lin_flight_mode | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))))))) & (flight_mode -> (((Lin_flight_mode | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (Lin_flight_mode | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))) & (! (Lin_flight_mode | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))))))", + "pt": "((H ((Lin_flight_mode & (! FTP)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) & Fin_flight_mode))))) & (((! Lin_flight_mode) S ((! Lin_flight_mode) & Fin_flight_mode)) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) & Fin_flight_mode))))", + "ftExpanded": "((LAST V ((! ((((! flight_mode) & (! LAST)) & (X flight_mode)) & (! LAST))) | (X (((((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))))))) & (flight_mode -> (((((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))))))", + "ptExpanded": "((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))))))))", + "component": "planner_module", + "CoCoSpecCode": "((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 )) )))) ))))", + "diagramVariables": "M = flight_mode, TC = (conflict_detected), n = 10, Response = (( replanning_mode )).", + "description": "ENFORCED: in every interval where flight_mode holds.\nTRIGGER: first point in the interval if (conflict_detected) is true and any point in the interval where (conflict_detected) becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=10 from the trigger, except if the end of the interval occurs sooner.", + "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_within_satisfaction.svg" + }, + "_id": "fbc0a840-a04b-11ea-b135-098996762962" +} diff --git a/tests/fret_good.json b/tests/fret_good.json new file mode 100644 --- /dev/null +++ b/tests/fret_good.json @@ -0,0 +1,64 @@ +{ + "reqid": "test_req1", + "parent_reqid": "", + "project": "Test", + "rationale": "", + "fulltext": "during flight_mode when conflict_detected planner_module shall within 10 seconds satisfy (replanning_mode).", + "semantics": { + "type": "nasa", + "scope": { + "type": "in" + }, + "condition": "regular", + "timing": "within", + "response": "satisfaction", + "variables": { + "regular": [ + "conflict_detected", + "replanning_mode" + ], + "modes": [ + "flight_mode" + ] + }, + "scope_mode": "flight_mode", + "scopeTextRange": [ + 0, + 17 + ], + "regular_condition": "(conflict_detected)", + "qualifier_word": "when", + "pre_condition": "(conflict_detected)", + "conditionTextRange": [ + 19, + 40 + ], + "component_name": "planner_module", + "componentTextRange": [ + 42, + 55 + ], + "duration": [ + "10" + ], + "timingTextRange": [ + 63, + 79 + ], + "post_condition": "(( replanning_mode ))", + "responseTextRange": [ + 81, + 105 + ], + "ft": "((LAST V ((! (Fin_flight_mode & (! LAST))) | (X (((Lin_flight_mode | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (Lin_flight_mode | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))) & (! (Lin_flight_mode | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))))))) & (flight_mode -> (((Lin_flight_mode | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (Lin_flight_mode | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))) & (! (Lin_flight_mode | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (Lin_flight_mode | LAST)))))))", + "pt": "((H ((Lin_flight_mode & (! FTP)) -> (Y (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) & Fin_flight_mode))))) & (((! Lin_flight_mode) S ((! Lin_flight_mode) & Fin_flight_mode)) -> (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) S (((O[=10] (((conflict_detected) & ((Y (! (conflict_detected))) | Fin_flight_mode)) & (! (( replanning_mode ))))) -> (O[<10] (Fin_flight_mode | (( replanning_mode ))))) & Fin_flight_mode))))", + "ftExpanded": "((LAST V ((! ((((! flight_mode) & (! LAST)) & (X flight_mode)) & (! LAST))) | (X (((((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))))))) & (flight_mode -> (((((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST) V (((! (conflict_detected)) & ((! LAST) & ((X (conflict_detected)) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) -> ((X ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))) & (! (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST))))) & ((conflict_detected) -> ((F[<=10] (( replanning_mode ))) | (F[<10] (((flight_mode & (! LAST)) & (X (! flight_mode))) | LAST)))))))", + "ptExpanded": "((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))))))))", + "component": "planner_module", + "CoCoSpecCode": "((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 )) )))) ))))", + "diagramVariables": "M = flight_mode, TC = (conflict_detected), n = 10, Response = (( replanning_mode )).", + "description": "ENFORCED: in every interval where flight_mode holds.\nTRIGGER: first point in the interval if (conflict_detected) is true and any point in the interval where (conflict_detected) becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=10 from the trigger, except if the end of the interval occurs sooner.", + "diagram": "_media/user-interface/examples/svgDiagrams/in_regular_within_satisfaction.svg" + }, + "_id": "fbc0a840-a04b-11ea-b135-098996762962" +}