XML Schema Documentation
Schema Document Properties
| Target Namespace | https://www.atelierb.eu/Formats/bxml |
|---|---|
| Element and Attribute Namespaces |
|
The purpose of this document is to describe and illustrate
the bxml format: an XML representation of a B or Event-B
component.
This documentation corresponds to version 1.0.0 of the format.
Each element corresponding to a node in the abstract syntax tree
may have an optional child element "Attr" containing tool-specific
information. This element is always the first child element.
For elements corresponding to lists of entities of the same class
(identifiers, assertions, etc.), the order of the child elements
matches the order in the source file.
Copyright © CLEARSY 2019.
### Licensing
© 2019 by CLEARSY Systems Engineering.
This work is available under a [Creative Commons Attribution-NonCommercial 4.0 International (CC-BY-NC) License](http://creativecommons.org/licenses/by-nc/4.0/).
Global Declarations
Element: ANY_Sub
Represents an unbounded choice substitution: **ANY X WHERE P THEN S END**.
<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 |
Represents the ABSTRACT_CONSTANTS clause of a component.
<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 |
Represents the ABSTRACT_VARIABLES clause of a component.
<xs:element name="Abstract_Variables" type="tns:identifier_list_type"/>
Element: Abstraction
Element "Abstraction" is a child of a machine element that corresponds
to a refinement or an implementation and contains the name of the refined component.
Element: Assert_Sub
Represents an **ASSERTION** substitution.
Element: Assertions
Represents the ASSERTIONS clause of a component.
Each child is an element of type "pred_group" and represents an assertion.
<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>
Element: Assignement_Sub
Represents a becomes equal substitution: **v := E**.
<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
Element to attach optional information to abstract syntax tree nodes for added functionalities.
Two optional informations are available built-in the format:
1. Child element `Pos` represents the position of the represented syntactic element in the source file.
2. Child element `B0Type` represents the concrete type of the element, if any.
<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
Represents a becomes element substitution: **v :: S**.
Element: Becomes_Such_That
Represents a becomes such that substitution, i.e. **v :( P )**.
Element: Binary_Exp
Represents a binary expression.
* Two child elements represent the argument expressions.
* Attribute `op` represents the operator.
<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
Represent either an implication (attribute `op="=>"`) or
an equivalence (`op="<=>"`).
Has two child elements that represent predicate arguments.
<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>
Element: Bloc_Sub
Represents a **BLOCK** substitution.
<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>
Element: Boolean_Exp
Represents a `bool` expression, that yields the Boolean value of
a predicate.
* There is a child element that represents the predicate argument.
<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>
Element: Boolean_Literal
Represents a Boolean literal (i.e. `TRUE` or `FALSE`).
* Attribute `value` represents which of `TRUE` or `FALSE` the literal is.
Element: Case_Sub
Represents a **CASE** conditional substitution.
<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 |
Represents the CONCRETE_CONSTANTS clause of a component.
<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 |
Represents the CONCRETE_VARIABLES clause of a component.
<xs:element name="Concrete_Variables" type="tns:identifier_list_type"/>
Element: Constraints
Represents the CONSTRAINTS clause of a component.
It has a single child element for the constraint predicate.
<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>
Element: EmptySeq
Represents an empty sequence expression.
Element: EmptySet
Represents an empty set expression.
Element: Enumerated_Values
No documentation provided.
Element: Exp_Comparison
Represent a comparison, identified by attribute `op`.
Has two child elements that represent expression arguments.
<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>
Element: Extends
| Name | Extends |
|---|---|
| Type | tns:instance_list_type |
| Nillable | no |
| Abstract | no |
Represents the EXTENDS clause of a component.
A non-empty list of elements represent the extended component instances.
<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
Represents the occurence of an identifier.
* Attribute "value" is the identifier string.
* Attribute "typref" is the type of the element
identified. If the element is not used (e.g., an unused
local variable), then this attribute is omitted.
* Optional attribute "suffix" applies to identifiers for the
previous value of a variable (e.g. "var$0").
<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
Represents an **IF** conditional substitution.
<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
| Name | Imports |
|---|---|
| Type | tns:instance_list_type |
| Nillable | no |
| Abstract | no |
Represents the imports clause of a component.
Then, a non-empty list of elements represent the imported component instances.
<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
| Name | Includes |
|---|---|
| Type | tns:instance_list_type |
| Nillable | no |
| Abstract | no |
Represents the INCLUDES clause of a component.
Then, a non-empty list of elements represent the included component instances.
<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
Represents the INITIALISATION clause of a component.
Then a unique child element of type "Sub" represents the initialisation substitution.
<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>
Element: Integer_Literal
Represents an integer literal.
* Attribute `value` represents which number the literal is.
Element: Invariant
Represents the **INVARIANT** clause of a component.
A child element of type `Pred` represents the invariant predicate.
<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>
Element: LET_Sub
Represents a local definition substitution: **LET id BE id = E IN S END**.
<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
Represents the LOCAL_OPERATIONS clause of a component.
Each child element is named "Operation" and represent the local
operations of the component.
Element: Machine
This is the main element of a BXml document.
It represents a unique B component.
The attribute `version` represents the version of the format
used.
<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
Represents a nary expression (essentially, either a
set enumeration or a sequence).
* Child elements represent the argument expressions.
* Attribute `op` represents the operator.
<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
Represent either a conjunction (attribute `op="&"`) or
a disjunction (`op="or"`).
Has child elements that represent argument predicates.
<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
* If attribute `op` is `";"`, then represents a sequencing substitution.
* If attribute `op` is `"||"`, then represents a simultaneous substitution.
* If attribute `op` is `"CHOICE"`, then represents a bounded **CHOICE** substitution.
All child elements other than optional `Attr` are substitutions.
<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>
Element: Operation
Represent an operation or an event.
* Optional element `Refines` is optional and is a list. The
list has a single element in case of an operation in a
software component. It may have multiple elements in case of
an event in a system component.
* Optional element `Output_Parameters` represents the list
of output parameters of the operation.
* Optional element `Input_Parameters` represents the list
of input parameters of the operation.
* Optional element `Precondition` represents the precondition
of the operation and is a predicate.
* Mandatory element `Body` represents the body of the operation
and is a substitution.
* Attribute `name` is the name of the operation.
<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
Represents an operation call substitution.
If the called operation is named `op`, the attributes
are as follows
* if `op` is prefixed by an instance name
`inst`, then `value="inst.op"`, `instance="inst"`
and `componente="op";
* otherwise, `value="op"` and the remaining
attributes are not present.
<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
Represents the OPERATIONS clause of a component.
Each child element is named "Operation" and represent the local
operations of the component.
Element: Parameters
Represents the parameters of a component.
Child elements "Id" represent the name of the parameters.
Element: Pos
Represents the position of a syntactic element in a source file.
Attributes "c", "l", "s" represent respectively the column, line
and span.
<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
Represents the PROMOTES clause of a component.
* Non-empty list of "Promoted_Operation" child elements represents
the promoted operations.
Element: Properties
Represents the PROPERTIES clause of a component.
<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>
Element: Quantified_Exp
Represents a quantified expression (essentially, a lambda expression
or a generalizes sum, product, intersection or union).
* Child element `Variables` represents the list of quantified variables.
* Child element `Pred` represents the characterizing predicate.
* Child element `Body` represent the list of quantified variables.
* Attribute `type` represents the operator.
<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
Represent either an existential quantification (attribute `type="#"`)
or a universal quantification (attribute `type="!"`).
* Child element `Variables` represents the list of quantified variables;
* Child element `Body` represents the quantified predcate.
<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
Represents a set defined in comprehension.
* Child element `Variables` represents the list of quantified variables.
* Child element `Body` represents the characterizing predicate.
<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
Represents a real literal (i.e. a decimal number).
* Attribute `value` represents which number the literal is.
Element: Record
Represents a record.
* Child elements represent the record fields.
<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
Represents the value of a field in a record.
* Child element represents the record.
<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
Represents an instance of (or reference to) a component.
Optional child element "Attr" contains tool-specific information.
Child element "Name" represents the name of the component.
Optional child element "Instance" is for the renaming prefix.
Optional element "Parameters" is the list of actual parameters.
<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
Represents a character string literal.
* Attribute `value` represents the string itself.
Element: Sees
Represents the SEES clause of a component.
* Has a non-empty list of child elements `Referenced_Machine` to represent the seen components.
Element: Select
Represents a conditional bounded substitution, i.e. **SELECT P THEN S ... END**.
<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
Represents a set introduced in the SET clause of a B component.
Child element "Id" corresponds to the name of the set.
Optional element "Enumerated_Values" is present for enumerations and
represents the list of enumerated values.
Element: Sets
Represents the SETS clause of a component.
Each child element "Set" represents the declaration of a set
(enumerated or deferred).
Element: Skip
Represents an identical (**skip**) substitution.
Element: Struct
Represents a set of records.
* Child elements represent the record fields.
<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
Represents a ternary expression (essentially, a tree expression).
* Three children elements represent the argument expressions.
* Attribute `op` represents the operator.
<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
Represents the types of the expressions found in the component. Each child element
is named `Type` and represents a different type.
Element: Unary_Exp
Represents a unary expression.
* A child element represents the argument expression.
* Attribute `op` represents the operator.
<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
Represent a negation.
A child element represents the argument predicate.
<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>
Element: Uses
| Name | Uses |
|---|---|
| Type | tns:instance_list_type |
| Nillable | no |
| Abstract | no |
Represents the USES clause of a component.
Then, a non-empty list of elements represent the used component instances.
<tns:Uses> <tns:Attr> ... </tns:Attr> [0..1] <tns:Referenced_Machine> ... </tns:Referenced_Machine> [1..*] </tns:Uses>
<xs:element name="Uses" type="tns:instance_list_type"/>
Element: VAR_IN
Represents a local variable substitution: **VAR v IN S END**.
Element: Valuation
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>
Element: Variant
Represents the VARIANT clause of a component.
Then a unique child element of type "Exp" represents the variant expression.
<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>
Element: While
Represents a **WHILE** loop substitution.
<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
Represents a **WITNESS** clause in an operation.
<