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.
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.
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.
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.
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/).
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.
Global Declarations
Element: ANY_Sub
Represents an unbounded choice substitution: **ANY X WHERE P THEN S END**.
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.
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.
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 "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.
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.
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**.
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.
Element to attach optional information to abstract syntax tree nodes for added functionalities.
Two optional informations are available built-in the format:
Child element
Posrepresents the position of the represented syntactic element in the source file.Child element
B0Typerepresents 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**.
Represents a becomes element substitution: v :: S.
Element: Becomes_Such_That
Represents a becomes such that substitution, i.e. **v :( P )**.
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.
Represents a binary expression.
Two child elements represent the argument expressions.
Attribute
oprepresents 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.
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.
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.
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.
Represents a Boolean literal (i.e. TRUE or FALSE).
- Attribute
valuerepresents which ofTRUEorFALSEthe literal is.
Element: Case_Sub
Represents a **CASE** conditional substitution.
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.
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.
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.
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.
Represents an empty sequence expression.
Element: EmptySet
Represents an empty set expression.
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.
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.
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").
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.
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.
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.
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.
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.
Represents an integer literal.
- Attribute
valuerepresents which number the literal is.
Element: Invariant
Represents the **INVARIANT** clause of a component.
A child element of type `Pred` represents the invariant predicate.
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**.
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.
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.
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.
Represents a nary expression (essentially, either a set enumeration or a sequence).
Child elements represent the argument expressions.
Attribute
oprepresents 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.
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.
- If attribute
opis";", then represents a sequencing substitution. - If attribute
opis"||", then represents a simultaneous substitution. - If attribute
opis"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.
Represent an operation or an event.
Optional element
Refinesis 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_Parametersrepresents the list of output parameters of the operation.Optional element
Input_Parametersrepresents the list of input parameters of the operation.Optional element
Preconditionrepresents the precondition of the operation and is a predicate.Mandatory element
Bodyrepresents the body of the operation and is a substitution.Attribute
nameis 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.
Represents an operation call substitution.
If the called operation is named op, the attributes
are as follows
if
opis prefixed by an instance nameinst, thenvalue="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.
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.
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.
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.
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.
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.
Represents a quantified expression (essentially, a lambda expression or a generalizes sum, product, intersection or union).
Child element
Variablesrepresents the list of quantified variables.Child element
Predrepresents the characterizing predicate.Child element
Bodyrepresent the list of quantified variables.Attribute
typerepresents 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.
Represent either an existential quantification (attribute type="#")
or a universal quantification (attribute type="!").
Child element
Variablesrepresents the list of quantified variables;Child element
Bodyrepresents 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.
Represents a set defined in comprehension.
Child element
Variablesrepresents the list of quantified variables.Child element
Bodyrepresents 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.
Represents a real literal (i.e. a decimal number).
- Attribute
valuerepresents which number the literal is.
Element: Record
Represents a record.
* Child elements represent the record fields.
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.
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.
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.
Represents a character string literal.
- Attribute
valuerepresents 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.
Represents the SEES clause of a component.
- Has a non-empty list of child elements
Referenced_Machineto represent the seen components.
Element: Select
Represents a conditional bounded substitution, i.e. **SELECT P THEN S ... END**.
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.
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).
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.
Represents an identical (skip) substitution.
Element: Struct
Represents a set of records.
* Child elements represent the record fields.
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.
Represents a ternary expression (essentially, a tree expression).
Three children elements represent the argument expressions.
Attribute
oprepresents 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.
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.
Represents a unary expression.
A child element represents the argument expression.
Attribute
oprepresents 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.
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.
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**.
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.
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.
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.
Represents a WITNESS clause in an operation.
Global Definitions
Complex Type: expression_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | expression_type |
|---|---|
| Abstract | no |
No documentation provided.
<...> 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 </...>
Complex Type: identifier_list_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | identifier_list_type |
|---|---|
| Abstract | no |
Optional child element "Attr" contains tool-specific information.
Then, a non-empty list of elements represent the listed identifiers.
Optional child element "Attr" contains tool-specific information. Then, a non-empty list of elements represent the listed identifiers.
Complex Type: instance_list_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | instance_list_type |
|---|---|
| Abstract | no |
A non-empty list of elements representing component instances.
A non-empty list of elements representing component instances.
<...> <tns:Attr> ... </tns:Attr> [0..1] <tns:Referenced_Machine> ... </tns:Referenced_Machine> [1..*] </...>
Complex Type: predicate_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | predicate_type |
|---|---|
| Abstract | no |
No documentation provided.
<...> 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 </...>
<xs:complexType name="predicate_type"> <xs:group ref="tns:pred_group"/> </xs:complexType>
Complex Type: promoted_operation_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | promoted_operation_type |
|---|---|
| Abstract | no |
No documentation provided.
Complex Type: record_item_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | record_item_type |
|---|---|
| Abstract | no |
No documentation provided.
<... 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 </...>
Complex Type: seen_machine_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | seen_machine_type |
|---|---|
| Abstract | no |
A non-empty list of elements representing seen component instances.
A non-empty list of elements representing seen component instances.
<xs:complexType name="seen_machine_type"> <xs:sequence> <xs:element ref="tns:Attr" minOccurs="0" maxOccurs="1"/> <xs:element name="Name" type="xs:string" minOccurs="1" maxOccurs="1"/> <xs:element name="Rename" type="xs:string" minOccurs="0" maxOccurs="1"/> <-- TODO La valeur de rename peut être r1.r2.r3, cela devrait être une liste cf. MRLB:7.8 --> </xs:sequence> </xs:complexType>
Complex Type: substitution_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | substitution_type |
|---|---|
| Abstract | no |
No documentation provided.
<...> 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 </...>
Complex Type: typeinfos_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | typeinfos_type |
|---|---|
| Abstract | no |
No documentation provided.
<... id="xs:integer" [1] > Start Choice [1] <tns:Binary_Exp op="*" [1] > [1] Circular model group reference: tns:Type [2..2] </tns:Binary_Exp> <tns:Id value="xs:string" [1] /> [1] <tns:Unary_Exp op="POW" [1] > [1] Circular model group reference: tns:Type [1] </tns:Unary_Exp> <tns:Struct > [1] <tns:Record_Item label="xs:string" [1] > [1..*] Circular model group reference: tns:Type [1] </tns:Record_Item> </tns:Struct> <tns:Generic_Type/> [1] End Choice </...>
Complex Type: variables_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | variables_type |
|---|---|
| Abstract | no |
No documentation provided.
Complex Type: witness_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | witness_type |
|---|---|
| Abstract | no |
Represents a **WITNESS** clause in an operation.
Represents a WITNESS clause in an operation.
<... op="=" [1] > <tns:Attr> ... </tns:Attr> [0..1] <tns:Id> ... </tns:Id> [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 </...>
Complex Type: witnesses_type
| Super-types: | None |
|---|---|
| Sub-types: | None |
| Name | witnesses_type |
|---|---|
| Abstract | no |
No documentation provided.
<xs:complexType name="witnesses_type"> <xs:choice> <xs:element name="Exp_Comparison" type="tns:witness_type"/> <xs:element name="Nary_Pred"> <xs:complexType> <xs:sequence> <xs:element name="Exp_Comparison" type="tns:witness_type" minOccurs="0" maxOccurs="unbounded"/> </xs:sequence> <xs:attribute name="op" type="xs:string" use="required" fixed="&"/> </xs:complexType> </xs:element> </xs:choice> </xs:complexType>
Model Group: B0Type
| Name | B0Type |
|---|
Elements that represent types for B0 expressions.
These are expression types and are built recursively using selected B expression elements,
restricted so that their arguments are B0 type representations.
Elements that represent types for B0 expressions.
These are expression types and are built recursively using selected B expression elements, restricted so that their arguments are B0 type representations.
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
<xs:group name="B0Type"> <xs:choice> <xs:element ref="tns:Id"/> <xs:element ref="tns:Integer_Literal"/> <-- FIXME as interval bounds only --> <xs:element name="Binary_Exp"> <xs:complexType> <xs:sequence> <xs:group ref="tns:B0Type" minOccurs="2" maxOccurs="2"/> </xs:sequence> <xs:attribute name="op" type="tns:binary_b0_op" use="required"/> </xs:complexType> </xs:element> <xs:element name="Struct"> <xs:complexType> <xs:sequence> <xs:element name="Record_Item" minOccurs="1" maxOccurs="unbounded"> <xs:complexType> <xs:group ref="tns:B0Type"/> <xs:attribute name="label" type="xs:string" use="required"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> </xs:choice> </xs:group>
Model Group: Exp
| Name | Exp |
|---|
The elements of this group represent expressions.
* Elements of this group have an attribute `typref`; its
value is an integer that represents the index of the `Type`
element for the type of this expression.
* All such `Type` elements are gathered under a `TypeInfos`
element, which is a child of the document root element.
The elements of this group represent expressions.
Elements of this group have an attribute
typref; its value is an integer that represents the index of theTypeelement for the type of this expression.All such
Typeelements are gathered under aTypeInfoselement, which is a child of the document root element.
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
<xs:group name="Exp"> <xs:choice> <xs:element ref="tns:Unary_Exp"/> <xs:element ref="tns:Binary_Exp"/> <xs:element ref="tns:Ternary_Exp"/> <xs:element ref="tns:Nary_Exp"/> <xs:element ref="tns:Boolean_Literal"/> <xs:element ref="tns:Boolean_Exp"/> <xs:element ref="tns:EmptySet"/> <xs:element ref="tns:EmptySeq"/> <xs:element ref="tns:Id"/> <xs:element ref="tns:Integer_Literal"/> <xs:element ref="tns:Quantified_Exp"/> <xs:element ref="tns:Quantified_Set"/> <xs:element ref="tns:STRING_Literal"/> <xs:element ref="tns:Struct"/> <xs:element ref="tns:Record"/> <xs:element ref="tns:Real_Literal"/> <xs:element ref="tns:Record_Field_Access"/> </xs:choice> </xs:group>
Model Group: Sub
| Name | Sub |
|---|
No documentation provided.
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
<xs:group name="Sub"> <xs:choice> <xs:element ref="tns:Bloc_Sub"/> <xs:element ref="tns:Skip"/> <xs:element ref="tns:Assert_Sub"/> <xs:element ref="tns:If_Sub"/> <xs:element ref="tns:Becomes_Such_That"/> <xs:element ref="tns:Assignement_Sub"/> <xs:element ref="tns:Select"/> <xs:element ref="tns:Case_Sub"/> <xs:element ref="tns:ANY_Sub"/> <xs:element ref="tns:LET_Sub"/> <xs:element ref="tns:VAR_IN"/> <xs:element ref="tns:Nary_Sub"/> <xs:element ref="tns:Operation_Call"/> <xs:element ref="tns:Becomes_In"/> <xs:element ref="tns:While"/> <xs:element ref="tns:Witness"/> </xs:choice> </xs:group>
Model Group: Type
| Name | Type |
|---|
Elements that represent types for B expressions.
These are expression types and are built recursively using selected B expression elements,
restricted so that their arguments are type representations.
Elements that represent types for B expressions.
These are expression types and are built recursively using selected B expression elements, restricted so that their arguments are type representations.
Start Choice [1] <tns:Binary_Exp op="*" [1] > [1] Circular model group reference: tns:Type [2..2] </tns:Binary_Exp> <tns:Id value="xs:string" [1] /> [1] <tns:Unary_Exp op="POW" [1] > [1] Circular model group reference: tns:Type [1] </tns:Unary_Exp> <tns:Struct > [1] <tns:Record_Item label="xs:string" [1] > [1..*] Circular model group reference: tns:Type [1] </tns:Record_Item> </tns:Struct> <tns:Generic_Type/> [1] End Choice
<xs:group name="Type"> <xs:choice> <xs:element name="Binary_Exp"> <xs:complexType> <xs:group ref="tns:Type" minOccurs="2" maxOccurs="2"/> <xs:attribute name="op" type="xs:string" use="required" fixed="*"/> </xs:complexType> </xs:element> <xs:element name="Id"> <xs:complexType> <xs:attribute name="value" type="xs:string" use="required"/> </xs:complexType> </xs:element> <xs:element name="Unary_Exp"> <xs:complexType> <xs:group ref="tns:Type"/> <xs:attribute name="op" type="xs:string" use="required" fixed="POW"/> </xs:complexType> </xs:element> <xs:element name="Struct"> <xs:complexType> <xs:sequence> <xs:element name="Record_Item" minOccurs="1" maxOccurs="unbounded"> <xs:complexType> <xs:group ref="tns:Type"/> <xs:attribute name="label" type="xs:string" use="required"/> </xs:complexType> </xs:element> </xs:sequence> </xs:complexType> </xs:element> <xs:element name="Generic_Type"> <xs:complexType/> </xs:element> </xs:choice> </xs:group>
Model Group: pred_group
| Name | pred_group |
|---|
Elements of this group represent predicates.
Elements of this group represent predicates.
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
<xs:group name="pred_group"> <xs:choice> <xs:element ref="tns:Binary_Pred"/> <xs:element ref="tns:Exp_Comparison"/> <xs:element ref="tns:Quantified_Pred"/> <xs:element ref="tns:Unary_Pred"/> <xs:element ref="tns:Nary_Pred"/> </xs:choice> </xs:group>
Simple Type: binary_b0_op
| Super-types: | xs:string < binary_b0_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | binary_b0_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: binary_exp_op
| Super-types: | xs:string < binary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | binary_exp_op |
|---|---|
| Content |
|
No documentation provided.
<xs:simpleType name="binary_exp_op"> <xs:restriction base="xs:string"> <xs:enumeration value=","/> <xs:enumeration value="*"/> <xs:enumeration value="*i"/> <xs:enumeration value="*r"/> <xs:enumeration value="*f"/> <xs:enumeration value="*s"/> <xs:enumeration value="**"/> <xs:enumeration value="**i"/> <xs:enumeration value="**r"/> <xs:enumeration value="+"/> <xs:enumeration value="+i"/> <xs:enumeration value="+r"/> <xs:enumeration value="+f"/> <xs:enumeration value="+->"/> <xs:enumeration value="+->>"/> <xs:enumeration value="-"/> <xs:enumeration value="-i"/> <xs:enumeration value="-r"/> <xs:enumeration value="-f"/> <xs:enumeration value="-s"/> <xs:enumeration value="-->"/> <xs:enumeration value="-->>"/> <xs:enumeration value="->"/> <xs:enumeration value=".."/> <xs:enumeration value="/"/> <xs:enumeration value="/i"/> <xs:enumeration value="/r"/> <xs:enumeration value="/f"/> <xs:enumeration value="/\"/> <xs:enumeration value="/|\"/> <xs:enumeration value=";"/> <xs:enumeration value="<+"/> <xs:enumeration value="<->"/> <xs:enumeration value="<-"/> <xs:enumeration value="<<|"/> <xs:enumeration value="<|"/> <xs:enumeration value=">+>"/> <xs:enumeration value=">->"/> <xs:enumeration value=">+>>"/> <xs:enumeration value=">->>"/> <xs:enumeration value="><"/> <xs:enumeration value="||"/> <xs:enumeration value="\/"/> <xs:enumeration value="\|/"/> <xs:enumeration value="^"/> <xs:enumeration value="mod"/> <xs:enumeration value="|->"/> <xs:enumeration value="|>"/> <xs:enumeration value="|>>"/> <xs:enumeration value="["/> <xs:enumeration value="("/> <xs:enumeration value="<'"/> <xs:enumeration value="prj1"/> <xs:enumeration value="prj2"/> <xs:enumeration value="iterate"/> <xs:enumeration value="const"/> <xs:enumeration value="rank"/> <xs:enumeration value="father"/> <xs:enumeration value="subtree"/> <xs:enumeration value="arity"/> </xs:restriction> </xs:simpleType>
Simple Type: binary_pred_op
| Super-types: | xs:string < binary_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | binary_pred_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: boolean_literal_type
| Super-types: | xs:string < boolean_literal_type (by restriction) |
|---|---|
| Sub-types: | None |
| Name | boolean_literal_type |
|---|---|
| Content |
|
No documentation provided.
Simple Type: comparison_op
| Super-types: | xs:string < comparison_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | comparison_op |
|---|---|
| Content |
|
No documentation provided.
<xs:simpleType name="comparison_op"> <xs:restriction base="xs:string"> <xs:enumeration value=":"/> <xs:enumeration value="/:"/> <xs:enumeration value="<:"/> <xs:enumeration value="/<:"/> <xs:enumeration value="<<:"/> <xs:enumeration value="/<<:"/> <xs:enumeration value="="/> <xs:enumeration value="/="/> <-- untyped comparison --> <xs:enumeration value=">="/> <xs:enumeration value=">"/> <xs:enumeration value="<"/> <xs:enumeration value="<="/> <-- integer comparison --> <xs:enumeration value=">=i"/> <xs:enumeration value=">i"/> <xs:enumeration value="<i"/> <xs:enumeration value="<=i"/> <-- real comparison --> <xs:enumeration value=">=r"/> <xs:enumeration value=">r"/> <xs:enumeration value="<r"/> <xs:enumeration value="<=r"/> <-- float comparison --> <xs:enumeration value=">=f"/> <xs:enumeration value=">f"/> <xs:enumeration value="<f"/> <xs:enumeration value="<=f"/> </xs:restriction> </xs:simpleType>
Simple Type: machine_type
| Super-types: | xs:string < machine_type (by restriction) |
|---|---|
| Sub-types: | None |
| Name | machine_type |
|---|---|
| Content |
|
Represents the type of a B component.
The value "abstraction" corresponds either to a MACHINE or a SYSTEM component.
Represents the type of a B component. The value "abstraction" corresponds either to a MACHINE or a SYSTEM component.
Simple Type: nary_exp_op
| Super-types: | xs:string < nary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | nary_exp_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: nary_pred_op
| Super-types: | xs:string < nary_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | nary_pred_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: nary_sub_op
| Super-types: | xs:string < nary_sub_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | nary_sub_op |
|---|---|
| Content |
|
Either `";"` or `"||"` or `CHOICE`.
Either ";" or "||" or CHOICE.
Simple Type: quantified_exp_op
| Super-types: | xs:string < quantified_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | quantified_exp_op |
|---|---|
| Content |
|
No documentation provided.
<xs:simpleType name="quantified_exp_op"> <xs:restriction base="xs:string"> <xs:enumeration value="%"/> <xs:enumeration value="SIGMA"/> <xs:enumeration value="iSIGMA"/> <xs:enumeration value="rSIGMA"/> <xs:enumeration value="PI"/> <xs:enumeration value="iPI"/> <xs:enumeration value="rPI"/> <xs:enumeration value="INTER"/> <xs:enumeration value="UNION"/> </xs:restriction> </xs:simpleType>
Simple Type: quantified_pred_op
| Super-types: | xs:string < quantified_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | quantified_pred_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: ternary_exp_op
| Super-types: | xs:string < ternary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | ternary_exp_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: unary_exp_op
| Super-types: | xs:string < unary_exp_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | unary_exp_op |
|---|---|
| Content |
|
No documentation provided.
<xs:simpleType name="unary_exp_op"> <xs:restriction base="xs:string"> <xs:enumeration value="max"/> <xs:enumeration value="imax"/> <xs:enumeration value="rmax"/> <xs:enumeration value="min"/> <xs:enumeration value="imin"/> <xs:enumeration value="rmin"/> <xs:enumeration value="card"/> <xs:enumeration value="dom"/> <xs:enumeration value="ran"/> <xs:enumeration value="POW"/> <xs:enumeration value="POW1"/> <xs:enumeration value="FIN"/> <xs:enumeration value="FIN1"/> <xs:enumeration value="union"/> <xs:enumeration value="inter"/> <xs:enumeration value="seq"/> <xs:enumeration value="seq1"/> <xs:enumeration value="iseq"/> <xs:enumeration value="iseq1"/> <xs:enumeration value="-"/> <xs:enumeration value="-i"/> <xs:enumeration value="-r"/> <xs:enumeration value="~"/> <xs:enumeration value="size"/> <xs:enumeration value="perm"/> <xs:enumeration value="first"/> <xs:enumeration value="last"/> <xs:enumeration value="id"/> <xs:enumeration value="closure"/> <xs:enumeration value="closure1"/> <xs:enumeration value="tail"/> <xs:enumeration value="front"/> <xs:enumeration value="rev"/> <xs:enumeration value="conc"/> <xs:enumeration value="succ"/> <xs:enumeration value="pred"/> <xs:enumeration value="rel"/> <xs:enumeration value="fnc"/> <xs:enumeration value="real"/> <xs:enumeration value="floor"/> <xs:enumeration value="ceiling"/> <xs:enumeration value="tree"/> <xs:enumeration value="btree"/> <xs:enumeration value="top"/> <xs:enumeration value="sons"/> <xs:enumeration value="prefix"/> <xs:enumeration value="postfix"/> <xs:enumeration value="sizet"/> <xs:enumeration value="mirror"/> <xs:enumeration value="left"/> <xs:enumeration value="right"/> <xs:enumeration value="infix"/> <xs:enumeration value="bin"/> </xs:restriction> </xs:simpleType>
Simple Type: unary_pred_op
| Super-types: | xs:string < unary_pred_op (by restriction) |
|---|---|
| Sub-types: | None |
| Name | unary_pred_op |
|---|---|
| Content |
|
No documentation provided.
Simple Type: version_type
| Super-types: | xs:string < version_type (by restriction) |
|---|---|
| Sub-types: | None |
| Name | version_type |
|---|---|
| Content |
|
Represents the possible values for the `version` attribute for
the root element. Currently a unique value is possible, but if
the format evolves then new values will be created here.
Represents the possible values for the version attribute for
the root element. Currently a unique value is possible, but if
the format evolves then new values will be created here.
Glossary
Abstract (Applies to complex type definitions and element declarations). An abstract element or complex type cannot used to validate an element instance. If there is a reference to an abstract element, only element declarations that can substitute the abstract element can be used to validate the instance. For references to abstract type definitions, only derived types can be used.
All Model Group Child elements can be provided in any order in instances. See: http://www.w3.org/TR/xmlschema-1/#element-all.
Choice Model Group Only one from the list of child elements and model groups can be provided in instances. See: http://www.w3.org/TR/xmlschema-1/#element-choice.
Collapse Whitespace Policy Replace tab, line feed, and carriage return characters with space character (Unicode character 32). Then, collapse contiguous sequences of space characters into single space character, and remove leading and trailing space characters.
Disallowed Substitutions (Applies to element declarations). If substitution is specified, then substitution group members cannot be used in place of the given element declaration to validate element instances. If derivation methods, e.g. extension, restriction, are specified, then the given element declaration will not validate element instances that have types derived from the element declaration's type using the specified derivation methods. Normally, element instances can override their declaration's type by specifying an xsi:type attribute.
Key Constraint Like Uniqueness Constraint, but additionally requires that the specified value(s) must be provided. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.
Key Reference Constraint Ensures that the specified value(s) must match value(s) from a Key Constraint or Uniqueness Constraint. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.
Model Group Groups together element content, specifying the order in which the element content can occur and the number of times the group of element content may be repeated. See: http://www.w3.org/TR/xmlschema-1/#Model_Groups.
Nillable (Applies to element declarations). If an element declaration is nillable, instances can use the xsi:nil attribute. The xsi:nil attribute is the boolean attribute, nil, from the http://www.w3.org/2001/XMLSchema-instance namespace. If an element instance has an xsi:nil attribute set to true, it can be left empty, even though its element declaration may have required content.
Notation A notation is used to identify the format of a piece of data. Values of elements and attributes that are of type, NOTATION, must come from the names of declared notations. See: http://www.w3.org/TR/xmlschema-1/#cNotation_Declarations.
Preserve Whitespace Policy Preserve whitespaces exactly as they appear in instances.
Prohibited Derivations (Applies to type definitions). Derivation methods that cannot be used to create sub-types from a given type definition.
Prohibited Substitutions (Applies to complex type definitions). Prevents sub-types that have been derived using the specified derivation methods from validating element instances in place of the given type definition.
Replace Whitespace Policy Replace tab, line feed, and carriage return characters with space character (Unicode character 32).
Sequence Model Group Child elements and model groups must be provided in the specified order in instances. See: http://www.w3.org/TR/xmlschema-1/#element-sequence.
Substitution Group Elements that are members of a substitution group can be used wherever the head element of the substitution group is referenced.
Substitution Group Exclusions (Applies to element declarations). Prohibits element declarations from nominating themselves as being able to substitute a given element declaration, if they have types that are derived from the original element's type using the specified derivation methods.
Target Namespace The target namespace identifies the namespace that components in this schema belongs to. If no target namespace is provided, then the schema components do not belong to any namespace.
Uniqueness Constraint Ensures uniqueness of an element/attribute value, or a combination of values, within a specified scope. See: http://www.w3.org/TR/xmlschema-1/#cIdentity-constraint_Definitions.