BNF for tla+.jj

NON-TERMINALS

PrefixOpToken ::= ( <op_26> | <op_29> | <op_58> | <CASESEP> | <op_61> | <op_112> | <op_113> | <op_114> | <op_115> | <op_116> )
NEPrefixOpToken ::= ( <op_26> | <op_29> | <op_58> | <CASESEP> | <op_61> | <op_76> | <op_112> | <op_113> | <op_114> | <op_115> | <op_116> )
InfixOpToken ::= ( <op_1> | <AND> | <op_3> | <op_4> | <OR> | <op_6> | <op_7> | <op_8> | <op_9> | <op_10> | <op_11> | <op_12> | <op_13> | <op_14> | <op_15> | <op_16> | <op_17> | <op_18> | <op_19> | <IN> | <op_21> | <op_22> | <op_23> | <op_24> | <op_25> | <op_27> | <op_30> | <op_31> | <op_32> | <op_33> | <op_34> | <op_35> | <op_36> | <op_37> | <op_38> | <op_39> | <op_40> | <op_41> | <op_42> | <op_43> | <op_44> | <op_45> | <op_46> | <op_47> | <op_48> | <op_49> | <op_50> | <op_51> | <op_52> | <op_53> | <op_54> | <op_55> | <op_56> | <op_59> | <op_62> | <op_63> | <op_64> | <EQUALS> | <op_66> | <op_67> | <op_71> | <op_72> | <op_73> | <op_74> | <op_75> | <op_77> | <op_78> | <op_79> | <op_80> | <op_81> | <op_82> | <op_83> | <op_84> | <op_85> | <op_86> | <op_87> | <op_88> | <op_89> | <op_90> | <op_91> | <op_92> | <op_93> | <op_94> | <op_95> | <op_96> | <op_97> | <op_98> | <op_100> | <op_101> | <op_102> | <op_103> | <op_104> | <op_105> | <op_106> | <op_107> | <op_108> | <op_109> | <op_110> | <op_111> | <op_117> | <op_118> | <op_119> )
PostfixOpToken ::= ( <op_57> | <op_68> | <op_69> | <op_70> )
CompilationUnit ::= ( Prelude )? Module
Prelude ::= <BEGIN_PRAGMA> ( <NUMBER> | <IDENTIFIER> )*
Module ::= BeginModule Extends Body EndModule
BeginModule ::= ( <_BM0> | <_BM1> | <_BM2> ) Identifier <SEPARATOR>
EndModule ::= <END_MODULE>
Extends ::= ( <EXTENDS> Identifier ( <COMMA> Identifier )* )?
Body ::= ( ( <SEPARATOR> | VariableDeclaration | ParamDeclaration | OperatorOrFunctionDefinition | Recursive | Instance | Assumption | Theorem | Module | UseOrHideOrBy ) )*
VariableDeclaration ::= <VARIABLE> Identifier ( <COMMA> Identifier )*
ParamDeclaration ::= ParamSubDecl ConstantDeclarationItems ( <COMMA> ConstantDeclarationItems )*
ParamSubDecl ::= <CONSTANT>
Recursive ::= <RECURSIVE> ConstantDeclarationItems ( <COMMA> ConstantDeclarationItems )*
ConstantDeclarationItems ::= ( Identifier ( <LBR> <US> ( <COMMA> <US> )* <RBR> )? | NonExpPrefixOp <US> | <US> ( InfixOp <US> | PostfixOp ) )
OperatorOrFunctionDefinition ::= ( <LOCAL> )? <DEFBREAK> ( Identifier <LSB> QuantBound ( <COMMA> QuantBound )* <RSB> <DEF> Expression | PostfixLHS <DEF> Expression | InfixLHS <DEF> Expression | IdentLHS <DEF> ( Expression | Instantiation ) | PrefixLHS <DEF> Expression )
IdentifierTuple ::= <LAB> ( Identifier ( <COMMA> Identifier )* )? <RAB>
IdentLHS ::= Identifier ( ( <LBR> ( IdentDecl | SomeFixDecl ) ( <COMMA> ( IdentDecl | SomeFixDecl ) )* <RBR> )? )
PrefixLHS ::= NEPrefixOpToken Identifier
InfixLHS ::= Identifier InfixOpToken Identifier
PostfixLHS ::= Identifier PostfixOpToken
IdentDecl ::= Identifier ( <LBR> <US> ( <COMMA> <US> )* <RBR> )?
SomeFixDecl ::= ( NonExpPrefixOp <US> | ( <US> ( InfixOp <US> | PostfixOp ) ) )
Instance ::= ( <LOCAL> )? Instantiation
Instantiation ::= <INSTANCE> Identifier ( <WITH> Substitution ( <COMMA> Substitution )* )?
Substitution ::= ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) <SUBSTITUTE> OpOrExpr
OldSubstitution ::= ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) <SUBSTITUTE> ( <op_76> | Expression | Lambda )
PrefixOp ::= PrefixOpToken
NonExpPrefixOp ::= NEPrefixOpToken
InfixOp ::= InfixOpToken
PostfixOp ::= PostfixOpToken
Identifier ::= <IDENTIFIER>
Assumption ::= ( <ASSUMPTION> | <ASSUME> ) ( ( <DEFBREAK> )? Identifier <DEF> )? Expression
AssumeProve ::= ( Identifier <COLONCOLON> AssumeProve )? <ASSUME> ( AssumeProve | NewSymb | Expression ) ( <COMMA> ( AssumeProve | NewSymb | Expression ) )* <PROVE> Expression
NewSymb ::= ( ( <NEW> <CONSTANT> | <NEW> | <CONSTANT> ) ( IdentDecl ( <IN> Expression )? | SomeFixDecl ) | ( <NEW> )? <VARIABLE> Identifier | ( <NEW> )? ( <STATE> | <ACTION> | <TEMPORAL> ) ( IdentDecl | SomeFixDecl ) )
MaybeBound ::= ( <IN> Expression )?
Theorem ::= ( <THEOREM> | <PROPOSITION> ) ( Identifier <DEF> )? ( ( ) AssumeProve | Expression ) ( Proof )?
Proof ::= ( UseOrHideOrBy | ( <PROOF> )? ( <OBVIOUS> | <OMITTED> ) | ( <PROOF> )? ( Step )* QEDStep )
UseOrHideOrBy ::= ( ( <PROOF> )? <BY> ( <ONLY> )? | <USE> ( <ONLY> )? | <HIDE> ) ( ( <MODULE> Identifier | Expression ) ( <COMMA> ( <MODULE> Identifier | Expression ) )* )? ( <DF> ( <MODULE> Identifier | Expression ) ( <COMMA> ( <MODULE> Identifier | Expression ) )* )?
StepStartToken ::= ( <ProofStepLexeme> | <ProofImplicitStepLexeme> | <ProofStepDotLexeme> | <BareLevelLexeme> | <UnnumberedStepLexeme> )
QEDStep ::= StepStartToken <QED> ( Proof )?
Step ::= StepStartToken ( UseOrHideOrBy | Instantiation | DefStep | HaveStep | TakeStep | WitnessStep | PickStep | CaseStep | AssertStep ) ( Proof )?
DefStep ::= ( <DEFINE> )? ( OperatorOrFunctionDefinition )+
HaveStep ::= <HAVE> Expression
TakeStep ::= <TAKE> ( QuantBound ( <COMMA> QuantBound )* | Identifier ( <COMMA> Identifier )* )
WitnessStep ::= <WITNESS> Expression ( <COMMA> Expression )*
PickStep ::= <PICK> ( Identifier ( <COMMA> Identifier )* | QuantBound ( <COMMA> QuantBound )* ) <COLON> Expression
CaseStep ::= <CASE> Expression
AssertStep ::= ( <SUFFICES> )? ( Expression | AssumeProve )
GeneralId ::= IdPrefix Identifier
IdPrefix ::= ( IdPrefixElement )*
IdPrefixElement ::= Identifier ( OpArgs )? <BANG>
ParenthesesExpression ::= ( ParenExpr | BraceCases | SBracketCases | SetExcept | TupleOrAction | FairnessExpr )
ClosedExpressionOrOp ::= ( ElementaryExpression | ParenthesesExpression )
ClosedExpressionOnly ::= ClosedExpressionOrOp
OpenExpression ::= ( SomeQuant | SomeTQuant | IfThenElse | Case | LetIn | UnboundOrBoundChoose )
ElementaryExpression ::= ( Extension | String | Number )
String ::= <STRING_LITERAL>
Number ::= <NUMBER_LITERAL> ( <DOT> <NUMBER_LITERAL> )?
Extension ::= ( PrefixOp | InfixOp | PostfixOp | Identifier ( OpArgs )? ( <BANG> Extension )? )
OpArgs ::= <LBR> OpSuite ( <COMMA> OpSuite )* <RBR>
OpOrExpr ::= ( ( NonExpPrefixOp | InfixOp | PostfixOp ) | Lambda | Expression )
OpSuite ::= OpOrExpr
ParenExpr ::= <LBR> Expression <RBR>
SomeQuant ::= ( <EXISTS> | <FORALL> ) ( ( Identifier ( <COMMA> Identifier )* ) | QuantBound ( <COMMA> QuantBound )* ) <COLON> Expression
SomeTQuant ::= ( <T_EXISTS> | <T_FORALL> ) Identifier ( <COMMA> Identifier )* <COLON> Expression
QuantBound ::= ( IdentifierTuple | Identifier ( <COMMA> Identifier )* ) <IN> Expression
BraceCases ::= <LBC> ( ( IdentifierTuple | Identifier ) <IN> Expression ( ( <COLON> Expression ) | ( <COMMA> Expression )+ )? | Expression ( <COMMA> Expression )* | Expression <COLON> QuantBound ( <COMMA> QuantBound )* | Expression ( <COLON> QuantBound ( <COMMA> QuantBound )* | ( <COMMA> Expression )+ )? )? <RBC>
SBracketCases ::= <LSB> ( QuantBound ( <COMMA> QuantBound )* <MAPTO> Expression <RSB> | FieldVal ( <COMMA> FieldVal )* <RSB> | FieldVal ( <COMMA> FieldVal )* <RSB> | FieldSet ( <COMMA> FieldSet )* <RSB> | Expression ( ( <COMMA> Expression )* <RSB> | <ARROW> Expression <RSB> | <EXCEPT> ExceptSpec ( <COMMA> ExceptSpec )* <RSB> | <ARSB> ReducedExpression ) )
FieldVal ::= Identifier <MAPTO> Expression
FieldSet ::= Identifier <COLON> Expression
ExceptSpec ::= <BANG> ( ExceptComponent )+ <EQUALS> Expression
ExceptComponent ::= ( <DOT> Identifier | <LSB> Expression ( <COMMA> Expression )* <RSB> )
SetExcept ::= <LWB> Expression <EXCEPT> SExceptSpec ( <COMMA> SExceptSpec )* <RWB>
SExceptSpec ::= <BANG> ExceptComponent ( <EQUALS> | <IN> ) Expression
TupleOrAction ::= <LAB> ( Expression ( <COMMA> Expression )* )? ( <RAB> | <ARAB> ReducedExpression )
NoOpExtension ::= ( Identifier ( OpArgs )? ( <BANG> NoOpExtension )? )
ReducedExpression ::= ( NoOpExtension | ParenExpr | BraceCases | SBracketCases | SetExcept | TupleOrAction )
FairnessExpr ::= ( <WF> | <SF> ) ReducedExpression ( <LBR> Expression <RBR> )?
IfThenElse ::= <IF> Expression <THEN> Expression <ELSE> Expression
Case ::= <CASE> CaseArm ( <CASESEP> CaseArm )* ( <CASESEP> OtherArm )?
CaseArm ::= Expression <ARROW> Expression
OtherArm ::= <OTHER> <ARROW> Expression
LetIn ::= <LET> LetDefinitions <LETIN> Expression
LetDefinitions ::= ( OperatorOrFunctionDefinition | Recursive )+
Junctions ::= ( DisjList | ConjList )
DisjList ::= JuncItem ( JuncItem )*
ConjList ::= JuncItem ( JuncItem )*
JuncItem ::= ( <OR> | <AND> ) Expression
UnboundOrBoundChoose ::= <CHOOSE> ( Identifier | IdentifierTuple ) MaybeBound <COLON> Expression
Lambda ::= <LAMBDA> Identifier ( <COMMA> ( Identifier ) )* <COLON> Expression
Expression ::= ( ( PrefixOp | InfixOp ) )* ( OpenExpression | ExtendableExpr )
ExtendableExpr ::= ( Junctions | ParenthesesExpression | PrimitiveExp ) ( PostfixOp | <DOT> ( ) Identifier | SBracketCases )* ( InfixOp ( ( PrefixOp | InfixOp ) )* ( OpenExpression | ExtendableExpr ) | <COLONCOLON> Expression )?
PrimitiveExp ::= ( String | Number | ( ( ( Identifier | ( <ProofStepLexeme> | <ProofImplicitStepLexeme> ) | InfixOp | PostfixOp | NonExpPrefixOp ) ( OpArgs )? ) ( BangExt )* ) )
BangExt ::= <BANG> ( ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) ( OpArgs )? | OpArgs | StructOp )
StructOp ::= ( <LAB> | <RAB> | <COLON> | Number | <IDENTIFIER> )
OpenStart ::= <CASE>
| <CHOOSE>
| <EXISTS>
| <FORALL>
| <IF>
| <LET>
| <T_EXISTS>
| <T_FORALL>