/* converted on Fri Jan 6, 2023, 16:50 (UTC+01) by antlr_4-to-w3c v0.62 which is Copyright (c) 2011-2022 by Gunther Rademacher <grd@gmx.net> */
program ::= topDecl* EOF
iden ::= Iden
int ::= IntLiteral
type ::= ( ( 'seq' | 'set' ) '[' | 'map' '[' type ',' ) type ']'
| '(' ( type ( ',' type )* | idenTypeList ) ')'
| 'bool'
| 'int'
| 'float'
| 'string'
| 'event'
| 'machine'
| 'data'
| 'any'
| iden
idenTypeList
::= idenType ( ',' idenType )*
idenType ::= iden ':' type
funParamList
::= funParam ( ',' funParam )*
funParam ::= iden ':' type
topDecl ::= typeDefDecl
| enumTypeDefDecl
| eventDecl
| eventSetDecl
| interfaceDecl
| implMachineDecl
| specMachineDecl
| funDecl
| namedModuleDecl
| testDecl
| implementationDecl
typeDefDecl
::= 'type' iden ( '=' type )? ';'
enumTypeDefDecl
::= 'enum' iden '{' ( enumElemList | numberedEnumElemList ) '}'
enumElemList
::= enumElem ( ',' enumElem )*
enumElem ::= iden
numberedEnumElemList
::= numberedEnumElem ( ',' numberedEnumElem )*
numberedEnumElem
::= iden '=' IntLiteral
eventDecl
::= 'event' iden cardinality? ( ':' type )? ';'
cardinality
::= ( 'assert' | 'assume' ) IntLiteral
eventSetDecl
::= 'eventset' iden '=' '{' eventSetLiteral '}' ';'
eventSetLiteral
::= nonDefaultEvent ( ',' nonDefaultEvent )*
interfaceDecl
::= 'interface' iden '(' type? ')' 'receives' nonDefaultEventList? ';'
implMachineDecl
::= 'machine' iden cardinality? receivesSends* machineBody
idenList ::= iden ( ',' iden )*
receivesSends
::= ( 'receives' | 'sends' ) eventSetLiteral? ';'
specMachineDecl
::= 'spec' iden 'observes' eventSetLiteral machineBody
machineBody
::= '{' machineEntry* '}'
machineEntry
::= varDecl
| funDecl
| stateDecl
varDecl ::= 'var' idenList ':' type ';'
funDecl ::= 'fun' iden '(' funParamList? ')' ( ':' type )? ( ( 'creates' iden )? ';' | functionBody )
stateDecl
::= 'start'? ( 'hot' | 'cold' )? 'state' iden '{' stateBodyItem* '}'
stateBodyItem
::= 'entry' ( anonEventHandler | iden ';' )
| 'exit' ( noParamAnonEventHandler | iden ';' )
| ( 'defer' | 'ignore' ) nonDefaultEventList ';'
| 'on' eventList ( 'do' ( iden ';' | anonEventHandler ) | 'goto' stateName ( ';' | 'with' ( anonEventHandler | iden ';' ) ) )
nonDefaultEventList
::= nonDefaultEvent ( ',' nonDefaultEvent )*
nonDefaultEvent
::= 'halt'
| iden
eventList
::= eventId ( ',' eventId )*
eventId ::= 'null'
| 'halt'
| iden
stateName
::= iden
functionBody
::= '{' varDecl* statement* '}'
statement
::= ( '{' statement* | 'receive' '{' recvCase+ ) '}'
| ( ( 'assert' ( expr ',' )? | 'print' ) expr | 'return' expr? | 'break' | 'continue' | 'new'? iden '(' rvalueList? ')' | ( ( 'raise' | 'send' expr ',' | 'announce' ) expr | 'goto' stateName ) ( ',' rvalueList )? | iden ( '.' ( iden | int ) | '[' expr ']' )* ( '=' rvalue | '-=' expr | '+=' '(' ( expr ',' )? rvalue ')' ) )? ';'
| ( ( 'while' '(' | 'foreach' '(' iden 'in' ) expr ')' | 'if' '(' expr ')' ( statement 'else' )? ) statement
recvCase ::= 'case' eventList ':' anonEventHandler
anonEventHandler
::= ( '(' funParam ')' )? functionBody
noParamAnonEventHandler
::= functionBody
expr ::= primitive
| ( '(' ( unnamedTupleBody | namedTupleBody | expr ) | ( 'keys' | 'values' | 'sizeof' ) '(' expr | 'default' '(' type | 'new'? iden '(' rvalueList? | 'choose' '(' expr? ) ')'
| expr ( '.' ( iden | int ) | '[' expr ']' | ( '*' | '/' | '%' | '+' | '-' | '<' | '>' | '>=' | '<=' | 'in' | '==' | '!=' | '&&' | '||' ) expr | ( 'as' | 'to' ) type )
| ( '-' | '!' ) expr
| formatedString
formatedString
::= StringLiteral
| 'format' '(' StringLiteral ( ',' rvalueList )? ')'
primitive
::= iden
| floatLiteral
| BoolLiteral
| IntLiteral
| 'null'
| '$'
| '$$'
| 'halt'
| 'this'
floatLiteral
::= IntLiteral? '.' IntLiteral
| 'float' '(' IntLiteral ',' IntLiteral ')'
unnamedTupleBody
::= rvalue ( ',' | ( ',' rvalue )+ )
namedTupleBody
::= iden '=' rvalue ( ',' | ( ',' iden '=' rvalue )+ )
rvalueList
::= rvalue ( ',' rvalue )*
rvalue ::= expr
modExpr ::= '(' modExpr ')'
| '{' bindExpr ( ',' bindExpr )* '}'
| iden
| ( ( 'compose' | 'union' ) ( modExpr ',' )+ | ( 'hidee' nonDefaultEventList | ( 'hidei' | 'assert' ) idenList | ( 'rename' iden 'to' | 'main' ) iden ) 'in' ) modExpr
bindExpr ::= iden ( '->' iden )?
namedModuleDecl
::= 'module' iden '=' modExpr ';'
testDecl ::= 'test' iden '[' 'main' '=' iden ']' ':' modExpr ( 'refines' modExpr )? ';'
implementationDecl
::= 'implementation' iden ( '[' 'main' '=' iden ']' )? ':' modExpr ';'
_ ::= Whitespace
| BlockComment
| LineComment
/* ws: definition */
<?TOKENS?>
BoolLiteral
::= 'true'
| 'false'
IntLiteral
::= [0-9]+
StringLiteral
::= '"' StringCharacters? '"'
StringCharacters
::= StringCharacter+
StringCharacter
::= [^"\]
| EscapeSequence
EscapeSequence
::= '\' .
Iden ::= PLetter PLetterOrDigit*
PLetter ::= [a-zA-Z_]
PLetterOrDigit
::= [a-zA-Z0-9_]
Whitespace
::= [ #x9#xd#xa#xc]+
BlockComment?
::= '/*' .* '*/'
LineComment
::= '//' [^#xd#xa]*
EOF ::= $
Using some online tools like https://www.bottlecaps.de/rr/ui and https://www.bottlecaps.de/convert/ with https://github.com/p-org/P/blob/master/Src/PCompiler/CompilerCore/Parser/PParser.g4 and https://github.com/p-org/P/blob/master/Src/PCompiler/CompilerCore/Parser/PLexer.g4 joined and commenting
//lexer grammar PLexer;we can have a nice navigable railroad diagram.Copy and paste the
EBNFshown bellow on https://www.bottlecaps.de/rr/ui on the tabEdit Grammarthe click on the tabView Diagramto see/download a navigable railroad diagram.