<?xml version="1.0" encoding="UTF-8"?>
<!-- edited with XML Spy v4.2 U (http://www.xmlspy.com) by jaco (technion) -->
<!ELEMENT Program (decl?, procdecl?, rules?)>
<!ATTLIST Program
	ID ID #REQUIRED
>
<!ELEMENT decl (constdecl*, typedecl*, vardecl*)>
<!ATTLIST decl 
	ID ID #REQUIRED
>
<!ELEMENT constdecl (ID, expr)>
<!ATTLIST constdecl 
	ID ID #REQUIRED
>
<!ELEMENT typedecl (ID, typeExpr)>
<!ATTLIST typedecl 
	ID ID #REQUIRED
>
<!ELEMENT typeExpr (ID | range | enum | record | array | boolean)>
<!ATTLIST typeExpr 
	ID ID #REQUIRED
>
<!ELEMENT range (expr, expr)>
<!ATTLIST range 
	ID ID #REQUIRED
>
<!ELEMENT enum (ID+)>
<!ATTLIST enum 
	ID ID #REQUIRED
>
<!ELEMENT record (vardecl?)>
<!ATTLIST record 
	ID ID #REQUIRED
>
<!ELEMENT array (typeExpr, typeExpr)>
<!ATTLIST array 
	ID ID #REQUIRED
>
<!ELEMENT vardecl (ID+, typeExpr)>
<!ATTLIST vardecl 
	ID ID #REQUIRED
>
<!ELEMENT procdecl (procedure, function)>
<!ATTLIST procdecl 
	ID ID #REQUIRED
>
<!ELEMENT procedure (ID, formal*, decl?, stmts?)>
<!ATTLIST procedure 
	ID ID #REQUIRED
>
<!ELEMENT function (ID, formal*, typeExpr, decl?, stmts?)>
<!ATTLIST function 
	ID ID #REQUIRED
>
<!ELEMENT formal (ID+, typeExpr)>
<!ATTLIST formal 
	ID ID #REQUIRED
>
<!ELEMENT expr (designator | integer-constant | func-call | uni-quant | exist-quant | PLUS | MINUS | TIMES | DIV | MOD | NOT | OR | AND | IMPL | LT | LE | GT | GE | EQ | NOTEQ | COND | boolconst)>
<!ATTLIST expr 
	ID ID #REQUIRED
>
<!ELEMENT designator (ID, (field-sel? | array-elem?))>
<!ATTLIST designator 
	ID ID #REQUIRED
>
<!ELEMENT func-call ((ID, actuals*))>
<!ATTLIST func-call
	ID ID #REQUIRED
>
<!ELEMENT actuals (ID+)>
<!ATTLIST actuals 
	ID ID #REQUIRED
>
<!ELEMENT uni-quant ((quantifier, expr))>
<!ATTLIST uni-quant
	ID ID #REQUIRED
>
<!ELEMENT exist-quant ((quantifier, expr))>
<!ATTLIST exist-quant
	ID ID #REQUIRED
>
<!ELEMENT field-sel ((ID*))>
<!ATTLIST field-sel 
	ID ID #REQUIRED
>
<!ELEMENT array-elem ((expr*))>
<!ATTLIST  array-elem 
	ID ID #REQUIRED
>
<!ELEMENT PLUS (expr, expr)>
<!ATTLIST PLUS 
	ID ID #REQUIRED
>
<!ELEMENT MINUS (expr, expr)>
<!ATTLIST MINUS 
	ID ID #REQUIRED
>
<!ELEMENT TIMES (expr, expr)>
<!ATTLIST TIMES 
	ID ID #REQUIRED
>
<!ELEMENT DIV (expr, expr)>
<!ATTLIST DIV 
	ID ID #REQUIRED
>
<!ELEMENT MOD (expr, expr)>
<!ATTLIST MOD 
	ID ID #REQUIRED
>
<!ELEMENT NOT (expr)>
<!ATTLIST NOT 
	ID ID #REQUIRED
>
<!ELEMENT OR (expr, expr)>
<!ATTLIST OR 
	ID ID #REQUIRED
>
<!ELEMENT AND (expr, expr)>
<!ATTLIST AND 
	ID ID #REQUIRED
>
<!ELEMENT IMPL (expr, expr)>
<!ATTLIST IMPL 
	ID ID #REQUIRED
>
<!ELEMENT LT (expr, expr)>
<!ATTLIST LT 
	ID ID #REQUIRED
>
<!ELEMENT LE (expr, expr)>
<!ATTLIST LE 
	ID ID #REQUIRED
>
<!ELEMENT GT (expr, expr)>
<!ATTLIST GT 
	ID ID #REQUIRED
>
<!ELEMENT GE (expr, expr)>
<!ATTLIST GE 
	ID ID #REQUIRED
>
<!ELEMENT EQ (expr, expr)>
<!ATTLIST EQ 
	ID ID #REQUIRED
>
<!ELEMENT NOTEQ (expr, expr)>
<!ATTLIST NOTEQ 
	ID ID #REQUIRED
>
<!ELEMENT COND (expr, expr, expr)>
<!ATTLIST COND 
	ID ID #REQUIRED
>
<!ELEMENT stmts (stmt+)>
<!ATTLIST stmts 
	ID ID #REQUIRED
>
<!ELEMENT stmt (assignment | ifstmt | switchstmt | forstmt | whilestmt | aliasstmt | proccall | clearstmt | errorstmt | assertstmt | putstmt | returnstmt)>
<!ATTLIST stmt 
	ID ID #REQUIRED
>
<!ELEMENT assignment (designator, expr)>
<!ATTLIST assignment 
	ID ID #REQUIRED
>
<!ELEMENT ifstmt (expr, stmts?, elseif*, else?)>
<!ATTLIST ifstmt 
	ID ID #REQUIRED
>
<!ELEMENT elseif (expr, stmts?)>
<!ATTLIST elseif 
	ID ID #REQUIRED
>
<!ELEMENT else (stmts?)>
<!ATTLIST else 
	ID ID #REQUIRED
>
<!ELEMENT switchstmt (expr, case*, else?)>
<!ATTLIST switchstmt 
	ID ID #REQUIRED
>
<!ELEMENT case (expr+, stmts?)>
<!ATTLIST case 
	ID ID #REQUIRED
>
<!ELEMENT forstmt (quantifier, stmts?)>
<!ATTLIST forstmt 
	ID ID #REQUIRED
>
<!ELEMENT quantifier (type | expr-to-expr)>
<!ATTLIST quantifier 
	ID ID #REQUIRED
>
<!ELEMENT type (ID, typeExpr)>
<!ATTLIST type 
	ID ID #REQUIRED
>
<!ELEMENT expr-to-expr (expr, expr, expr?)>
<!ATTLIST expr-to-expr 
	ID ID #REQUIRED
>
<!ELEMENT whilestmt (expr, stmts?)>
<!ATTLIST whilestmt 
	ID ID #REQUIRED
>
<!ELEMENT aliasstmt (alias+, stmts?)>
<!ATTLIST aliasstmt 
	ID ID #REQUIRED
>
<!ELEMENT alias (ID, expr)>
<!ATTLIST alias 
	ID ID #REQUIRED
>
<!ELEMENT proccall (ID, expr*)>
<!ATTLIST proccall 
	ID ID #REQUIRED
>
<!ELEMENT clearstmt (designator)>
<!ATTLIST clearstmt 
	ID ID #REQUIRED
>
<!ELEMENT errorstmt (string)>
<!ATTLIST errorstmt 
	ID ID #REQUIRED
>
<!ELEMENT assertstmt (expr, string?)>
<!ATTLIST assertstmt 
	ID ID #REQUIRED
>
<!ELEMENT putstmt (expr | string)>
<!ATTLIST putstmt 
	ID ID #REQUIRED
>
<!ELEMENT returnstmt (expr)>
<!ATTLIST returnstmt 
	ID ID #REQUIRED
>
<!ELEMENT rules (rule+)>
<!ATTLIST rules 
	ID ID #REQUIRED
>
<!ELEMENT rule (simplerule | startstate | invariant | ruleset | aliasrule)>
<!ATTLIST rule 
	ID ID #REQUIRED
>
<!ELEMENT simplerule (string?, expr?, decl?, stmts?)>
<!ATTLIST simplerule 
	ID ID #REQUIRED
>
<!ELEMENT startstate (string?, decl?, stmts?)>
<!ATTLIST startstate 
	ID ID #REQUIRED
>
<!ELEMENT invariant (string?, expr)>
<!ATTLIST invariant 
	ID ID #REQUIRED
>
<!ELEMENT ruleset (quantifier+, rules?)>
<!ATTLIST ruleset 
	ID ID #REQUIRED
>
<!ELEMENT aliasrule (alias+, rules?)>
<!ATTLIST aliasrule 
	ID ID #REQUIRED
>
<!ELEMENT ID (#PCDATA)>
<!ATTLIST ID 
	ID ID #REQUIRED
>
<!ELEMENT string (#PCDATA)>
<!ATTLIST string 
	ID ID #REQUIRED
>
<!ELEMENT integer-constant (#PCDATA)>
<!ATTLIST  integer-constant
	ID ID #REQUIRED
>
<!ELEMENT boolean EMPTY >
<!ATTLIST  boolean	
	ID ID #REQUIRED
>
<!ELEMENT boolconst (TRUE | FALSE)>
<!ATTLIST  boolconst	
	ID ID #REQUIRED
>
<!ELEMENT TRUE EMPTY>
<!ATTLIST  TRUE	
	ID ID #REQUIRED
>
<!ELEMENT FALSE EMPTY>
<!ATTLIST  FALSE
	ID ID #REQUIRED
>
