<?xml version="1.0" encoding="UTF-8"?>

<!-- The DTD for the Symbolic Analysis Laboratory (SAL) Language -->

<!ENTITY % TYPE
  "( TYPENAME
   | QUALIFIEDTYPENAME
   | SUBRANGE
   | ARRAYTYPE
   | TUPLETYPE
   | FUNCTIONTYPE
   | RECORDTYPE
   | SUBTYPE
   | STATETYPE )">

<!ENTITY % TYPEORVARDECL "( %TYPE; | VARDECL )"> 

<!ENTITY % TYPEDEF "( %TYPE; | SCALARTYPE | DATATYPE )">
<!ENTITY % SETEXPRESSION "(SETLISTEXPRESSION | SETPREDEXPRESSION)">

<!ENTITY % EXPRESSION
  "( NAMEEXPR
   | QUALIFIEDNAMEEXPR
   | NEXTOPERATOR
   | NUMERAL
   | STRINGEXPR
   | APPLICATION
   | ARRAYSELECTION
   | RECORDSELECTION
   | TUPLESELECTION
   | UPDATEEXPRESSION
   | LAMBDAABSTRACTION
   | QUANTIFIEDEXPRESSION
   | LETEXPRESSION
   | %SETEXPRESSION;
   | ARRAYLITERAL
   | RECORDLITERAL
   | TUPLELITERAL
   | CONDITIONAL
   | MODINIT
   | MODTRANS )">

<!ENTITY % MODULE
 "( BASEMODULE
  | SYNCHRONOUSCOMPOSITION
  | ASYNCHRONOUSCOMPOSITION
  | MULTISYNCHRONOUS
  | MULTIASYNCHRONOUS
  | HIDING
  | NEWOUTPUT
  | RENAMING
  | MODULEINSTANCE
  | WITHMODULE
  | OBSERVEMODULE)">

<!ENTITY % LHS "(%EXPRESSION;)">

<!ENTITY % DEFINITION "( SIMPLEDEFINITION | FORALLDEFINITION )">

<!ENTITY % SOMECOMMAND "(GUARDEDCOMMAND|LABELEDCOMMAND|MULTICOMMAND)">

<!ENTITY % DEFINITIONORCOMMAND "(%DEFINITION;|SOMECOMMANDS)">

<!ENTITY % NAME "#PCDATA">
<!ENTITY % QUALIFIEDNAME "(IDENTIFIER, CONTEXTNAME)">

<!ENTITY % INDEXTYPE "(TYPENAME|SUBRANGE)">
<!ENTITY % BOUND "(%EXPRESSION;)">

<!ENTITY % MODULEASSERTION "(MODULEMODELS|MODULEIMPLEMENTS)">
<!ENTITY % ASSERTIONEXPRESSION
  "(ASSERTIONPROPOSITION|QUANTIFIEDASSERTION|%MODULEASSERTION;|%EXPRESSION;)">

<!ENTITY % COMMONATTS 'PLACE CDATA #IMPLIED'>

<!ELEMENT CONTEXT (IDENTIFIER, PARAMETERS, CONTEXTBODY)>
<!ATTLIST CONTEXT %COMMONATTS;
                  LOGIC (YES|NO) "NO">

<!ELEMENT PARAMETERS (TYPEDECLS?, VARDECLS?)>
<!ATTLIST PARAMETERS %COMMONATTS;>

<!ELEMENT TYPEDECLS (TYPEDECL*)>
<!ATTLIST TYPEDECLS %COMMONATTS;>

<!ELEMENT VARDECLS (VARDECL*)>
<!ATTLIST VARDECLS %COMMONATTS;>

<!ELEMENT CONTEXTBODY ( CONSTANTDECLARATION
                      | TYPEDECLARATION
		      | ASSERTIONDECLARATION
		      | CONTEXTDECLARATION
		      | MODULEDECLARATION)*>
<!ATTLIST CONTEXTBODY %COMMONATTS;>

<!ELEMENT CONSTANTDECLARATION (IDENTIFIER,%TYPE;,(%EXPRESSION;)?)>
<!ATTLIST CONSTANTDECLARATION %COMMONATTS;
                              FUNCTIONAL (YES|NO) "NO">

<!ELEMENT TYPEDECLARATION (IDENTIFIER,(%TYPEDEF;)?)>
<!ATTLIST TYPEDECLARATION %COMMONATTS;>

<!ELEMENT CONTEXTDECLARATION (IDENTIFIER, CONTEXTNAME)>
<!ATTLIST CONTEXTDECLARATION %COMMONATTS;>

<!ELEMENT CONTEXTNAME (IDENTIFIER, ACTUALPARAMETERS?)>
<!ATTLIST CONTEXTNAME %COMMONATTS;>

<!ELEMENT ACTUALPARAMETERS (ACTUALTYPES?, ACTUALEXPRS?)>
<!ATTLIST ACTUALPARAMETERS %COMMONATTS;>

<!ELEMENT ACTUALTYPES ((%TYPE;)*)>
<!ATTLIST ACTUALTYPES %COMMONATTS;>

<!ELEMENT ACTUALEXPRS ((%EXPRESSION;)*)>
<!ATTLIST ACTUALEXPRS %COMMONATTS;>

<!ELEMENT MODULEDECLARATION (IDENTIFIER, VARDECLS, %MODULE;)>
<!ATTLIST MODULEDECLARATION %COMMONATTS;>

<!ELEMENT BASEMODULE ( INPUTDECL
                     | OUTPUTDECL
		     | GLOBALDECL
		     | LOCALDECL
		     | DEFDECL
		     | INITDECL
		     | TRANSDECL )*>
<!ATTLIST BASEMODULE %COMMONATTS;
                     PARENS CDATA "0">

<!ELEMENT INPUTDECL (VARDECL*)>
<!ATTLIST INPUTDECL %COMMONATTS;>

<!ELEMENT OUTPUTDECL (VARDECL*)>
<!ATTLIST OUTPUTDECL %COMMONATTS;>

<!ELEMENT GLOBALDECL (VARDECL*)>
<!ATTLIST GLOBALDECL %COMMONATTS;>

<!ELEMENT LOCALDECL (VARDECL*)>
<!ATTLIST LOCALDECL %COMMONATTS;>

<!ELEMENT DEFDECL ((%DEFINITION;)*)>
<!ATTLIST DEFDECL %COMMONATTS;>

<!ELEMENT INITDECL ((%DEFINITIONORCOMMAND;)*)>
<!ATTLIST INITDECL %COMMONATTS;>

<!ELEMENT TRANSDECL ((%DEFINITIONORCOMMAND;)*)>
<!ATTLIST TRANSDECL %COMMONATTS;>

<!ELEMENT SIMPLEDEFINITION (%LHS;, (RHSEXPRESSION|RHSSELECTION))>
<!ATTLIST SIMPLEDEFINITION %COMMONATTS;>

<!ELEMENT RHSEXPRESSION (%EXPRESSION;)>
<!ATTLIST RHSEXPRESSION %COMMONATTS;>

<!ELEMENT RHSSELECTION (%EXPRESSION;)>
<!ATTLIST RHSSELECTION %COMMONATTS;>

<!ELEMENT FORALLDEFINITION (VARDECLS, (%DEFINITION;)*)>
<!ATTLIST FORALLDEFINITION %COMMONATTS;>


<!ELEMENT LABELEDCOMMAND (LABEL, GUARDEDCOMMAND)>
<!ATTLIST LABELEDCOMMAND %COMMONATTS;>

