ogma-language-fret-reqs (empty) → 1.0.6

raw patch · 8 files changed

+450/−0 lines, 8 filesdep +QuickCheckdep +aesondep +basesetup-changedbinary-added

Dependencies added: QuickCheck, aeson, base, ogma-extra, ogma-language-cocospec, ogma-language-fret-reqs, ogma-language-smv, test-framework, test-framework-quickcheck2, text

Files

CHANGELOG.md +31/−0
LICENSE.pdf binary
Setup.hs +2/−0
ogma-language-fret-reqs.cabal +102/−0
src/Language/FRETReqsDB/AST.hs +104/−0
tests/Main.hs +83/−0
tests/fret_bad.json +64/−0
tests/fret_good.json +64/−0

+ CHANGELOG.md view

@@ -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.

+ LICENSE.pdf view

binary file changed (absent → 117991 bytes)

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ ogma-language-fret-reqs.cabal view

@@ -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+                     <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 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

+ src/Language/FRETReqsDB/AST.hs view

@@ -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")

+ tests/Main.hs view

@@ -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

+ tests/fret_bad.json view

@@ -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_<b><i>flight_mode</i></b> & (! LAST))) | (X (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))",+        "pt": "((H ((Lin_<b><i>flight_mode</i></b> & (! FTP)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))) & (((! Lin_<b><i>flight_mode</i></b>) S ((! Lin_<b><i>flight_mode</i></b>) & Fin_<b><i>flight_mode</i></b>)) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))",+        "ftExpanded": "((LAST V ((! ((((! <b><i>flight_mode</i></b>) & (! LAST)) & (X <b><i>flight_mode</i></b>)) & (! LAST))) | (X (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))",+        "ptExpanded": "((H ((((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>)) & (Y TRUE)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))) & (((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) S ((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))",+        "component": "<b><i>planner_module</i></b>",+        "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 = <b><i>flight_mode</i></b>, TC = <b><i>(conflict_detected)</i></b>,  n = <b><i>10</i></b>, Response = <b><i>(( replanning_mode ))</i></b>.",+        "description": "ENFORCED: in every interval where <b><i>flight_mode</i></b> holds.\nTRIGGER: first point in the interval if <b><i>(conflict_detected)</i></b> is true and any point in the interval where <b><i>(conflict_detected)</i></b> becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=<b><i>10</i></b> 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"+}

+ tests/fret_good.json view

@@ -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_<b><i>flight_mode</i></b> & (! LAST))) | (X (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((Lin_<b><i>flight_mode</i></b> | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))) & (! (Lin_<b><i>flight_mode</i></b> | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (Lin_<b><i>flight_mode</i></b> | LAST)))))))",+        "pt": "((H ((Lin_<b><i>flight_mode</i></b> & (! FTP)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))) & (((! Lin_<b><i>flight_mode</i></b>) S ((! Lin_<b><i>flight_mode</i></b>) & Fin_<b><i>flight_mode</i></b>)) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | Fin_<b><i>flight_mode</i></b>)) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] (Fin_<b><i>flight_mode</i></b> | <b><i>(( replanning_mode ))</i></b>))) & Fin_<b><i>flight_mode</i></b>))))",+        "ftExpanded": "((LAST V ((! ((((! <b><i>flight_mode</i></b>) & (! LAST)) & (X <b><i>flight_mode</i></b>)) & (! LAST))) | (X (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))) & (<b><i>flight_mode</i></b> -> (((((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST) V (((! <b><i>(conflict_detected)</i></b>) & ((! LAST) & ((X <b><i>(conflict_detected)</i></b>) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) -> ((X ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))) & (! (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST))))) & (<b><i>(conflict_detected)</i></b> -> ((F[<=<b><i>10</i></b>] <b><i>(( replanning_mode ))</i></b>) | (F[<<b><i>10</i></b>] (((<b><i>flight_mode</i></b> & (! LAST)) & (X (! <b><i>flight_mode</i></b>))) | LAST)))))))",+        "ptExpanded": "((H ((((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>)) & (Y TRUE)) -> (Y (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))) & (((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) S ((! ((! <b><i>flight_mode</i></b>) & (Y <b><i>flight_mode</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) -> (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) S (((O[=<b><i>10</i></b>] ((<b><i>(conflict_detected)</i></b> & ((Y (! <b><i>(conflict_detected)</i></b>)) | (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))))) & (! <b><i>(( replanning_mode ))</i></b>))) -> (O[<<b><i>10</i></b>] ((<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>)))) | <b><i>(( replanning_mode ))</i></b>))) & (<b><i>flight_mode</i></b> & ((! (Y TRUE)) | (Y (! <b><i>flight_mode</i></b>))))))))",+        "component": "<b><i>planner_module</i></b>",+        "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 = <b><i>flight_mode</i></b>, TC = <b><i>(conflict_detected)</i></b>,  n = <b><i>10</i></b>, Response = <b><i>(( replanning_mode ))</i></b>.",+        "description": "ENFORCED: in every interval where <b><i>flight_mode</i></b> holds.\nTRIGGER: first point in the interval if <b><i>(conflict_detected)</i></b> is true and any point in the interval where <b><i>(conflict_detected)</i></b> becomes true (from false).\nREQUIRES: for every trigger, RES must hold at some point with distance <=<b><i>10</i></b> 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"+}