Grammar railroad diagram

[mingodad]

Hello !

I've done some work to convert bison grammars to EBNF understood by https://www.bottlecaps.de/rr/ui and applying it to this project mu.y and with a bit of manual fixes I've got the EBNF shown bellow, copy and paste it on the tab Edit Grammar at https://www.bottlecaps.de/rr/ui then switch to the tab View Diagram.

I hope it'll help potential users to understand Murphi language !

Cheers !

/*************************************************************
 * The structure of this file is loosely a depth-first preorder
 * traversal of the tree of the grammar.
 /*/

/* The whole thing. /*/
prog		::=
		  decls
 		  procDecls
		  rules



/* general strongly-typed declarations. /*/
decls		::= decls decl
                | /* empty /*/


/* A single declaration. /*/
decl		::= CONST constDecls
		| TYPE typeDecls
		| VAR varDecls


/* constant declarations. /*/
constDecls	::= constDecls constDecl semi
		| /* empty /*/


/* an optional semicolon. /*/
/* BUG:  please decide whether to have empty or not /*/
semi		::= ';'
/*		| /* empty /*/


/* a single constant declaration. /*/
constDecl	::= ID ':' expr



/* type declarations. /*/
typeDecls	::= typeDecls typeDecl semi
		| /* empty /*/


/* a single type declaration. /*/
typeDecl	::= ID ':' typeExpr



/* a type expression, using the default $$ = $1 action. /*/
typeExpr	::= typeid /* An already defined type. /*/
		| enumtype
		| subrangetype
		| recordtype
		| arraytype
                | scalarsettype
                | uniontype
		| multisettype


/* an already defined type. /*/
typeid		::= ID



/* an enumerated type. /*/
enumtype	::= ENUM
		  '{' enums '}' /* should this be optenums? /*/



/* a possibly-empty comma-separated list. /*/
/* optenums	: enums
			 /*/
/*		| /* empty /*/
/*
/*/


/* a comma-separated list of words. /*/
enums		::= enums ',' ID
		| enums ID
		| ID



/* a subrange of an enumerated type /*/
subrangetype	::= expr DOTDOT expr /* must be constants. /*/



/* a record type, like the records of every Wirth language. /*/
recordtype	::= RECORD optInterleaved
			  /* Yea, verily, _two_ null nonterminals--we need
			   * to save both the curfields and the offset. /*/
		  fields endrecord



/* End of a record. /*/
endrecord	::= ENDRECORD
		| END


/* optional keyword INTERLEAVED. /*/
optInterleaved	::= /* INTERLEAVED
		| /*/ /* empty /*/



/* a list of fields, with ; as a separator. /*/
fields		::= fields semi field
		| fields semi
		  /* Why doesn't this cause a shift-reduce conflict?/*/
		  /* Oh, I see, it only considers the expansions that
		   * can go into a valid parse. I am filled with a new
		   * respect for LALR parsing. /*/
		| field



/* a single field entry. /*/
field		::=
		  ID fieldtail



/* end of a field--this is useful because it allows multiple fields
 * to be declared on a single line. /*/
fieldtail	::= ',' ID fieldtail

		| ':' typeExpr /* the associated type. /*/



/* an array. /*/
arraytype	::= ARRAY optInterleaved '[' typeExpr ']' OF typeExpr
		  /* $4 must be a simple type, not an array or record./*/


/* an multiset array. /*/
multisettype	::= MULTISET optInterleaved '[' expr ']' OF typeExpr
		  /* $4 must be an integer, signifying the maximium size./*/


/* scalarset extension /*/
scalarsettype   ::= SCALARSET "(" expr ")" // a single scalarset

/* union extension /*/
uniontype       ::= UNION ""  // a union of scalarsets and/or enum


unionlist       ::= unionlist "," unionlistelt
                | unionlistelt "," unionlistelt

unionlistelt
                ::= ID
                | scalarsettype
                | enumtype




/* var declarations. /*/
varDecls	::= varDecls varDecl semi
		| /* empty /*/



/* a single var declaration. /*/
varDecl		::=
		  ID vardecltail



/* end of a vardecl--this is useful because it allows multiple vars
 * to be declared on a single line. /*/
vardecltail	::= ',' ID vardecltail
		| ':' typeExpr /* the associated type. /*/



