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-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. 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-cs.cabal b/ogma-language-fret-cs.cabal new file mode 100644 --- /dev/null +++ b/ogma-language-fret-cs.cabal @@ -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 + , 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 diff --git a/src/Language/FRETComponentSpec/AST.hs b/src/Language/FRETComponentSpec/AST.hs new file mode 100644 --- /dev/null +++ b/src/Language/FRETComponentSpec/AST.hs @@ -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) diff --git a/tests/Main.hs b/tests/Main.hs new file mode 100644 --- /dev/null +++ b/tests/Main.hs @@ -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 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,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 ((((! 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))))))))", + "fretish": "Meaning not specified" + } + ] + } +} 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,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 ((((! 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))))))))", + "fretish": "Meaning not specified" + } + ] + } +}