plugins/contracts/org.polarsys.chess.contracts.verificationService.test.runtime/resources/tools/xSAP/data/schema/tfpg.xsd

<?xml version="1.0"?>
<xsd:schema
  xmlns:xsd="http://www.w3.org/2001/XMLSchema"
  elementFormDefault="qualified">


  <!-- TFPG -->

  <xsd:element name="tfpg" type="tfpgType" />

  <xsd:complexType name="tfpgType">
    <xsd:sequence>
      <xsd:element name="nodesList" type="nodesListType" />
      <xsd:element name="modesList" type="modesListType" />
      <xsd:element name="edgesList" type="edgesListType" />
    </xsd:sequence>
    <xsd:attribute name="name" type="identifierType" />
    <xsd:attribute name="infty_semantics" type="xsd:string" />
  </xsd:complexType>



  <!-- Nodes -->

  <xsd:complexType name="nodesListType">
    <xsd:sequence>
       <xsd:element name="node" type="nodeType" maxOccurs="unbounded" />
    </xsd:sequence>
  </xsd:complexType>

  <xsd:complexType name="nodeType">
    <xsd:sequence>
      <xsd:element name="type" type="nodeValType" />
    </xsd:sequence>
    <xsd:attribute name="name" type="identifierType" />
    <xsd:attribute name="isMonitored" type="xsd:boolean" use="optional"/>
  </xsd:complexType>



  <!-- Modes -->

  <xsd:complexType name="modesListType">
    <xsd:sequence>
      <xsd:element name="mode" type="identifierType" maxOccurs="unbounded" />
    </xsd:sequence>
  </xsd:complexType>


  <!-- Edges -->

  <xsd:complexType name="edgesListType">
    <xsd:sequence>
      <xsd:element name="edge" type="edgeType" minOccurs="0" maxOccurs="unbounded" />
    </xsd:sequence>
  </xsd:complexType>

  <xsd:complexType name="edgeType">
    <xsd:sequence>
      <xsd:element name="srcNode" type="identifierType" />
      <xsd:element name="tMin" type="xsd:float" />
      <xsd:element name="tMax" type="xsd:float" />
      <xsd:element name="modesList" type="modesListType" />
      <xsd:element name="destNode" type="identifierType" />
    </xsd:sequence>
    <xsd:attribute name="name" type="identifierType" />
  </xsd:complexType>

  <!-- Define the type of an Identifier -->

  <xsd:simpleType name="identifierType">
    <xsd:restriction base="xsd:string">
      <xsd:pattern value="([a-zA-Z0-9_-])+"/>
    </xsd:restriction>
  </xsd:simpleType>

  <!-- Define the type of a Node -->
  <xsd:simpleType name="nodeValType">
    <xsd:restriction base="xsd:string">
      <xsd:enumeration value="AND"/>
      <xsd:enumeration value="OR"/>
      <xsd:enumeration value="FM"/>
    </xsd:restriction>
  </xsd:simpleType>

</xsd:schema>