ogma-language-smv (empty) → 1.0.6

raw patch · 9 files changed

+352/−0 lines, 9 filesdep +QuickCheckdep +arraydep +basebuild-type:Customsetup-changedbinary-added

Dependencies added: QuickCheck, array, base, ogma-language-smv, test-framework, test-framework-quickcheck2

Files

CHANGELOG.md +32/−0
LICENSE.pdf binary
Setup.hs +27/−0
grammar/SMV.cf +111/−0
ogma-language-smv.cabal +112/−0
src/.keep +0/−0
tests/Main.hs +68/−0
tests/smv_bad +1/−0
tests/smv_good +1/−0

+ CHANGELOG.md view

@@ -0,0 +1,32 @@+# Revision history for ogma-language-smv++## [1.0.6] - 2022-11-21++* Version bump 1.0.6 (#64).+* Update license in cabal file to OtherLicense (#62).+* Add empty file to keep directory structure in distributable package (#65).++## [1.0.5] - 2022-09-21++* Version bump 1.0.5 (#60).+* Support floating point numbers in SMV expressions (#58).++## [1.0.4] - 2022-07-21++* Version bump 1.0.4 (#53).++## [1.0.3] - 2022-05-21++* Version bump 1.0.3 (#49).++## [1.0.2] - 2022-03-21++* Version bump 1.0.2 (#43).++## [1.0.1] - 2022-01-21++* Version bump 1.0.1 (#39).++## [1.0.0] - 2021-11-22++* Initial release.

+ LICENSE.pdf view

binary file changed (absent → 117991 bytes)

+ Setup.hs view

@@ -0,0 +1,27 @@+-- | Custom Setup that runs bnfc to generate the language sub-libraries+-- for the parsers included in Ogma.+module Main (main) where++import Distribution.Simple         ( defaultMainWithHooks, hookedPrograms,+                                     postConf, preBuild, simpleUserHooks )+import Distribution.Simple.Program ( Program (..), findProgramVersion,+                                     simpleProgram )+import System.Process              ( system )++-- | Run BNFC on the grammar before the actual build step.+--+-- All options for bnfc are hard-coded here. There is an open bug in Cabal's+-- github repo about supporting BNFC.+main :: IO ()+main = defaultMainWithHooks $ simpleUserHooks+  { hookedPrograms = [ bnfcProgram ]+  , postConf       = \args flags packageDesc localBuildInfo -> do+      _ <- system "bnfc --haskell -p Language.SMV -o src/ grammar/SMV.cf"+      postConf simpleUserHooks args flags packageDesc localBuildInfo+  }++-- | TODO: This should be in Cabal.Distribution.Simple.Program.Builtin.+bnfcProgram :: Program+bnfcProgram = (simpleProgram "bnfc")+  { programFindVersion = findProgramVersion "--version" id+  }

+ grammar/SMV.cf view

