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