ogma-language-fret-cs (empty) → 1.0.6
raw patch · 8 files changed
+491/−0 lines, 8 filesdep +QuickCheckdep +aesondep +basesetup-changedbinary-added
Dependencies added: QuickCheck, aeson, base, ogma-extra, ogma-language-cocospec, ogma-language-fret-cs, ogma-language-smv, test-framework, test-framework-quickcheck2
Files
- CHANGELOG.md +32/−0
- LICENSE.pdf binary
- Setup.hs +2/−0
- ogma-language-fret-cs.cabal +101/−0
- src/Language/FRETComponentSpec/AST.hs +233/−0
- tests/Main.hs +81/−0
- tests/fret_bad.json +21/−0
- tests/fret_good.json +21/−0
+ CHANGELOG.md view
@@ -0,0 +1,32 @@+# Revision history for ogma-language-fret-cs++## [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; adjust code to work with Aeson 2 (#55).+* 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.
+ LICENSE.pdf view
binary file changed (absent → 117991 bytes)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ ogma-language-fret-cs.cabal view
@@ -0,0 +1,101 @@+-- 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-cs+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 Specification 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 Specifications.++library++ exposed-modules:+ Language.FRETComponentSpec.AST++ build-depends:+ base >= 4.11.0.0 && < 5+ , aeson >= 2.0.0.0 && < 2.2++ , 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-cs++ hs-source-dirs:+ tests++ default-language:+ Haskell2010++ ghc-options:+ -Wall
+ src/Language/FRETComponentSpec/AST.hs view
@@ -0,0 +1,233 @@+-- 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 OverloadedStrings #-}+{- HLINT ignore "Functor law" -}++-- | Representation and parser of FRET Component Specifications.+--+-- FRET files are JSON files, implemented in Haskell using type classes, so the+-- parser is defined in the same module as the AST to avoid having orphan+-- instances.+module Language.FRETComponentSpec.AST where++-- External imports+import Data.Aeson ( FromJSON (..), Value (Object), (.:) )+import Data.Aeson.Types ( prependFailure, typeMismatch )+import Data.Aeson.Key ( toString )+import qualified Data.Aeson.KeyMap as M++-- 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 )++-- | Abstract representation of a FRET file.+data FRETComponentSpec = FRETComponentSpec+ { fretName :: String+ , fretInternalVariables :: [ FRETInternalVariableDef ]+ , fretExternalVariables :: [ FRETExternalVariableDef ]+ , fretRequirements :: [ FRETRequirement ]+ }+ deriving (Show)++-- | Instance to parse FRET semantics keys in JSON format.+instance FromJSON FRETComponentSpec where+ parseJSON (Object v)+ | (specName, Object specValues) <- head (M.toList v)+ = FRETComponentSpec (toString specName)+ <$> specValues .: "Internal_variables"+ <*> specValues .: "Other_variables"+ <*> specValues .: "Requirements"++ | (specName, specValues) <- head (M.toList v)+ = prependFailure "parsing FRET Component Specification failed, "+ (typeMismatch "Object" specValues)++ parseJSON invalid =+ prependFailure "parsing FRET Component Specification failed, "+ (typeMismatch "Object" invalid)++-- | Internal variable definition, with a given name, its type and either a+-- Lustre or a Copilot expression.+data FRETInternalVariableDef = FRETInternalVariableDef+ { fretInternalVariableName :: String+ , fretInternalVariableType :: String+ , fretInternalVariableLustre :: String+ , fretInternalVariableCopilot :: String+ }+ deriving (Show)++instance FromJSON FRETInternalVariableDef where+ parseJSON (Object v) = FRETInternalVariableDef+ <$> v .: "name"+ <*> v .: "type"+ <*> v .: "assignmentLustre"+ <*> v .: "assignmentCopilot"++ parseJSON invalid =+ prependFailure "parsing FRET Internal Variable definition failed, "+ (typeMismatch "Object" invalid)++-- | External variable definition, with a given name and type.+--+-- The value of external variables is assigned outside Copilot, so they have no+-- defining expression in this type..+data FRETExternalVariableDef = FRETExternalVariableDef+ { fretExternalVariableName :: String+ , fretExternalVariableType :: String+ }+ deriving (Show)++instance FromJSON FRETExternalVariableDef where+ parseJSON (Object v) = FRETExternalVariableDef+ <$> v .: "name"+ <*> v .: "type"++ parseJSON invalid =+ prependFailure "parsing FRET External Variable failed, "+ (typeMismatch "Object" invalid)++-- | Requirement with a given name and a CoCoSpec expression.+data FRETRequirement = FRETRequirement+ { fretRequirementName :: String+ , fretRequirementCoCoSpec :: Maybe (Either String CoCoSpec.BoolSpec)+ , fretRequirementPTExpanded :: Maybe (Either String SMV.BoolSpec)+ , fretRequirementFretish :: String+ }+ deriving (Show)++instance FromJSON FRETRequirement where+ parseJSON (Object v) = FRETRequirement+ <$> v .: "name"+ <*> (fmap (CoCoSpec.pBoolSpec . CoCoSpec.myLexer) <$> v .: "CoCoSpecCode")+ <*> (fmap (SMV.pBoolSpec . SMV.myLexer) <$> v .: "ptLTL")+ <*> (v .: "fretish")++ parseJSON invalid =+ prependFailure "parsing FRET Requirement failed, "+ (typeMismatch "Object" invalid)++-- | Apply a variable subsitution to variables and requirements in a FRET+-- file.+applySubstitution :: (String, String) -> FRETComponentSpec -> FRETComponentSpec+applySubstitution sub file =+ FRETComponentSpec tlName+ tlInternalVariables+ tlExternalVariables+ tlReqs+ where++ -- Result component spec fields+ tlName = fretName file+ tlInternalVariables = map internalVarMapF $ fretInternalVariables file+ tlExternalVariables = map externalVarMapF $ fretExternalVariables file+ tlReqs = map reqMapF $ fretRequirements file++ -- Mapping function for fields with names to substitute+ internalVarMapF x = x { fretInternalVariableName =+ subsName sub (fretInternalVariableName x) }++ externalVarMapF x = x { fretExternalVariableName =+ subsName sub (fretExternalVariableName x)}++ reqMapF x = x { fretRequirementName =+ subsName sub (fretRequirementName x)++ , fretRequirementPTExpanded =+ fmap (fmap (subBS sub)) (fretRequirementPTExpanded x)+ }++ -- Substitute name x if it matches the old name oName+ subsName (oName, nName) x = if x == oName then nName else x++ -- Substitute a name in all identifiers in a boolean expression+ subBS sub' = mapBoolSpecIdent (subsName sub')++ -- Traverse a boolean expression applying a function to all identifiers+ mapBoolSpecIdent :: (String -> String) -> SMV.BoolSpec -> SMV.BoolSpec+ mapBoolSpecIdent f boolSpec =+ case boolSpec of+ SMV.BoolSpecSignal (SMV.Ident i) -> SMV.BoolSpecSignal (SMV.Ident (f i))++ SMV.BoolSpecConst bc -> SMV.BoolSpecConst bc++ SMV.BoolSpecNum e -> SMV.BoolSpecNum (mapNumExprIdent f e)++ SMV.BoolSpecCmp spec1 op2 spec2 -> SMV.BoolSpecCmp+ (mapBoolSpecIdent f spec1) op2+ (mapBoolSpecIdent f spec2)++ SMV.BoolSpecNeg spec -> SMV.BoolSpecNeg (mapBoolSpecIdent f spec)++ SMV.BoolSpecAnd spec1 spec2 -> SMV.BoolSpecAnd+ (mapBoolSpecIdent f spec1)+ (mapBoolSpecIdent f spec2)++ SMV.BoolSpecOr spec1 spec2 -> SMV.BoolSpecOr+ (mapBoolSpecIdent f spec1)+ (mapBoolSpecIdent f spec2)++ SMV.BoolSpecXor spec1 spec2 -> SMV.BoolSpecXor+ (mapBoolSpecIdent f spec1)+ (mapBoolSpecIdent f spec2)++ SMV.BoolSpecImplies spec1 spec2 -> SMV.BoolSpecImplies+ (mapBoolSpecIdent f spec1)+ (mapBoolSpecIdent f spec2)++ SMV.BoolSpecEquivs spec1 spec2 -> SMV.BoolSpecEquivs+ (mapBoolSpecIdent f spec1)+ (mapBoolSpecIdent f spec2)++ SMV.BoolSpecOp1 op spec -> SMV.BoolSpecOp1 op (mapBoolSpecIdent f spec)++ SMV.BoolSpecOp2 spec1 op2 spec2 -> SMV.BoolSpecOp2+ (mapBoolSpecIdent f spec1) op2+ (mapBoolSpecIdent f spec2)++ -- Traverse a numeric expression applying a function to all identifiers+ mapNumExprIdent :: (String -> String) -> SMV.NumExpr -> SMV.NumExpr+ mapNumExprIdent f numExpr =+ case numExpr of+ SMV.NumId (SMV.Ident i) -> SMV.NumId (SMV.Ident (f i))+ SMV.NumConstI c -> SMV.NumConstI c+ SMV.NumConstD c -> SMV.NumConstD c+ SMV.NumAdd expr1 op expr2 -> SMV.NumAdd+ (mapNumExprIdent f expr1)+ op+ (mapNumExprIdent f expr2)+ SMV.NumMult expr1 op expr2 -> SMV.NumMult+ (mapNumExprIdent f expr1)+ op+ (mapNumExprIdent f expr2)
+ tests/Main.hs view
@@ -0,0 +1,81 @@+-- 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 FRETCS 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.FRETComponentSpec.AST ( FRETComponentSpec )++-- | Run all unit tests for the FRETCS parser.+main :: IO ()+main =+ defaultMainWithOpts tests mempty++-- | All unit tests for the FRETCS parser.+tests :: [Test.Framework.Test]+tests =+ [ testProperty "Parse FRETCS (correct case)" propParseFRETCSOk+ , testProperty "Parse FRETCS (incorrect case)" propParseFRETCSFail+ ]++-- | Test the FRETCS parser on a well-formed boolean specification.+propParseFRETCSOk :: Property+propParseFRETCSOk = monadicIO $ do+ content <- run $ parseFretComponentSpec "tests/fret_good.json"+ assert (isRight content)++-- | Test the FRETCS parser on an incorrect boolean specification.+propParseFRETCSFail :: Property+propParseFRETCSFail = monadicIO $ do+ componentSpec <- run $ parseFretComponentSpec "tests/fret_bad.json"+ assert (isLeft componentSpec)++-- | Parse a JSON file containing a FRET component specification.+--+-- 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.+parseFretComponentSpec :: FilePath -> IO (Either String FRETComponentSpec)+parseFretComponentSpec fp = do+ componentSpec <- B.safeReadFile fp+ return $ eitherDecode =<< componentSpec
+ tests/fret_bad.json view
@@ -0,0 +1,21 @@+{+ "RTSASpec": {+ "Middle_variables": [],+ "Other_variables": [+ {"name":"param_is_short", "type":"bool"},+ {"name":"param_value_short", "type":"real"},+ {"name":"param_value_long", "type":"real"},+ {"name":"upper_param_limit", "type":"real"},+ {"name":"lower_param_limit", "type":"real"},+ {"name":"envelope_issue", "type":"bool"}+ ],+ "Requirements": [+ {+ "name": "behnazOne",+ "CoCoSpecCode": "",+ "ptltl": "((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>))))))))",+ "fretish": "Meaning not specified"+ }+ ]+ }+}
+ tests/fret_good.json view
@@ -0,0 +1,21 @@+{+ "RTSASpec": {+ "Internal_variables": [],+ "Other_variables": [+ {"name":"param_is_short", "type":"bool"},+ {"name":"param_value_short", "type":"real"},+ {"name":"param_value_long", "type":"real"},+ {"name":"upper_param_limit", "type":"real"},+ {"name":"lower_param_limit", "type":"real"},+ {"name":"envelope_issue", "type":"bool"}+ ],+ "Requirements": [+ {+ "name": "behnazOne",+ "CoCoSpecCode": "",+ "ptLTL": "((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>))))))))",+ "fretish": "Meaning not specified"+ }+ ]+ }+}