/* a list of procedures. /*/
procDecls	::= procDecls procDecl
		| procDecls funcDecl
		| /* empty /*/


/* a single procdure. /*/
procDecl	::= PROCEDURE ID
		  '(' optformals ')' semi
		    optdecls
		    optstmts endprocedure semi



endprocedure	::= ENDPROCEDURE
		| END


/* a single function. /*/
funcDecl	::= FUNCTION ID
		  '(' optformals ')'
  		  ':' typeExpr semi
		  optdecls
		  optstmts endfunction semi /*decls and BEGIN added by rlm./*/



endfunction	::= ENDFUNCTION
		| END


/* an optional set of formals /*/
optformals	::= formals
		| /* empty /*/


/* a nonempty list of formals /*/
formals		::= formals semi formal
		| formals semi
		| formal
 		| formals ',' formal



/* a single formal. /*/
/* To add a type of parameter, you
 * must add a line that sets up paramclass correctly,
 * and add a case to the switch on paramclass in formaltail. /*/
formal		::= VAR
		  formalrest
		|
		  formalrest



formalrest	::= ID formaltail



/* the end of a formal declaration. /*/
formaltail	::= ',' ID formaltail
		| ':' typeExpr
                        /* was a TypeExpr, but I had to require param\'s types to be defined before. /*/



/* an optional declaration section and BEGIN keyword. /*/
optdecls	::= decls bEGIN
		| /* empty /*/



/* expression syntax. /*/
/* a designator is an lvalue. /*/
designator	::= ID
		| designator '[' expr ']'
		  /* array reference. /*/
		| designator '.' ID
		  /* record reference. /*/



/* general expression. /*/
expr		::= expr '?' expr ':' expr
  		| expr IMPLIES expr
		| expr '|' expr
		| expr '&' expr
		| NOT expr
		| expr '<' expr
		| expr LEQ expr
		| expr '>' expr
		| expr GEQ expr
		| expr '=' expr
		| expr NEQ expr
		| expr '+' expr
		| expr '-' expr
		| '+' expr	//%prec '*'
 		| '-' expr	//%prec '*'
		| expr '*' expr
		| expr '/' expr
		| expr '%' expr /* extension to V1.6. by rlm. /*/
		| INTCONST
		| designator
		| ID actuals /* a function call. /*/
		| ISUNDEFINED '(' designator ')'	// scalarset extension
                | ISMEMBER '(' designator ',' typeExpr ')' // scalarset extension
		| '(' expr ')'
		| FORALL
		   quantifiers do expr endforall
		| EXISTS
		  quantifiers do expr endexists
		| error
                | MULTISETCOUNT '('
		  ID ':' designator ','
		  expr ')'



endforall	::= ENDFORALL
		| END


endexists	::= ENDEXISTS
		| END


/* actual parameters for a function or procedure. /*/
actuals 	::= '(' exprlist ')'
		| '(' ')'



/* a nonempty list of expressions. /*/
/* generated in reverse order. /*/
exprlist	::= exprlist ',' expr
		| expr
		| exprlist ',' UNDEFINED
		| UNDEFINED



/* the two types of FOR construct, marked off by braces in the following
 * examples:
 * 1) FOR  DO ...
 * 2) FOR  DO ...
 /*/
quantifier	::= ID ':' typeExpr
		| ID ASSIGN expr TO expr optBy



/* a semi-colon separated list of quantifiers. Only used for rulesets. /*/
quantifiers	::= quantifier ';' quantifiers
		| quantifier



/* We've decided to try to let a colon substitute for the word 'do'. /*/
do		::= DO
		| ':'


/* an optional BY phrase. /*/
optBy		::= BY expr
		| /* empty /*/




/* statement rules. /*/
/* an optional list of statements. /*/
optstmts	::=
		stmts
		| /* empty /*/



/* a list of statements, with ; as a separator. /*/
stmts		::= stmts semi stmt
		| stmts semi /* allow extra semi-colons. /*/
		| stmt



/* a ;-separated statement. /*/
stmt		::= assignment
		| ifstmt
		| whilestmt
		| switchstmt
		| forstmt
		| proccall
		| clearstmt
		| errorstmt
		| assertstmt
		| putstmt
		| aliasstmt
		| returnstmt
		| undefinestmt // scalarset extension
                | multisetaddstmt
                | multisetremovestmt

