<?xml version="1.0" encoding="UTF-8"?>
<!--
	Hybrid Logic Model Checker 1.0 - HL Kripke Structure DTD

	Copyright (C) 2005 Luigi Dragone
	
	This program is free software; you can redistribute it and/or modify 	
	it under the terms of the GNU General Public License as published by 
	the Free Software Foundation; version 2.

	This program is distributed in the hope that it will be useful,
	but WITHOUT ANY WARRANTY; without even the implied warranty of
	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
	GNU General Public License for more details.
 
	You should have received a copy of the GNU General Public License
	along with this program; if not, write to the Free Software
	Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA  02111-1307, USA.

	Luigi Dragone <luigi@luigidragone.com>
-->
<!-- document root element, an HL Kripke structure is defined in terms of worlds, 
	 modalities, propositional symbol and nominal -->
<!ELEMENT hl-kripke-struct (world+,modality*,prop-sym*,nominal*)>
<!-- name of the Kripke structure -->
<!ATTLIST hl-kripke-struct 
					name CDATA "M">
<!-- definition of a model's world -->
<!ELEMENT world EMPTY>
<!-- the identifying label of the world in the model and formulas -->
<!ATTLIST world 
					label ID #REQUIRED>
<!-- definition of a modality relation as a collection of access pair -->
<!ELEMENT modality (acc-pair*)>
<!-- the identifying label of the modality in the model and formulas -->
<!ATTLIST modality
					label ID #REQUIRED>
<!-- definition of an access pair in a modality -->
<!ELEMENT acc-pair EMPTY>					
<!-- references to source and target world labels of the access pair -->
<!ATTLIST acc-pair
					from-world-label IDREF #REQUIRED
					to-world-label IDREF #REQUIRED>
<!-- definition of a propositional symbol -->
<!ELEMENT prop-sym EMPTY>
<!-- the identifying label of the propositional symbols in the model and 
	 formulas and its truth assignment as the collection of the labels of the 
	 worlds in which the symbol is true -->
<!ATTLIST prop-sym
					label ID #REQUIRED
					truth-assignments IDREFS #IMPLIED>
<!-- definition of a nominal -->
<!ELEMENT nominal EMPTY>
<!-- the identifying label of the nominal in the model and formulas and its 
	 truth assignment as the the label of the world to which the nominal is 
	 assigned -->
<!ATTLIST nominal
					label ID #REQUIRED
					truth-assignment IDREF #REQUIRED>