Difference between pages "Constrained Dynamic Parser" and "Current Developments"

From Event-B
(Difference between pages)
Jump to navigationJump to search
imported>Mathieu
 
imported>Renato
 
Line 1: Line 1:
 
{{TOCright}}
 
{{TOCright}}
−
This page describes the requirements for a '''generic parser''' for the [[Event-B Mathematical Language]].
+
This page sum up the known developments that are being done around or for the [[Rodin Platform]]. ''Please contributes informations about your own development to keep the community informed''
  
−
A first design proposal is also drafted.
+
== Deploy Tasks ==
 +
The following tasks were planned at some stage of the [[Deploy]] project.
 +
=== Core Platform ===
 +
==== New Mathematical Language ====
 +
==== Rodin Index Manager ====
 +
[[Systerel]] is in charge of this task.
 +
{{details|Rodin Index Design|Rodin index design}}
  
−
== Requirements ==
+
The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.  
−
In order to be usable [[mathematical extensions]] require that the event-b mathematical language syntax can be extended by the final user.  
 
  
−
The lexical analyser and the syntaxic parser thus have to be extensible in a simple enough way (from a user point of vue).
+
==== Text Editor ====
 +
[[Düsseldorf]] has a prototype text-based editor for Event-B (courtesy of [[User:Fabian|Fabian]]). As of end of sempteber 2008, it still needs more work to fully integrate into Rodin.
  
