Difference between pages "Mathematical Extensions" and "Parallel Composition using Event-B"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Pascal
 
imported>Mathieu
 
Line 1: Line 1:
−
Currently the operators and basic predicates of the Event-B mathematical language supported by Rodin are fixed.
+
[[User:Renato]] at [[Southampton]] is in charge of the [[Parallel Composition using Event-B]].
−
We propose to extend Rodin to define basic predicates, new operators or new algebraic types.
 
  
−
== Requirements ==
+
Composition is the process by which it is possible to combine different sub-systems into a larger system. Known and studied in several areas, this has the advantage of reusability and combination of systems especially when it comes to distributed systems. While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Our goal is to add this feature to the Rodin Platform (using Event-B notation) and study the concerns, properties, conditions, proof obligations, advantages and disadvantages when create/analysing system specifications. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties.
  
−
=== User Requirements ===
+
[[Image:share_event_machine.jpeg]]
−
* Binary operators (prefix form, infix form or suffix form).
 
−
* Operators on boolean expressions.
 
−
* Unary operators, such as absolute values.
 
−
: Note that the pipe, which is already used for set comprehension, cannot be used to enter absolute values (''in fact, as in the new design the pipe used in set comprehension is only a syntaxic sugar, the same symbol may be used for absolute value. To be confirmed with the prototyped parser. It may however be not allowed in a first time until backtracking is implemented, due to use of lookahead making assumptions on how the pipe symbol is used. -Mathieu ).
 
−
* Basic predicates (e.g., the symmetry of relations <math>sym(R) \defi R=R^{-1}</math>).
 
−
: Having a way to enter such predicates may be considered as syntactic sugar, because it is already possible to use sets (e.g., <math>R \in sym</math>, where <math>sym \defi \{R \mid R=R ^{-1}\}</math>) or functions (e.g., <math>sym(R) = \True</math>, where <math>sym \defi (\lambda R \qdot R \in A \rel B \mid \bool(R = R^{-1}))</math>).
 
−
* Quantified expressions (e.g., <math>\sum x \qdot P \mid y</math>, <math>\prod x \qdot P \mid y</math>, <math>~\min(S)</math>, <math>~\max(S)</math>).
 
−
* Types.
 
−
** Enumerated types.
 
−
** Scalar types.
 
  
−
=== User Input ===
+
[[Image:share_event_mach_comp1.jpeg]]
−
The end-user shall provide the following information:
+
[[Image:share_event_machine_comp2.jpg]]
−
* keyboard input
 
−
* Lexicon and Syntax. <br/>More precisely, it includes the symbols, the form (prefix, infix, postfix), the grammar, associativity (left-associative or right associative), commutativity, priority, the mode (flattened or not), ...
 
−
* Pretty-print. <br/>Alternatively, the rendering may be determined from the notation parameters passed to the parser.
 
−
* Typing rules.
 
