Alloy is a language for describing structures and a tool for exploring them. It has been used in a wide range of applications from finding holes in security mechanisms to designing telephone switching networks. This repository contains the code for the tool.
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"
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: