<?xml version="1.0" encoding="UTF-8"?>
<!--promela.dtd version 1.0-->
<!--Author: Estefania Rosales Montes-->
<!--GISUM Group. University of Malaga. 9/01-->
<!--claim: never; events: trace - notrace-->
<!ELEMENT model (proc | init | never | (trace | notrace) | declaration | typedef | inline)+>
<!-- proc definition -->
<!-- decl: parameters -->
<!ELEMENT proc (parameters?, priority?, Opt_enabler?, body)>
<!ATTLIST proc
	instances CDATA #IMPLIED
	type (PROCTYPE | D_PROCTYPE) #REQUIRED
	name CDATA #REQUIRED
>
<!ELEMENT priority (#PCDATA)>
<!ELEMENT parameters (declaration+)>
<!ELEMENT declaration (var+ | enumtype)>
<!ATTLIST declaration
	vis (HIDDEN | SHOW | ISLOCAL) #IMPLIED
	typename (BIT | BOOL | BYTE | SHORT | INT | MTYPE | CHANNEL | UNSIGNED | TYPEDEF) #REQUIRED
	name CDATA #IMPLIED
>
<!ELEMENT var (messages)?>
<!ATTLIST var
	name CDATA #REQUIRED
	value CDATA #IMPLIED
	array_elements CDATA #IMPLIED
>
<!ELEMENT messages (field+)>
<!ATTLIST messages
	number CDATA #REQUIRED
	synchronous (yes | no) #REQUIRED
>
<!ELEMENT field EMPTY>
<!ATTLIST field
	type (BIT | BOOL | BYTE | SHORT | INT | MTYPE | CHANNEL | UNSIGNED | STRUCT) #REQUIRED
>
<!ELEMENT enumtype (enumelement+)>
<!ELEMENT enumelement EMPTY>
<!ATTLIST enumelement
	name CDATA #REQUIRED
>
<!ENTITY % varref "(var | array | struct)">
<!--We define statements as entity including all sentences existing in promela-->
<!ENTITY % Special_statements "(receive | send | if | do | break | goto | labeled_statement)">
<!ENTITY % Special_expression "(run | len | enabled | const | receive | %varref; | timeout | nonprogress | pc_val |  remote_reference | channel_test | conditional_expression | unary_expression)">
<!ENTITY % Other_statements "(debug | assert | else | atomic | non_atomic | d_step | inlinecall |  (expression | %Special_expression;) )">
<!--full-expr: ((expression| %Special_expresion;)|other_expresion-->
<!--sequence entity includes information contained in  body, option, d_step, atomic, sequence-->
<!ENTITY % sequence "(declaration | xuexclusive | (%Special_statements; | %Other_statements;) | unless)">
<!--La entidad varref sirve para definir los diferentes tipos de referencia a variables que se dan en un prog.-->
<!ELEMENT struct ((var | array), struct_field+)>
<!ELEMENT struct_field (index?)>
<!ATTLIST struct_field
	name CDATA #REQUIRED
>
<!ELEMENT array (var, index)>
<!ELEMENT index (var | expression | %Special_expression;)>
<!ELEMENT const (#PCDATA)>
<!--   type (skip | false | true) #IMPLIED all are const-->
<!ELEMENT body (%sequence;)+>
<!--xuexclusive , falta por detallar-->
<!ELEMENT xuexclusive (%varref;)+>
<!ATTLIST xuexclusive
	exclusive (xr | xs) #REQUIRED
>
<!--Elementos que componen la entidad %Special_statements-->
<!ELEMENT channel (%varref;)>
<!ELEMENT receive (channel, receive_arguments)>
<!ATTLIST receive
	rtype (normal | random | fifo_poll | random_receive_poll | fifopoll_nosideeffect | random_receive_poll_nosideeffect) #REQUIRED
 >
<!ELEMENT send (channel, send_arguments)>
<!ATTLIST send
	mtype (fifo_send | sorted_send) #REQUIRED
>
<!ELEMENT if (option+)>
<!ELEMENT do (option+)>
<!ELEMENT break EMPTY>
<!ELEMENT goto EMPTY>
<!ATTLIST goto
	label_name CDATA #REQUIRED
>
<!ELEMENT labeled_statement (%Special_statements; | %Other_statements;)>
<!ATTLIST labeled_statement
	label_name CDATA #REQUIRED
>
<!--Fin de elementos que componen la entidad %Special_statements-->
<!--Elementos que componen  la entidad %Other_statements-->
<!ELEMENT else EMPTY>
<!ELEMENT atomic (%sequence;)+>
<!ELEMENT non_atomic (%sequence;)+>
<!ELEMENT d_step (%sequence;)+>
<!ELEMENT debug (string, debug_arguments?)>
<!ELEMENT assert (expression | %Special_expression;)>
<!--Fin de elementos de la entidad %Other_statements-->
<!-- Elementos que componen la entidad %Special_expression-->
<!ELEMENT run (run_arguments?)>
<!ATTLIST run
	name CDATA #REQUIRED
	priority CDATA #IMPLIED
>
<!ELEMENT run_arguments (expression | %Special_expression;)+>
<!ELEMENT len (channel)>
<!ELEMENT enabled (expression | %Special_expression;)>
<!ELEMENT timeout EMPTY>
<!ELEMENT nonprogress EMPTY>
<!ELEMENT pc_val (expression | %Special_expression;)>
<!ELEMENT remote_reference (expression | %Special_expression;)>
<!ATTLIST remote_reference
	proctype_name CDATA #REQUIRED
	label_name CDATA #REQUIRED
>
<!--Nota: Los elementos channel_test no se pueden negar-->
<!ELEMENT channel_test (channel)>
<!ATTLIST channel_test
	type (full | nfull | empty | nempty) #REQUIRED
>
<!-- Fin de elementos de la entidad %Special_expression-->
<!ELEMENT option (%sequence;)+>
<!ELEMENT eval_operator (expression | %Special_expression;)>
<!ELEMENT receive_arguments (expression | %Special_expression; | eval_operator)+>
<!ELEMENT send_arguments (expression | %Special_expression;)+>
<!ELEMENT debug_arguments (expression | %Special_expression;)+>
<!ELEMENT string (#PCDATA)>
<!--expression son las expresiones tipo exp op exp, asgn, incr,decr,probe-->
<!ELEMENT expression (left, right?)>
<!ATTLIST expression
	type (ADD | SUBST | MULT | MOD | DIV | BINAND | BINXOR | BINOR | GT | LT | GE | LE | EQ | NE | AND | OR | LSHIFT | RSHIFT | COMP1 | MINUS | NEG | ASGN | INCR | DECR) #REQUIRED
>
<!ELEMENT unary_expression (expression | %Special_expression;)>
<!ATTLIST unary_expression
	type (COMP1 | MINUS | NEG) #REQUIRED
>
<!ELEMENT left (expression | %Special_expression;)>
<!ELEMENT right (expression | %Special_expression;)>
<!ELEMENT conditional_expression (condition, on_true, on_false)>
<!ELEMENT condition (expression | %Special_expression;)>
<!ELEMENT on_true (expression | %Special_expression;)>
<!ELEMENT on_false (expression | %Special_expression;)>
<!--model: unless-->
<!ELEMENT unless (normal_seq, escape_seq)>
<!ELEMENT normal_seq (%Special_statements; | %Other_statements;)>
<!ELEMENT escape_seq (%Special_statements; | %Other_statements;)>
<!-- model: init-->
<!ELEMENT init (body)>
<!ATTLIST init
	priority CDATA #IMPLIED
>
<!--  model: claim -> never-->
<!ELEMENT never (body)>
<!--model: events -> trace-->
<!ELEMENT trace (body)>
<!--model: events -> notrace-->
<!ELEMENT notrace (body)>
<!-- model: utype-->
<!ELEMENT typedef (declaration+)>
<!ATTLIST typedef
	name CDATA #REQUIRED
>
<!-- model ->inline (ns) -->
<!ELEMENT inline (inline_arguments?, inline_body)>
<!ATTLIST inline
	name CDATA #REQUIRED
>
<!ELEMENT inlinecall (inline_arguments?)>
<!ATTLIST inlinecall
	name CDATA #REQUIRED
>
<!ELEMENT inline_arguments (expression | %Special_expression;)+>
<!ELEMENT inline_body (#PCDATA)>
<!ELEMENT Opt_enabler (expression | %Special_expression;)>