-- Copyright 2020 United States Government as represented by the Administrator
-- of the National Aeronautics and Space Administration. All Rights Reserved.
--
-- Disclaimers
--
-- Licensed under the Apache License, Version 2.0 (the "License"); you may
-- not use this file except in compliance with the License. You may obtain a
-- copy of the License at
--
--      https://www.apache.org/licenses/LICENSE-2.0
--
-- Unless required by applicable law or agreed to in writing, software
-- distributed under the License is distributed on an "AS IS" BASIS, WITHOUT
-- WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the
-- License for the specific language governing permissions and limitations
-- under the License.

-- This is a simplified grammar of SMV temporal logic expressions. This grammar
-- allows for the presence of tags around some expressions, which some tools
-- that produce SMV include in expressions.

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";