mingodad
commented
1 year ago And here is the EBNF output from https://www.bottlecaps.de/convert/ based on https://github.com/tlaplus/tlaplus/blob/master/tlatools/org.lamport.tlatools/javacc/tla%2B.jj (after removing \f form feed characters).
/* converted on Fri Jan 13, 2023, 09:28 (UTC+01) by javacc-to-w3c v0.62 which is Copyright (c) 2011-2022 by Gunther Rademacher <grd@gmx.net> */
PrefixOpToken
::= '\lnot'
| '\neg'
| '~'
| '[]'
| '<>'
| 'ENABLED'
| 'UNCHANGED'
| 'SUBSET'
| 'UNION'
| 'DOMAIN'
NEPrefixOpToken
::= '\lnot'
| '\neg'
| '~'
| '[]'
| '<>'
| '-.'
| 'ENABLED'
| 'UNCHANGED'
| 'SUBSET'
| 'UNION'
| 'DOMAIN'
InfixOpToken
::= '//'
| '/\'
| '/='
| '/'
| '\/'
| '\approx'
| '\asymp'
| '\bigcirc'
| '\bullet'
| '\cap'
| '\cdot'
| '\circ'
| '\cong'
| '\cup'
| '\div'
| '\doteq'
| '\equiv'
| '\geq'
| '\gg'
| '\in'
| '\intersect'
| '\union'
| '\land'
| '\leq'
| '\ll'
| '\lor'
| '\o'
| '\odot'
| '\ominus'
| '\oplus'
| '\oslash'
| '\otimes'
| '\prec'
| '\preceq'
| '\propto'
| '\sim'
| '\simeq'
| '\sqcap'
| '\sqcup'
| '\sqsubset'
| '\sqsupset'
| '\sqsubseteq'
| '\sqsupseteq'
| '\star'
| '\subset'
| '\subseteq'
| '\succ'
| '\succeq'
| '\supset'
| '\supseteq'
| '\uplus'
| '\wr'
| '\'
| '~>'
| '=>'
| '=<'
| '=|'
| '='
| '##'
| '#'
| '^^'
| '^'
| '--'
| '-|'
| '-+->'
| '-'
| '**'
| '*'
| '++'
| '+'
| '<=>'
| '<:'
| '<='
| '<'
| '>='
| '>'
| '...'
| '..'
| '||'
| '|'
| '|-'
| '|='
| '&&'
| '&'
| '$$'
| '$'
| '??'
| '%%'
| '%'
| '@@'
| '!!'
| ':>'
| ':='
| '::='
| '(+)'
| '(-)'
| '(.)'
| '(/)'
| '(\X)'
| '\notin'
| '\times'
| '\X'
PostfixOpToken
::= "'"
| '^+'
| '^*'
| '^#'
CompilationUnit
::= Prelude? Module
Prelude ::= '--->' ( NUMBER | IDENTIFIER )*
Module ::= BeginModule Extends Body EndModule
BeginModule
::= ( _BM0 | _BM1 | _BM2 ) Identifier SEPARATOR
EndModule
::= END_MODULE
Extends ::= ( 'EXTENDS' Identifier ( ',' Identifier )* )?
Body ::= ( SEPARATOR | VariableDeclaration | ParamDeclaration | OperatorOrFunctionDefinition | Recursive | Instance | Assumption | Theorem | Module | UseOrHideOrBy )*
VariableDeclaration
::= VARIABLE Identifier ( ',' Identifier )*
ParamDeclaration
::= ParamSubDecl ConstantDeclarationItems ( ',' ConstantDeclarationItems )*
ParamSubDecl
::= CONSTANT
Recursive
::= 'RECURSIVE' ConstantDeclarationItems ( ',' ConstantDeclarationItems )*
ConstantDeclarationItems
::= Identifier ( '(' '_' ( ',' '_' )* ')' )?
| NonExpPrefixOp '_'
| '_' ( InfixOp '_' | PostfixOp )
OperatorOrFunctionDefinition
::= 'LOCAL'? '-|-' ( ( Identifier '[' QuantBound ( ',' QuantBound )* ']' | PostfixLHS | InfixLHS | PrefixLHS ) '==' Expression | IdentLHS '==' ( Expression | Instantiation ) )
IdentifierTuple
::= '<<' ( Identifier ( ',' Identifier )* )? '>>'
IdentLHS ::= Identifier ( '(' ( IdentDecl | SomeFixDecl ) ( ',' ( IdentDecl | SomeFixDecl ) )* ')' )?
PrefixLHS
::= NEPrefixOpToken Identifier
InfixLHS ::= Identifier InfixOpToken Identifier
PostfixLHS
::= Identifier PostfixOpToken
IdentDecl
::= Identifier ( '(' '_' ( ',' '_' )* ')' )?
SomeFixDecl
::= NonExpPrefixOp '_'
| '_' ( InfixOp '_' | PostfixOp )
Instance ::= 'LOCAL'? Instantiation
Instantiation
::= 'INSTANCE' Identifier ( 'WITH' Substitution ( ',' Substitution )* )?
Substitution
::= ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) '<-' OpOrExpr
OldSubstitution
::= ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) '<-' ( '-.' | Expression | Lambda )
PrefixOp ::= PrefixOpToken
NonExpPrefixOp
::= NEPrefixOpToken
InfixOp ::= InfixOpToken
PostfixOp
::= PostfixOpToken
Identifier
::= IDENTIFIER
Assumption
::= ( ASSUMPTION | 'ASSUME' ) ( '-|-'? Identifier '==' )? Expression
AssumeProve
::= ( Identifier '::' AssumeProve )? ( 'ASSUME' | '[]ASSUME' ) ( AssumeProve | NewSymb | Expression ) ( ',' ( AssumeProve | NewSymb | Expression ) )* ( 'PROVE' | '[]PROVE' ) Expression
NewSymb ::= ( 'NEW' CONSTANT? | CONSTANT ) ( IdentDecl ( '\in' Expression )? | SomeFixDecl )
| 'NEW'? ( VARIABLE Identifier | ( 'STATE' | ACTION | TEMPORAL ) ( IdentDecl | SomeFixDecl ) )
MaybeBound
::= ( '\in' Expression )?
Theorem ::= ( 'THEOREM' | PROPOSITION ) ( Identifier '==' )? ( AssumeProve | Expression ) Proof?
Proof ::= UseOrHideOrBy
| 'PROOF'? ( 'OBVIOUS' | 'OMITTED' | Step* QEDStep )
UseOrHideOrBy
::= ( ( 'PROOF'? 'BY' | 'USE' ) 'ONLY'? | 'HIDE' ) ( ( 'MODULE' Identifier | Expression ) ( ',' ( 'MODULE' Identifier | Expression ) )* )? ( DF ( 'MODULE' Identifier | Expression ) ( ',' ( '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 ( ',' QuantBound )* | Identifier ( ',' Identifier )* )
WitnessStep
::= 'WITNESS' Expression ( ',' Expression )*
PickStep ::= 'PICK' ( Identifier ( ',' Identifier )* | QuantBound ( ',' QuantBound )* ) ':' Expression
CaseStep ::= 'CASE' Expression
AssertStep
::= 'SUFFICES'? ( Expression | AssumeProve )
GeneralId
::= IdPrefix Identifier
IdPrefix ::= IdPrefixElement*
IdPrefixElement
::= Identifier OpArgs? '!'
ParenthesesExpression
::= ParenExpr
| BraceCases
| SBracketCases
| SetExcept
| TupleOrAction
| FairnessExpr
ClosedExpressionOrOp
::= ElementaryExpression
| ParenthesesExpression
ClosedExpressionOnly
::= ClosedExpressionOrOp
OpenExpression
::= SomeQuant
| SomeTQuant
| IfThenElse
| Case
| LetIn
| UnboundOrBoundChoose
ElementaryExpression
::= ( Identifier OpArgs? '!' )* ( PrefixOp | InfixOp | PostfixOp | Identifier OpArgs? )
| String
| Number
String ::= STRING_LITERAL
Number ::= NUMBER_LITERAL ( '.' NUMBER_LITERAL )?
OpArgs ::= '(' OpSuite ( ',' OpSuite )* ')'
OpOrExpr ::= NonExpPrefixOp
| InfixOp
| PostfixOp
| Lambda
| Expression
OpSuite ::= OpOrExpr
ParenExpr
::= '(' Expression ')'
SomeQuant
::= ( EXISTS | FORALL ) ( Identifier ( ',' Identifier )* | QuantBound ( ',' QuantBound )* ) ':' Expression
SomeTQuant
::= ( '\EE' | '\AA' ) Identifier ( ',' Identifier )* ':' Expression
QuantBound
::= ( IdentifierTuple | Identifier ( ',' Identifier )* ) '\in' Expression
BraceCases
::= '{' ( ( IdentifierTuple | Identifier ) '\in' Expression ( ':' Expression | ( ',' Expression )* ) | Expression ( ( ',' Expression )* | ':' QuantBound ( ',' QuantBound )* ) )? '}'
SBracketCases
::= '[' ( ( QuantBound ( ',' QuantBound )* '|->' Expression | FieldVal ( ',' FieldVal )* | FieldSet ( ',' FieldSet )* ) ']' | Expression ( ( ( ',' Expression )* | '->' Expression | 'EXCEPT' ExceptSpec ( ',' ExceptSpec )* ) ']' | ']_' ReducedExpression ) )
FieldVal ::= Identifier '|->' Expression
FieldSet ::= Identifier ':' Expression
ExceptSpec
::= '!' ExceptComponent+ '=' Expression
ExceptComponent
::= '.' Identifier
| '[' Expression ( ',' Expression )* ']'
SetExcept
::= '{|' Expression 'EXCEPT' SExceptSpec ( ',' SExceptSpec )* '|}'
SExceptSpec
::= '!' ExceptComponent ( '=' | '\in' ) Expression
TupleOrAction
::= '<<' ( Expression ( ',' Expression )* )? ( '>>' | '>>_' ReducedExpression )
ReducedExpression
::= Identifier OpArgs? ( '!' Identifier OpArgs? )*
| ParenExpr
| BraceCases
| SBracketCases
| SetExcept
| TupleOrAction
FairnessExpr
::= ( 'WF_' | 'SF_' ) ReducedExpression ( '(' Expression ')' )?
IfThenElse
::= 'IF' Expression 'THEN' Expression 'ELSE' Expression
Case ::= 'CASE' CaseArm ( '[]' CaseArm )* ( '[]' OtherArm )?
CaseArm ::= Expression '->' Expression
OtherArm ::= 'OTHER' '->' Expression
LetIn ::= 'LET' LetDefinitions 'IN' Expression
LetDefinitions
::= ( OperatorOrFunctionDefinition | Recursive )+
Junctions
::= DisjList
| ConjList
DisjList ::= JuncItem+
ConjList ::= JuncItem+
JuncItem ::= ( '\/' | '/\' ) Expression
UnboundOrBoundChoose
::= 'CHOOSE' ( Identifier | IdentifierTuple ) MaybeBound ':' Expression
Lambda ::= 'LAMBDA' Identifier ( ',' Identifier )* ':' Expression
Expression
::= ( PrefixOp | InfixOp )* ( OpenExpression | ( Junctions | ParenthesesExpression | PrimitiveExp ) ( PostfixOp | '.' Identifier | SBracketCases )* ( InfixOp ( PrefixOp | InfixOp )* ( Junctions | ParenthesesExpression | PrimitiveExp ) ( PostfixOp | '.' Identifier | SBracketCases )* )* ( InfixOp ( PrefixOp | InfixOp )* OpenExpression | '::' Expression )? )
PrimitiveExp
::= String
| Number
| ( Identifier | ProofStepLexeme | ProofImplicitStepLexeme | InfixOp | PostfixOp | NonExpPrefixOp ) OpArgs? BangExt*
BangExt ::= '!' ( ( Identifier | NonExpPrefixOp | InfixOp | PostfixOp ) OpArgs? | OpArgs | StructOp )
StructOp ::= '<<'
| '>>'
| ':'
| Number
| IDENTIFIER
OpenStart
::= 'CASE'
| 'CHOOSE'
| EXISTS
| FORALL
| 'IF'
| 'LET'
| '\EE'
| '\AA'
<?TOKENS?>
BEGIN_MODULE
::= '----' '-'* ' '* 'MODULE'
_BM1 ::= BEGIN_MODULE
CASE0 ::= '_' ( LETTER | '_' | DIGIT )* LETTER ( LETTER | '_' | DIGIT )*
CASE1 ::= DIGIT ( LETTER | '_' | DIGIT )* LETTER ( LETTER | '_' | DIGIT )*
CASE1b ::= DIGIT ( LETTER | DIGIT )* '.\/'
CASE1c ::= DIGIT ( LETTER | DIGIT )* './\'
CASE2 ::= ( 'W' | 'S' ) ( ( [a-zA-EG-Z_] | DIGIT ) ( LETTER | '_' | DIGIT )* )?
CASE2b ::= ( 'W' | 'S' ) ( [a-zA-EG-Z] | DIGIT ) ( LETTER | DIGIT )* '.\/'
CASE2c ::= ( 'W' | 'S' ) ( [a-zA-EG-Z] | DIGIT ) ( LETTER | DIGIT )* './\'
CASE3 ::= ( 'WF' | 'SF' ) ( ( LETTER | DIGIT ) ( LETTER | '_' | DIGIT )* )?
CASE6 ::= [a-zA-RT-VX-Z] ( LETTER | '_' | DIGIT )*
CASE6b ::= [a-zA-RT-VX-Z] ( LETTER | DIGIT )* '.\/'
CASE6c ::= [a-zA-RT-VX-Z] ( LETTER | DIGIT )* './\'
CASEN ::= DIGIT+ LETTER ( LETTER | DIGIT | '_' )*
LETTER ::= [a-zA-Z]
DIGIT ::= [0-9]
NUMBER ::= DIGIT+
| '0'
_BM2 ::= BEGIN_MODULE
_BM0 ::= BEGIN_MODULE
SEPARATOR
::= '----' '-'*
END_MODULE
::= '====' '='*
ACTION ::= 'ACTION'
| 'ACTIONS'
ASSUMPTION
::= 'ASSUMPTION'
| 'AXIOM'
CONSTANT ::= 'CONSTANT'
| 'CONSTANTS'
EXISTS ::= '\E'
| '\exists'
FORALL ::= '\A'
| '\forall'
PROPOSITION
::= 'PROPOSITION'
| 'LEMMA'
| 'COROLLARY'
DF ::= 'DEF'
| 'DEFS'
TEMPORAL ::= 'TEMPORAL'
| 'TEMPORALS'
VARIABLE ::= 'VARIABLE'
| 'VARIABLES'
NUMBER_LITERAL
::= DIGIT+
| '0'
| '\' ( [oO] [0-7]+ | [bB] [0-1]+ | [hH] [0-9a-fA-F]+ )
STRING_LITERAL
::= '"' ( [^"`\#xA#xD] | '`' [^']* "'" | '\' [ntrf\"] )* '"'
BAND ::= CASE1c
| CASE2c
| CASE6c
BOR ::= CASE1b
| CASE2b
| CASE6b
IDENTIFIER
::= CASE0
| CASE1
| CASE2
| CASE3
| CASE6
| CASEN
| '@'
ProofStepLexeme
::= '<' DIGIT+ '>' ( LETTER | DIGIT | '_' )+
ProofImplicitStepLexeme
::= '<' ( '+' | '*' ) '>' ( LETTER | DIGIT )+
ProofStepDotLexeme
::= '<' ( DIGIT+ | '+' | '*' ) '>' ( LETTER | DIGIT | '_' )+ '.'+
BareLevelLexeme
::= '<' ( DIGIT+ | '+' | '*' ) '>'
UnnumberedStepLexeme
::= '<' ( DIGIT+ | '+' | '*' ) '>' ( '*' | '-' | '.' ) '.'*
ahelwer
Using this script https://github.com/mingodad/plgh/blob/main/json2ebnf.js (with quickjs) and with some manual fixes we can have a navigable railroad diagram.
Copy and paste the EBNF shown bellow on https://www.bottlecaps.de/rr/ui on the tab Edit Grammar the click on the tab View Diagram to see/download a navigable railroad diagram.