−
* Well-definedness.
 
  
−
=== Development Requirements ===
+
A machine '''''S''''' with events '''''e1, e2, e3''''' and '''''e4''''' and variables '''''v1, v2''''' and '''''v3''''' can be decomposed using event (de)-composition of event ''e2'' (as can be seen above). This would result in the machine '''''S1''''' and '''''S2''''' that have a partial part of the event ''e2'': machine ''S1'' has the part related to the variable ''v1'' (''e2''') and machine ''S2'' has the part related to the machine ''v2'' (''e2''<nowiki>''</nowiki>). Also some other events are separated (''e1'' and ''v1'' only exist on machine ''S1'' and events ''e3'' and ''e4'' with variable ''v3'' only exist on the machine ''S2'') as can be seen above.
−
* Scalability.
 
  
−
== Towards a generic AST ==
+
The composition is based on proposals for parallel composition in Event-B in the following paper: [http://deploy-eprints.ecs.soton.ac.uk/51/].
  
−
The following AST parts are to become generic, or at least parameterised:
+
A release of the composition plugin for Rodin 0.8.2 is available (email me:ras07r@ecs.soton.ac.uk).  
−
* [[Constrained_Dynamic_Lexer | Lexer]]
 
−
* [[Constrained Dynamic Parser | Parser]]
 
−
* Nodes ( Formula class hierarchy ): parameters needed for:
 
−
** Type Solve (type rule needed to synthesize the type)
 
−
** Type Check (type rule needed to verify constraints on children types)
 
−
** WD (WD predicate)
 
−
** PrettyPrint (tag image + notation (prefix, infix, postfix) + needs parentheses)
 
−
** Visit Formula (getting children + visitor callback mechanism)
 
−
** Rewrite Formula (associative formulæ have a specific flattening treatment)
 
−
* Types (Type class hierarchy): parameters needed for:
 
−
** Building the type expression (type rule needed)
 
−
** PrettyPrint (set operator image)
 
−
** getting Base / Source / Target type (type rule needed)
 
−
* Verification of preconditions (see for example <tt>AssociativeExpression.checkPreconditions</tt>)
 
  
−
=== Vocabulary ===
+
A release for Rodin 0.9.2.1 is now available from the Rodin Main Update Site.
  
−
An '''extension''' is to be understood as a single additional operator definition.  
+
1. To create a new composition file (bcp file), go to Toolbar (on top), New>>Other... Event-B>>Composition Machine. Then select the project (if not selected already) and filename (by default is cm.bcp).
  
−
=== Tags ===
+
2. Bcp files are visible on Event-B perspective(from Rodin 0.9). For Rodin 0.8.2, go to Resource or Java perspective to edit the file.
  
−
Every extension is associated with an integer tag, just like existing operators. Thus, questions arise about how to allocate new tags and how to deal with existing tags.<br />
+
3. After editing the properties of the bcp file, you can generate a new bum file (machine), by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choose the option :'Create Composed Machine'. You will have to introduce a name for the new machine and after that is just press 'OK'.
−
The solution proposed here consists in keeping existing tags 'as is'. They are already defined and hard coded in the <tt>Formula</tt> class, so this choice is made with backward compatibility in mind.
 
  
−
Now concerning extension tags, we will first introduce a few hypotheses:
 
−
* Tags_Hyp1: tags are never persisted across sessions on a given platform
 
−
* Tags_Hyp2: tags are never referenced for sharing purposes across various platforms
 
−
In other words, cross-platform/session formula references are always made through their ''String'' representation. These assumptions, which were already made and verified for Rodin before extensions, lead us to restrict further considerations to the scope of a single session on a single platform.
 
  
−
The following definitions hold at a given instant <math>t</math> and for the whole platform.<br />
+
'''
−
Let <math>\mathit{EXTENSION}_t</math> be the set of extensions supported by the platform at instant <math>t</math>;<br /> let <math>\mathit{tag}_t</math> denote the affectation of tags to a extensions at instant <math>t</math> (<math>\mathit{tag}_t \in \mathit{EXTENSION}_t \pfun \intg</math>);<br /> let <math>\mathit{COMMON}</math> be the set of existing tags defined by the <tt>Formula</tt> class (<math>\mathit{COMMON} \sub \intg</math>).<br /> The following requirements emerge:
+
==User Manual==
−
* Tags_Req1: <math>\forall t \qdot \mathit{tag}_t \in \mathit{EXTENSION}_t \tinj \intg</math>
+
'''
−
* Tags_Req2: <math>\forall e, t_1,t_2 \qdot \mathit{tag}_{t_1}(e)=\mathit{tag}_{t_2}(e)</math> where <math>t_1, t_2</math> are two instants during a given session
 
−
* Tags_Req3: <math>\forall t \qdot \ran(\mathit{tag}_t) \cap \mathit{COMMON} = \empty</math>
 
  
−
The above-mentioned scope-restricting hypothesis can be reformulated into: <math>\mathit{tag}</math> needs not be stable across sessions nor across platforms.
+
The Shared Event Composition Plugin is divided in 6 sections:
  
−
=== Formula Factory ===
+
* '''Refines''' : allows to define an abstract machine of this composed machine. It is a valid machine that exists on the project.
 +
* '''Includes''': to compose a model, it is necessary to define which sub-systems(machines) interact. The machines must be abstract (not refinements of other machines) and have to be valid. It is also possible to choose if the included machine invariant should be visible to the composed machine or not (for proof optimization).
 +
* '''Sees''': allows to add contexts to the composed machine. The contexts seen by the ''included machines'' are visible to the composed machine. So it is only allowed to see contexts that are not already seen by the composed machine.
 +
* '''Invariants''': allows the inclusion of invariant clauses to the composed file. The inclusion of more invariants (from the included machines) depends on the user’s choice on ''Includes''. The defined invariants on the composed machine are “joint” properties between the included machines (gluing invariants), so variables and contexts from all the included machines become part of the composed machine scope.
 +
*'''Variant''': since the composed machine can be a refinement of an abstract model, there is the possibility of introducing new events. In order to avoid divergence, variants are necessary for the new events.
 +
*'''Composes Events''': the interaction between systems only happens when the composed events are synchronised and ready to be executed. The systems can interact through shared parameters. It is possible to define the following properties for composes events:
 +
** Name: name of the composes event
 +
** Extended/Not Extended: in the composes machine refines an abstract machine and if there are events with the same name, the concrete event can extend the abstract one (from Rodin 0.9).
 +
** Convergence: event can be chosen from ''Ordinary'', ''Convergence'' or ''Anticipated''.
  
−
The requirements about tags give rise to a need for centralising the <math>\mathit{tag}</math> relation in order to enforce tag uniqueness.
 
−
The Formula Factory appears to be a convenient and logical candidate for playing this role. Each time an extension is used to make a formula, the factory is called and it can check whether its associated tag exists, create it if needed, then return the new extended formula while maintaining tag consistency.
 
  
−
The factory can also provide API for requests about tags and extensions: getting the tag from an extension and conversely.
+
Still under '''Composes Events''', there are more properties that characterise a composed event:
 +
* '''Refines''' : possibility to choose if the composes event it is a refinement of an abstract event
 +
* '''Combines Event''': selection of the events that shall be composed. First the machine (out from the included machine list) is chosen and after, which event is supposed to be combined. It is possible to have only one combined event.
  
−
We also need additional methods to create extended formulæ. A first problem to address is: which type should these methods return ?
 
−
We could define as many extended types as the common AST API does, namely <tt>ExtendedUnaryPredicate</tt>, <tt>ExtendedAssociativeExpression</tt>, and so on, but this would lead to a large number of new types to deal with (in visitors, filters, …), together with a constraint about which types extensions would be forced to fit into. It is thus preferable to have as few extended types as possible, but with as much parameterisation as can be. Considering that the two basic types <tt>Expression</tt> and <tt>Predicate</tt> have to be extensible, we come to add two extended types <tt>ExtendedExpression</tt> and <tt>ExtendedPredicate</tt>.
 
  
−
ExtendedExpression makeExtendedExpression( ? )
+
The '''Combination of Events''' can be expressed as:
−
ExtendedPredicate makeExtendedPredicate( ? )
+
* The parameters are listed in one single (composed) event. Parameters (from different events) with the same name will be merged (becoming only one parameter). This correspond to the shared event composition with message passing, where a parameter is passed from one event to other.
 +
* The guards from the different combined events are merged using conjuction. So this composed event will be available if all the guards are true.
 +
* the actions are also merged and executed in parallel.
  
−
Second problem to address: which arguments should these methods take ?
+
Like mention above,a machine can be generated containing all the properties defined on the composed machine file. The generation of the new machine can be executed by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choosing the option :''Create Composed Machine''. A name for the new machine have to be introduced (a name is suggested by default ) and by clicking 'OK' or 'Override', a new machine file is generated.
−
Other factory methods take the tag, a collection of children where applicable, and a source location. In order to discuss what can be passed as argument to make extended formulæ, we have to recall that the make… factory methods have various kinds of clients, namely:
 
−
* parser
 
−
* POG
 
−
* provers
 
−
(other factory clients use the parsing or identifier utility methods: SC modules, indexers, …)
 
  
−
Thus, the arguments should be convenient for clients, depending on which information they have at hand.
 
−
The source location does not obviously seem to require any adaptation and can be taken as argument the same way. Concerning the tag, it depends on whether clients have a tag or an extension at hand. Both are intended to be easily retrieved from the factory. As a preliminary choice, we can go for the tag and adjust this decision when we know more about client convenience.
 
  
−
As for children, the problem is more about their types. We want to be able to handle as many children as needed, and of all possible types. Looking to existing formula children configurations, we can find:
 
−
* expressions with predicate children: <math>\mathit{bool}(P)</math>
 
−
* expressions with expression children: <math>E_1 + E_2</math>
 
−
* predicates with predicate children: <math>P_1 \limp P_2</math>
 
−
* predicates with expression children: <math>\mathit{partition}(S, E_1, E_2)</math>
 
−
* mixed operators: <math>\{x \qdot P(x) \mid E(x)\}</math>, but it is worth noting that the possibility of introducing bound variables in extended formulæ is not established yet.
 
−
Thus, for the sake of generality, children of both types should be supported for both extended predicates and extended expressions.
 
  
−
ExtendedExpression makeExtendedExpression(int tag, Expression[] expressions, Predicate[] predicates, SourceLocation location)
 
−
ExtendedPredicate makeExtendedPredicate(int tag, Expression[] expressions, Predicate[] predicates, SourceLocation location)
 
  
−
=== Defining Extensions ===
+
[[Category:Parallel composition plugin]]
−
 
+
[[Category:User documentation]]
−
An extension is meant to contain every information and behaviour required by:
 
−
* Keyboard
 
−
* (Extensible Fonts ?)
 
−
* Lexer
 
−
* Parser
 
−
* AST
 
−
* Static Checker
 
−
* Proof Obligation Generator
 
−
* Provers
 
−
 
 
−
==== Keyboard requirements ====
 
−
 
 
−
'''Kbd_req1''': an extension must provide an association combo/translation for every uncommon symbol involved in the notation.
 
−
 
 
−
==== Lexer requirements ====
 
−
 
 
−
'''Lex_req1''': an extension must provide an association lexeme/token for every uncommon symbol involved in the notation.
 
−
 
 
−
==== Parser requirements ====
 
−
 
 
−
According to [[Constrained_Dynamic_Parser| the Parser page]], the following informations are required by the parser in order to be able to parse a formula containing a given extension.
 
−
 
 
−
* symbol compatibility
 
−
* group compatibility
 
−
* symbol precedence
 
−
* group precedence
 
−
* notation (see below)
 
−
 
 
−
==== AST requirements ====
 
−
 
 
−
The following hard-coded concepts need to be reified for supporting extensions in the AST. An extension instance will then provide these reified informations to an extended formula class for it to be able to fulfil its API. It is the expression of the missing information for a ''ExtendedExpression'' (resp. ''ExtendedPredicate'') to behave as a ''Expression'' (resp. ''Predicate''). It can also be viewed as the parametrization of the AST.
 
−
 
 
−
===== Notation =====
 
−
 
 
−
The notation defines how the formula will be printed. In this document, we use the following convention:
 
−
* <math>e_i</math> is the i-th child expression of the extended formula
 
−
* <math>p_i</math> is the i-th child predicate of the extended formula
 
−
 
 
−
''Example'': infix operator "<math>\lozenge</math>"
 
−
<math>e_1 \lozenge e_2 \lozenge \ldots \lozenge e_n</math>
 
−
 
 
−
We define the following notation framework:
 
−
 
 
−
[[Image:notation_uml.png]]
 
−
 
 
−
On the "<math>\lozenge</math>" infix operator example, the iterable notation would return sucessively:
 
−
* a ''IFormulaChild'' with index 1
 
−
* the ''INotationSymbol'' "<math>\lozenge</math>"
 
−
* a ''IFormulaChild'' with index 2
 
−
* the ''INotationSymbol'' "<math>\lozenge</math>"
 
−
* &hellip;
 
−
* a ''IFormulaChild'' with index <math>n</math>
 
−
 
 
−
For the iteration not to run forever, the limit <math>n</math> needs to be known: this is the role of the ''mapsTo()'' method, which fixes the number of children, called when this number is known (i.e. for a particular formula instance).
 
−
 
 
−
'''Open question''': how to integrate bound identifier lists in the notation ?
 
−
 
 
−
We may make a distinction between fixed-size notations (like n-ary operators for a given n) and variable-size notations (like associative infix operators).
 
−
While fixed-size notations would have no specific expressivity limitations (besides parser conflicts with other notations), only a finite set of pre-defined variable-size notation patterns will be proposed to the user. For technical reasons related to the parser,
 
−
 
 
−
The following features need to be implemented to support the notation framework:
 
−
* special meta variables that represent children (<math>e_i</math>, <math>p_i</math>)
 
−
* a notation parser that extracts a fixed-size notation pattern from a user-input String
 
−
 
 
−
===== Well-Definedness =====
 
−
 
 
−
WD predicates also are user-provided data.
 
−
 
 
−
''Example'':
 
−
<math>\mathit{D}(e_1) \land (\forall i \cdot i \in 1\mathit{..}(n-1) \Rightarrow (\mathit{D}(e_i) \Rightarrow \mathit{D}(e_{i+1})))</math>
 
−
 
 
−
In order to process WD predicates, we need to add the following features to the AST:
 
−
* the <math>\mathit{D}</math> operator
 
−
* expression variables (predicate variables already exist)
 
−
* special expression variables and predicate variables that denote a particular formula child (we need to refer to <math>e_1</math> and <math>e_i</math> in the above example)
 
−
* a ''parse()'' method that accepts these special meta variables and the <math>\mathit{D}</math> operator and returns a ''Predicate'' (a WD Predicate Pattern)
 
−
* a ''makeWDPredicate''(aWDPredicatePattern, aPatternInstantiation) method that makes an actual WD predicate
 
−
 
 
−
===== Type Check =====
 
−
 
 
−
An extension shall give a type rule, which consists in:
 
−
* type check predicates (addressed in this very section)
 
−
* a resulting type expression (only for expressions)
 
−
 
 
−
''Example'':
 
−
<math>(\forall i \cdot \mathit{type}(e_i) = \pow(\alpha)) \land (\forall i,j \cdot \mathit{type}(e_i)=\mathit{type}(e_j))</math>
 
−
 
 
−
Type checking can be reified provided the following new AST features:
 
−
* the <math>\mathit{type}</math> operator
 
−
* type variables (<math>\alpha</math>)
 
−
* the above-mentioned expression variables and predicate variables
 
−
* a ''parse()'' method that accepts these special meta variables and the <math>\mathit{type}</math> operator and returns a ''Predicate'' (a Type Predicate Pattern)
 
−
* a ''makeTypePredicate''(aTypePredicatePattern, aPatternInstantiation) method that makes an actual Type predicate
 
−
 
 
−
===== Type Solve =====
 
−
 
 
−
This section addresses type synthesizing for extended expressions (the resulting type part of a type rule). It is given as a type expression pattern, so that the actual type can be computed from the children.
 
−
 
 
−
''Example'':
 
−
  <math>\pow(\mathit{type}(e_1))</math>
 
−
 
 
−
In addition to the requirements for Type Check, the following features are needed:
 
−
* a ''parse()'' method that accepts special meta variables and the <math>\mathit{type}</math> operator and returns an ''Expression'' (a Type Expression Pattern)
 
−
* a ''makeTypeExpression''(aTypeExpressionPattern, aPatternInstantiation) method that makes an actual Type expression
 
−
 
 
−
==== Static Checker requirements ====
 
−
{{TODO}}
 
−
==== Proof Obligation Generator requirements ====
 
−
{{TODO}}
 
−
==== Provers requirements ====
 
−
{{TODO}}
 
−
 
 
−
=== Extension compatibility issues ===
 
−
{{TODO}}
 
−
 
 
−
== User Input Summarization ==
 
−
 
 
−
Identified required data entail the following user input:
 
−
 
 
−
{{TODO}}
 
−
 
 
−
== Impact on other tools ==
 
−
 
 
−
Impacted plug-ins (use a factory to build formulæ):
 
−
* <tt>org.eventb.core</tt>
 
−
: In particular, the static checker and proof obligation generator are impacted.
 
−
* <tt>org.eventb.core.seqprover</tt>
 
−
* <tt>org.eventb.pp</tt>
 
−
* <tt>org.eventb.pptrans</tt>
 
−
* <tt>org.eventb.ui</tt>
 
−
 
 
−
== Identified Problems ==
 
−
The parser shall enforce verifications to detect the following situations:
 
−
* Two mathematical extensions are not compatible (the extensions define symbols with the same name but with a different semantics).
 
−
* A mathematical extension is added to a model and there is a conflict between a symbol and an identifier.
 
−
* An identifier which conflicts with a symbol of a visible mathematical extension is added to a model.
 
−
 
 
−
Beyond that, the following situations are problematic:
 
−
* A formula has been written with a given parser configuration and is read with another parser configuration.
 
−
: As a consequence, it appears as necessary to remember the parser configuration.
 
−
: The static checker will then have a way to invalid the sources of conflicts (e.g., priority of operators, etc).
 
−
:: ''The static checker will then have a way to invalid the formula upon detecting a conflict (name clash, associativity change, semantic change...) [[User:Mathieu|mathieu]]
 
−
 
 
−
* A proof may free a quantified expression which is in conflict with a mathematical extension.
 
−
: SOLUTION #1: Renaming the conflicting identifiers in proofs?
 
−
 
 
−
== Open Questions ==
 
−
 
 
−
=== New types ===
 
−
Which option should we prefer for new types?
 
−
* OPTION #1: Transparent mode.
 
−
:In transparent mode, it is always referred to the base type. As a consequence, the type conversion is implicitly supported (weak typing).
 
−
:For example, it is possible to define the <tt>DISTANCE</tt> and <tt>SPEED</tt> types, which are both derived from the <math>\intg</math> base type, and to multiply a value of the former type with a value of the latter type.
 
−
 
 
−
* OPTION #2: Opaque mode.
 
−
:In opaque mode, it is never referred to the base type. As a consequence, values of one type cannot be converted to another type (strong typing).
 
−
:Thus, the above multiplication is not allowed.
 
−
:This approach has at least two advantages:
 
−
:* Stronger type checking.
 
−
:* Better prover performances.
 
−
:It also has some disadvantages:
 
−
:* need of ''extractors'' to convert back to base types.
 
−
:* need of extra circuitry to allow things like <math>x:=d*2</math> where <math>x, d</math> are of type <tt>DISTANCE</tt>
 
−
 
 
−
* OPTION #3: Mixed mode.
 
−
:In mixed mode, the transparent mode is applied to scalar types and the opaque mode is applied to other types.
 
−
 
 
−
=== Scope of the mathematical extensions ===
 
−
* OPTION #1: Project scope.
 
−
:The mathematical extensions are implicitly visible to all components of the project that has imported them.
 
−
* OPTION #2: Component scope.
 
−
:The mathematical extensions are only visible to the components that have explicitly imported them. However, note that this visibility is propagated through the hierarchy of contexts and machines (<tt>EXTENDS</tt>, <tt>SEES</tt> and <tt>REFINES</tt> clauses).
 
−
:An issue has been identified. Suppose that <tt>ext1</tt> extension is visible to component <tt>C1</tt> and <tt>ext2</tt> is visible to component <tt>C2</tt>, and there is no compatibility issue between <tt>ext1</tt> and <tt>ext2</tt>. It is not excluded that an identifier declared in <tt>C1</tt> conflict with a symbol in <tt>ext2</tt>. As a consequence, a global verification is required when adding a new mathematical extension.
 
−
 
 
−
== Bibliography ==
 
−
* J.R. Abrial, M.Butler, M.Schmalz, S.Hallerstede, L.Voisin, [http://deploy-eprints.ecs.soton.ac.uk/80 ''Proposals for Mathematical Extensions for Event-B''], 2009.
 
−
:This proposal consists in considering three kinds of extension:
 
−
# Extensions of set-theoretic expressions or predicates: example extensions of this kind consist in adding the transitive closure of relations or various ordered relations.
 
−
# Extensions of the library of theorems for predicates and operators.
 
−
# Extensions of the Set Theory itself through the definition of algebraic types such as  lists or ordered trees using new set constructors.
 
−
 
 
−
[[Category:Design proposal]]
 

Revision as of 08:59, 4 March 2009

User:Renato at Southampton is in charge of the Parallel Composition using Event-B.

Composition is the process by which it is possible to combine different sub-systems into a larger system. Known and studied in several areas, this has the advantage of reusability and combination of systems especially when it comes to distributed systems. While applying composition, properties must be maintained and proofs obligations need to be discharged in order for the final result to be considered valid. Our goal is to add this feature to the Rodin Platform (using Event-B notation) and study the concerns, properties, conditions, proof obligations, advantages and disadvantages when create/analysing system specifications. Since the composition maintains the monotonicity property of the systems, the sub-systems can be refined independently on a further stage, preserving composition properties.

Share event machine.jpeg

Share event mach comp1.jpeg Share event machine comp2.jpg

A machine S with events e1, e2, e3 and e4 and variables v1, v2 and v3 can be decomposed using event (de)-composition of event e2 (as can be seen above). This would result in the machine S1 and S2 that have a partial part of the event e2: machine S1 has the part related to the variable v1 (e2') and machine S2 has the part related to the machine v2 (e2''). Also some other events are separated (e1 and v1 only exist on machine S1 and events e3 and e4 with variable v3 only exist on the machine S2) as can be seen above.

The composition is based on proposals for parallel composition in Event-B in the following paper: [1].

A release of the composition plugin for Rodin 0.8.2 is available (email me:ras07r@ecs.soton.ac.uk).

A release for Rodin 0.9.2.1 is now available from the Rodin Main Update Site.

1. To create a new composition file (bcp file), go to Toolbar (on top), New>>Other... Event-B>>Composition Machine. Then select the project (if not selected already) and filename (by default is cm.bcp).

2. Bcp files are visible on Event-B perspective(from Rodin 0.9). For Rodin 0.8.2, go to Resource or Java perspective to edit the file.

3. After editing the properties of the bcp file, you can generate a new bum file (machine), by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choose the option :'Create Composed Machine'. You will have to introduce a name for the new machine and after that is just press 'OK'.


User Manual

The Shared Event Composition Plugin is divided in 6 sections:

  • Refines : allows to define an abstract machine of this composed machine. It is a valid machine that exists on the project.
  • Includes: to compose a model, it is necessary to define which sub-systems(machines) interact. The machines must be abstract (not refinements of other machines) and have to be valid. It is also possible to choose if the included machine invariant should be visible to the composed machine or not (for proof optimization).
  • Sees: allows to add contexts to the composed machine. The contexts seen by the included machines are visible to the composed machine. So it is only allowed to see contexts that are not already seen by the composed machine.
  • Invariants: allows the inclusion of invariant clauses to the composed file. The inclusion of more invariants (from the included machines) depends on the user’s choice on Includes. The defined invariants on the composed machine are “joint” properties between the included machines (gluing invariants), so variables and contexts from all the included machines become part of the composed machine scope.
  • Variant: since the composed machine can be a refinement of an abstract model, there is the possibility of introducing new events. In order to avoid divergence, variants are necessary for the new events.
  • Composes Events: the interaction between systems only happens when the composed events are synchronised and ready to be executed. The systems can interact through shared parameters. It is possible to define the following properties for composes events:
    • Name: name of the composes event
    • Extended/Not Extended: in the composes machine refines an abstract machine and if there are events with the same name, the concrete event can extend the abstract one (from Rodin 0.9).
    • Convergence: event can be chosen from Ordinary, Convergence or Anticipated.


Still under Composes Events, there are more properties that characterise a composed event:

  • Refines : possibility to choose if the composes event it is a refinement of an abstract event
  • Combines Event: selection of the events that shall be composed. First the machine (out from the included machine list) is chosen and after, which event is supposed to be combined. It is possible to have only one combined event.


The Combination of Events can be expressed as:

  • The parameters are listed in one single (composed) event. Parameters (from different events) with the same name will be merged (becoming only one parameter). This correspond to the shared event composition with message passing, where a parameter is passed from one event to other.
  • The guards from the different combined events are merged using conjuction. So this composed event will be available if all the guards are true.
  • the actions are also merged and executed in parallel.

Like mention above,a machine can be generated containing all the properties defined on the composed machine file. The generation of the new machine can be executed by using the green button on the toolbar (CM - symbol of machine) or by right clicling on the bcp file and choosing the option :Create Composed Machine. A name for the new machine have to be introduced (a name is suggested by default ) and by clicking 'OK' or 'Override', a new machine file is generated.

Retrieved from ‘https://wiki.event-b.org/index.php?title=Mathematical_Extensions&oldid=6309’