-- 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 "]";
Op1MTLRange. OpOne ::= Op1Name "[" Number "," Number "]";

NumberInt . Number ::= Integer;
_ . Number ::= "<b>" Number "</b>";
_ . Number ::= "<i>" Number "</i>";

OrdOpLT . OrdOp ::= "<";
OrdOpLE . OrdOp ::= "<=";
OrdOpEQ . OrdOp ::= "=";
OrdOpNE . 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";