将WS-CDL转换为事件B [英] Convert WS-CDL to Event B

问题描述

亲爱的大家！

请帮我编写将ws-cdl格式的文件转换为事件B的程序，并且可以由Rodin Platform读取.

Dear everybody !

Please, help me write program convert file ws-cdl format to Event B and it is can read by Rodin Platform.

<?xml version="1.0" encoding="UTF-8"?>
<schema xmlns="http://www.w3.org/2001/XMLSchema"

    xmlns:cdl="http://www.w3.org/2005/10/cdl"

    targetNamespace="http://www.w3.org/2005/10/cdl"

    elementFormDefault="qualified">

  <complexType name="tExtensibleElements">
    <annotation>
      <documentation>
        This type is extended by other WS-CDL component types to allow 
          elements and attributes from other namespaces to be added. 
        This type also contains the optional description element that 
        is applied to all WS-CDL constructs.
       </documentation>
    </annotation>
    <sequence>
      <element name="description" minOccurs="0">
        <complexType mixed="true">
          <sequence minOccurs="0" maxOccurs="unbounded">
            <any processContents="lax"/>
          </sequence>
          <attribute name="type" type="cdl:tDescriptionType" use="optional" 

                 default="documentation"/>
        </complexType>
      </element>
      <element name="CDLExtension" minOccurs="0" maxOccurs="unbounded">
        <complexType>
          <sequence minOccurs="0" maxOccurs="unbounded">
            <any processContents="lax"/>
          </sequence>
        </complexType>
      </element>
    </sequence>
    <anyAttribute namespace="##other" processContents="lax"/>
  </complexType>

    <element name="package" type="cdl:tPackage"/>
    
  <complexType name="tPackage">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="informationType" type="cdl:tInformationType" 

                  minOccurs="0" maxOccurs="unbounded"/>
          <element name="token" type="cdl:tToken" minOccurs="0"

                  maxOccurs="unbounded"/>
          <element name="tokenLocator" type="cdl:tTokenLocator" 

                  minOccurs="0" maxOccurs="unbounded"/>
          <element name="roleType" type="cdl:tRoleType" minOccurs="0"

                  maxOccurs="unbounded"/>
          <element name="relationshipType" type="cdl:tRelationshipType" 

                  minOccurs="0" maxOccurs="unbounded"/>
          <element name="participantType" type="cdl:tParticipantType" 

                  minOccurs="0" maxOccurs="unbounded"/>
          <element name="channelType" type="cdl:tChannelType"

                  minOccurs="0" maxOccurs="unbounded"/>
          <element name="choreography" type="cdl:tChoreography" 

                  minOccurs="0" maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="author" type="string" use="optional"/>
        <attribute name="version" type="string" use="optional"/>
        <attribute name="targetNamespace" type="anyURI" 

                 use="required"/>
      </extension>
    </complexContent>
  </complexType>
    
  <complexType name="tInformationType">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="type" type="QName" use="optional"/>
        <attribute name="element" type="QName" use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tToken">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="informationType" type="QName"

                 use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tTokenLocator">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="tokenName" type="QName" use="required"/>
        <attribute name="informationType" type="QName"

                 use="required"/>
        <attribute name="part" type="NCName" use="optional" />
        <attribute name="query" type="cdl:tXPath-expr" 

                 use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRoleType">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="behavior" type="cdl:tBehavior"

                  maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tBehavior">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="interface" type="QName" use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRelationshipType">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="roleType" type="cdl:tRoleRef" minOccurs="2"

                  maxOccurs="2"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRoleRef">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="typeRef" type="QName" use="required"/>
        <attribute name="behavior" use="optional">
          <simpleType>
             <list itemType="NCName"/>
          </simpleType>
        </attribute>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tParticipantType">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="roleType" type="cdl:tRoleRef2" 

                  maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRoleRef2">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="typeRef" type="QName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tChannelType">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="passing" type="cdl:tPassing" minOccurs="0"

                  maxOccurs="unbounded"/>
          <element name="roleType" type="cdl:tRoleRef3"/>
          <element name="reference" type="cdl:tReference"/>
          <element name="identity" type="cdl:tIdentity" minOccurs="0" 

                  maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="usage" type="cdl:tUsage" use="optional" 

                     default="distinct"/>
        <attribute name="action" type="cdl:tAction" use="optional"

                     default="request"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRoleRef3">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="typeRef" type="QName" use="required"/>
        <attribute name="behavior" type="NCName" use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tPassing">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="channel" type="QName" use="required"/>
        <attribute name="action" type="cdl:tAction" use="optional" 

                 default="request"/>
        <attribute name="new" type="boolean" use="optional"

                 default="false"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tReference">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="token" type="cdl:tTokenReference"

                      minOccurs="1" maxOccurs="1"/>
        </sequence>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tTokenReference">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="name" type="QName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tIdentity">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="token" type="cdl:tTokenReference" 

                  minOccurs="1" maxOccurs="unbounded"/>
        </sequence>
        <attribute name="usage" type="cdl:tUsageI" use="optional" 

                     default="primary"/>
      </extension>
    </complexContent>
  </complexType>


  <complexType name="tChoreography">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="relationship" type="cdl:tRelationshipRef" 

                  maxOccurs="unbounded"/>
          <element name="variableDefinitions"

                  type="cdl:tVariableDefinitions" minOccurs="0"/>
          <element name="choreography" type="cdl:tChoreography"

                   minOccurs="0" maxOccurs="unbounded"/>
          <group ref="cdl:activity"/>
          <element name="exceptionBlock" type="cdl:tException"

                  minOccurs="0"/>
          <element name="finalizerBlock" type="cdl:tFinalizer"

                      minOccurs="0" maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="complete" type="cdl:tBoolean-expr" 

                     use="optional"/>
        <attribute name="isolation" type="boolean" 

                     use="optional" default="false"/>
        <attribute name="root" type="boolean" use="optional" 

                     default="false"/>
        <attribute name="coordination" type="boolean" use="optional" 

                     default="false"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRelationshipRef">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="type" type="QName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tVariableDefinitions">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="variable" type="cdl:tVariable"

                  maxOccurs="unbounded"/>
        </sequence>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tVariable">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="informationType" type="QName" 

                 use="optional"/>
        <attribute name="channelType" type="QName" use="optional"/>
        <attribute name="mutable" type="boolean" use="optional"

                 default="true"/>
        <attribute name="free" type="boolean" use="optional" 

                 default="false"/>
        <attribute name="silent" type="boolean" use="optional"

                 default="false"/>
        <attribute name="roleTypes" use="optional">
           <simpleType>
              <list itemType="QName"/>
           </simpleType>
        </attribute>
      </extension>
    </complexContent>
  </complexType>

  <group name="activity">
    <choice>
      <element name="sequence" type="cdl:tSequence"/>
      <element name="parallel" type="cdl:tParallel"/>
      <element name="choice" type="cdl:tChoice"/>
      <element name="workunit" type="cdl:tWorkunit"/>
      <element name="interaction" type="cdl:tInteraction"/>
      <element name="perform" type="cdl:tPerform"/>
      <element name="assign" type="cdl:tAssign"/>
      <element name="silentAction" type="cdl:tSilentAction"/>
      <element name="noAction" type="cdl:tNoAction"/>
      <element name="finalize" type="cdl:tFinalize"/>
      <any namespace="##other" processContents="lax"/>
    </choice>
  </group>

  <complexType name="tSequence">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <group ref="cdl:activity" maxOccurs="unbounded"/>
        </sequence>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tParallel">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <group ref="cdl:activity" maxOccurs="unbounded"/>
        </sequence>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tChoice">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <group ref="cdl:activity" maxOccurs="unbounded"/>
        </sequence>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tWorkunit">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <group ref="cdl:activity"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="guard" type="cdl:tBoolean-expr" 

                 use="optional"/>
        <attribute name="repeat" type="cdl:tBoolean-expr" 

                 use="optional"/>
        <attribute name="block" type="boolean" 

                 use="optional" default="false"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tPerform">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="bind" type="cdl:tBind" 

                  minOccurs="0" maxOccurs="unbounded"/>
          <element name="choreography" type="cdl:tChoreography"

                   minOccurs="0" maxOccurs="1"/>
        </sequence>
        <attribute name="choreographyName" type="QName" use="required"/>
        <attribute name="choreographyInstanceId" type="cdl:tXPath-expr" use="optional"/>
        <attribute name="block" type="boolean" 

                 use="optional" default="true"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tBind">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="this" type="cdl:tBindVariable"/>
          <element name="free" type="cdl:tBindVariable"/>
        </sequence>
         <attribute name="name" type="NCName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tBindVariable">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="variable" type="cdl:tXPath-expr" 

                 use="required"/>
        <attribute name="roleType" type="QName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tInteraction">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="participate" type="cdl:tParticipate"/>
          <element name="exchange" type="cdl:tExchange" minOccurs="0"

                  maxOccurs="unbounded"/>
          <element name="timeout" type="cdl:tTimeout" minOccurs="0"

                  maxOccurs="1"/>
          <element name="record" type="cdl:tRecord" minOccurs="0" 

                  maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="channelVariable" type="QName" 

                 use="required"/>
        <attribute name="operation" type="NCName" use="required"/>
        <attribute name="align" type="boolean" use="optional" 

                 default="false"/>
        <attribute name="initiate" type="boolean" 

                 use="optional" default="false"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tTimeout">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="time-to-complete" type="cdl:tXPath-expr" use="required"/>
        <attribute name="fromRoleTypeRecordRef" use="optional">
          <simpleType>
             <list itemType="NCName"/>
          </simpleType>
        </attribute>
        <attribute name="toRoleTypeRecordRef" use="optional">
          <simpleType>
             <list itemType="NCName"/>
          </simpleType>
        </attribute>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tParticipate">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="relationshipType" type="QName" use="required"/>
        <attribute name="fromRoleTypeRef" type="QName" use="required"/>
        <attribute name="toRoleTypeRef" type="QName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tExchange">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="send" type="cdl:tVariableRecordRef"/>
          <element name="receive" type="cdl:tVariableRecordRef"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="faultName" type="QName" 

                 use="optional"/>
        <attribute name="informationType" type="QName" 

                 use="optional"/>
        <attribute name="channelType" type="QName" 

                 use="optional"/>
        <attribute name="action" type="cdl:tAction2" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tVariableRecordRef">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="variable" type="cdl:tXPath-expr" 

                use="optional"/>
        <attribute name="recordReference" use="optional">
          <simpleType>
             <list itemType="NCName"/>
          </simpleType>
        </attribute>
        <attribute name="causeException" type="QName" 

                use="optional" />
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tRecord">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="source" type="cdl:tSourceVariableRef"/>
          <element name="target" type="cdl:tVariableRef"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="causeException" type="QName" use="optional" />
        <attribute name="when" type="cdl:tWhenType" use="required"/>
      </extension>
    </complexContent>
  </complexType>

   <complexType name="tSourceVariableRef">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="variable" type="cdl:tXPath-expr" 

                use="optional"/>
        <attribute name="expression" type="cdl:tXPath-expr" 

                use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tVariableRef">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="variable" type="cdl:tXPath-expr" 

                use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tAssign">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
      <element name="copy" type="cdl:tCopy"

               maxOccurs="unbounded"/>
        </sequence>
        <attribute name="roleType" type="QName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tCopy">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="source" type="cdl:tSourceVariableRef"/>
          <element name="target" type="cdl:tVariableRef"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="causeException" type="QName" 

                use="optional" />
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tSilentAction">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="roleType" type="QName" use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tNoAction">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="roleType" type="QName" use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tFinalize">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <attribute name="name" type="NCName" use="required"/>
        <attribute name="choreographyName" type="NCName" use="required"/>
        <attribute name="choreographyInstanceId" type="cdl:tXPath-expr"

                                                      use="optional"/>
        <attribute name="finalizerName" type="NCName" use="optional"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tException">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <element name="workunit" type="cdl:tWorkunit"

                  maxOccurs="unbounded"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <complexType name="tFinalizer">
    <complexContent>
      <extension base="cdl:tExtensibleElements">
        <sequence>
          <group ref="cdl:activity"/>
        </sequence>
        <attribute name="name" type="NCName" use="required"/>
      </extension>
    </complexContent>
  </complexType>

  <simpleType name="tAction">
    <restriction base="string">
      <enumeration value="request-respond"/>
      <enumeration value="request"/>
      <enumeration value="respond"/>
    </restriction>
  </simpleType>

  <simpleType name="tAction2">
    <restriction base="string">
      <enumeration value="request"/>
      <enumeration value="respond"/>
    </restriction>
  </simpleType>

  <simpleType name="tUsage">
    <restriction base="string">
      <enumeration value="once"/>
      <enumeration value="distinct"/>
      <enumeration value="shared"/>
    </restriction>
  </simpleType>

  <simpleType name="tUsageI">
    <restriction base="string">
      <enumeration value="primary"/>
      <enumeration value="alternate"/>
      <enumeration value="derived"/>
      <enumeration value="association"/>
    </restriction>
  </simpleType>

  <simpleType name="tWhenType">
    <restriction base="string">
      <enumeration value="before"/>
      <enumeration value="after"/>
      <enumeration value="timeout"/>
    </restriction>
  </simpleType>


  <simpleType name="tBoolean-expr">
    <restriction base="string"/>
  </simpleType>

  <simpleType name="tXPath-expr">
    <restriction base="string"/>
  </simpleType>

  <simpleType name="tDescriptionType">
    <restriction base="string">
      <enumeration value="documentation"/>
      <enumeration value="reference"/>
      <enumeration value="semantics"/>
    </restriction>
  </simpleType>

</schema>

推荐答案

Rodin Handbook[^] - worth reading.

Rodin Handbook[^] - worth reading.

i reading this book. But very hard to do.

Pls, help me.

i reading this book. But very hard to do.

Pls, help me.

这篇关于将WS-CDL转换为事件B的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！