@@ -0,0 +1,111 @@+-- Copyright 2020 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS."+--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.++-- This is a simplified grammar of SMV temporal logic expressions, extended+-- with the tags that FRET uses around names.+--+-- The format of FRET files itself uses JSON, so this grammar applies+-- only to specific fields in those files.++entrypoints BoolSpec;++BoolSpecSignal.  BoolSpec9 ::= Ident;+BoolSpecConst.   BoolSpec9 ::= BoolConst ;+BoolSpecNum.     BoolSpec9 ::= NumExpr;+BoolSpecCmp.     BoolSpec8 ::= BoolSpec8 OrdOp BoolSpec9;+BoolSpecNeg.     BoolSpec7 ::= "!" BoolSpec8;+BoolSpecAnd.     BoolSpec6 ::= BoolSpec6 "&" BoolSpec7;+BoolSpecOr.      BoolSpec5 ::= BoolSpec5 "|" BoolSpec6;+BoolSpecXor.     BoolSpec4 ::= BoolSpec4 "xor" BoolSpec5;+BoolSpecImplies. BoolSpec3 ::= BoolSpec3 "->" BoolSpec4;+BoolSpecEquivs.  BoolSpec2 ::= BoolSpec2 "<->" BoolSpec3;+BoolSpecOp1.     BoolSpec1 ::= OpOne BoolSpec2;+BoolSpecOp2.     BoolSpec  ::= BoolSpec OpTwo BoolSpec1;++_ . BoolSpec9 ::= "(" BoolSpec ")";+_ . BoolSpec9 ::= "<b>" BoolSpec "</b>";+_ . BoolSpec9 ::= "<i>" BoolSpec "</i>";+_ . BoolSpec8 ::= BoolSpec9 ;+_ . BoolSpec7 ::= BoolSpec8 ;+_ . BoolSpec6 ::= BoolSpec7 ;+_ . BoolSpec5 ::= BoolSpec6 ;+_ . BoolSpec4 ::= BoolSpec5 ;+_ . BoolSpec3 ::= BoolSpec4 ;+_ . BoolSpec2 ::= BoolSpec3 ;+_ . BoolSpec1 ::= BoolSpec2 ;+_ . BoolSpec  ::= BoolSpec1 ;++NumId     . NumExpr2 ::= Ident ;+NumConstI . NumExpr2 ::= Integer ;+NumConstD . NumExpr2 ::= Double;+NumAdd    . NumExpr1 ::= NumExpr1 AdditiveOp NumExpr2;+NumMult   . NumExpr  ::= NumExpr MultOp NumExpr1;++_ . NumExpr2 ::= "(" NumExpr ")" ;+_ . NumExpr1 ::= NumExpr2 ;+_ . NumExpr  ::= NumExpr1;++OpPlus  . AdditiveOp ::= "+" ;+OpMinus . AdditiveOp ::= "-" ;++OpTimes . MultOp ::= "*" ;+OpDiv   . MultOp ::= "/" ;++BoolConstTrue.  BoolConst ::= "TRUE";+BoolConstFalse. BoolConst ::= "FALSE";+BoolConstFTP.   BoolConst ::= "FTP";+BoolConstLAST.  BoolConst ::= "LAST";++Op1Alone . OpOne ::= Op1Name;+Op1MTL.    OpOne ::= Op1Name "[" OrdOp Number "]";++NumberInt . Number ::= Integer;+_ . Number ::= "<b>" Number "</b>";+_ . Number ::= "<i>" Number "</i>";++OrdOpLT . OrdOp ::= "<";+OrdOpLE . OrdOp ::= "<=";+OrdOpEQ . OrdOp ::= "=";+OrdOpGT . OrdOp ::= ">";+OrdOpGE . OrdOp ::= ">=";++Op1Pre.  Op1Name ::= "pre";+Op1X.    Op1Name ::= "X";+Op1G.    Op1Name ::= "G";+Op1F.    Op1Name ::= "F";+Op1Y.    Op1Name ::= "Y";+Op1Z.    Op1Name ::= "Z";+Op1Hist. Op1Name ::= "H";+Op1O.    Op1Name ::= "O";++Op2S.     OpTwo ::= "S";+Op2T.     OpTwo ::= "T";+Op2V.     OpTwo ::= "V";+Op2U.     OpTwo ::= "U";

+ ogma-language-smv.cabal view

@@ -0,0 +1,112 @@+-- Copyright 2020 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS." +--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.++cabal-version:       2.0+build-type:          Custom++name:                ogma-language-smv+version:             1.0.6+homepage:            http://nasa.gov+license:             OtherLicense+license-file:        LICENSE.pdf+author:              Ivan Perez, Alwyn Goodloe+maintainer:          ivan.perezdominguez@nasa.gov+category:            Aerospace+extra-source-files:  CHANGELOG.md+                     grammar/SMV.cf+                     src/.keep+                     tests/smv_good+                     tests/smv_bad++synopsis:            Ogma: Runtime Monitor translator: SMV Language Frontend++description:         Ogma is a tool to facilitate the integration of safe runtime monitors into+                     other systems. Ogma extends+                     <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 SMV Boolean expressions, used by+                     the tool FRET to capture requirement specifications.++custom-setup+  setup-depends:+      base    >= 4.11.0.0 && < 5+    , Cabal   >= 2.0+    , process+    , BNFC    >= 2.9.1++library++  exposed-modules:+    -- Automatically generated+    Language.SMV.AbsSMV+    Language.SMV.LexSMV+    Language.SMV.ParSMV+    Language.SMV.PrintSMV++  autogen-modules:+    Language.SMV.AbsSMV+    Language.SMV.LexSMV+    Language.SMV.ParSMV+    Language.SMV.PrintSMV++  build-depends:+      base  >= 4.11.0.0 && < 5+    , array >= 0.5.2.0++  hs-source-dirs:+    src++  default-language:+    Haskell2010++test-suite unit-tests+  type:+    exitcode-stdio-1.0++  main-is:+    Main.hs++  build-depends:+      base                       >= 4.11.0.0 && < 5+    , QuickCheck+    , test-framework+    , test-framework-quickcheck2++    , ogma-language-smv++  hs-source-dirs:+    tests++  default-language:+    Haskell2010++  ghc-options:+    -Wall

+ src/.keep view

+ tests/Main.hs view

