<xsd:schema xmlns:xsd="http://www.w3.org/2001/XMLSchema">

  <xsd:element name="alloy" type="AlloyType"/>

  <xsd:complexType name="AlloyType">
    <xsd:sequence>
      <xsd:element name="instance" type="InstanceType" minOccurs="1" maxOccurs="unbounded"/>
      <xsd:element name="source"   type="SourceType"   minOccurs="0" maxOccurs="unbounded"/>
    </xsd:sequence>
    <xsd:attribute name="builddate" type="xsd:string"/>
  </xsd:complexType>

  <xsd:complexType name="InstanceType">
    <xsd:choice minOccurs="0" maxOccurs="unbounded">
      <xsd:element name="sig"    type="SigType"    minOccurs="1" maxOccurs="1"/>
      <xsd:element name="skolem" type="SkolemType" minOccurs="1" maxOccurs="1"/>
      <xsd:element name="field"  type="FieldType"  minOccurs="1" maxOccurs="1"/>
    </xsd:choice>
    <xsd:attribute name="bitwidth"  type="xsd:string" use="required"/>
    <xsd:attribute name="maxseq"    type="xsd:string" use="required"/>
    <xsd:attribute name="filename"  type="xsd:string"/>
    <xsd:attribute name="command"   type="xsd:string"/>
    <xsd:attribute name="metamodel" type="xsd:string"/>
  </xsd:complexType>

  <xsd:complexType name="SigType">
    <xsd:sequence>
       <xsd:element name="atom" type="AtomType" minOccurs="0" maxOccurs="unbounded"/>
       <xsd:element name="type" type="TypeType" minOccurs="0" maxOccurs="unbounded"/>
    </xsd:sequence>
    <xsd:attribute name="ID"       type="xsd:string" use="required"/>
    <xsd:attribute name="label"    type="xsd:string"/>
    <xsd:attribute name="parentID" type="xsd:string"/>
    <xsd:attribute name="builtin"  type="xsd:string"/>
    <xsd:attribute name="abstract" type="xsd:string"/>
    <xsd:attribute name="one"      type="xsd:string"/>
    <xsd:attribute name="lone"     type="xsd:string"/>
    <xsd:attribute name="some"     type="xsd:string"/>
    <xsd:attribute name="private"  type="xsd:string"/>
    <xsd:attribute name="leaf"     type="xsd:string"/>
    <xsd:attribute name="meta"     type="xsd:string"/>
  </xsd:complexType>

  <xsd:complexType name="FieldType">
    <xsd:sequence>
       <xsd:element name="tuple" type="TupleType" minOccurs="0" maxOccurs="unbounded"/>
       <xsd:element name="types" type="TypesType" minOccurs="1" maxOccurs="unbounded"/>
    </xsd:sequence>
    <xsd:attribute name="ID"       type="xsd:string" use="required"/>
    <xsd:attribute name="label"    type="xsd:string"/>
    <xsd:attribute name="parentID" type="xsd:string" use="required"/>
    <xsd:attribute name="private"  type="xsd:string"/>
    <xsd:attribute name="meta"     type="xsd:string"/>
  </xsd:complexType>

  <xsd:complexType name="SkolemType">
    <xsd:sequence>
       <xsd:element name="tuple" type="TupleType" minOccurs="0" maxOccurs="unbounded"/>
       <xsd:element name="types" type="TypesType" minOccurs="1" maxOccurs="unbounded"/>
    </xsd:sequence>
    <xsd:attribute name="ID"       type="xsd:string" use="required"/>
    <xsd:attribute name="label"    type="xsd:string"/>
  </xsd:complexType>

  <xsd:complexType name="AtomType">
    <xsd:attribute name="label" type="xsd:string" use="required"/>
  </xsd:complexType>

  <xsd:complexType name="TypeType">
    <xsd:attribute name="ID" type="xsd:string" use="required"/>
  </xsd:complexType>

  <xsd:complexType name="TypesType">
    <xsd:sequence>
       <xsd:element name="type" type="TypeType" minOccurs="1" maxOccurs="unbounded"/>
    </xsd:sequence>
  </xsd:complexType>

  <xsd:complexType name="TupleType">
    <xsd:sequence>
       <xsd:element name="atom" type="AtomType" minOccurs="1" maxOccurs="unbounded"/>
    </xsd:sequence>
  </xsd:complexType>

  <xsd:complexType name="SourceType">
    <xsd:attribute name="filename" type="xsd:string" use="required"/>
    <xsd:attribute name="content"  type="xsd:string" use="required"/>
  </xsd:complexType>

</xsd:schema>