XML Schema Documentation

Schema Document Properties

Target Namespace https://www.atelierb.eu/Formats/bxml
Element and Attribute Namespaces
  • Global element and attribute declarations belong to this schema's target namespace.
  • By default, local element declarations belong to this schema's target namespace.
  • By default, local attribute declarations have no namespace.








Prefix Namespace
xml http://www.w3.org/XML/1998/namespace
xs http://www.w3.org/2001/XMLSchema
tns https://www.atelierb.eu/Formats/bxml
<xs:schema targetNamespace="https://www.atelierb.eu/Formats/bxml" elementFormDefault="qualified">
...
</xs:schema>

Global Declarations

Element: ANY_Sub

Name ANY_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:ANY_Sub>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Pred> tns:predicate_type </tns:Pred> [1]
   <tns:Then> tns:substitution_type </tns:Then> [1]
</tns:ANY_Sub>
<xs:element name="ANY_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Pred" type="tns:predicate_type"/>
         <xs:element name="Then" type="tns:substitution_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Abstract_Constants

Name Abstract_Constants
Type tns:identifier_list_type
Nillable no
Abstract no
<tns:Abstract_Constants>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Id> ... </tns:Id> [1..*]
</tns:Abstract_Constants>
<xs:element name="Abstract_Constants" type="tns:identifier_list_type"/>

Element: Abstract_Variables

Name Abstract_Variables
Type tns:identifier_list_type
Nillable no
Abstract no
<tns:Abstract_Variables>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Id> ... </tns:Id> [1..*]
</tns:Abstract_Variables>
<xs:element name="Abstract_Variables" type="tns:identifier_list_type"/>

Element: Abstraction

Name Abstraction
Type xs:string
Nillable no
Abstract no
<tns:Abstraction> xs:string </tns:Abstraction>
<xs:element name="Abstraction" type="xs:string"/>

Element: Assert_Sub

Name Assert_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Assert_Sub>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Guard> tns:predicate_type </tns:Guard> [1]
   <tns:Body> tns:substitution_type </tns:Body> [1]
</tns:Assert_Sub>
<xs:element name="Assert_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Guard" type="tns:predicate_type"/>
         <xs:element name="Body" type="tns:substitution_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Assertions

Name Assertions
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Assertions>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:pred_group [1..*]
      Start Choice [1]
         <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
         <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
         <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
         <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
         <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
      End Choice
   End Group: tns:pred_group
</tns:Assertions>
<xs:element name="Assertions">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Assignement_Sub

Name Assignement_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Assignement_Sub>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables   > [1] 
      Start Group: tns:Exp [1..*]
         Start Choice [1]
            <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
            <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
            <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
            <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
            <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
            <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
            <tns:EmptySet> ... </tns:EmptySet> [1]
            <tns:EmptySeq> ... </tns:EmptySeq> [1]
            <tns:Id> ... </tns:Id> [1]
            <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
            <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
            <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
            <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
            <tns:Struct> ... </tns:Struct> [1]
            <tns:Record> ... </tns:Record> [1]
            <tns:Real_Literal> ... </tns:Real_Literal> [1]
            <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
         End Choice
      End Group: tns:Exp
   </tns:Variables>
   <tns:Values   > [1] 
      Start Group: tns:Exp [1..*]
         Start Choice [1]
            <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
            <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
            <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
            <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
            <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
            <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
            <tns:EmptySet> ... </tns:EmptySet> [1]
            <tns:EmptySeq> ... </tns:EmptySeq> [1]
            <tns:Id> ... </tns:Id> [1]
            <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
            <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
            <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
            <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
            <tns:Struct> ... </tns:Struct> [1]
            <tns:Record> ... </tns:Record> [1]
            <tns:Real_Literal> ... </tns:Real_Literal> [1]
            <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
         End Choice
      End Group: tns:Exp
   </tns:Values>
</tns:Assignement_Sub>
<xs:element name="Assignement_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables">
            <xs:complexType>
               <xs:sequence>
                  <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="unbounded"/>
<-- FIXME on pourrait etre plus précis -->               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Values">
            <xs:complexType>
               <xs:sequence>
                  <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Attr

Name Attr
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Attr>
   <tns:Pos> ... </tns:Pos> [1..*]
   <tns:B0Type   > [0..1] 
      Start Choice [1]
         <tns:Id> ... </tns:Id> [1]
         <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
         <tns:Binary_Exp
          op="tns:binary_b0_op" [1]
         > [1] 
            Circular model group reference: tns:B0Type [2..2]
         </tns:Binary_Exp>
         <tns:Struct         > [1] 
            <tns:Record_Item
             label="xs:string" [1]
            > [1..*] 
               Circular model group reference: tns:B0Type [1]
            </tns:Record_Item>
         </tns:Struct>
      End Choice
   </tns:B0Type>
   Allow any elements from any namespace (strict validation). [0..1]
</tns:Attr>
<xs:element name="Attr">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Pos" minOccurs="1" maxOccurs="unbounded"/>
         <xs:element name="B0Type" minOccurs="0">
            <xs:complexType>
               <xs:group ref="tns:B0Type"/>
            </xs:complexType>
         </xs:element>
         <xs:any namespace="##any" minOccurs="0"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Becomes_In

Name Becomes_In
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Becomes_In>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Value> tns:expression_type </tns:Value> [1]
</tns:Becomes_In>
<xs:element name="Becomes_In">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Value" type="tns:expression_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Becomes_Such_That

Name Becomes_Such_That
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Becomes_Such_That>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Pred> tns:predicate_type </tns:Pred> [1]
</tns:Becomes_Such_That>
<xs:element name="Becomes_Such_That">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Pred" type="tns:predicate_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Binary_Exp

Name Binary_Exp
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Binary_Exp
 op="tns:binary_exp_op" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:Exp [2..2]
      Start Choice [1]
         <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
         <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
         <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
         <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
         <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
         <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
         <tns:EmptySet> ... </tns:EmptySet> [1]
         <tns:EmptySeq> ... </tns:EmptySeq> [1]
         <tns:Id> ... </tns:Id> [1]
         <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
         <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
         <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
         <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
         <tns:Struct> ... </tns:Struct> [1]
         <tns:Record> ... </tns:Record> [1]
         <tns:Real_Literal> ... </tns:Real_Literal> [1]
         <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
      End Choice
   End Group: tns:Exp
</tns:Binary_Exp>
<xs:element name="Binary_Exp">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp" minOccurs="2" maxOccurs="2"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:binary_exp_op" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Binary_Pred

Name Binary_Pred
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Binary_Pred
 op="tns:binary_pred_op" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:pred_group [2..2]
      Start Choice [1]
         <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
         <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
         <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
         <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
         <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
      End Choice
   End Group: tns:pred_group
</tns:Binary_Pred>
<xs:element name="Binary_Pred">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group" minOccurs="2" maxOccurs="2"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:binary_pred_op" use="required"/>
   </xs:complexType>
</xs:element>

Element: Bloc_Sub

Name Bloc_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Bloc_Sub>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Bloc_Sub> ... </tns:Bloc_Sub> [1]
      <tns:Skip> ... </tns:Skip> [1]
      <tns:Assert_Sub> ... </tns:Assert_Sub> [1]
      <tns:If_Sub> ... </tns:If_Sub> [1]
      <tns:Becomes_Such_That> ... </tns:Becomes_Such_That> [1]
      <tns:Assignement_Sub> ... </tns:Assignement_Sub> [1]
      <tns:Select> ... </tns:Select> [1]
      <tns:Case_Sub> ... </tns:Case_Sub> [1]
      <tns:ANY_Sub> ... </tns:ANY_Sub> [1]
      <tns:LET_Sub> ... </tns:LET_Sub> [1]
      <tns:VAR_IN> ... </tns:VAR_IN> [1]
      <tns:Nary_Sub> ... </tns:Nary_Sub> [1]
      <tns:Operation_Call> ... </tns:Operation_Call> [1]
      <tns:Becomes_In> ... </tns:Becomes_In> [1]
      <tns:While> ... </tns:While> [1]
      <tns:Witness> ... </tns:Witness> [1]
   End Choice
</tns:Bloc_Sub>
<xs:element name="Bloc_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Sub"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Boolean_Exp

Name Boolean_Exp
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Boolean_Exp
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
      <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
      <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
      <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
      <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
   End Choice
</tns:Boolean_Exp>
<xs:element name="Boolean_Exp">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Boolean_Literal

Name Boolean_Literal
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Boolean_Literal
 value="tns:boolean_literal_type" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:Boolean_Literal>
<xs:element name="Boolean_Literal">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="value" type="tns:boolean_literal_type" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Case_Sub

Name Case_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Case_Sub>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Value> tns:expression_type </tns:Value> [1]
   <tns:Choices   > [1] 
      <tns:Choice      > [1..*] 
         <tns:Attr> ... </tns:Attr> [0..1]
         <tns:Value> tns:expression_type </tns:Value> [1..*]
         <tns:Then> tns:substitution_type </tns:Then> [1]
      </tns:Choice>
   </tns:Choices>
   <tns:Else> tns:substitution_type </tns:Else> [0..1]
</tns:Case_Sub>
<xs:element name="Case_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Value" type="tns:expression_type"/>
         <xs:element name="Choices">
            <xs:complexType>
               <xs:sequence>
                  <xs:element name="Choice" minOccurs="1" maxOccurs="unbounded">
                     <xs:complexType>
                        <xs:sequence>
                           <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                           <xs:element name="Value" type="tns:expression_type" minOccurs="1" maxOccurs="unbounded"/>
                           <xs:element name="Then" type="tns:substitution_type"/>
                        </xs:sequence>
                     </xs:complexType>
                  </xs:element>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Else" type="tns:substitution_type" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Concrete_Constants

Name Concrete_Constants
Type tns:identifier_list_type
Nillable no
Abstract no
<tns:Concrete_Constants>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Id> ... </tns:Id> [1..*]
</tns:Concrete_Constants>
<xs:element name="Concrete_Constants" type="tns:identifier_list_type"/>

Element: Concrete_Variables

Name Concrete_Variables
Type tns:identifier_list_type
Nillable no
Abstract no
<tns:Concrete_Variables>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Id> ... </tns:Id> [1..*]
</tns:Concrete_Variables>
<xs:element name="Concrete_Variables" type="tns:identifier_list_type"/>

