You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Using a script to convert (with some manual fixes) Alloy.cup to an EBNF understood by (IPV6) https://www.bottlecaps.de/rr/ui or (IPV4) https://rr.red-dove.com/ui to generate a nice navigable railroad diagram that can be used to document/develop/debug this project grammar.
Follow the instructions shown bellow at the top:
//
// EBNF to be viewd at
// (IPV6) https://www.bottlecaps.de/rr/ui
// (IPV4) https://rr.red-dove.com/ui
//
// Copy and paste this at one url shown above in the 'Edit Grammar' tab
// then click the 'View Diagram' tab.
//
File ::= Spec
Spec ::= Spec MODULE Name
Spec ::= Spec MODULE Name LBRACKET Namex RBRACKET
Spec ::= Spec Vis OPEN Name
Spec ::= Spec Vis OPEN Name AS Name
Spec ::= Spec Vis OPEN Name LBRACKET SigRefs RBRACKET
Spec ::= Spec Vis OPEN Name LBRACKET SigRefs RBRACKET AS Name
Spec ::= Spec Vis ENUM Name LBRACE Names RBRACE
Spec ::= Spec Vis ENUM Name LBRACE RBRACE
Spec ::= Spec FACT Super
Spec ::= Spec FACT Name Super
Spec ::= Spec FACT STR Super
Spec ::= Spec ASSERT Super
Spec ::= Spec ASSERT Name Super
Spec ::= Spec ASSERT STR Super
Spec ::= Spec Sig
Spec ::= Spec Function
Spec ::= Spec Predicate
Spec ::= Spec Macro
Spec ::= Spec Command
Spec ::=
CommandPrefix ::= CHECK
CommandPrefix ::= RUN
Command ::= CommandPrefix Name Super Scope Expects
Command ::= CommandPrefix Super Scope Expects
Command ::= Command IMPLIES CommandPrefix Name Super Scope Expects
Command ::= Command IMPLIES CommandPrefix Super Scope Expects
Command ::= CommandPrefix Name Name Scope Expects
Command ::= CommandPrefix Name Scope Expects
Command ::= Command IMPLIES CommandPrefix Name Name Scope Expects
Command ::= Command IMPLIES CommandPrefix Name Scope Expects
Expects ::=
Expects ::= EXPECT NUMBER
Scope ::= FOR NUMBER
Scope ::= FOR NUMBER BUT Typescopes
Scope ::= FOR Typescopes
Scope ::=
Typescopes ::= Typescope
Typescopes ::= Typescopes COMMA Typescope
Typescope ::= TypeNumber Name
//[AM] -> SIGINT
Typescope ::= TypeNumber SIGINT
Typescope ::= TypeNumber INT
Typescope ::= TypeNumber SEQ
Typescope ::= TypeNumber UNIV
Typescope ::= TypeNumber STRING
// [electrum] scope on Time
Typescope ::= TypeNumber TIME
//[AM] Typescope ::= TypeNumber SIGINT
Typescope ::= TypeNumber NONE
// [electrum] distinguish between "n" and "n..n" the latter become exact; open ended scopes "n.."
TypeNumber ::= EXACTLY NUMBER
TypeNumber ::= EXACTLY NUMBER DOT DOT NUMBER
TypeNumber ::= EXACTLY NUMBER DOT DOT
TypeNumber ::= EXACTLY NUMBER DOT DOT NUMBER COLON NUMBER
TypeNumber ::= EXACTLY NUMBER COLON NUMBER
TypeNumber ::= NUMBER
TypeNumber ::= NUMBER DOT DOT NUMBER
TypeNumber ::= NUMBER DOT DOT
TypeNumber ::= NUMBER DOT DOT NUMBER COLON NUMBER
TypeNumber ::= NUMBER COLON NUMBER
Macro ::= Vis LET Name LPAREN Names RPAREN MacroBody
Macro ::= Vis LET Name LPAREN RPAREN MacroBody
Macro ::= Vis LET Name LBRACKET Names RBRACKET MacroBody
Macro ::= Vis LET Name LBRACKET RBRACKET MacroBody
Macro ::= Vis LET Name MacroBody
MacroBody ::= Super
MacroBody ::= EQUALS Expr
Function ::= Vis FUN Name LPAREN Decls RPAREN COLON Expr Super
Function ::= Vis FUN Name LBRACKET Decls RBRACKET COLON Expr Super
Function ::= Vis FUN Name COLON Expr Super
Function ::= Vis FUN SigRef DOT Name LPAREN Decls RPAREN COLON Expr Super
Function ::= Vis FUN SigRef DOT Name LBRACKET Decls RBRACKET COLON Expr Super
Function ::= Vis FUN SigRef DOT Name COLON Expr Super
Predicate ::= Vis PRED Name LPAREN Decls RPAREN Super
Predicate ::= Vis PRED Name LBRACKET Decls RBRACKET Super
Predicate ::= Vis PRED Name Super
Predicate ::= Vis PRED SigRef DOT Name LPAREN Decls RPAREN Super
Predicate ::= Vis PRED SigRef DOT Name LBRACKET Decls RBRACKET Super
Predicate ::= Vis PRED SigRef DOT Name Super
Vis ::=
Vis ::= PRIVATE
Sig ::= SigQuals Names SigIn LBRACE Decls RBRACE SuperOpt
// [electrum] additional attribute for variable sigs
SigQual ::= ABSTRACT
SigQual ::= LONE
SigQual ::= ONE
SigQual ::= SOME
SigQual ::= PRIVATE
SigQual ::= VAR
SigQuals ::= SIG
SigQuals ::= SigQual SigQuals
SigIn ::= EXTENDS SigRef
SigIn ::= IN SigRefu
SigIn ::= EQUALS SigRefu
SigIn ::=
SigRef ::= Name
SigRef ::= UNIV
SigRef ::= STRING
SigRef ::= TIME
SigRef ::= SIGINT
SigRef ::= SEQ SLASH SIGINT
SigRef ::= NONE
SigRefs ::=
SigRefs ::= SigRefp
SigRefp ::= SigRef
SigRefp ::= SigRefp COMMA SigRef
SigRefu ::= SigRef
SigRefu ::= SigRefu PLUS SigRef
Name ::= NameHelper
Name ::= THIS SLASH NameHelper
Name ::= SEQ SLASH NameHelper
NameHelper ::= ID
NameHelper ::= NameHelper SLASH ID
Names ::= Name
Names ::= Names COMMA Name
Namex ::= Name
Namex ::= EXACTLY Name
Namex ::= Namex COMMA Name
Namex ::= Namex COMMA EXACTLY Name
// [electrum] additional parameter for variable declarations (for fields)
Decla ::= DISJ Names COLON Expr
Decla ::= PRIVATE DISJ Names COLON Expr
Decla ::= PRIVATE Names COLON Expr
Decla ::= Names COLON Expr
Decla ::= VAR DISJ Names COLON Expr
Decla ::= VAR PRIVATE DISJ Names COLON Expr
Decla ::= VAR PRIVATE Names COLON Expr
Decla ::= VAR Names COLON Expr
Decla ::= DISJ Names COLON DISJ Expr
Decla ::= PRIVATE DISJ Names COLON DISJ Expr
Decla ::= PRIVATE Names COLON DISJ Expr
Decla ::= Names COLON DISJ Expr
Decla ::= VAR DISJ Names COLON DISJ Expr
Decla ::= VAR PRIVATE DISJ Names COLON DISJ Expr
Decla ::= VAR PRIVATE Names COLON DISJ Expr
Decla ::= VAR Names COLON DISJ Expr
Declb ::= Decla
Declb ::= DISJ Names EQUALS Expr
Declb ::= PRIVATE DISJ Names EQUALS Expr
Declb ::= PRIVATE Names EQUALS Expr
Declb ::= Names EQUALS Expr
Declb ::= DISJ Names EQUALS DISJ Expr
Declb ::= PRIVATE DISJ Names EQUALS DISJ Expr
Declb ::= PRIVATE Names EQUALS DISJ Expr
Declb ::= Names EQUALS DISJ Expr
Declz ::= Declz COMMA Decla
Declz ::= Decla
Declp ::= Declp COMMA Declb
Declp ::= Declb
Decls ::=
Decls ::= Declb
Decls ::= Declb COMMA Decls
Decls ::= COMMA Decls
Let ::= Name EQUALS Expr SuperOrBar
Let ::= Name EQUALS Expr COMMA Let
// [electrum] temporal seq expressions have the lowest precedence
SuperOpt ::=
SuperOpt ::= Super
Super ::= LBRACE SuperP RBRACE
Super ::= LBRACE RBRACE
SuperP ::= Expr
SuperP ::= SuperP Expr
SuperP ::= Expr TRCSEQ SuperP
SuperOrBar ::= BAR ExprNoSeq
SuperOrBar ::= Super
SuperOrBar ::= BAR ExprNoSeq TRCSEQ Expr
Exprs ::=
Exprs ::= Exprp
Exprp ::= Expr
Exprp ::= Exprp COMMA Expr
//=============================================================================
Expr ::= ExprNoSeq
Expr ::= ExprNoSeq TRCSEQ Expr
ExprNoSeq ::= OrExprA
ExprNoSeq ::= OrExprB
ExprNoSeq ::= Bind
Bind ::= LET Let
Bind ::= ALL2 Declp SuperOrBar
Bind ::= NO2 Declp SuperOrBar
Bind ::= SOME2 Declp SuperOrBar
Bind ::= LONE2 Declp SuperOrBar
Bind ::= ONE2 Declp SuperOrBar
Bind ::= SUM2 Declp SuperOrBar
OrExprA ::= EquivExprA
OrExprA ::= OrExprB OR Bind
OrExprB ::= EquivExprB
OrExprB ::= OrExprB OR EquivExprB
EquivExprA ::= ImpliesExprA
EquivExprA ::= EquivExprB IFF Bind
EquivExprB ::= ImpliesExprB
EquivExprB ::= EquivExprB IFF ImpliesExprB
ImpliesExprA ::= ImpliesExprCloseA
ImpliesExprA ::= ImpliesExprOpenA
ImpliesExprCloseA ::= AndExprA
ImpliesExprCloseA ::= AndExprB IMPLIES ImpliesExprCloseB ELSE ImpliesExprCloseA
ImpliesExprOpenA ::= AndExprB IMPLIES ImpliesExprCloseB ELSE ImpliesExprOpenA
ImpliesExprOpenA ::= AndExprB IMPLIES ImpliesExprA
ImpliesExprCloseA ::= AndExprB IMPLIES ImpliesExprCloseB ELSE Bind
ImpliesExprOpenA ::= AndExprB IMPLIES Bind
ImpliesExprB ::= ImpliesExprCloseB
ImpliesExprB ::= ImpliesExprOpenB
ImpliesExprCloseB ::= AndExprB
ImpliesExprCloseB ::= AndExprB IMPLIES ImpliesExprCloseB ELSE ImpliesExprCloseB
ImpliesExprOpenB ::= AndExprB IMPLIES ImpliesExprCloseB ELSE ImpliesExprOpenB
ImpliesExprOpenB ::= AndExprB IMPLIES ImpliesExprB
AndExprA ::= TempBinaryA
AndExprA ::= AndExprB AND Bind
AndExprB ::= TempBinaryB
AndExprB ::= AndExprB AND TempBinaryB
// [electrum] binary temporal formulas highest precedence among binary operators
TempBinaryA ::= UnaryExprA
TempBinaryA ::= TempBinaryB UNTIL Bind
TempBinaryA ::= TempBinaryB SINCE Bind
TempBinaryA ::= TempBinaryB TRIGGERED Bind
TempBinaryA ::= TempBinaryB RELEASES Bind
TempBinaryB ::= UnaryExprB
TempBinaryB ::= TempBinaryB UNTIL UnaryExprB
TempBinaryB ::= TempBinaryB SINCE UnaryExprB
TempBinaryB ::= TempBinaryB RELEASES UnaryExprB
TempBinaryB ::= TempBinaryB TRIGGERED UnaryExprB
// [electrum] unary temporal formulas same precedence as other unary operators
UnaryExprA ::= CompareExprA
UnaryExprA ::= NOT Bind
UnaryExprA ::= NOT UnaryExprA
UnaryExprA ::= ALWAYS Bind
UnaryExprA ::= ALWAYS UnaryExprA
UnaryExprA ::= EVENTUALLY Bind
UnaryExprA ::= EVENTUALLY UnaryExprA
UnaryExprA ::= AFTER Bind
UnaryExprA ::= AFTER UnaryExprA
UnaryExprA ::= HISTORICALLY Bind
UnaryExprA ::= HISTORICALLY UnaryExprA
UnaryExprA ::= ONCE Bind
UnaryExprA ::= ONCE UnaryExprA
UnaryExprA ::= BEFORE Bind
UnaryExprA ::= BEFORE UnaryExprA
UnaryExprB ::= CompareExprB
UnaryExprB ::= NOT UnaryExprB
UnaryExprB ::= ALWAYS UnaryExprB
UnaryExprB ::= EVENTUALLY UnaryExprB
UnaryExprB ::= AFTER UnaryExprB
UnaryExprB ::= HISTORICALLY UnaryExprB
UnaryExprB ::= ONCE UnaryExprB
UnaryExprB ::= BEFORE UnaryExprB
CompareExprA ::= CompareExprB IN ShiftExprA
CompareExprA ::= CompareExprB EQUALS ShiftExprA
CompareExprA ::= CompareExprB LT ShiftExprA
CompareExprA ::= CompareExprB GT ShiftExprA
CompareExprA ::= CompareExprB LTE ShiftExprA
CompareExprA ::= CompareExprB GTE ShiftExprA
CompareExprA ::= CompareExprB NOTIN ShiftExprA
CompareExprA ::= CompareExprB NOTEQUALS ShiftExprA
CompareExprA ::= CompareExprB NOTLT ShiftExprA
CompareExprA ::= CompareExprB NOTGT ShiftExprA
CompareExprA ::= CompareExprB NOTLTE ShiftExprA
CompareExprA ::= CompareExprB NOTGTE ShiftExprA
CompareExprA ::= ALL ShiftExprA
CompareExprA ::= NO ShiftExprA
CompareExprA ::= SOME ShiftExprA
CompareExprA ::= LONE ShiftExprA
CompareExprA ::= ONE ShiftExprA
CompareExprA ::= SET ShiftExprA
CompareExprA ::= SEQ ShiftExprA
CompareExprA ::= ShiftExprA
CompareExprB ::= CompareExprB IN ShiftExprB
CompareExprB ::= CompareExprB EQUALS ShiftExprB
CompareExprB ::= CompareExprB LT ShiftExprB
CompareExprB ::= CompareExprB GT ShiftExprB
CompareExprB ::= CompareExprB LTE ShiftExprB
CompareExprB ::= CompareExprB GTE ShiftExprB
CompareExprB ::= CompareExprB NOTIN ShiftExprB
CompareExprB ::= CompareExprB NOTEQUALS ShiftExprB
CompareExprB ::= CompareExprB NOTLT ShiftExprB
CompareExprB ::= CompareExprB NOTGT ShiftExprB
CompareExprB ::= CompareExprB NOTLTE ShiftExprB
CompareExprB ::= CompareExprB NOTGTE ShiftExprB
CompareExprB ::= ALL ShiftExprB
CompareExprB ::= NO ShiftExprB
CompareExprB ::= SOME ShiftExprB
CompareExprB ::= LONE ShiftExprB
CompareExprB ::= ONE ShiftExprB
CompareExprB ::= SET ShiftExprB
CompareExprB ::= SEQ ShiftExprB
CompareExprB ::= ShiftExprB
ShiftExprA ::= UnionDiffExprA
ShiftExprA ::= ShiftExprB SHL Bind
ShiftExprA ::= ShiftExprB SHR Bind
ShiftExprA ::= ShiftExprB SHA Bind
ShiftExprB ::= UnionDiffExprB
ShiftExprB ::= ShiftExprB SHL UnionDiffExprB
ShiftExprB ::= ShiftExprB SHR UnionDiffExprB
ShiftExprB ::= ShiftExprB SHA UnionDiffExprB
UnionDiffExprA ::= MulExprA
UnionDiffExprA ::= UnionDiffExprB PLUS Bind
UnionDiffExprA ::= UnionDiffExprB MINUS Bind
UnionDiffExprA ::= UnionDiffExprB INTADD Bind
UnionDiffExprA ::= UnionDiffExprB INTSUB Bind
UnionDiffExprB ::= MulExprB
UnionDiffExprB ::= UnionDiffExprB PLUS MulExprB
UnionDiffExprB ::= UnionDiffExprB MINUS MulExprB
UnionDiffExprB ::= UnionDiffExprB INTADD MulExprB
UnionDiffExprB ::= UnionDiffExprB INTSUB MulExprB
MulExprA ::= NumUnopExprA
MulExprA ::= MulExprB INTMUL Bind
MulExprA ::= MulExprB INTDIV Bind
MulExprA ::= MulExprB INTREM Bind
MulExprB ::= NumUnopExprB
MulExprB ::= MulExprB INTMUL NumUnopExprB
MulExprB ::= MulExprB INTDIV NumUnopExprB
MulExprB ::= MulExprB INTREM NumUnopExprB
NumUnopExprA ::= OverrideExprA
NumUnopExprA ::= HASH Bind
NumUnopExprA ::= SUM Bind
//[AM]->SIGINT
NumUnopExprA ::= INT Bind
NumUnopExprA ::= HASH NumUnopExprA
NumUnopExprA ::= SUM NumUnopExprA
//[AM]->SIGINT
NumUnopExprA ::= INT NumUnopExprA
NumUnopExprB ::= OverrideExprB
NumUnopExprB ::= HASH NumUnopExprB
NumUnopExprB ::= SUM NumUnopExprB
//[AM]->SIGINT
NumUnopExprB ::= INT NumUnopExprB
OverrideExprA ::= IntersectExprA
OverrideExprA ::= OverrideExprB PLUSPLUS Bind
OverrideExprB ::= IntersectExprB
OverrideExprB ::= OverrideExprB PLUSPLUS IntersectExprB
IntersectExprA ::= RelationExprA
IntersectExprA ::= IntersectExprB AMPERSAND Bind
IntersectExprB ::= RelationExprB
IntersectExprB ::= IntersectExprB AMPERSAND RelationExprB
RelOp ::= ARROW
RelOp ::= ANY_ARROW_SOME
RelOp ::= ANY_ARROW_ONE
RelOp ::= ANY_ARROW_LONE
RelOp ::= SOME_ARROW_ANY
RelOp ::= SOME_ARROW_SOME
RelOp ::= SOME_ARROW_ONE
RelOp ::= SOME_ARROW_LONE
RelOp ::= ONE_ARROW_ANY
RelOp ::= ONE_ARROW_SOME
RelOp ::= ONE_ARROW_ONE
RelOp ::= ONE_ARROW_LONE
RelOp ::= LONE_ARROW_ANY
RelOp ::= LONE_ARROW_SOME
RelOp ::= LONE_ARROW_ONE
RelOp ::= LONE_ARROW_LONE
RelationExprA ::= DomainExprA
RelationExprA ::= DomainExprB RelOp Bind
RelationExprB ::= DomainExprB
RelationExprB ::= DomainExprB RelOp RelationExprB
DomainExprA ::= RangeExprA
DomainExprA ::= DomainExprB DOMAIN Bind
DomainExprB ::= RangeExprB
DomainExprB ::= DomainExprB DOMAIN RangeExprB
RangeExprA ::= BracketExprA
RangeExprA ::= RangeExprB RANGE Bind
RangeExprB ::= BracketExprB
RangeExprB ::= RangeExprB RANGE BracketExprB
BracketExprA ::= DotExprA
BracketExprB ::= DotExprB
BracketExprB ::= BracketExprB LBRACKET Exprs RBRACKET
BracketExprB ::= DISJ LBRACKET Exprs RBRACKET
BracketExprB ::= TOTALORDER LBRACKET Exprs RBRACKET
//[AM]->SIGINT
BracketExprB ::= INT LBRACKET Exprs RBRACKET
BracketExprB ::= SUM LBRACKET Exprs RBRACKET
DotExprA ::= UnopExprA
DotExprA ::= BracketExprB DOT Bind
DotExprB ::= UnopExprB
DotExprB ::= BracketExprB DOT UnopExprB
DotExprB ::= BracketExprB DOT DISJ
DotExprB ::= BracketExprB DOT TOTALORDER
//[AM]->SIGINT
DotExprB ::= BracketExprB DOT INT
DotExprB ::= BracketExprB DOT SUM
// [electrum] unary temporal expressions same precedence as other unary operators
UnopExprA ::= TILDE Bind
UnopExprA ::= STAR Bind
UnopExprA ::= CARET Bind
UnopExprA ::= TILDE UnopExprA
UnopExprA ::= STAR UnopExprA
UnopExprA ::= CARET UnopExprA
UnopExprB ::= BaseExpr
UnopExprB ::= TILDE UnopExprB
UnopExprB ::= STAR UnopExprB
UnopExprB ::= CARET UnopExprB
UnopExprA ::= Bind PRIME
UnopExprA ::= UnopExprA PRIME
UnopExprB ::= UnopExprB PRIME
BaseExpr ::= NUMBER
BaseExpr ::= STR
BaseExpr ::= IDEN
BaseExpr ::= THIS
BaseExpr ::= INTMIN
BaseExpr ::= INTMAX
BaseExpr ::= INTNEXT
BaseExpr ::= LPAREN Expr RPAREN
BaseExpr ::= SigRef
BaseExpr ::= AT Name
BaseExpr ::= Super
BaseExpr ::= LBRACE Declz SuperOrBar RBRACE
BaseExpr ::= LBRACE Declz RBRACE
//Tokens
//ch\.put(CompSym\.\([^,]+\), \("[^"]+"\));
ARROW ::= "->"
ANY_ARROW_SOME ::= "->"
ANY_ARROW_ONE ::= "->"
ANY_ARROW_LONE ::= "->"
SOME_ARROW_ANY ::= "some"
SOME_ARROW_SOME ::= "some"
SOME_ARROW_ONE ::= "some"
SOME_ARROW_LONE ::= "some"
ONE_ARROW_ANY ::= "one"
ONE_ARROW_SOME ::= "one"
ONE_ARROW_ONE ::= "one"
ONE_ARROW_LONE ::= "one"
LONE_ARROW_ANY ::= "lone"
LONE_ARROW_SOME ::= "lone"
LONE_ARROW_ONE ::= "lone"
LONE_ARROW_LONE ::= "lone"
INTADD ::= "fun"
INTSUB ::= "fun"
INTMUL ::= "fun"
INTDIV ::= "fun"
INTREM ::= "fun"
INTMIN ::= "fun"
INTMAX ::= "fun"
INTNEXT ::= "fun"
TOTALORDER ::= "pred"
ABSTRACT ::= "abstract"
ALL ::= "all"
ALL2 ::= "all"
AMPERSAND ::= "&"
AND ::= "&&"
AS ::= "as"
ASSERT ::= "assert"
AT ::= "@"
BAR ::= "|"
BUT ::= "but"
CARET ::= "^"
CHECK ::= "check"
COLON ::= ":"
COMMA ::= ", "
DISJ ::= "disj"
DOMAIN ::= "<:"
DOT ::= "."
ELSE ::= "else"
ENUM ::= "enum"
EQUALS ::= "="
EXACTLY ::= "exactly"
EXPECT ::= "expect"
EXTENDS ::= "extends"
FACT ::= "fact"
FOR ::= "for"
FUN ::= "fun"
GT ::= ">"
GTE ::= ">="
HASH ::= "#"
IDEN ::= "iden"
IFF ::= "iff"
IMPLIES ::= "=>"
IN ::= "in"
INT ::= "int"
LBRACE ::= "{"
LBRACKET ::= "["
LET ::= "let"
LONE2 ::= "lone"
LONE ::= "lone"
LPAREN ::= "("
LT ::= "<"
LTE ::= "<="
MINUS ::= "-"
MODULE ::= "module"
NO2 ::= "no"
NO ::= "no"
NONE ::= "none"
NOT ::= "!"
NOTEQUALS ::= "!"
NOTGT ::= "!"
NOTGTE ::= "!"
NOTIN ::= "!"
NOTLT ::= "!"
NOTLTE ::= "!"
ONE2 ::= "one"
ONE ::= "one"
OPEN ::= "open"
OR ::= "||"
PLUS ::= "+"
PLUSPLUS ::= "++"
PRED ::= "pred"
PRIVATE ::= "private"
RANGE ::= ":>"
RBRACE ::= "}"
RBRACKET ::= "]"
RPAREN ::= ")"
RUN ::= "run"
SEQ ::= "seq"
SET ::= "set"
SHL ::= "<<"
SHR ::= ">>>"
SHA ::= ">>"
SIG ::= "sig"
SIGINT ::= "Int"
SLASH ::= "/"
SOME2 ::= "some"
SOME ::= "some"
STAR ::= "*"
STRING ::= "String"
SUM2 ::= "sum"
SUM ::= "sum"
THIS ::= "this"
TILDE ::= "~"
UNIV ::= "univ"
ID ::= "NAME"
NUMBER ::= "NUMBER"
STR ::= "STRING"
VAR ::= "var"
ALWAYS ::= "always"
EVENTUALLY ::= "eventually"
AFTER ::= "after"
BEFORE ::= "before"
HISTORICALLY ::= "historically"
ONCE ::= "once"
RELEASES ::= "releases"
UNTIL ::= "until"
SINCE ::= "since"
TRIGGERED ::= "triggered"
TRCSEQ ::= ";"
PRIME ::= "'"
TIME ::= "steps"
The text was updated successfully, but these errors were encountered:
Using a script to convert (with some manual fixes)
Alloy.cup
to anEBNF
understood by (IPV6) https://www.bottlecaps.de/rr/ui or (IPV4) https://rr.red-dove.com/ui to generate a nice navigable railroad diagram that can be used to document/develop/debug this project grammar.Follow the instructions shown bellow at the top:
The text was updated successfully, but these errors were encountered: