plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/data/schema/fe.dtd

<!--
     Author: Alessandro Mariotti
     Date:   2011.11.18

     Author: Roberto Cavada
     Date:   2014.07.22  (Common Cause)
     Date:   2014.09.05  (fei text support)
-->

<!ENTITY % lineattr
'lineno   CDATA       #IMPLIED'>


<!ELEMENT fault_extension (extensions, common_causes?)>
<!ATTLIST fault_extension
          name CDATA #REQUIRED
          smv_file CDATA #REQUIRED
          fei_txt CDATA #IMPLIED
          %lineattr;>
<!ELEMENT extensions (nominal_component_extensions*)>
<!ELEMENT nominal_component_extensions (fault_models)>
<!ATTLIST nominal_component_extensions
          module CDATA #REQUIRED
          desc CDATA #IMPLIED
          %lineattr;>

<!ELEMENT fault_models (fault_model)*>
<!ELEMENT fault_model (instances?, fault_modes?, global_dynamics_model?)>

<!ATTLIST fault_model
          name CDATA #REQUIRED
          symbols CDATA #REQUIRED
          desc CDATA #IMPLIED
          %lineattr;>

<!ELEMENT instances (pat)*>
<!ELEMENT pat (#PCDATA)>

<!ELEMENT fault_modes (fault_mode)*>

<!ELEMENT fault_mode (effects_model?, local_dynamics_model?, latent?)>

<!ATTLIST fault_mode
          name CDATA #REQUIRED
          symbols CDATA #REQUIRED
          probability CDATA #IMPLIED
          %lineattr;>

<!ELEMENT effects_model (values?, effect?, raw?)>

<!ATTLIST effects_model
          name CDATA #REQUIRED
          %lineattr;>

<!ELEMENT latent EMPTY>

<!ATTLIST latent
          is_latent (yes | no) #REQUIRED
          probability CDATA #IMPLIED
          %lineattr;>

<!ELEMENT values (input | output)*>

<!ELEMENT input EMPTY>

<!ATTLIST input
          reads CDATA #REQUIRED
          value CDATA #IMPLIED>

<!ELEMENT output EMPTY>

<!ATTLIST output
          reads CDATA #REQUIRED
          writes CDATA #REQUIRED
          binds CDATA #REQUIRED
          type CDATA #REQUIRED>

<!ELEMENT effect ((during, entering) | (entering, during))>

<!ELEMENT raw (#PCDATA)>

<!ELEMENT entering (#PCDATA)>

<!ATTLIST entering
          language (smv) #IMPLIED>

<!ELEMENT during (#PCDATA)>

<!ATTLIST during
          language (smv) #IMPLIED>

<!-- Here we mean that each tag MUST appear once, no matter the order.-->

<!ELEMENT local_dynamics_model (events?, transitions?, raw?)>

<!ATTLIST local_dynamics_model
          name CDATA #REQUIRED
          desc CDATA #IMPLIED
          %lineattr;>

<!ELEMENT events (event)*>

<!ELEMENT event EMPTY>

<!ATTLIST event
          type (input | output) #REQUIRED
          name CDATA #REQUIRED
          connected (yes | no) #REQUIRED
          value CDATA #IMPLIED
          binds CDATA #IMPLIED
          %lineattr;>

<!ELEMENT transitions (transition)*>

<!ELEMENT transition (trigger | guard)*>

<!ATTLIST transition
          from CDATA #REQUIRED
          to CDATA #REQUIRED
          %lineattr;>

<!ELEMENT trigger (#PCDATA)>

<!ELEMENT guard (#PCDATA)>

<!ELEMENT global_dynamics_model (events?, transitions?)>
<!ATTLIST global_dynamics_model
          %lineattr;>

<!--
     Common Cause stuff
-->
<!ELEMENT common_causes (cause)*>
<!ELEMENT cause (cc_module)*>
<!ATTLIST cause
	  name CDATA #REQUIRED
	  desc CDATA #IMPLIED
          probability CDATA #IMPLIED
          %lineattr;>
<!ELEMENT cc_module (instances?, cc_mode*)>
<!ATTLIST cc_module
	  name CDATA #REQUIRED
	  desc CDATA #IMPLIED
          %lineattr;>
<!ELEMENT cc_mode (cc_range)>
<!ATTLIST cc_mode
	  slice CDATA #REQUIRED
	  mode CDATA #REQUIRED
          %lineattr;>
<!ELEMENT cc_range EMPTY>
<!ATTLIST cc_range
          low CDATA #REQUIRED
          high CDATA #REQUIRED
          %lineattr;>