<!ELEMENT LABEL (#PCDATA)>
<!ATTLIST LABEL %COMMONATTS;>

<!ELEMENT GUARDEDCOMMAND (GUARD, ASSIGNMENTS)>
<!ATTLIST GUARDEDCOMMAND %COMMONATTS;>

<!ELEMENT GUARD (%EXPRESSION;)>
<!ATTLIST GUARD %COMMONATTS;>

<!ELEMENT ASSIGNMENTS (SIMPLEDEFINITION*)>
<!ATTLIST ASSIGNMENTS %COMMONATTS;>

<!ELEMENT SOMECOMMANDS ((%SOMECOMMAND;)*)>
<!ATTLIST SOMECOMMANDS %COMMONATTS;>

<!ELEMENT MULTICOMMAND (VARDECLS, %SOMECOMMAND;)>
<!ATTLIST MULTICOMMAND %COMMONATTS;>


<!ELEMENT SYNCHRONOUSCOMPOSITION (%MODULE;, %MODULE;)>
<!ATTLIST SYNCHRONOUSCOMPOSITION %COMMONATTS;
                                 PARENS CDATA "0">

<!ELEMENT ASYNCHRONOUSCOMPOSITION (%MODULE;, %MODULE;)>
<!ATTLIST ASYNCHRONOUSCOMPOSITION %COMMONATTS;
                                  PARENS CDATA "0">

<!ELEMENT MULTISYNCHRONOUS (INDEXVARDECL, %MODULE;)>
<!ATTLIST MULTISYNCHRONOUS %COMMONATTS;
                           PARENS CDATA "0">

<!ELEMENT MULTIASYNCHRONOUS (INDEXVARDECL, %MODULE;)>
<!ATTLIST MULTIASYNCHRONOUS %COMMONATTS;
                            PARENS CDATA "0">

<!ELEMENT HIDING (IDENTIFIERS, %MODULE;)>
<!ATTLIST HIDING %COMMONATTS;
                 PARENS CDATA "0">

<!ELEMENT NEWOUTPUT (IDENTIFIERS, %MODULE;)>
<!ATTLIST NEWOUTPUT %COMMONATTS;
                    PARENS CDATA "0">

<!ELEMENT RENAMING (RENAMES, %MODULE;)>
<!ATTLIST RENAMING %COMMONATTS;
                   PARENS CDATA "0">

<!ELEMENT WITHMODULE (NEWVARDECLS, %MODULE;)>
<!ATTLIST WITHMODULE %COMMONATTS;
                     PARENS CDATA "0">

<!ELEMENT NEWVARDECLS ((INPUTDECL|OUTPUTDECL|GLOBALDECL)*)>
<!ATTLIST NEWVARDECLS %COMMONATTS;>

<!ELEMENT RENAMES (RENAME*)>
<!ATTLIST RENAMES %COMMONATTS;>

<!ELEMENT RENAME (%LHS;, %LHS;)>
<!ATTLIST RENAME %COMMONATTS;>

<!ELEMENT MODULEINSTANCE ((MODULENAME|QUALIFIEDMODULENAME), MODULEACTUALS)>
<!ATTLIST MODULEINSTANCE %COMMONATTS;
                         PARENS CDATA "0">

<!ELEMENT MODULENAME (%NAME;)>
<!ATTLIST MODULENAME %COMMONATTS;>

<!ELEMENT QUALIFIEDMODULENAME (%QUALIFIEDNAME;)>
<!ATTLIST QUALIFIEDMODULENAME %COMMONATTS;>

<!ELEMENT MODULEACTUALS ((%EXPRESSION;)*)>
<!ATTLIST MODULEACTUALS %COMMONATTS;>

<!ELEMENT OBSERVEMODULE (%MODULE;, %MODULE;)>
<!ATTLIST OBSERVEMODULE %COMMONATTS;
                        PARENS CDATA "0">


<!ELEMENT SCALARTYPE (SCALARELEMENT*)>
<!ATTLIST SCALARTYPE %COMMONATTS;>

<!ELEMENT SCALARELEMENT (#PCDATA)>
<!ATTLIST SCALARELEMENT %COMMONATTS;>

<!ELEMENT DATATYPE (CONSTRUCTOR*)>
<!ATTLIST DATATYPE %COMMONATTS;>

<!ELEMENT CONSTRUCTOR (IDENTIFIER, ACCESSOR*)>
<!ATTLIST CONSTRUCTOR %COMMONATTS;>

<!ELEMENT ACCESSOR (IDENTIFIER, %TYPE;)>
<!ATTLIST ACCESSOR %COMMONATTS;>

<!ELEMENT TYPENAME (%NAME;)>
<!ATTLIST TYPENAME %COMMONATTS;>

<!ELEMENT QUALIFIEDTYPENAME (%QUALIFIEDNAME;)>
<!ATTLIST QUALIFIEDTYPENAME %COMMONATTS;>

<!ELEMENT SUBRANGE (%BOUND;, %BOUND;)>
<!ATTLIST SUBRANGE %COMMONATTS;>

<!ELEMENT ARRAYTYPE (%INDEXTYPE;, %TYPE;)>
<!ATTLIST ARRAYTYPE %COMMONATTS;>

<!ELEMENT TUPLETYPE ((%TYPEORVARDECL;)*)>
<!ATTLIST TUPLETYPE %COMMONATTS;>

<!ELEMENT RECORDTYPE (FIELDDECLARATION*)>
<!ATTLIST RECORDTYPE %COMMONATTS;>

<!ELEMENT FIELDDECLARATION (IDENTIFIER, %TYPE;)>
<!ATTLIST FIELDDECLARATION %COMMONATTS;>

<!ELEMENT FUNCTIONTYPE (%TYPEORVARDECL;, %TYPE;)>
<!ATTLIST FUNCTIONTYPE %COMMONATTS;>

<!ELEMENT SUBTYPE (%EXPRESSION;)>
<!ATTLIST SUBTYPE %COMMONATTS;>

<!ELEMENT STATETYPE (%MODULE;)>
<!ATTLIST STATETYPE %COMMONATTS;>

<!ELEMENT NEXTOPERATOR (NAMEEXPR)>
<!ATTLIST NEXTOPERATOR %COMMONATTS;
                       PARENS CDATA "0">

<!ELEMENT NAMEEXPR (%NAME;)>
<!ATTLIST NAMEEXPR %COMMONATTS;
                   PARENS CDATA "0">

<!ELEMENT QUALIFIEDNAMEEXPR (%QUALIFIEDNAME;)>
<!ATTLIST QUALIFIEDNAMEEXPR %COMMONATTS;
                            PARENS CDATA "0">

<!-- APPLICATIONS have 2 parts: the operator and the argument, which -->
<!--   is a TUPLEEXPRESSION for functions of arity > 1 -->
<!-- "A AND B" is an <APPLICATION INFIX="YES">, with operator AND -->
<!ELEMENT APPLICATION (%EXPRESSION;, %EXPRESSION;)>
<!ATTLIST APPLICATION %COMMONATTS;
                      INFIX (YES|NO) "NO"
                      UNARY (YES|NO) "NO"
                      PARENS CDATA "0">

<!ELEMENT ARRAYSELECTION (%EXPRESSION;, %EXPRESSION;)>
<!ATTLIST ARRAYSELECTION %COMMONATTS;
                         PARENS CDATA "0">

<!ELEMENT RECORDSELECTION (%EXPRESSION;, IDENTIFIER)>
<!ATTLIST RECORDSELECTION %COMMONATTS;
                          PARENS CDATA "0">

<!ELEMENT TUPLESELECTION (%EXPRESSION;, NUMERAL)>
<!ATTLIST TUPLESELECTION %COMMONATTS;
                         PARENS CDATA "0">

<!ELEMENT RECORDLITERAL (RECORDENTRY*)>
<!ATTLIST RECORDLITERAL %COMMONATTS;
                        PARENS CDATA "0">

<!ELEMENT RECORDENTRY (IDENTIFIER, %EXPRESSION;)>
<!ATTLIST RECORDENTRY %COMMONATTS;>

<!ELEMENT TUPLELITERAL ((%EXPRESSION;)*)>
<!ATTLIST TUPLELITERAL %COMMONATTS;
                       PARENS CDATA "0">

<!ELEMENT UPDATEEXPRESSION (%EXPRESSION;, %EXPRESSION;, %EXPRESSION;)>
<!ATTLIST UPDATEEXPRESSION %COMMONATTS;
                           PARENS CDATA "0">

<!ELEMENT ARRAYLITERAL (INDEXVARDECL, %EXPRESSION;)>
<!ATTLIST ARRAYLITERAL %COMMONATTS;
                       PARENS CDATA "0">

<!ELEMENT INDEXVARDECL (IDENTIFIER, %INDEXTYPE;)>
<!ATTLIST INDEXVARDECL %COMMONATTS;>

<!ELEMENT LAMBDAABSTRACTION (VARDECLS, %EXPRESSION;)>
<!ATTLIST LAMBDAABSTRACTION %COMMONATTS;
                            PARENS CDATA "0">

<!ELEMENT QUANTIFIEDEXPRESSION (QUANTIFIER, VARDECLS, %EXPRESSION;)>
<!ATTLIST QUANTIFIEDEXPRESSION %COMMONATTS;
                               PARENS CDATA "0">

<!-- FORALL | EXISTS -->
<!ELEMENT QUANTIFIER (#PCDATA)>
<!ATTLIST QUANTIFIER %COMMONATTS;>

<!ELEMENT LETEXPRESSION (LETDECLARATIONS, %EXPRESSION;)>
<!ATTLIST LETEXPRESSION %COMMONATTS;
                        PARENS CDATA "0">

<!ELEMENT LETDECLARATIONS ((LETDECLARATION)*)>
<!ATTLIST LETDECLARATIONS %COMMONATTS;>

<!ELEMENT LETDECLARATION (IDENTIFIER, %TYPE;, %EXPRESSION;)>
<!ATTLIST LETDECLARATION %COMMONATTS;>

<!ELEMENT SETPREDEXPRESSION (IDENTIFIER, %TYPE;, %EXPRESSION;)>
<!ATTLIST SETPREDEXPRESSION %COMMONATTS;
                            PARENS CDATA "0">

<!ELEMENT SETLISTEXPRESSION ((%EXPRESSION;)*)>
<!ATTLIST SETLISTEXPRESSION %COMMONATTS;
                            PARENS CDATA "0">

<!ELEMENT CONDITIONAL (%EXPRESSION;, %EXPRESSION;, %EXPRESSION;)>
<!ATTLIST CONDITIONAL %COMMONATTS;
                      ELSIF (YES|NO) "NO"
                      PARENS CDATA "0">

<!ELEMENT MODINIT (%MODULE;)>
<!ATTLIST MODINIT %COMMONATTS;
                      PARENS CDATA "0">

<!ELEMENT MODTRANS (%MODULE;)>
<!ATTLIST MODTRANS %COMMONATTS;
                      PARENS CDATA "0">

<!ELEMENT NUMERAL (#PCDATA)>
<!ATTLIST NUMERAL %COMMONATTS;
                  PARENS CDATA "0">

<!ELEMENT STRINGEXPR (#PCDATA)>
<!ATTLIST STRINGEXPR %COMMONATTS;
                     PARENS CDATA "0">

<!ELEMENT VARDECL (IDENTIFIER, %TYPE;)>
<!ATTLIST VARDECL
        %COMMONATTS;
        CHAIN (YES|NO) "NO">

<!ELEMENT TYPEDECL (IDENTIFIER)>
<!ATTLIST TYPEDECL %COMMONATTS;>

<!ELEMENT IDENTIFIERS (IDENTIFIER*)>
<!ATTLIST IDENTIFIERS %COMMONATTS;>

<!ELEMENT IDENTIFIER (#PCDATA)>
<!ATTLIST IDENTIFIER %COMMONATTS;>

<!ELEMENT ASSERTIONDECLARATION (IDENTIFIER,ASSERTIONFORM,%ASSERTIONEXPRESSION;)>
<!ATTLIST ASSERTIONDECLARATION %COMMONATTS;>

<!-- ASSERTIONFORM is one of OBLIGATION, CLAIM, LEMMA, THEOREM -->
<!ELEMENT ASSERTIONFORM (#PCDATA)>
<!ATTLIST ASSERTIONFORM %COMMONATTS;>

<!ELEMENT ASSERTIONPROPOSITION (ASSERTIONOPERATOR,((%ASSERTIONEXPRESSION;)*))>
<!ATTLIST ASSERTIONPROPOSITION %COMMONATTS;>

<!ELEMENT ASSERTIONOPERATOR (#PCDATA)>
<!ATTLIST ASSERTIONOPERATOR %COMMONATTS;>

<!ELEMENT QUANTIFIEDASSERTION (QUANTIFIER, VARDECLS, %ASSERTIONEXPRESSION;)>
<!ATTLIST QUANTIFIEDASSERTION %COMMONATTS;>

<!ELEMENT MODULEMODELS (%MODULE;, %EXPRESSION;)>
<!ATTLIST MODULEMODELS %COMMONATTS;>

<!ELEMENT MODULEIMPLEMENTS (%MODULE;, %MODULE;)>
<!ATTLIST MODULEIMPLEMENTS %COMMONATTS;>