−
=== Requirements Exported by the Current Language Design ===
+
[[Newcastle]] has another text editor based on EMF.  Among other things, it defines an EMF model of Event-B machines and contexts. At some point, the editor code is to be split into two plugins - an EMF adapater to rodin and the editor itself. Source code is currently available from [http://iliasov.org/editor-source.zip].
−
==== Operator Priority ====
 
−
* operator are defined by group,
 
−
* group of operator have a defined precedences,
 
−
* there may be precedences defined inside groups.
 
  
−
==== Operator Compatibility ====
+
=== Plug-ins ===
−
* a compatibility table defines allowed associativities inside a group,
+
==== Requirement Management Plug-in ====
−
* a compatibility table defines allowed associativities between groups (it allows to forbid a syntaxic construction like <math>f(x)^{-1}\;</math>
+
[[User:Jastram|Michael]] at [[Düsseldorf]] is in charge of the [[:Category:Requirement Plugin|Requirements Management Plug-in]].
−
: nota: this requirement was added afterwards with consistency in mind.
 
  
−
=== Expected Extension Schemes ===
+
{{See also|ReqsManagement|Requirements Tutorial|l1=Requirements Management Plug-in}}
−
We do want to at least define operators of the following form :
 
−
* infix : <math>a + b\;</math> or <math>a \vdash b : c\;</math>
 
−
* prefix : <math>\neg a\;</math>
 
−
* postfix : <math> R^*\;</math>
 
−
* closed : <math>\|a\|\;</math>
 
−
* parentheses sugar : <math>(a +b) * c\;</math>
 
−
* functional postfix : <math> a \langle b \rangle\;</math>
 
−
* functional prefix : <math>  \langle b \rangle f\;</math>
 
−
* lambda like : <math> \lambda x\mapsto y . P | E\;</math>
 
−
* Union like : <math> \Union\{ e \mid P\}</math> or <math> \Union\{ x,y . P \mid e\}</math>
 
−
* sets : <math>\{a, b, c + e\}\;</math> or <math>\{ e \mid P\}\;</math> or <math>\{x,y . P \mid e\}\;</math>
 
  
−
We also like to define precisely precedences and associativity between existing and new operators.
+
This plug-in allows:
 +
* Requirements to be edited in a set of documents (independently from Rodin)
 +
* Requirements to be viewed within Rodin
 +
* Individual Requirements to be linked to individual Event-B-Entities
 +
* A basic completion test to be performed
  
−
=== Requirements exported by the dynamic feature ===
+
==== UML-B Plug-in ====
−
* the precedence should not be enumerated but defined by a relation, like: '+' < '*' and '*' < '**', ...
+
[[Southampton]] is in charge of [[UML-B]] plug-in.
  
−
== Limitations ==
+
* Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
  
−
== Design Alternatives ==
+
*Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which has formerly been denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
  
−
=== Make Existing Parser Extensible ===
+
* Better support for state machine refinement in UML-B. This revision to UML-B allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines.
−
The existing parser is a LL recursive descent parser generated by the [http://www.ssw.uni-linz.ac.at/Coco/ Coco/R Compiler Generator], which makes extensive use of pre-computed lookahead, which makes it very difficult to be transformed in a sufficiently enough generic parser.
 
  
−
=== Parser Combinator ===
+
==== ProB Plug-in ====
−
:* on [http://en.wikipedia.org/wiki/Parser_combinator wikipedia]. Some implementations are referenced [http://pdos.csail.mit.edu/~baford/packrat/ here].
+
[[Düsseldorf]] is in charge of [[ProB]].
−
:* with functionnal language [http://wiki.portal.chalmers.se/agda/Agda Agda] : ''[http://www.cs.nott.ac.uk/~nad/publications/danielsson-norell-mixfix.pdf Parsing Mixfix Operators]
+
<!-- {{details|ProB current developments|ProB current developments}} -->
−
:: This paper is interesting in its proposal of using an acyclic graph to define operator precedence.
 
−
:* with functional language [http://user.cs.tu-berlin.de/~opal/opal-language.html OPAL] : ''[http://citeseerx.ist.psu.edu/viewdoc/download;jsessionid=8A8A8B39FFBF1AEF17C782C4822C5AF6?doi=10.1.1.58.655&rep=rep1&type=url&i=0 How To Obtain Powerful Parsers That Are Elegant and Practical]''
 
  
−
=== Pratt Parser ===
+
===== Work already performed =====
−
:* [http://portal.acm.org/citation.cfm?id=512931 original paper from Vaughan Pratt]
 
−
:* [http://effbot.org/zone/tdop-index.htm SImple ''Pratt'' parsing in python]
 
−
:* [http://javascript.crockford.com/tdop/tdop.html ''Pratt'' parsing in javascript]
 
−
Note that a ''pratt'' parser is essentially a parser for expressions (where expression parts are themselves expressions)... But it may be tweaked to limit the accepted sub-expressions or to enforce some non-expression parts inside an expression. More on that hereafter.
 
  
−
=== Some Existing Extensible Languages ===
+
We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences.
−
* [http://www.chrisseaton.com/katahdin/ Katahdin], and the associated paper [http://www.chrisseaton.com/katahdin/katahdin-thesis.pdf A Programming Language Where the Syntax and Semantics Are Mutable at Runtime] which describes the language and its implementation (in C#).
+
The model checking feature is now also accessible.
−
* [http://itcentre.tvu.ac.uk/~clark/xmf.html XMF] whose implementation seems not be describes in details.
+
It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB.
−
* [http://xlr.sourceforge.net/index.html XLR: Extensible Language and Runtime], which looks like a ''pratt'' parser according to the [http://xlr.svn.sourceforge.net/viewvc/xlr/trunk/xl2/xlr/parser.cpp?revision=805&view=markup sources].
+
On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB
−
* [http://www.pi-programming.org/What.html <math>\pi</math>] whose implementation seems not be describes in details (but sources availables).
+
specifications from Siemens).
  
−
== Design Proposal ==
+
On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.
−
=== Main Concepts ===
 
−
;symbol: a symbol is a lexem known by the parser.
 
−
;group: each symbol belongs to one and only one group.
 
−
;symbol compatibility: a relation telling if inside a group two symbol are compatibles.
 
−
:Two symbol are compatibles is they can be parsed without parentheses (see [[Event-B Mathematical Language]] for more on compatibility).
 
−
;group compatibility: a relation telling if two groups are compatibles.
 
−
:Two symbol of different groups are said compatibles if their group are compatibles.
 
−
;symbol associativity: a relation which gives the associative precedence of symbols inside a given group.
 
−
;group associativity: a relation which gives the associative precedence of groups.
 
−
:Two symbol of different groups have a relative precedence given by the associative precedence of their groups.
 
−
;generic parser: the parser which is defined.
 
−
: This parser may be called recursively (an infix expression being build upon a left and right sub-expression) and is often the default parser used when building the AST associated with a ''symbol''.
 
−
;specific parser: some specific parser, predefined as helper functions to build specific AST.
 
−
:Some example of specific parser are the one used to parse and build list of identifiers (for quantified predicates), mapplets lists (for lambda), and so one...
 
  
−
=== Proposed User Interface ===
+
===== Ongoing and future developments=====
−
''The hereafter proposition does not preclude the final UI to take other (more user friendly forms). But the concepts should probably stay the same''
 
  
−
We propose that the user will be able to create several predefined type of symbols (new types may certainly be further added by mean of eclipse extension points). When defining a symbol, the user can choose the parser used to parse the sub-expressions (default to generic parser, but a specific parser may be used) and can enforce the form of the resulting parsed sub-expression in terms of their AST root type.
+
We are currently developing a new, better user interface.
 +
We also plan to support multi-level animation with checking of the gluing invariant.
  
−
==== Predefined Symbol Builders ====
+
We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:
−
The proposed predefined symbol builders are:
+
* an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
−
;infix: For example predicate conjunction which expects two predicates for left and right parts may be defined by <code>infix("∧", gid="(logic pred)", expected_nonterm=["predicate", "predicate"])</code>
+
* a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
−
:As another example, substitution ≔ of group '(infix subst)' which expect two ''ident list'' for left and right expressions may be defined by <code>infix(symbol="≔", gid="(infix subst)", parsers=["ident_list", "ident_list"], expected_nonterm=["ident_list", "ident_list"])</code>
+
* a 2D viewer to inspect the state space of the specification
  
−
;prefix: <code>prefix("¬", "(not pred)", expected_nonterm=["predicate"])</code>
+
==== B2Latex Plug-in ====
 +
[[Southampton]] is in charge of [[B2Latex]].
  
−
;atomic: <code>atomic("⊤", "(atomic pred)")</code>
+
Kriangsak Damchoom will update the plug-in to add [[Event Extension|extensions of events]].
  
−
;prefix closed: used to build prefix symbol which must be followed by enclosing symbol(brackets, parentheses,..). For example <tt>finite</tt> may be defined by: <code>prefix_closed("finite", "(", ")","(atomic pred)", expected_nonterm=["expression"])</code>
+
==== Parallel Composition Plug-in ====
 +
[[Southampton]] is in charge of the [[Parallel Composition using Event-B]] .
  
−
:postfix: <code>postfix("∼", gid="(unary relation)", expected_nonterm=["expression"])</code>
+
The intention of the plug-in is to allow the parallel composition of events using Event-B syntax. The composition uses a value-passing style (shared event composition), where parameters can be shared/merged.
  
−
;quantified: <code>quantified("∀", "·", expected_nonterm=["predicate"]</code>
+
This plug-in allows:
 +
* Selection of machines that will be part of the composition (''Includes'' Section)
 +
* Possible selection of an abstract machine (''Refines'' Section)
 +
* Possible inclusion of invariants that relate the included machines (''Invariant'' Section and use of the monotonicity )
 +
* Invariants of included machines are conjoined.
 +
* Selection of events that will be merged. The event(s) must come from different machines. At the moment, events with parameters with same name are merged. If it is a refinement composition, it is possible to choose the abstract event that is being refined.
 +
* Initialisation event is the parallel composition of all the included machines' initialisations.
 +
* For a composed event, the guards are conjoined and the all the actions are composed in parallel.
  
−
;lambda like: <code>lambda_like("λ", "·", u"∣", gid="(quantification)", expected_nonterm=["ident list", "predicate", "expression"])</code>
+
Currently, after the conclusion of the composition machine, a new machine can be generated, resulting from the properties defined on the composition file. This allows proofs to be generated as well as a visualisation of the composition machine file. In the future, the intention is to make the validation directly on the composition machine file directly where proofs would be generated ( and discharged) - the new machine generation would be optional. An event-b model for the validation/generation of proofs in currently being developed. Another functionality which should be quite useful for the composition (but not restricted to that) is '''renaming''':
  
−
;quantified union like: <code>Union_like("⋃", "·", "∣", gid="(quantification)")</code>
+
* while composing, two machines may have variables with the same name for instance (which is not allowed for this type of composition). In order to solve this problem, one would have to rename one of the variables in order to avoid the clash, which would mean change the original machine. A possible solution for that would be to rename the variable but just on composition machine file, keeping the original machine intact. A renaming framework designed and developed by Stefan Hallerstede and Sonja Holl exists currently although still on a testing phase. The framework was developed to be used in a general fashion (not constrained to event-b syntax). The idea is to extend the development of this framework and apply to Event-B syntax (current development).
  
−
;closed sugar: use for parentheses added to enforce associativity: <code>closed_sugar("(", ")")</code>
+
There is a prototype for the composition plug-in available, but only works for Rodin 0.8.2. A release for the Rodin 0.9 is concluded and will be available from the Rodin Main Update Site soon, under the update 'Shared Event Composition'.
  
−
;functional postfix: <code>functional_postfix("(", ")", gid="(functional)", expected_nonterm=["expression", "expression"])</code>
+
==== Refactoring Framework Plug-in ====
 +
[[Southampton]] is in charge of the [[Refactoring Framework]].
  
−
Some right associative versions of those symbol builders may also be supplied (infix_right, or a specific parameter ''right associative'' parameter may also be provided to the ''infix'' symbol builder).
+
The intention of the plug-in is to allow the renaming/refactoring of elements on a file (and possible related files). Although created to be used in a general way, the idea is to embed this framework on the Rodin platform, using Event-B syntax. This plug-in was initially designed and developed by Stefan Hallerstede and Sonja Holl.
  
−
==== Predefined Specific Parser ====
+
This plug-in allows:
−
* expression lists
+
* Defining extensions that can be used to select related files.
−
* ident lists
+
* Defining extensions that can be used to rename elements based on the type of file.
−
* maplet tree (for lambda)
+
* Renaming of elements on a file and possible occurrences on related files.
 +
* Generating of a report of possible problems (clashes) that can occur while renaming.
  
 +
== Exploratory Tasks ==
 +
=== One Single View ===
 +
[[Maria]] is in charge of this exploratory work during is internship.
 +
{{details|Single View Design|Single View Design}}
 +
The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.
  
−
==== Defining Compatibility and Precedences ====
 
−
Inside a group, ''compatibility'' may be defined like:
 
−
<code>
 
−
    g = group["(binop)"]
 
−
    g.add_many_compatibility(
 
−
            [  ("∪", "∪"),
 
−
                ("∩", "∩"),
 
−
                ("∩", "∖"),
 
−
                ("∩", "▷"),
 
−
                ("∩", "⩥"),
 
−
                ("∘", "∘"),
 
−
                (";", ";"),
 
−
                (";", "▷"),
 
−
                (";", "⩥"),
 
−
                ("", ""),
 
−
                ("◁", "∩"),
 
−
                ("◁", "∖"),
 
−
                ("◁", ";"),
 
−
                ("◁", "⊗"),
 
−
                ("◁", "▷"),
 
−
                ("◁", "⩥"),
 
−
                ("⩥", "∩"),
 
−
                ("⩥", "∖"),
 
−
                ("⩥", ";"),
 
−
                ("⩥", "⊗"),
 
−
                ("⩥", "▷"),
 
−
                ("⩥", "⩥"),
 
−
                ("×", "×"), ]
 
−
</code>
 
−
which defines the compatibility table for expression binary operator as defined in [[Event-B Mathematical Language]].
 
  
  
−
Inside a group, ''precedence'' may be defined like:
+
== Others ==
−
<code>
 
−
g = group["(arithmetic)"]
 
−
g.add_many_precedence(
 
−
            [  ("^", "÷"),
 
−
                ("^", "∗"),
 
−
                ("^", "+"),
 
−
                ("^", "−"),
 
−
                ("^", "mod"),
 
−
                ("+", "∗"),
 
−
                ("−", "∗"),
 
−
                ("+", "÷"),
 
−
                ("−", "÷"),
 
−
                ("+", "mod"),
 
−
                ("−", "mod"), ] )
 
−
</code>
 
−
which defines ^ as having the least precedence amongst the operators of the expression arithmetic group.
 
  
−
Similarly, precedences and compatibilities between groups may be defined :
+
=== AnimB ===
−
<code>
+
[[Christophe]] devotes some of its spare time for this plug-in.
−
    group_precedence.add(("(binop)", "(interval)"))
+
{{details|AnimB Current Developments|AnimB Current Developments}}
−
    group_precedence.add(("(interval)", "(arithmetic)"))
+
The current developments around the [[AnimB]] plug-in encompass the following topics:
−
    group_precedence.add(("(arithmetic)", "(unary relation)"))
+
;Live animation update
−
    group_precedence.add(("(unary relation)", "(bound unary)"))
+
:where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
−
    group_precedence.add(( "(bound unary)", "(bool)"))
+
;Collecting history
 +
:The history of the animation will be collected.
  
−
    group_compatibility.add_all( [ "(binop)", "(interval)", (arithmetic)", "(unary relation)", "(unary relation)", "(bound unary)",....])
+
=== Team-Based Development ===
−
</code>
 
  
−
==== Some Difficulties ====
+
; Usage Scenarios
−
Some difficulties appear when trying to implement an event-b parser with the preceding scheme:
+
: In order to understand the problem properly, [http://www.stups.uni-duesseldorf.de/ Düsseldorf] created a number of usage [[Scenarios for Team-based Development]].
−
* A symbol may be declared by several different builders (thinf of unary and infix minus for example).
+
: A page as also been opened for [[Scenarios for Merging Proofs|merging proofs scenarios]].
−
** ''pratt'' parser are able to cope with a symbol appearing either at the beginning of an expression or inside an expression (see ''led'' and ''nud'' hereafter). For example, unary minus and infix minus wan be both defined by the proposed scheme.
+
[[Category:Work in progress]]
−
** but in their default form, ''pratt'' parser failed in parsing symbol like '{' which appears at the beginning of extension sets, comprehension sets and quantified sets.  
 
−
::The existing event-b parser use infinite lookahead to determine which one of those three sets is actually being parsed. We can not afford such a solution, as it would hinder extensibility of the parser. Implementing a backtracking parser is probably our best solution provided that we use memoisation to alleviate the cost of parsing formulas that require heavy backtracking.
 
  
−
* Defining a grammar or a grammar extension is not an easy job, even with those simple mechanisms.  
+
=== B2C ===
−
: It would certainly be a good idea to implement a user interface to grammar testing so that an extension designer as the mean to ensure that he agree with the parser on the semantic of (or at least on the AST obtained by using) its extension.
+
This plug-in translates Event-B models to C source code, which may then be compiled using external C development tools. [[Steve]] wrote B2C with the specific purpose of translating the [http://dx.doi.org/10.1007/978-3-540-87603-8_21 MIDAS] model, an Event-B implementation of a Virtual Machine instruction set.
  
−
=== Core Algorithm ===
+
B2C supports a sub-set of Event-B that can be easily translated to C form. The user provides a final refinement step that does nothing except restate the model in this translatable form: symbolic constants must be replaced by their literal values, range membership guards are replaced by greater-than and less-than guards, and actions are restated not to use global statments on their left-sides (this because the variable may have been modified by an earlier action, and may not be valid). The manipulations are done within EventB where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliability. This re-write process is currently a manual step, but could in principle be done by another plug-in
−
=== Sample Implementation ===
 
−
A prototype as been developed in Python to quickly try different solutions.  
 
  
−
The development tree is available at http://bitbucket.org/matclab/eventb_pratt_parser/
+
B2C source code is not currently available for download: contact [[Steve]] directly if it is required.
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
 
 
−
[[Category:Design Proposal]]
 

Revision as of 17:11, 10 December 2008

This page sum up the known developments that are being done around or for the Rodin Platform. Please contributes informations about your own development to keep the community informed

Deploy Tasks

The following tasks were planned at some stage of the Deploy project.

Core Platform

New Mathematical Language

Rodin Index Manager

Systerel is in charge of this task.

For more details on Rodin index design, see Rodin Index Design.

The purpose of the Rodin index manager is to store in a uniform way the entities that are declared in the database together with their occurrences. This central repository of declarations and occurrences will allow for fast implementations of various refactoring mechanisms (such as renaming) and support for searching models or browsing them.

Text Editor

Düsseldorf has a prototype text-based editor for Event-B (courtesy of Fabian). As of end of sempteber 2008, it still needs more work to fully integrate into Rodin.

Newcastle has another text editor based on EMF. Among other things, it defines an EMF model of Event-B machines and contexts. At some point, the editor code is to be split into two plugins - an EMF adapater to rodin and the editor itself. Source code is currently available from [1].

Plug-ins

Requirement Management Plug-in

Michael at Düsseldorf is in charge of the Requirements Management Plug-in.

See also: Requirements Management Plug-in and Requirements Tutorial

This plug-in allows:

  • Requirements to be edited in a set of documents (independently from Rodin)
  • Requirements to be viewed within Rodin
  • Individual Requirements to be linked to individual Event-B-Entities
  • A basic completion test to be performed

UML-B Plug-in

Southampton is in charge of UML-B plug-in.

  • Support for synchronisation of transitions from different statemachines. This feature will allow two or more transitions in different statemachines to contribute to a single event. This feature is needed because a single event can alter several variables (in this case statemachines) simultaneously.
  • Allow user to allocate the name of the 'implicit contextual instance' used in a class. Events and Transitions owned by a class are implicitly acting upon an instance of the class which has formerly been denoted by the reserved word 'self'. This modification allows the modeller to override 'self' (which is now the default name) with any other identifier. This feature is needed to avoid name clashes when synchronising transitions into a single event. It also allows events to be moved between different classes (or outside of all classes) during refinement without creating name clashes.
  • Better support for state machine refinement in UML-B. This revision to UML-B allows a statemachine to be recognised as a refinement of another one and to be treated in an appropriate way during translation to Event-B. The states and transitions of a refined statemachine can be elaborated by adding more detailed hierarchical statemachines.

ProB Plug-in

Düsseldorf is in charge of ProB.

Work already performed

We have now ported ProB to work directly on the Rodin AST. Animation is working and the user can now set a limited number of preferences. The model checking feature is now also accessible. It is also possible to create CSP and classical B specification files. These files can be edited with BE4 and animated/model checked with ProB. On the classical B side we have moved to a new, more robust parser (which is now capable of parsing some of the more complicated AtelierB specifications from Siemens).

On the developer side, we have moved to a continuous integration infrastructure using CruiseControl. Rodin is also building from CVS in that infrastructure.

Ongoing and future developments

We are currently developing a new, better user interface. We also plan to support multi-level animation with checking of the gluing invariant.

We have prototypes for several extensions working, but they need to be fully tested and integrated into the plugin:

  • an inspector that allows the user to inspect complex predicates (such as invariants or guards) as well as expressions in a tree-like manner
  • a graphical animator based on SWT that allows the user to design his/her own animations easily within the tool
  • a 2D viewer to inspect the state space of the specification

B2Latex Plug-in

Southampton is in charge of B2Latex.

Kriangsak Damchoom will update the plug-in to add extensions of events.

Parallel Composition Plug-in

Southampton is in charge of the Parallel Composition using Event-B .

The intention of the plug-in is to allow the parallel composition of events using Event-B syntax. The composition uses a value-passing style (shared event composition), where parameters can be shared/merged.

This plug-in allows:

  • Selection of machines that will be part of the composition (Includes Section)
  • Possible selection of an abstract machine (Refines Section)
  • Possible inclusion of invariants that relate the included machines (Invariant Section and use of the monotonicity )
  • Invariants of included machines are conjoined.
  • Selection of events that will be merged. The event(s) must come from different machines. At the moment, events with parameters with same name are merged. If it is a refinement composition, it is possible to choose the abstract event that is being refined.
  • Initialisation event is the parallel composition of all the included machines' initialisations.
  • For a composed event, the guards are conjoined and the all the actions are composed in parallel.

Currently, after the conclusion of the composition machine, a new machine can be generated, resulting from the properties defined on the composition file. This allows proofs to be generated as well as a visualisation of the composition machine file. In the future, the intention is to make the validation directly on the composition machine file directly where proofs would be generated ( and discharged) - the new machine generation would be optional. An event-b model for the validation/generation of proofs in currently being developed. Another functionality which should be quite useful for the composition (but not restricted to that) is renaming:

  • while composing, two machines may have variables with the same name for instance (which is not allowed for this type of composition). In order to solve this problem, one would have to rename one of the variables in order to avoid the clash, which would mean change the original machine. A possible solution for that would be to rename the variable but just on composition machine file, keeping the original machine intact. A renaming framework designed and developed by Stefan Hallerstede and Sonja Holl exists currently although still on a testing phase. The framework was developed to be used in a general fashion (not constrained to event-b syntax). The idea is to extend the development of this framework and apply to Event-B syntax (current development).

There is a prototype for the composition plug-in available, but only works for Rodin 0.8.2. A release for the Rodin 0.9 is concluded and will be available from the Rodin Main Update Site soon, under the update 'Shared Event Composition'.

Refactoring Framework Plug-in

Southampton is in charge of the Refactoring Framework.

The intention of the plug-in is to allow the renaming/refactoring of elements on a file (and possible related files). Although created to be used in a general way, the idea is to embed this framework on the Rodin platform, using Event-B syntax. This plug-in was initially designed and developed by Stefan Hallerstede and Sonja Holl.

This plug-in allows:

  • Defining extensions that can be used to select related files.
  • Defining extensions that can be used to rename elements based on the type of file.
  • Renaming of elements on a file and possible occurrences on related files.
  • Generating of a report of possible problems (clashes) that can occur while renaming.

Exploratory Tasks

One Single View

Maria is in charge of this exploratory work during is internship.

For more details on Single View Design, see Single View Design.

The goal of this project is to present everything in a single view in Rodin. So the user won't have to switch perspectives.


Others

AnimB

Christophe devotes some of its spare time for this plug-in.

For more details on AnimB Current Developments, see AnimB Current Developments.

The current developments around the AnimB plug-in encompass the following topics:

Live animation update
where the modification of the animated event-B model is instantaneously taken into account by the animator, without the need to restart the animation.
Collecting history
The history of the animation will be collected.

Team-Based Development

Usage Scenarios
In order to understand the problem properly, Düsseldorf created a number of usage Scenarios for Team-based Development.
A page as also been opened for merging proofs scenarios.

B2C

This plug-in translates Event-B models to C source code, which may then be compiled using external C development tools. Steve wrote B2C with the specific purpose of translating the MIDAS model, an Event-B implementation of a Virtual Machine instruction set.

B2C supports a sub-set of Event-B that can be easily translated to C form. The user provides a final refinement step that does nothing except restate the model in this translatable form: symbolic constants must be replaced by their literal values, range membership guards are replaced by greater-than and less-than guards, and actions are restated not to use global statments on their left-sides (this because the variable may have been modified by an earlier action, and may not be valid). The manipulations are done within EventB where they can be checked by the Proof Obligation system, and B2C made as simple as possible to maximise reliability. This re-write process is currently a manual step, but could in principle be done by another plug-in

B2C source code is not currently available for download: contact Steve directly if it is required.

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