Grammar railroad diagram

[mingodad]

Using an experimental extesnion to peg/leg to convert the grammar to an EBNF understood by https://www.bottlecaps.de/rr/ui and manually fixing small errors we can have nice railroad diagram (https://en.wikipedia.org/wiki/Syntax_diagram) to help show/understand the syntax.

Copy and paste the EBNF shown bellow at https://www.bottlecaps.de/rr/ui on the tab Edit Grammar then click on the tab View Diagram.

ProtoconFile ::= ( WS? ( Protocol WS? )? ( ConstDecl WS? )* ( ( ( VarDecl WS? )+ ) | ( [^;]+ END_STMT? ) ) ( ( NamedPredicate | GlobalAssume | GlobalLegit | GlobalLegitBehav | ProcDecl | ( . .* ) ) WS? )* END_OF_FILE )
WS ::= ( ( WHITE_SPACE | LINE_COMMENT )+ )
Protocol ::= ( "protocol" WS ID END_STMT )
ConstDecl ::= ( "constant" WS ID DEFEQ ( ( ConstIntExpr ) | ( ConstIntList ) ) END_STMT )
VarDecl ::= ( OptionalShadowPuppetRole "variable" WS ID "[" WS? ( NatDom | ( ConstIntExpr ) ) WS? "]" WS? InNatDom END_STMT )
END_STMT ::= ( WS? ";" )
NamedPredicate ::= ( "predicate" WS ID DEFEQ Expr END_STMT )
GlobalAssume ::= ( "(" WS? ASSUME_AND_CLOSED WS? ")" WS? "(" WS? Expr WS? ")" END_STMT )
GlobalLegit ::= ( LegitStmt )
GlobalLegitBehav ::= ( ( ( FUTURE_SILENT ) | ( FUTURE_ACTIVE_SHADOW ) ) END_STMT )
ProcDecl ::= ( NOP NOP "process" WS ID "[" WS? ID WS? ( ( IN WS? "map" WS ID WS? "<" WS? ConstIntExpr SUCH_THAT IntExpr ) | InNatDom ) WS? "]" WS? "{" WS? ( "let" WS ID DEFEQ Expr END_STMT WS? )* ( ( ( VblAccessType WS? VblARef WS? ( "," WS? VblARef WS? )* END_STMT WS? ) | ( SymmetricLinks WS? ) )+ | ( [^;]+ END_STMT? WS? ) ) ( ( ProcNamedPredicate | ProcAssume | ProcLegit | ShadowActionDef | DirectActionDef | PuppetActionDef | PermitActionDef | ForbidActionDef | ConflictActionDef | ( [^};]+ END_STMT? ) ) WS? )* "}" )
END_OF_FILE ::= NOT_ .
ID ::= ( [A-Za-z] [0-9A-Za-z_]* )
DEFEQ ::= ( WS? ":=" WS? )
ConstIntExpr ::= ( ConstSum )
ConstIntList ::= ( "(" WS? ConstIntExpr WS? ( "," WS? ConstIntExpr WS? )* ")" )
OptionalShadowPuppetRole ::= ( ( ( SHADOW WS ) | ( PUPPET WS ) | ( DIRECT WS ) | ( "underlying" WS ) )? )
SHADOW ::= "shadow"
PUPPET ::= ( "puppet" | "superposed" )
DIRECT ::= "direct"
NatDom ::= ( ( "Int" | "Nat" ) WS? "%" WS? ConstValue )
InNatDom ::= ( ( IN WS? NatDom ) | ( "<" WS? ConstIntExpr ) )
ActionExpr ::= ( "(" WS? Expr WS? ( ( "-->" ) | ( "-=>" ) ) WS? ( ( ( VblARef DEFEQ ( ( WILD ) | ( Expr ) ) ) | ( VblARef ) | ( WILD DEFEQ WILD ) | ( WILD ) ) END_STMT WS? )* ")" )
Expr ::= ( ( Quantify ) | ( IfThenElse ) | ( BiImplication ) | ( [^)}#x5D;]+ ) )
VblARef ::= ( ID "[" WS? Expr WS? "]" )
WILD ::= ( "_" )
ShadowActionDef ::= ( ( SHADOW | "underlying" ) ( ( WS ACTION ) | ":" ) WS? ( ActionExpr WS? ( "," WS? )? )* END_STMT )
ACTION ::= ( "act:" | "action:" )
DirectActionDef ::= ( ( ( ( DIRECT WS )? ACTION ) | ( DIRECT ":" ) ) WS? ( ActionExpr WS? ( "," WS? )? )* END_STMT )
PuppetActionDef ::= ( PUPPET ( ( WS ACTION ) | ":" ) WS? ( ActionExpr WS? ( "," WS? )? )* END_STMT )
PermitActionDef ::= ( "permit" ( ( WS ACTION ) | ":" ) WS? ( ActionExpr WS? ( "," WS? )? )* END_STMT )
ForbidActionDef ::= ( "forbid" ( ( WS ACTION ) | ":" ) WS? ( ActionExpr WS? ( "," WS? )? )* END_STMT )
ConflictActionDef ::= ( "conflict:" WS? ( ActionExpr WS? ( "," WS? )? )* END_STMT )
ProcNamedPredicate ::= ( "predicate" WS ID DEFEQ Expr END_STMT )
ProcAssume ::= ( "(" WS? ASSUME_AND_CLOSED WS? ")" WS? "(" WS? Expr WS? ")" END_STMT )
ASSUME_AND_CLOSED ::= ( ( ASSUME ANDPOS CLOSED ) | ( CLOSED ANDPOS ASSUME ) )
ProcLegit ::= ( LegitStmt )
LegitStmt ::= ( "(" WS? LegitMode WS? ")" WS? "(" WS? Expr WS? ")" END_STMT )
NOP ::=
IN ::= "<-"
SUCH_THAT ::= ( WS? ":" WS? )
IntExpr ::= ( Sum )
VblAccessType ::= ( ( "read:" ) | ( "write:" ) | ( "yield:" ) | ( "effect:" ) | ( RANDOM WS "read:" ) | ( RANDOM WS "write:" ) )
SymmetricLinks ::= ( "symmetric" WS ( ( ID WS? IN WS? "{#" WS? Expr WS? ( "," WS? Expr WS? )* ) | ( "(" ID WS? ( "," WS? ID WS? )* ")" WS? IN WS? "{#" WS? ValueList WS? ( "," WS? ValueList WS? )* ) ) "#}" WS? "{" WS? ( VblAccessType WS? VblARef WS? ( "," WS? VblARef WS? )* END_STMT WS? )+ "}" )
RANDOM ::= "random"
ValueList ::= ( "(" WS? Expr WS? ( "," WS? Expr WS? )* ")" )
LegitMode ::= ( ( FUTURE_AND_SILENT ) | ( FUTURE_AND_SHADOW ) | ( FUTURE_AND_CLOSED ) | ( FUTURE_AND_ACTIVE_SHADOW ) | ( FUTURE_AND_SILENT_MOD_PUPPET ) | ( FUTURE_AND_SHADOW_MOD_PUPPET ) | ( FUTURE_AND_ACTIVE_SHADOW_MOD_PUPPET ) | ( FUTURE_AND_FUTURE_SILENT ) | ( FUTURE_AND_FUTURE_SHADOW ) | ( FUTURE_AND_FUTURE_ACTIVE_SHADOW ) | ( FUTURE_AND_SILENT ) )
FUTURE_AND_SILENT ::= ( ( FUTURE ANDPOS SILENT ) | ( SILENT ANDPOS FUTURE ) )
FUTURE_AND_SHADOW ::= ( ( FUTURE ANDPOS SHADOW ) | ( SHADOW ANDPOS FUTURE ) )
FUTURE_AND_CLOSED ::= ( ( FUTURE ANDPOS CLOSED ) | ( CLOSED ANDPOS FUTURE ) )
FUTURE_AND_ACTIVE_SHADOW ::= ( ( FUTURE ANDPOS ACTIVE_SHADOW ) | ( ACTIVE_SHADOW ANDPOS FUTURE ) )
FUTURE_AND_SILENT_MOD_PUPPET ::= ( "(" WS? FUTURE_AND_SILENT WS? ")" WS? MOD_PUPPET )
FUTURE_AND_SHADOW_MOD_PUPPET ::= ( "(" WS? FUTURE_AND_SHADOW WS? ")" WS? MOD_PUPPET )
FUTURE_AND_ACTIVE_SHADOW_MOD_PUPPET ::= ( "(" WS? FUTURE_AND_ACTIVE_SHADOW WS? ")" WS? MOD_PUPPET )
FUTURE_AND_FUTURE_SILENT ::= ( ( FUTURE ANDPOS FUTURE_SILENT ) | ( FUTURE_SILENT ANDPOS FUTURE ) )
FUTURE_AND_FUTURE_SHADOW ::= ( ( FUTURE ANDPOS FUTURE_SHADOW ) | ( FUTURE_SHADOW ANDPOS FUTURE ) )
FUTURE_AND_FUTURE_ACTIVE_SHADOW ::= ( ( FUTURE ANDPOS FUTURE_ACTIVE_SHADOW ) | ( FUTURE_ACTIVE_SHADOW ANDPOS FUTURE ) )
FUTURE_SILENT ::= ( FUTURE WS SILENT )
FUTURE_ACTIVE_SHADOW ::= ( FUTURE WS ACTIVE_SHADOW )
ConstSum ::= ( ConstProduct ( WS? NOP ( ( "+" ) | ( "-" ) ) WS? ConstProduct )* )
ConstProduct ::= ( ConstNeg ( WS? NOP ( ( "*" ) | ( "/" ) | ( "%" ) ) WS? ConstNeg )* )
ConstNeg ::= ( OptionalArithNeg ConstPower )
OptionalArithNeg ::= ( ( "-" WS? )? )
ConstPower ::= ( ConstIntFuncall ( WS? "^" WS? ConstNeg )* )
ConstIntFuncall ::= ( ( NOP ( ( "max" ) | ( "min" ) ) WS? "(" WS? ConstIntExpr WS? "," WS? ConstIntExpr WS? ")" ) | ( ConstValue ) )
ConstValue ::= ( ( NAT ) | ( ID ) | ( "(" WS? ConstIntExpr WS? ")" ) )
NAT ::= ( [0-9]+ )
Quantify ::= ( NOP ( ( "forall" ) | ( "exists" ) | ( "unique" ) ) WS ID WS? InNatDom SUCH_THAT Expr )
IfThenElse ::= ( "if" WS Expr WS "then" WS Expr WS "else" WS Expr )
BiImplication ::= ( Implication ( WS? "<=>" WS? Implication )* )
Implication ::= ( Disjunction ( WS? "==>" WS? Disjunction )* )
Disjunction ::= ( Conjunction ( WS? "||" WS? Conjunction )* )
Conjunction ::= ( ChainlessFormula ( WS? "&&" WS? ChainlessFormula )* )
ChainlessFormula ::= ( ( Quantify ) | ( Comparison ) )
Comparison ::= ( IntExpr ( WS? NOP ( ( "==" ) | ( "!=" ) | ( "<=" ) | ( ">=" ) | ( "<" ) | ( ">" ) ) WS? IntExpr )? )
Sum ::= ( Product ( WS? NOP ( ( "+" ) | ( "-" ) ) WS? Product )* )
Product ::= ( Neg ( WS? NOP ( ( "*" ) | ( "/" ) | ( "%" ) ) WS? Neg )* )
Neg ::= ( OptionalNeg Power )
OptionalNeg ::= ( ( NOP ( ( "-" ) | ( "!" ) ) WS? )? )
Power ::= ( IntFuncall ( WS? "^" WS? Neg )* )
IntFuncall ::= ( ( NOP ( ( "max" ) | ( "min" ) ) WS? "(" WS? IntExpr WS? "," WS? IntExpr WS? ")" ) | ( Value ) )
Value ::= ( ( VblARef ) | ( ID ) | ( NAT ) | ( "(" WS? Expr WS? ")" ) )
ANDPOS ::= ( WS? "&" WS? )
FUTURE ::= ( "future" | "eventually" | "<>" )
CLOSED ::= "closed"
ASSUME ::= "assume"
SILENT ::= "silent"
ACTIVE ::= "active"
ACTIVE_SHADOW ::= ( ACTIVE WS SHADOW )
MOD_PUPPET ::= ( "%" WS? PUPPET )
FUTURE_SHADOW ::= ( FUTURE WS SHADOW )
FUTURE_AND_CLOSED_AND_FUTURE_SILENT ::= ( ( FUTURE_AND_CLOSED ANDPOS FUTURE_SILENT ) | ( FUTURE_AND_FUTURE_SILENT ANDPOS CLOSED ) | ( FUTURE_SILENT ANDPOS FUTURE_AND_CLOSED ) | ( CLOSED ANDPOS FUTURE_AND_FUTURE_SILENT ) )
LINE_COMMENT ::= ( "//" [^\n]* [\n] )
WHITE_SPACE ::= ( [ \t\r] | ( [\n] ) )+

[grencez]

Very cool, thanks! Were the small errors due to problems in the grammar itself?

Feel free to send a PR. Otherwise, I'll add this as doc/grammar.html with inline SVGs later today.

[grencez]

Ooh I see. The blank space chars should be converted to [#x20#x9#xA#xD].

After trying this out on a branch, I realize that GitHub doesn't automatically render the html unless it's viewed from GitHub pages. But the docs are best not viewed on GitHub Pages because they link to a bunch of example files directly (which GH Pages would provide as a download rather than a preview).

Anyway, cool idea. Think I'll instead just put the EBNF in a markdown file and hint that a curious reader can let bottlecaps load it. Direct linking like https://www.bottlecaps.de/rr/ui?uri=https://github.com/grencez/protocon/blob/ebnf/doc/grammar.md might work too, but it's probably bad netiquette.

[mingodad]

I just created a repository with all my changes to peg/leg here https://github.com/mingodad/peg with it I generated the basic EBNF with this command:

leg -e prot-xfile.leg

[grencez]

Thanks for sharing. Any of those changes worth upstreaming? Ian was pretty responsive when I sent him a patch, but it's been quite a while.

[mingodad]

I'll send him a propose, thank you !