Element: Constraints

Name Constraints
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Constraints>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
      <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
      <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
      <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
      <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
   End Choice
</tns:Constraints>
<xs:element name="Constraints">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: EmptySeq

Name EmptySeq
Type Locally-defined complex type
Nillable no
Abstract no
<tns:EmptySeq
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:EmptySeq>
<xs:element name="EmptySeq">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: EmptySet

Name EmptySet
Type Locally-defined complex type
Nillable no
Abstract no
<tns:EmptySet
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:EmptySet>
<xs:element name="EmptySet">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Enumerated_Values

Name Enumerated_Values
Type Locally-defined complex type
Nillable no
Abstract no
No documentation provided.
<tns:Enumerated_Values>
   <tns:Id> ... </tns:Id> [1..*]
</tns:Enumerated_Values>
<xs:element name="Enumerated_Values">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Id" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Exp_Comparison

Name Exp_Comparison
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Exp_Comparison
 op="tns:comparison_op" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:Exp [2..2]
      Start Choice [1]
         <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
         <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
         <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
         <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
         <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
         <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
         <tns:EmptySet> ... </tns:EmptySet> [1]
         <tns:EmptySeq> ... </tns:EmptySeq> [1]
         <tns:Id> ... </tns:Id> [1]
         <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
         <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
         <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
         <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
         <tns:Struct> ... </tns:Struct> [1]
         <tns:Record> ... </tns:Record> [1]
         <tns:Real_Literal> ... </tns:Real_Literal> [1]
         <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
      End Choice
   End Group: tns:Exp
</tns:Exp_Comparison>
<xs:element name="Exp_Comparison">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp" minOccurs="2" maxOccurs="2"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:comparison_op" use="required"/>
   </xs:complexType>
</xs:element>

Element: Extends

<tns:Extends>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Referenced_Machine> ... </tns:Referenced_Machine> [1..*]
</tns:Extends>
<xs:element name="Extends" type="tns:instance_list_type"/>

Element: Id