@@ -0,0 +1,68 @@+-- Copyright 2020 United States Government as represented by the Administrator+-- of the National Aeronautics and Space Administration. All Rights Reserved.+--+-- Disclaimers+--+-- No Warranty: THE SUBJECT SOFTWARE IS PROVIDED "AS IS" WITHOUT ANY WARRANTY+-- OF ANY KIND, EITHER EXPRESSED, IMPLIED, OR STATUTORY, INCLUDING, BUT NOT+-- LIMITED TO, ANY WARRANTY THAT THE SUBJECT SOFTWARE WILL CONFORM TO+-- SPECIFICATIONS, ANY IMPLIED WARRANTIES OF MERCHANTABILITY, FITNESS FOR A+-- PARTICULAR PURPOSE, OR FREEDOM FROM INFRINGEMENT, ANY WARRANTY THAT THE+-- SUBJECT SOFTWARE WILL BE ERROR FREE, OR ANY WARRANTY THAT DOCUMENTATION, IF+-- PROVIDED, WILL CONFORM TO THE SUBJECT SOFTWARE. THIS AGREEMENT DOES NOT, IN+-- ANY MANNER, CONSTITUTE AN ENDORSEMENT BY GOVERNMENT AGENCY OR ANY PRIOR+-- RECIPIENT OF ANY RESULTS, RESULTING DESIGNS, HARDWARE, SOFTWARE PRODUCTS OR+-- ANY OTHER APPLICATIONS RESULTING FROM USE OF THE SUBJECT SOFTWARE. FURTHER,+-- GOVERNMENT AGENCY DISCLAIMS ALL WARRANTIES AND LIABILITIES REGARDING+-- THIRD-PARTY SOFTWARE, IF PRESENT IN THE ORIGINAL SOFTWARE, AND DISTRIBUTES+-- IT "AS IS." +--+-- Waiver and Indemnity: RECIPIENT AGREES TO WAIVE ANY AND ALL CLAIMS AGAINST+-- THE UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS+-- ANY PRIOR RECIPIENT. IF RECIPIENT'S USE OF THE SUBJECT SOFTWARE RESULTS IN+-- ANY LIABILITIES, DEMANDS, DAMAGES, EXPENSES OR LOSSES ARISING FROM SUCH USE,+-- INCLUDING ANY DAMAGES FROM PRODUCTS BASED ON, OR RESULTING FROM, RECIPIENT'S+-- USE OF THE SUBJECT SOFTWARE, RECIPIENT SHALL INDEMNIFY AND HOLD HARMLESS THE+-- UNITED STATES GOVERNMENT, ITS CONTRACTORS AND SUBCONTRACTORS, AS WELL AS ANY+-- PRIOR RECIPIENT, TO THE EXTENT PERMITTED BY LAW. RECIPIENT'S SOLE REMEDY+-- FOR ANY SUCH MATTER SHALL BE THE IMMEDIATE, UNILATERAL TERMINATION OF THIS+-- AGREEMENT.+--+-- | Test SMV language library.+module Main where++-- External imports+import Data.Either                          ( isLeft, isRight )+import Test.Framework                       ( Test, defaultMainWithOpts )+import Test.Framework.Providers.QuickCheck2 ( testProperty )+import Test.QuickCheck                      ( Property )+import Test.QuickCheck.Monadic              ( assert, monadicIO, run )++-- Internal imports+import qualified Language.SMV.ParSMV as SMV ( myLexer, pBoolSpec )++-- | Run all unit tests for the SMV parser.+main :: IO ()+main =+  defaultMainWithOpts tests mempty++-- | All unit tests for the SMV parser.+tests :: [Test.Framework.Test]+tests =+  [ testProperty "Parse SMV (correct case)"   propParseSMVOk+  , testProperty "Parse SMV (incorrect case)" propParseSMVFail+  ]++-- | Test the SMV parser on a well-formed boolean specification.+propParseSMVOk :: Property+propParseSMVOk = monadicIO $ do+  content <- run $ readFile "tests/smv_good"+  let program = SMV.pBoolSpec $ SMV.myLexer content+  assert (isRight program)++-- | Test the SMV parser on an incorrect boolean specification.+propParseSMVFail :: Property+propParseSMVFail = monadicIO $ do+  content <- run $ readFile "tests/smv_bad"+  let program = SMV.pBoolSpec $ SMV.myLexer content+  assert (isLeft program)

+ tests/smv_bad view

@@ -0,0 +1,1 @@+((D ((((! <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>))))))))

+ tests/smv_good view

@@ -0,0 +1,1 @@+((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>))))))))