<?xml version="1.0" encoding="UTF-8"?>
<!-- edited with XML Spy v4.4 U (http://www.xmlspy.com) by Efrat Shabtai (technion) -->
<!--The file smv.dtd consists with grammer.y - the yacc file of smv-->
<!--This is a partial dtd for smv includes only the most commom features.-->
<!--It is possible to add all features of smv to the existing file.-->
<!ELEMENT begin (module+)>
<!ATTLIST begin
	ID ID #IMPLIED
>
<!ELEMENT module (moduletype, declaration*)>
<!ATTLIST module
	ID ID #IMPLIED
>
<!ELEMENT moduletype (ATOM, neatomlist?)>
<!ATTLIST moduletype
	ID ID #IMPLIED
>
<!ELEMENT neatomlist (ATOM+)>
<!ATTLIST neatomlist
	ID ID #IMPLIED
>
<!ELEMENT declaration (var | init | trans | invar | define | spec | fairness | assign)>
<!ATTLIST declaration
	ID ID #IMPLIED
>
<!ELEMENT var (vlist)>
<!ATTLIST var
	ID ID #IMPLIED
>
<!ELEMENT vlist (vardecl*)>
<!ATTLIST vlist
	ID ID #IMPLIED
>
<!ELEMENT vardecl (term, type)>
<!ATTLIST vardecl
	ID ID #IMPLIED
>
<!ELEMENT init (expr)>
<!ATTLIST init
	ID ID #IMPLIED
>
<!ELEMENT trans (expr)>
<!ATTLIST trans
	ID ID #IMPLIED
>
<!ELEMENT invar (expr)>
<!ATTLIST invar
	ID ID #IMPLIED
>
<!ELEMENT define (dlist)>
<!ATTLIST define
	ID ID #IMPLIED
>
<!ELEMENT dlist (dstatement*)>
<!ATTLIST dlist
	ID ID #IMPLIED
>
<!ELEMENT dstatement (term, expr)>
<!ATTLIST dstatement
	ID ID #IMPLIED
>
<!ELEMENT spec (expr)>
<!ATTLIST spec
	ID ID #IMPLIED
>
<!ELEMENT fairness (expr)>
<!ATTLIST fairness
	ID ID #IMPLIED
>
<!ELEMENT assign (alist)>
<!ATTLIST assign
	ID ID #IMPLIED
>
<!ELEMENT alist (astatement*)>
<!ATTLIST alist
	ID ID #IMPLIED
>
<!ELEMENT astatement (alhs, expr)>
<!ATTLIST astatement
	ID ID #IMPLIED
>
<!ELEMENT alhs (term | NEXT | SMALLINIT)>
<!ATTLIST alhs
	ID ID #IMPLIED
>
<!ELEMENT NEXT (term)>
<!ATTLIST NEXT
	ID ID #IMPLIED
>
<!ELEMENT SMALLINIT (term)>
<!ATTLIST SMALLINIT
	ID ID #IMPLIED
>
<!ELEMENT type (BOOLEAN | neconstlist | usertype | ARRAY | PROCESS | subrange)>
<!ATTLIST type
	ID ID #IMPLIED
>
<!ELEMENT BOOLEAN EMPTY>
<!ATTLIST BOOLEAN
	ID ID #IMPLIED
>
<!ELEMENT neconstlist (constant+)>
<!ATTLIST neconstlist
	ID ID #IMPLIED
>
<!ELEMENT usertype (ATOM, neexplist?)>
<!ATTLIST usertype
	ID ID #IMPLIED
>
<!ELEMENT neexplist (expr+)>
<!ATTLIST neexplist
	ID ID #IMPLIED
>
<!ELEMENT ARRAY (subrange, type)>
<!ATTLIST ARRAY
	ID ID #IMPLIED
>
<!ELEMENT PROCESS (usertype)>
<!ATTLIST PROCESS
	ID ID #IMPLIED
>
<!ELEMENT subrange (number, number)>
<!ATTLIST subrange
	ID ID #IMPLIED
>
<!ELEMENT term (ATOM | DOT | arrayelem)>
<!ATTLIST term
	ID ID #IMPLIED
>
<!ELEMENT DOT (term, ATOM)>
<!ATTLIST DOT
	ID ID #IMPLIED
>
<!ELEMENT arrayelem (term, expr)>
<!ATTLIST arrayelem
	ID ID #IMPLIED
>
<!ELEMENT expr (term | number | subrange | FALSEEXP | TRUEEXP | PAREN | OR | AND | NOT | EX | AX | EF | AF | EG | AG | AUNTIL | EUNTIL | CASE | NEXT | PLUS | MINUS | TIMES | DIVIDE | MOD | EQUAL | LT | GT | LE | GE | neatomset | UNION | SETIN)>
<!ATTLIST expr
	ID ID #IMPLIED
>
<!ELEMENT FALSEEXP EMPTY>
<!ATTLIST FALSEEXP
	ID ID #IMPLIED
>
<!ELEMENT TRUEEXP EMPTY>
<!ATTLIST TRUEEXP
	ID ID #IMPLIED
>
<!ELEMENT PAREN (expr)>
<!ATTLIST PAREN
	ID ID #IMPLIED
>
<!ELEMENT OR (expr, expr)>
<!ATTLIST OR
	ID ID #IMPLIED
>
<!ELEMENT AND (expr, expr)>
<!ATTLIST AND
	ID ID #IMPLIED
>
<!ELEMENT PLUS (expr, expr)>
<!ATTLIST PLUS
	ID ID #IMPLIED
>
<!ELEMENT MINUS (expr, expr)>
<!ATTLIST MINUS
	ID ID #IMPLIED
>
<!ELEMENT TIMES (expr, expr)>
<!ATTLIST TIMES
	ID ID #IMPLIED
>
<!ELEMENT DIVIDE (expr, expr)>
<!ATTLIST DIVIDE
	ID ID #IMPLIED
>
<!ELEMENT MOD (expr, expr)>
<!ATTLIST MOD
	ID ID #IMPLIED
>
<!ELEMENT EQUAL (expr, expr)>
<!ATTLIST EQUAL
	ID ID #IMPLIED
>
<!ELEMENT LT (expr, expr)>
<!ATTLIST LT
	ID ID #IMPLIED
>
<!ELEMENT GT (expr, expr)>
<!ATTLIST GT
	ID ID #IMPLIED
>
<!ELEMENT LE (expr, expr)>
<!ATTLIST LE
	ID ID #IMPLIED
>
<!ELEMENT GE (expr, expr)>
<!ATTLIST GE
	ID ID #IMPLIED
>
<!ELEMENT UNION (expr, expr)>
<!ATTLIST UNION
	ID ID #IMPLIED
>
<!ELEMENT SETIN (expr, expr)>
<!ATTLIST SETIN
	ID ID #IMPLIED
>
<!ELEMENT NOT (expr)>
<!ATTLIST NOT
	ID ID #IMPLIED
>
<!ELEMENT EX (expr)>
<!ATTLIST EX
	ID ID #IMPLIED
>
<!ELEMENT AX (expr)>
<!ATTLIST AX
	ID ID #IMPLIED
>
<!ELEMENT EF (expr)>
<!ATTLIST EF
	ID ID #IMPLIED
>
<!ELEMENT AF (expr)>
<!ATTLIST AF
	ID ID #IMPLIED
>
<!ELEMENT EG (expr)>
<!ATTLIST EG
	ID ID #IMPLIED
>
<!ELEMENT AG (expr)>
<!ATTLIST AG
	ID ID #IMPLIED
>
<!ELEMENT AUNTIL (expr, expr)>
<!ATTLIST AUNTIL
	ID ID #IMPLIED
>
<!ELEMENT EUNTIL (expr, expr)>
<!ATTLIST EUNTIL
	ID ID #IMPLIED
>
<!ELEMENT neatomset (constant+)>
<!ATTLIST neatomset
	ID ID #IMPLIED
>
<!ELEMENT constant (ATOM | number | FALSEEXP | TRUEEXP)>
<!ATTLIST constant
	ID ID #IMPLIED
>
<!ELEMENT CASE (caseentry*)>
<!ATTLIST CASE
	ID ID #IMPLIED
>
<!ELEMENT caseentry (expr, expr)>
<!ATTLIST caseentry
	ID ID #IMPLIED
>
<!ELEMENT number (NUMBER | UMINUS | UPLUS)>
<!ATTLIST number
	ID ID #IMPLIED
>
<!ELEMENT UMINUS (NUMBER)>
<!ATTLIST UMINUS
	ID ID #IMPLIED
>
<!ELEMENT UPLUS (NUMBER)>
<!ATTLIST UPLUS
	ID ID #IMPLIED
>
<!ELEMENT NUMBER (#PCDATA)>
<!ATTLIST NUMBER
	ID ID #IMPLIED
>
<!ELEMENT ATOM (#PCDATA)>
<!ATTLIST ATOM
	ID ID #IMPLIED
>