/* an assignment statement. /*/
assignment	::= designator ASSIGN expr
                | designator ASSIGN UNDEFINED // "undefined" extension



/* if statement. /*/
ifstmt		::= IF expr THEN
		    optstmts
		  optElses
		  endif



endif		::= ENDIF
		| END


/* elsif parts. /*/
optElses	::= elsif optElses
		| optElse



/* a single elsif. /*/
elsif		::= ELSIF expr THEN
		    optstmts



/* an optional else clause. /*/
optElse		::= ELSE optstmts
		| /* empty /*/



/* while statment. /*/
whilestmt	::= WHILE expr do
		    optstmts
		  endwhile



endwhile	::= ENDWHILE
		| END


/* switch statement. /*/
switchstmt 	::= SWITCH expr

		    optCases
		    optElse
		  endswitch



endswitch	::= ENDSWITCH
		| END


/* an optional list of cases. /*/
optCases	::= optCases case
		| /* empty /*/



/* a single case. /*/
case		::= CASE exprlist ':' optstmts



/* for statement. /*/
forstmt		::= FOR
		  quantifiers do
		    optstmts
		  endfor



endfor		::= ENDFOR
		| END


/* procedure call. /*/
proccall	::=  ID actuals



/* set all elements of basic type to their minima. /*/
clearstmt	::= CLEAR designator


/* undefine statement /*/
undefinestmt	::= UNDEFINE designator


/* multiset add statement /*/
multisetaddstmt ::= MULTISETADD '(' designator ',' designator ')'


/* multiset remove statement /*/
multisetremovestmt ::= MULTISETREMOVEPRED '('
		  ID ':' designator
		  ',' expr ')'
		| MULTISETREMOVE '(' expr ',' designator ')'


/* raise an error. /*/
errorstmt	::= ERROR STRING



/* check an assertion, error if it\'s not so. /*/
assertstmt	::= ASSERT expr optString



/* Print a message to output, I assume. /*/
putstmt		::= PUT expr
		| PUT STRING



/* simplify use of common expressions--sort of like a with statement. /*/
aliasstmt	::= ALIAS
		  aliases do optstmts endalias



endalias	::= ENDALIAS
		| END


/* a set of aliases. /*/
aliases		::= aliases semi alias
		| aliases semi /* I still don't see why this doesn't create conflicts. /*/
		  /* Oh, I see, it only considers the expansions that
		   * can go into a valid parse. I am filled with a new
		   * respect for LALR parsing. /*/
		| aliases ',' alias
		| alias



/* a single alias. /*/
alias		::= ID ':' expr



/* exit from a procedure, function or rule and return a value for a function /*/
returnstmt	::= RETURN optretexpr



/* an optional expression to be returned. /*/
optretexpr	::= expr
		| /* empty /*/


/* Murphi-specific stuff. /*/
/* A list of rules to be applied nondeterministically. /*/
/* Okay, so it\'s right-recursive. Forgive me, please. /*/
rules		::= rule semi rules
		| rule semi
		| rule


/* a single rule--in essence, a hunk of code to execute nondeterministically./*/
/* Now, it could be a startstate or an invariant, too. rlm. /*/
rule		::= simplerule
		| aliasrule
		| ruleset
		| startstate
		| invariant
//		| fairness	// liveness extension
//              | liveness 	// liveness extension
		| error
                | choose


/* a basic rule. /*/
simplerule	::= RULE optFair optPriority optString optCondition
		  optdecls optstmts endrule
			/*decls, BEGIN, and END added by rlm./*/



// liveness extension
optFair         ::= UNFAIR
                |

endrule		::= ENDRULE
		| END


/* an optional condition on a rule. /*/
optCondition	::= expr LONGARROW
		| /* empty /*/



/* an optional name. /*/
optString	::= STRING
		| /* empty /*/
/*		| ID
/*/

/* Vitaly /*/

/* an optional priority /*/

optPriority	::= INTCONST
		| /* empty /*/



/* an aliased ruleset. /*/
aliasrule	::= ALIAS
		  aliases do rules endalias



/* a parametrized ruleset. /*/
ruleset		::= RULESET
		  quantifiers
		  do rules endruleset



endruleset	::= ENDRULESET
		| END


/* choosing from a multiset /*/
choose		::= CHOOSE
                  ID ':' designator
		  do rules endchoose


onerule		::= rule semi
		| rule