Name Id
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Id
 value="xs:string" [1]
 suffix="xs:nonNegativeInteger" [0..1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:Id>
<xs:element name="Id">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="value" type="xs:string" use="required"/>
      <xs:attribute name="suffix" type="xs:nonNegativeInteger"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: If_Sub

Name If_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:If_Sub
 elseif="xs:string" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Condition> tns:predicate_type </tns:Condition> [1]
   <tns:Then> tns:substitution_type </tns:Then> [1]
   <tns:Else> tns:substitution_type </tns:Else> [0..1]
</tns:If_Sub>
<xs:element name="If_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Condition" type="tns:predicate_type"/>
         <xs:element name="Then" type="tns:substitution_type"/>
         <xs:element name="Else" type="tns:substitution_type" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="elseif" type="xs:string" use="required"/>
   </xs:complexType>
</xs:element>

Element: Imports

<tns:Imports>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Referenced_Machine> ... </tns:Referenced_Machine> [1..*]
</tns:Imports>
<xs:element name="Imports" type="tns:instance_list_type"/>

Element: Includes

<tns:Includes>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Referenced_Machine> ... </tns:Referenced_Machine> [1..*]
</tns:Includes>
<xs:element name="Includes" type="tns:instance_list_type"/>

Element: Initialisation

Name Initialisation
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Initialisation>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Bloc_Sub> ... </tns:Bloc_Sub> [1]
      <tns:Skip> ... </tns:Skip> [1]
      <tns:Assert_Sub> ... </tns:Assert_Sub> [1]
      <tns:If_Sub> ... </tns:If_Sub> [1]
      <tns:Becomes_Such_That> ... </tns:Becomes_Such_That> [1]
      <tns:Assignement_Sub> ... </tns:Assignement_Sub> [1]
      <tns:Select> ... </tns:Select> [1]
      <tns:Case_Sub> ... </tns:Case_Sub> [1]
      <tns:ANY_Sub> ... </tns:ANY_Sub> [1]
      <tns:LET_Sub> ... </tns:LET_Sub> [1]
      <tns:VAR_IN> ... </tns:VAR_IN> [1]
      <tns:Nary_Sub> ... </tns:Nary_Sub> [1]
      <tns:Operation_Call> ... </tns:Operation_Call> [1]
      <tns:Becomes_In> ... </tns:Becomes_In> [1]
      <tns:While> ... </tns:While> [1]
      <tns:Witness> ... </tns:Witness> [1]
   End Choice
</tns:Initialisation>
<xs:element name="Initialisation">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Sub"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Integer_Literal

Name Integer_Literal
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Integer_Literal
 value="xs:integer" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:Integer_Literal>
<xs:element name="Integer_Literal">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="value" type="xs:integer" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Invariant

Name Invariant
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Invariant>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
      <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
      <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
      <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
      <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
   End Choice
</tns:Invariant>
<xs:element name="Invariant">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: LET_Sub

Name LET_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:LET_Sub>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Values   > [1] 
      <tns:Attr> ... </tns:Attr> [0..1]
      <tns:Valuation> ... </tns:Valuation> [1..*]
   </tns:Values>
   <tns:Then> tns:substitution_type </tns:Then> [1]
</tns:LET_Sub>
<xs:element name="LET_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Values">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                  <xs:element ref="tns:Valuation" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Then" type="tns:substitution_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Local_Operations

Name Local_Operations
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Local_Operations>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Operation> ... </tns:Operation> [1..*]
</tns:Local_Operations>
<xs:element name="Local_Operations">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Operation" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Machine

Name Machine
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Machine
 version="tns:version_type" [1]
 name="xs:string" [1]
 type="tns:machine_type" [1]
 semantic="xs:boolean" [1]
 b0check="xs:boolean" [1]
 position="xs:boolean" [1]
>
   <tns:Abstraction> ... </tns:Abstraction> [0..1]
   <tns:Parameters> ... </tns:Parameters> [0..1]
   <tns:Constraints> ... </tns:Constraints> [0..1]
   <tns:Includes> ... </tns:Includes> [0..1]
   <tns:Imports> ... </tns:Imports> [0..1]
   <tns:Uses> ... </tns:Uses> [0..1]
   <tns:Sees> ... </tns:Sees> [0..1]
   <tns:Extends> ... </tns:Extends> [0..1]
   <tns:Promotes> ... </tns:Promotes> [0..1]
   <tns:Values   > [0..1]  
      <tns:Attr> ... </tns:Attr> [0..1]
      <tns:Valuation> ... </tns:Valuation> [1..*]
   </tns:Values>
   <tns:Sets> ... </tns:Sets> [0..1]
   <tns:Abstract_Constants> ... </tns:Abstract_Constants> [0..1]
   <tns:Concrete_Constants> ... </tns:Concrete_Constants> [0..1]
   <tns:Abstract_Variables> ... </tns:Abstract_Variables> [0..1]
   <tns:Concrete_Variables> ... </tns:Concrete_Variables> [0..1]
   <tns:Properties> ... </tns:Properties> [0..1]
   <tns:Invariant> ... </tns:Invariant> [0..1]
   <tns:Variant> ... </tns:Variant> [0..1]
   <tns:Initialisation> ... </tns:Initialisation> [0..1]
   <tns:Assertions> ... </tns:Assertions> [0..1]
   <tns:Local_Operations> ... </tns:Local_Operations> [0..1]
   <tns:Operations> ... </tns:Operations> [0..1]
   <tns:TypeInfos> ... </tns:TypeInfos> [0..1]
</tns:Machine>
<xs:element name="Machine">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Abstraction" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Parameters" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Constraints" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Includes" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Imports" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Uses" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Sees" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Extends" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Promotes" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Values" minOccurs="0" maxOccurs="1">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                  <xs:element ref="tns:Valuation" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element ref="tns:Sets" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Abstract_Constants" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Concrete_Constants" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Abstract_Variables" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Concrete_Variables" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Properties" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Invariant" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Variant" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Initialisation" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Assertions" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Local_Operations" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Operations" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:TypeInfos" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="version" type="tns:version_type" use="required"/>
      <xs:attribute name="name" type="xs:string" use="required"/>
      <xs:attribute name="type" type="tns:machine_type" use="required"/>
      <xs:attribute name="semantic" type="xs:boolean" use="required"/>
      <xs:attribute name="b0check" type="xs:boolean" use="required"/>
      <xs:attribute name="position" type="xs:boolean" use="required"/>
   </xs:complexType>
</xs:element>

Element: Nary_Exp

Name Nary_Exp
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Nary_Exp
 op="tns:nary_exp_op" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:Exp [1..*]
      Start Choice [1]
         <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
         <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
         <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
         <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
         <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
         <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
         <tns:EmptySet> ... </tns:EmptySet> [1]
         <tns:EmptySeq> ... </tns:EmptySeq> [1]
         <tns:Id> ... </tns:Id> [1]
         <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
         <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
         <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
         <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
         <tns:Struct> ... </tns:Struct> [1]
         <tns:Record> ... </tns:Record> [1]
         <tns:Real_Literal> ... </tns:Real_Literal> [1]
         <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
      End Choice
   End Group: tns:Exp
</tns:Nary_Exp>
<xs:element name="Nary_Exp">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:nary_exp_op" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Nary_Pred

Name Nary_Pred
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Nary_Pred
 op="tns:nary_pred_op" [0..1]
>
   Start Group: tns:pred_group [0..*]
      Start Choice [1]
         <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
         <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
         <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
         <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
         <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
      End Choice
   End Group: tns:pred_group
</tns:Nary_Pred>
<xs:element name="Nary_Pred">
   <xs:complexType>
      <xs:group ref="tns:pred_group" minOccurs="0" maxOccurs="unbounded"/>
      <xs:attribute name="op" type="tns:nary_pred_op"/>
   </xs:complexType>
</xs:element>

Element: Nary_Sub

Name Nary_Sub
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Nary_Sub
 op="tns:nary_sub_op" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:Sub [0..*]
      Start Choice [1]
         <tns:Bloc_Sub> ... </tns:Bloc_Sub> [1]
         <tns:Skip> ... </tns:Skip> [1]
         <tns:Assert_Sub> ... </tns:Assert_Sub> [1]
         <tns:If_Sub> ... </tns:If_Sub> [1]
         <tns:Becomes_Such_That> ... </tns:Becomes_Such_That> [1]
         <tns:Assignement_Sub> ... </tns:Assignement_Sub> [1]
         <tns:Select> ... </tns:Select> [1]
         <tns:Case_Sub> ... </tns:Case_Sub> [1]
         <tns:ANY_Sub> ... </tns:ANY_Sub> [1]
         <tns:LET_Sub> ... </tns:LET_Sub> [1]
         <tns:VAR_IN> ... </tns:VAR_IN> [1]
         <tns:Nary_Sub> ... </tns:Nary_Sub> [1]
         <tns:Operation_Call> ... </tns:Operation_Call> [1]
         <tns:Becomes_In> ... </tns:Becomes_In> [1]
         <tns:While> ... </tns:While> [1]
         <tns:Witness> ... </tns:Witness> [1]
      End Choice
   End Group: tns:Sub
</tns:Nary_Sub>
<xs:element name="Nary_Sub">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Sub" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:nary_sub_op" use="required"/>
   </xs:complexType>
</xs:element>

Element: Operation

Name Operation
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Operation
 name="xs:string" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Refines   > [0..1] 
      <tns:Attr> ... </tns:Attr> [0..1]
      <tns:Id> ... </tns:Id> [1..*]
   </tns:Refines>
   <tns:Output_Parameters   > [0..1] 
      <tns:Id> ... </tns:Id> [1..*]
   </tns:Output_Parameters>
   <tns:Input_Parameters   > [0..1] 
      <tns:Id> ... </tns:Id> [1..*]
   </tns:Input_Parameters>
   <tns:Precondition   > [0..1] 
      <tns:Attr> ... </tns:Attr> [0..1]
      Start Choice [1]
         <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
         <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
         <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
         <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
         <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
      End Choice
   </tns:Precondition>
   <tns:Body   > [1] 
      <tns:Attr> ... </tns:Attr> [0..1]
      Start Choice [1]
         <tns:Bloc_Sub> ... </tns:Bloc_Sub> [1]
         <tns:Skip> ... </tns:Skip> [1]
         <tns:Assert_Sub> ... </tns:Assert_Sub> [1]
         <tns:If_Sub> ... </tns:If_Sub> [1]
         <tns:Becomes_Such_That> ... </tns:Becomes_Such_That> [1]
         <tns:Assignement_Sub> ... </tns:Assignement_Sub> [1]
         <tns:Select> ... </tns:Select> [1]
         <tns:Case_Sub> ... </tns:Case_Sub> [1]
         <tns:ANY_Sub> ... </tns:ANY_Sub> [1]
         <tns:LET_Sub> ... </tns:LET_Sub> [1]
         <tns:VAR_IN> ... </tns:VAR_IN> [1]
         <tns:Nary_Sub> ... </tns:Nary_Sub> [1]
         <tns:Operation_Call> ... </tns:Operation_Call> [1]
         <tns:Becomes_In> ... </tns:Becomes_In> [1]
         <tns:While> ... </tns:While> [1]
         <tns:Witness> ... </tns:Witness> [1]
      End Choice
   </tns:Body>
</tns:Operation>
<xs:element name="Operation">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Refines" minOccurs="0" maxOccurs="1">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                  <xs:element ref="tns:Id" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Output_Parameters" minOccurs="0" maxOccurs="1">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Id" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Input_Parameters" minOccurs="0" maxOccurs="1">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Id" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Precondition" minOccurs="0" maxOccurs="1">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                  <xs:group ref="tns:pred_group"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Body">
            <xs:complexType>
               <xs:sequence>
                  <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                  <xs:group ref="tns:Sub"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
      </xs:sequence>
      <xs:attribute name="name" type="xs:string" use="required"/>
   </xs:complexType>
</xs:element>

Element: Operation_Call

Name Operation_Call
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Operation_Call>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Name   > [1] 
      <tns:Id
       value="xs:string" [1]
       instance="xs:string" [0..1]
       component="xs:string" [0..1]
      > [1] 
         <tns:Attr> ... </tns:Attr> [0..1]
      </tns:Id>
   </tns:Name>
   <tns:Input_Parameters   > [0..1] 
      Start Group: tns:Exp [1..*]
         Start Choice [1]
            <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
            <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
            <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
            <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
            <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
            <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
            <tns:EmptySet> ... </tns:EmptySet> [1]
            <tns:EmptySeq> ... </tns:EmptySeq> [1]
            <tns:Id> ... </tns:Id> [1]
            <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
            <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
            <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
            <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
            <tns:Struct> ... </tns:Struct> [1]
            <tns:Record> ... </tns:Record> [1]
            <tns:Real_Literal> ... </tns:Real_Literal> [1]
            <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
         End Choice
      End Group: tns:Exp
   </tns:Input_Parameters>
   <tns:Output_Parameters   > [0..1] 
      Start Group: tns:Exp [1..*]
         Start Choice [1]
            <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
            <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
            <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
            <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
            <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
            <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
            <tns:EmptySet> ... </tns:EmptySet> [1]
            <tns:EmptySeq> ... </tns:EmptySeq> [1]
            <tns:Id> ... </tns:Id> [1]
            <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
            <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
            <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
            <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
            <tns:Struct> ... </tns:Struct> [1]
            <tns:Record> ... </tns:Record> [1]
            <tns:Real_Literal> ... </tns:Real_Literal> [1]
            <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
         End Choice
      End Group: tns:Exp
   </tns:Output_Parameters>
</tns:Operation_Call>
<xs:element name="Operation_Call">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Name">
            <xs:complexType>
               <xs:sequence>
                  <xs:element name="Id" minOccurs="1" maxOccurs="1">
                     <xs:complexType>
                        <xs:sequence>
                           <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
                        </xs:sequence>
                        <xs:attribute name="value" type="xs:string" use="required"/>
                        <xs:attribute name="instance" type="xs:string" use="optional"/>
                        <xs:attribute name="component" type="xs:string" use="optional"/>
                     </xs:complexType>
                  </xs:element>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Input_Parameters" minOccurs="0">
            <xs:complexType>
               <xs:sequence>
                  <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Output_Parameters" minOccurs="0">
            <xs:complexType>
               <xs:sequence>
                  <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Operations

Name Operations
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Operations>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Operation> ... </tns:Operation> [1..*]
</tns:Operations>
<xs:element name="Operations">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Operation" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Parameters

Name Parameters
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Parameters>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Id> ... </tns:Id> [1..*]
</tns:Parameters>
<xs:element name="Parameters">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Id" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Pos

Name Pos
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Pos
 c="xs:integer" [1]
 l="xs:integer" [1]
 s="xs:integer" [1]
 endLine="xs:integer" [0..1]
 expanded="xs:string" [0..1]
 f="xs:string" [0..1]
/> 

<xs:element name="Pos">
   <xs:complexType>
      <xs:attribute name="c" type="xs:integer" use="required"/>
      <xs:attribute name="l" type="xs:integer" use="required"/>
      <xs:attribute name="s" type="xs:integer" use="required"/>
      <xs:attribute name="endLine" type="xs:integer" use="optional"/>
      <xs:attribute name="expanded" type="xs:string" use="optional"/>
      <xs:attribute name="f" type="xs:string" use="optional"/>
   </xs:complexType>
</xs:element>

Element: Promotes

Name Promotes
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Promotes>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Promoted_Operation> tns:promoted_operation_type </tns:Promoted_Operation> [1..*]
</tns:Promotes>
<xs:element name="Promotes">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Promoted_Operation" type="tns:promoted_operation_type" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Properties

Name Properties
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Properties>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
      <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
      <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
      <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
      <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
   End Choice
</tns:Properties>
<xs:element name="Properties">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Quantified_Exp

Name Quantified_Exp
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Quantified_Exp
 type="tns:quantified_exp_op" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Pred> tns:predicate_type </tns:Pred> [1]
   <tns:Body> tns:expression_type </tns:Body> [1]
</tns:Quantified_Exp>
<xs:element name="Quantified_Exp">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Pred" type="tns:predicate_type"/>
         <xs:element name="Body" type="tns:expression_type"/>
      </xs:sequence>
      <xs:attribute name="type" type="tns:quantified_exp_op" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Quantified_Pred

Name Quantified_Pred
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Quantified_Pred
 type="tns:quantified_pred_op" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Body> tns:predicate_type </tns:Body> [1]
</tns:Quantified_Pred>
<xs:element name="Quantified_Pred">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Body" type="tns:predicate_type"/>
      </xs:sequence>
      <xs:attribute name="type" type="tns:quantified_pred_op" use="required"/>
   </xs:complexType>
</xs:element>

Element: Quantified_Set

Name Quantified_Set
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Quantified_Set
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Body> tns:predicate_type </tns:Body> [1]
</tns:Quantified_Set>
<xs:element name="Quantified_Set">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Body" type="tns:predicate_type"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Real_Literal

Name Real_Literal
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Real_Literal
 value="xs:decimal" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:Real_Literal>
<xs:element name="Real_Literal">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="value" type="xs:decimal" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Record

Name Record
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Record
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Record_Item> tns:record_item_type </tns:Record_Item> [1..*]
</tns:Record>
<xs:element name="Record">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Record_Item" type="tns:record_item_type" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Record_Field_Access

Name Record_Field_Access
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Record_Field_Access
 typref="xs:integer" [0..1]
 label="xs:string" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
      <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
      <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
      <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
      <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
      <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
      <tns:EmptySet> ... </tns:EmptySet> [1]
      <tns:EmptySeq> ... </tns:EmptySeq> [1]
      <tns:Id> ... </tns:Id> [1]
      <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
      <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
      <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
      <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
      <tns:Struct> ... </tns:Struct> [1]
      <tns:Record> ... </tns:Record> [1]
      <tns:Real_Literal> ... </tns:Real_Literal> [1]
      <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
   End Choice
</tns:Record_Field_Access>
<xs:element name="Record_Field_Access">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
      <xs:attribute name="label" type="xs:string" use="required"/>
   </xs:complexType>
</xs:element>

Element: Referenced_Machine

Name Referenced_Machine
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Referenced_Machine>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Name> xs:string </tns:Name> [1]
   <tns:Instance> xs:string </tns:Instance> [0..1]
   <tns:Parameters   > [0..1] 
      Start Group: tns:Exp [1..*]
         Start Choice [1]
            <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
            <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
            <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
            <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
            <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
            <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
            <tns:EmptySet> ... </tns:EmptySet> [1]
            <tns:EmptySeq> ... </tns:EmptySeq> [1]
            <tns:Id> ... </tns:Id> [1]
            <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
            <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
            <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
            <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
            <tns:Struct> ... </tns:Struct> [1]
            <tns:Record> ... </tns:Record> [1]
            <tns:Real_Literal> ... </tns:Real_Literal> [1]
            <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
         End Choice
      End Group: tns:Exp
   </tns:Parameters>
</tns:Referenced_Machine>
<xs:element name="Referenced_Machine">
   <xs:complexType>
      <xs:sequence>
<--	  <xs:element name="Path" minOccurs="1" maxOccurs="1" type="xs:string"/> -->         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Name" type="xs:string" minOccurs="1" maxOccurs="1"/>
         <xs:element name="Instance" type="xs:string" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Parameters" minOccurs="0" maxOccurs="1">
            <xs:complexType>
               <xs:sequence>
                  <xs:group ref="tns:Exp" minOccurs="1" maxOccurs="unbounded"/>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: STRING_Literal

Name STRING_Literal
Type Locally-defined complex type
Nillable no
Abstract no
<tns:STRING_Literal
 value="xs:string" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:STRING_Literal>
<xs:element name="STRING_Literal">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
      <xs:attribute name="value" type="xs:string" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Sees

Name Sees
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Sees>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Referenced_Machine> tns:seen_machine_type </tns:Referenced_Machine> [1..*]
</tns:Sees>
<xs:element name="Sees">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Referenced_Machine" type="tns:seen_machine_type" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Select

Name Select
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Select>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:When_Clauses   > [1] 
      <tns:When      > [1..*] 
         <tns:Condition> tns:predicate_type </tns:Condition> [1]
         <tns:Then> tns:substitution_type </tns:Then> [1]
      </tns:When>
   </tns:When_Clauses>
   <tns:Else> tns:substitution_type </tns:Else> [0..1]
</tns:Select>
<xs:element name="Select">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="When_Clauses">
            <xs:complexType>
               <xs:sequence>
                  <xs:element name="When" minOccurs="1" maxOccurs="unbounded">
                     <xs:complexType>
                        <xs:sequence>
                           <xs:element name="Condition" type="tns:predicate_type"/>
                           <xs:element name="Then" type="tns:substitution_type"/>
                        </xs:sequence>
                     </xs:complexType>
                  </xs:element>
               </xs:sequence>
            </xs:complexType>
         </xs:element>
         <xs:element name="Else" type="tns:substitution_type" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Set

Name Set
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Set>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Id> ... </tns:Id> [1]
   <tns:Enumerated_Values> ... </tns:Enumerated_Values> [0..1]
</tns:Set>
<xs:element name="Set">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Id" minOccurs="1" maxOccurs="1"/>
         <xs:element ref="tns:Enumerated_Values" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Sets

Name Sets
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Sets>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Set> ... </tns:Set> [1..*]
</tns:Sets>
<xs:element name="Sets">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element ref="tns:Set" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Skip

Name Skip
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Skip>
   <tns:Attr> ... </tns:Attr> [0..1]
</tns:Skip>
<xs:element name="Skip">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Struct

Name Struct
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Struct
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Record_Item> tns:record_item_type </tns:Record_Item> [1..*]
</tns:Struct>
<xs:element name="Struct">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Record_Item" type="tns:record_item_type" minOccurs="1" maxOccurs="unbounded"/>
      </xs:sequence>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Ternary_Exp

Name Ternary_Exp
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Ternary_Exp
 op="tns:ternary_exp_op" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Group: tns:Exp [3..3]
      Start Choice [1]
         <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
         <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
         <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
         <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
         <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
         <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
         <tns:EmptySet> ... </tns:EmptySet> [1]
         <tns:EmptySeq> ... </tns:EmptySeq> [1]
         <tns:Id> ... </tns:Id> [1]
         <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
         <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
         <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
         <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
         <tns:Struct> ... </tns:Struct> [1]
         <tns:Record> ... </tns:Record> [1]
         <tns:Real_Literal> ... </tns:Real_Literal> [1]
         <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
      End Choice
   End Group: tns:Exp
</tns:Ternary_Exp>
<xs:element name="Ternary_Exp">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp" minOccurs="3" maxOccurs="3"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:ternary_exp_op" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: TypeInfos

Name TypeInfos
Type Locally-defined complex type
Nillable no
Abstract no
<tns:TypeInfos>
   <tns:Type> tns:typeinfos_type </tns:Type> [0..*]
</tns:TypeInfos>
<xs:element name="TypeInfos">
   <xs:complexType>
      <xs:sequence>
         <xs:element name="Type" type="tns:typeinfos_type" minOccurs="0" maxOccurs="unbounded"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Unary_Exp

Name Unary_Exp
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Unary_Exp
 op="tns:unary_exp_op" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
      <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
      <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
      <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
      <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
      <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
      <tns:EmptySet> ... </tns:EmptySet> [1]
      <tns:EmptySeq> ... </tns:EmptySeq> [1]
      <tns:Id> ... </tns:Id> [1]
      <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
      <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
      <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
      <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
      <tns:Struct> ... </tns:Struct> [1]
      <tns:Record> ... </tns:Record> [1]
      <tns:Real_Literal> ... </tns:Real_Literal> [1]
      <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
   End Choice
</tns:Unary_Exp>
<xs:element name="Unary_Exp">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:unary_exp_op" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Unary_Pred

Name Unary_Pred
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Unary_Pred
 op="tns:unary_pred_op" [1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Binary_Pred> ... </tns:Binary_Pred> [1]
      <tns:Exp_Comparison> ... </tns:Exp_Comparison> [1]
      <tns:Quantified_Pred> ... </tns:Quantified_Pred> [1]
      <tns:Unary_Pred> ... </tns:Unary_Pred> [1]
      <tns:Nary_Pred> ... </tns:Nary_Pred> [1]
   End Choice
</tns:Unary_Pred>
<xs:element name="Unary_Pred">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:pred_group"/>
      </xs:sequence>
      <xs:attribute name="op" type="tns:unary_pred_op" use="required"/>
   </xs:complexType>
</xs:element>

Element: Uses


Element: VAR_IN

Name VAR_IN
Type Locally-defined complex type
Nillable no
Abstract no
<tns:VAR_IN>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Variables> tns:variables_type </tns:Variables> [1]
   <tns:Body> tns:substitution_type </tns:Body> [1]
</tns:VAR_IN>
<xs:element name="VAR_IN">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Variables" type="tns:variables_type"/>
         <xs:element name="Body" type="tns:substitution_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Valuation

Name Valuation
Type Locally-defined complex type
Nillable no
Abstract no
No documentation provided.
<tns:Valuation
 ident="xs:string" [1]
 typref="xs:integer" [0..1]
>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
      <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
      <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
      <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
      <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
      <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
      <tns:EmptySet> ... </tns:EmptySet> [1]
      <tns:EmptySeq> ... </tns:EmptySeq> [1]
      <tns:Id> ... </tns:Id> [1]
      <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
      <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
      <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
      <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
      <tns:Struct> ... </tns:Struct> [1]
      <tns:Record> ... </tns:Record> [1]
      <tns:Real_Literal> ... </tns:Real_Literal> [1]
      <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
   End Choice
</tns:Valuation>
<xs:element name="Valuation">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp"/>
      </xs:sequence>
      <xs:attribute name="ident" type="xs:string" use="required"/>
      <xs:attribute name="typref" type="xs:integer"/>
   </xs:complexType>
</xs:element>

Element: Variant

Name Variant
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Variant>
   <tns:Attr> ... </tns:Attr> [0..1]
   Start Choice [1]
      <tns:Unary_Exp> ... </tns:Unary_Exp> [1]
      <tns:Binary_Exp> ... </tns:Binary_Exp> [1]
      <tns:Ternary_Exp> ... </tns:Ternary_Exp> [1]
      <tns:Nary_Exp> ... </tns:Nary_Exp> [1]
      <tns:Boolean_Literal> ... </tns:Boolean_Literal> [1]
      <tns:Boolean_Exp> ... </tns:Boolean_Exp> [1]
      <tns:EmptySet> ... </tns:EmptySet> [1]
      <tns:EmptySeq> ... </tns:EmptySeq> [1]
      <tns:Id> ... </tns:Id> [1]
      <tns:Integer_Literal> ... </tns:Integer_Literal> [1]
      <tns:Quantified_Exp> ... </tns:Quantified_Exp> [1]
      <tns:Quantified_Set> ... </tns:Quantified_Set> [1]
      <tns:STRING_Literal> ... </tns:STRING_Literal> [1]
      <tns:Struct> ... </tns:Struct> [1]
      <tns:Record> ... </tns:Record> [1]
      <tns:Real_Literal> ... </tns:Real_Literal> [1]
      <tns:Record_Field_Access> ... </tns:Record_Field_Access> [1]
   End Choice
</tns:Variant>
<xs:element name="Variant">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:group ref="tns:Exp"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: While

Name While
Type Locally-defined complex type
Nillable no
Abstract no
<tns:While>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Condition> tns:predicate_type </tns:Condition> [1]
   <tns:Body> tns:substitution_type </tns:Body> [1]
   <tns:Invariant> tns:predicate_type </tns:Invariant> [1]
   <tns:Variant> tns:expression_type </tns:Variant> [1]
</tns:While>
<xs:element name="While">
   <xs:complexType>
      <xs:sequence>
         <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/>
         <xs:element name="Condition" type="tns:predicate_type"/>
         <xs:element name="Body" type="tns:substitution_type"/>
         <xs:element name="Invariant" type="tns:predicate_type"/>
         <xs:element name="Variant" type="tns:expression_type"/>
      </xs:sequence>
   </xs:complexType>
</xs:element>

Element: Witness

Name Witness
Type Locally-defined complex type
Nillable no
Abstract no
<tns:Witness>
   <tns:Attr> ... </tns:Attr> [0..1]
   <tns:Witnesses> tns:witnesses_type </tns:Witnesses> [1]
   <tns:Body> tns:substitution_type </tns:Body> [1]
</tns:Witness>
<