endchoose	::= ENDCHOOSE
		| END


/* a single start state. /*/
startstate	::= STARTSTATE
  		  optString optdecls optstmts endstartstate



endstartstate	::= ENDSTARTSTATE
  		| END


/* a list of invariants. /*/
/* optInvariants	: optInvariants invariant /*/
/*		| /* empty /*/
/*


/* a single invariant. /*/
invariant	::= INVARIANT optString expr



/* a single fairness. /*/
fairness	::= FAIRNESS optString expr


liveness        ::= liveU
                | liveE
                | liveAE
                | liveEA
                | liveAIU
                | liveAIE

liveU           ::= LIVENESS optString expr UNTIL expr


liveE           ::= LIVENESS optString EVENTUALLY expr


liveEA          ::= LIVENESS optString EVENTUALLY ALWAYS expr


liveAE          ::= LIVENESS optString ALWAYS EVENTUALLY expr


liveAIE         ::= LIVENESS optString ALWAYS expr IMPLIES EVENTUALLY expr


liveAIU         ::= LIVENESS optString ALWAYS expr IMPLIES expr UNTIL expr


// Tokens

DOTDOT ::= ".."
LONGARROW ::= "==>"
ASSIGN ::= ":="
LEQ ::= "<="
NEQ ::= "!="
GEQ ::= ">="
NOT ::= "!"
IMPLIES ::= "->"

PROCESS ::=  "process"
END ::= "end"
PROGRAM ::= "program"
PROCEDURE ::= "procedure"
ENDPROCEDURE ::= "endprocedure"
FUNCTION ::= "function"
ENDFUNCTION ::= "endfunction"
RULE ::= "rule"
ENDRULE ::= "endrule"
RULESET ::= "ruleset"
ENDRULESET ::= "endruleset"
ALIAS ::= "alias"
ENDALIAS ::= "endalias"
IF ::= "if"
THEN ::= "then"
ELSIF ::= "elsif"
ELSE ::= "else"
ENDIF ::= "endif"
SWITCH ::= "switch"
CASE ::= "case"
ENDSWITCH ::= "endswitch"
FOR ::= "for"
FORALL ::= "forall"
EXISTS ::= "exists"
IN ::= "in"
DO ::= "do"
ENDFOR ::= "endfor"
ENDFORALL ::= "endforall"
ENDEXISTS ::= "endexists"
WHILE ::= "while"
ENDWHILE ::= "endwhile"
RETURN ::= "return"
TO ::= "to"
bEGIN ::= "begin"
BY ::= "by"
CLEAR ::= "clear"
ERROR ::= "error"
ASSERT ::= "assert"
PUT ::= "put"
CONST ::= "const"
TYPE ::= "type"
VAR ::= "var"
ENUM ::= "enum"
INTERLEAVED ::= "interleaved"
RECORD ::= "record"
ARRAY ::= "array"
OF ::= "of"
ENDRECORD ::= "endrecord"
STARTSTATE ::= "startstate"
ENDSTARTSTATE ::= "endstartstate"
 INVARIANT ::= "invariant"
TRACEUNTIL ::= "traceuntil"

  /* liveness */
FAIRNESS ::= "fairness"
FAIRNESSSET ::= "fairnessset"
ENDFAIRNESSSET ::= "endfairnessset"
LIVENESS ::= "liveness"
LIVENESSSET ::= "livenessset"
ENDLIVENESSSET ::= "endlivenessset"
ALWAYS ::= "always"
EVENTUALLY ::= "eventually"
UNTIL ::= "until"
UNFAIR ::= "unfair"

  /* scalarset */
SCALARSET ::= "scalarset"
ISMEMBER ::= "ismember"

  /* undefined */
UNDEFINE ::= "undefine"
ISUNDEFINED ::= "isundefined"
UNDEFINED ::= "undefined"

  /* general union */
UNION ::= "union"

  /* multiset */
MULTISET ::= "multiset"
MULTISETREMOVE ::= "multisetremove"
MULTISETREMOVEPRED ::= "multisetremovepred"
MULTISETADD ::= "multisetadd"
MULTISETCOUNT ::= "multisetcount"
CHOOSE ::= "choose"
ENDCHOOSE ::= "endchoose"

  /* first definitions. */
  //enter_reserved("boolean",ID);
  //enter_reserved("true",ID);
  //enter_reserved("false",ID);