Difference between pages "Generic Event-B EMF extensions" and "Rodin Platform 3.5.0 External Plug-ins"

From Event-B
(Difference between pages)
Jump to navigationJump to search
 
 
Line 1: Line 1:
==Modelling==
+
==== Rodin Update Site ====
  
==Persistence==
+
Available from http://rodin-b-sharp.sourceforge.net/updates
  
Event-B EMF Models may be persisted in several ways:
+
<!--
# inside a Rodin file by extending Rodin and the Event-B EMF persistence with new Rodin elements and synchronisers to load and save. (This is how the Event-B EMF core plugin works, except that the Rodin elements for standard Event-B already existed).
 
# inside a Rodin file as a String attribute containing XMI, using the SerialisedExtensionSynchroniser. (This is how UML-B diagrams are saved inside Machines)
 
# in EMF format as an XMI file.
 
# in plain text using the XText framework.
 
  
Here we mainly focus on methods 2 and 3.
+
  Please use one of the following templates for the Status column
We are also developing method 4. as a text persistence, but this is described elsewhere.
 
We do not intend to use method 1 as we do not need Rodin to understand the model (because we translate into standard Machines and Context for verification).
 
  
For method 2, declare your root meta-class to use the ''SerialisedExtensionSynchroniser'' using the extension point ''org.eventb.emf.persistence.synchroniser'' e.g.
+
    <span style="color:green"> available </span>
  <extension
+
    <span style="color:green"> new release </span>
        point="org.eventb.emf.persistence.synchroniser">
+
    <span style="color:#8B4513"> not checked </span>
      <emfPackage
+
    <span style="color:red"> not available </span>
            name="Statemachines Package"
 
            nsURI="http://soton.ac.uk/models/eventb/statemachines/2014">
 
        <synchroniser
 
              emf_class="Statemachine"
 
              name="Statemachine"
 
              rodin_id="ac.soton.eventb.emf.core.extension.persistence.serialisedExtension"
 
              synchroniser_class="ac.soton.eventb.emf.core.extension.persistence.SerialisedExtensionSynchroniser">
 
        </synchroniser>
 
      </emfPackage>
 
  </extension>
 
  
For method 3, due to the way the Event-B EMF framework implements references, it is important to save files using certain non-default styles.
+
-->
To achieve this, declare the content type of your file as ''ac.soton.eventb.emf.core.extension.persistence.contentType'' using the extension point ''org.eclipse.core.contenttype.contentTypes'' e.g.
 
  <extension
 
        point="org.eclipse.core.contenttype.contentTypes">
 
      <file-association
 
            content-type="ac.soton.eventb.emf.core.extension.persistence.contentType"
 
            file-extensions="umlb">
 
      </file-association>
 
  </extension>
 
  
==Navigator==
+
{{SimpleHeader}}
 +
|-
 +
! scope=col |  || Plug-in name || Version ||  Status || MCV* || Release Date || Contact || Additional info
 +
|-
 +
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Classdiagrams|Event-B Class Diagrams]] || 2.0.0 ||<span style="color:green"> new release </span> || 3.x.x || 4 Nov 2018  || [mailto:cfs@ecs.soton.ac.uk email] || Class diagrams contained in Event-B Machines.
 +
|-
 +
| [[Image:IUMLB_big.png|30px]] || [[Event-B_Statemachines|Event-B State-machines]] || 4.0.0 ||<span style="color:green"> new release </span> || 3.x.x || 4 Nov 2018  || [mailto:cfs@ecs.soton.ac.uk email] || State-machines contained in Event-B Machines.
 +
|-
 +
| [[Image:IUMLB_big.png|30px]] ||[[Event-B_Statemachines|Event-B State-machine Animation]] || 2.4.0 ||<span style="color:green"> new release </span> || 3.x.x || 4 Nov 2018 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with Event-B statemachines  3.x.x and ProB 3.0.x.
 +
|-
 +
| ||[[EMF_framework_for_Event-B|Event-B EMF framework]] || 6.0.0 ||<span style="color:green"> new release </span> || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
 +
|-
 +
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for extensions]] || 6.0.0 ||<span style="color:green"> new release </span> || 3.x.x || 17th Dec 2015  || [mailto:cfs@ecs.soton.ac.uk email] || Provided for plug-in developers.  End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
 +
|-
 +
| ||[[Generic_Event-B_EMF_extensions|Event-B EMF support for diagrams]] || 7.0.0 ||<span style="color:green"> new release </span> || 3.2.x || 17th Dec 2015  || [mailto:cfs@ecs.soton.ac.uk email] ||  Provided for plug-in developers.  End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
 +
|-
 +
| [[Image:Rose.gif|30px]]||[[Rose_(Structured)_Editor|Rose editor]] || 1.7.0 ||<span style="color:green"> new release </span> || 3.x.x || 4 Nov 2018 || [mailto:cfs@ecs.soton.ac.uk email] || Mainly useful for Plug-in developers. Tree-structured editor for Event-B EMF that handles extensions without modification
 +
|-
 +
| [[Image:Project diagram icon s.png|30px]]||[[Project_Diagram|Project Diagram]]|| 1.0.1 ||<span style="color:#8B4513"> not checked </span> || 3.x.x || 1st Feb. 2015 || [mailto:vs2@ecs.soton.ac.uk email] || Machine - Context relationship diagram
 +
|-
 +
| [[Image:Umlb32.gif|30px]] || [[UML-B|UML-B]] || 2.3.0 ||<span style="color:#8B4513"> not checked </span>|| 3.x.x || 18th Oct. 2014 || [mailto:cfs@ecs.soton.ac.uk email] || Original UML-B modelling environment
 +
|-
 +
| [[Image:Umlb32.gif|30px]] ||[[UML-B_-_Statemachine_Animation|UML-B Statemachine Animation]] || 1.3.0 ||<span style="color:#8B4513"> not checked </span> || 3.x.x || 18th Oct. 2014 || [mailto:vs2@ecs.soton.ac.uk email] || Compatible with UML-B 2.3 and ProB 3.0
 +
|-
 +
| ||[[EMF_Compare_Editor_installation|Teamwork]] || 1.2.0 || <span style="color:#8B4513"> not checked </span>  || 3.2.x || 5th Sept. 2016 || [mailto:cfs@ecs.soton.ac.uk email] || Provides a synchronised copy of Machines and Contexts for committing into a repository. It is recommended to also install the Rose editor,  EMF compare 3.1.0 and a recent repository client (e.g. Egit 4.1.4).
 +
|-
 +
| [[Image:Cmp_mch_obj.gif|20px]] ||[[Parallel_Composition_using_Event-B | Shared Event Composition]] || 1.7.1 || <span style="color:#8B4513"> not checked </span> || || 5th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 5/05/17)
 +
|-
 +
| [[Image:DecompositionPlug-in_logo.png|30px]] || [[Decomposition Plug-in User Guide | Decomposition]] || 1.3.1 || <span style="color:#8B4513"> not checked </span>|| || 4th July 2017 || [mailto:cfs@ecs.soton.ac.uk email] || Compatible with Rodin 3.x.x (checked by cfs 4/05/17)
 +
|-
 +
| ||[[Refactoring Framework | Refactory ]]|| 1.3.0 || <span style="color:#8B4513"> not checked</span>|| 3.x.x || 6th May 2014 || [mailto:asf08r@ecs.soton.ac.uk email] || Compatible with Rodin 3.0.x.
 +
|-
 +
| || [[Theory Plug-in| Theory Plug-in]] || 3.0.0 ||<span style="color:#8B4513"> not checked</span>||  || 17th Dec 2014|| [mailto:asf08r@ecs.soton.ac.uk email] ||
 +
|-.x
 +
| || [[Code Generation Activity | Code Generation]] || 0.2.5 ||<span style="color:#8B4513"> not checked</span>||  || 29th Aug. 2013|| [mailto:ae2@ecs.soton.ac.uk email] || For Java, Ada, and OpenMP C code
 +
|-.x
 +
|-
 +
| || Relevance Filter || 1.1.1 ||  <span style="color:green"> available </span>  || ?.x.x || || ||
 +
|-
 +
| || [[Isabelle for Rodin]] || || <span style="color:#8B4513"> not checked</span> || 2.x.x || || ||
 +
|-
 +
| || [[SMT_Plug-in | SMT Solvers ]] || 1.4.0 || <span style="color:green"> available </span> || || 15th March 2016|| [mailto:lvoisin@users.sourceforge.net Laurent Voisin]  ||
 +
|-
 +
| || [[Pattern | Pattern]] || 0.9.0 || <span style="color:#8B4513"> not checked</span> || 3.x.x || 13th March 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
 +
|-
 +
| || [[Event-B Qualitative Probability User Guide | Qualitative Probability]] || 0.2.3 || <span style="color:green"> available </span> || 3.x.x || 9th October 2015 || [mailto:tshoang@users.sourceforge.net Thai Son Hoang] ||
 +
|-
 +
| || [[B2Latex | B2Latex export]] || 0.7.0 ||<span style="color:green"> available </span>|| 2.5.x || 27th May 2015 || [mailto:lvoisin@users.sourceforge.net Laurent Voisin] ||
 +
|-
 +
| || [[Generic Instantiation Plug-in User Guide | Generic Instantiation (Soton)]] || 1.0.1 || <span style="color:#8B4513"> not checked</span> || || 05th March 2013 || [mailto:asf08r@ecs.soton.ac.uk email] ||
 +
|-
 +
| ||[[Records|Records]] || 2.0.0 || <span style="color:green"> available </span> || 2.x.x || 16th Oct. 2010 || [mailto:cfs@ecs.soton.ac.uk email] ||
 +
|}
  
This section describes how to extend the Event-B Navigator to support Event-B EMF extensions.
+
==== Atelier B Update Site ====
  
===Contributing new EMF element types to the Navigator view===
+
Available from http://methode-b.com/update_site/atelierb_provers
  
If the EMF element types are contained in a new file type, declare the new file extension using the extension point:
+
{{SimpleHeader}}
 +
|-
 +
! scope=col |  || Plug-in name || Version ||  Status || MCV* || Release Date || Contact || Additional info
 +
|-
 +
| || Atelier B provers || 2.2.1 || <span style="color:green">available</span> || 3.3.0 || 7 Aug 2017  || || Provers from Atelier B
 +
|}
  
ac.soton.eventb.emf.core.extension.navigator.emfFileExtensions
+
==== ProB Update Site ====
  
This tells the extensions plugin to adapt the emf contents of those files to be shown in the Navigator.
+
Available from http://www.stups.hhu.de/prob_updates_rodin3
  
To ensure the EMF elements are labeled and imaged correctly in the Navigator, declare the adapter factory using the extension point:
+
{{SimpleHeader}}
 +
|-
 +
! scope=col |  || Plug-in name || Version ||  Status || MCV* || Release Date || Contact || Additional info
 +
|-
 +
| || ProB || 3.0.10 || <span style="color:green">available</span> || 3.5.0 || 4 Sep 2020  || || The ProB animator and model checker
 +
|-
 +
| || ProB (Dis)Prover || 3.0.9 || <span style="color:green">available</span> || 3.5.0 || 4 Sep 2020  || || The ProB counter-example finder and prover
 +
|-
 +
| || ProB Symbolic constants support || 3.0.9 || <span style="color:green">available</span> || 3.5.0 || 4 Sep 2020  || ||
 +
|}
  
ac.soton.eventb.emf.core.extension.navigator.adapterFactories
+
==== Southampton Releases Update Site ====
 +
Available from http://eventb-soton.github.io/updateSite/releases
  
(Note - use the adapter factory generated by the EMF genmodel in the edit plugin).
+
{{SimpleHeader}}
 
+
|-
==Refinement==
+
! scope=col |  || Plug-in name || Version ||  Status || MCV* || Release Date || Contact || Additional info
 
+
|-
[THIS SECTION NEEDS REVIEW AND UPDATE]
+
| [[Image:CamilleX.png|CmX]] || [[CamilleX|CamilleX]] || 2.0.0 ||<span style="color:green"> new version </span> || 3.4.0 || 29 Jul 2020 || [mailto:T.S.Hoang@ecs.soton.ac.uk Thai Son Hoang] || CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.
 
+
|-
The Rodin platform provides an extension point for contributing behaviour to the 'Refine' action.
 
For Serialised Event-B EMF extensions, an abstract, reflective refinement contributor class is provided to simplify the task of making a refinement.
 
 
 
The class is:
 
  ac.soton.eventb.emf.core.extension.navigator.refiner$AbstractExtensionRefiner which implements IRefinementParticipant.
 
 
 
The class should be extended by a client plug-in and the client's class should be registered as a Refinement Participant using the relevant Rodin extension point
 
The client class must implement the method getExtensionID() to return the relevant Extension ID string that identifies such extensions.
 
The client class may override populateReferenceMap(Map<EReference,Boolean>) to add the EReference Features that need to be dealt with, defining which ones are back references to the corresponding abstract element (put true in map) and which ones should reference the corresponding element in the copy (put false in map).
 
The client class may also override populateFilterByTypeList(List<EClass>) to add the EClass of any types of element that should not be copied into the refinement.
 
 
 
The generic refiner class works as follows:
 
* All serialised extensions of the given Extension ID in the Rodin resource are loaded
 
* Each one is deep cloned using the Ecore copier utility
 
* The contents of the clone extension are then searched for any elements of the EClasses in the client supplied list to be filtered. Such elements are deleted from the clone.
 
* The contents of the clone extension are then searched for elements that own one of the client supplied EReferences.
 
* For each reference, the reference is either set to reference the corresponding source abstract element or copied so that it corresponds to the abstract reference
 
 
 
==Diagrams==
 
 
 
==Generator==
 
 
 
[THIS SECTION NEEDS REVIEW AND UPDATE -
 
Note: The generator is now based on a more generic EMF translator: https://github.com/eventB-Soton/EMF_Translator
 
It is adapted to Event-B : https://github.com/eventB-Soton/EventB_Translator_Support
 
There is a documentation plugin in the EMF translator source code that describes the necessary extension points and how to contribute a specific translation.]
 
 
 
A framework to support the implementation of generators is provided. The framework is designed to support the generation of standard Event-B models from higher-level model extensions that are based on the Event-B EMF modelling extensions framework.
 
 
 
The Generator framework provides:
 
 
 
* A toolbar button to initiate the generation
 
* Generic code to remove previously generated elements
 
* Generic code to organise the incorporation of newly generated elements
 
* Utilities to aid the creation of new elements
 
* An abstract basis for client defined rules
 
* An extension point for clients to declare generators and generation rules
 
 
 
The client rules return generation descriptors (rather than modifying the target model directly). The framework takes care of updating the model (within the clients Transactional Editing Domain) provided the generation completes successfully. This ensures that the model is not left in an inconsistent state should the generation fail. The generation descriptors allow the client to specify where the new element should be contained and a priority which will be used to influence the placement of the new element within the containment ordering.
 
 
 
To define a particular generator a client should:
 
 
 
* Define an extension of org.eclipse.ui.handlers to enable the generate command when the activePartID is their Editor (see [[Defining a generator handler]])
 
* Define an extension of ac.soton.eventb.emf.diagrams.generator.rule to make the generator framework aware of your generator and its rule classes.
 
* Implement your rule classes
 
 
 
=== Generation Descriptors ===
 
 
 
Each rule should return a collection of one or more Generation Descriptors. Generation Descriptors have the following fields which are explained in this section.
 
 
 
* EventBElement parent;
 
* EStructuralFeature feature;
 
* Object value;
 
* Integer priority;
 
* Boolean editable;
 
* Boolean remove;
 
 
 
The feature of the parent will be changed in the following ways:
 
 
 
If remove is false:
 
* 1) If the feature is a containment and the value is an element of the correct kind, the value will be added to the containment in a position according to the priority
 
* 2) If the feature is a reference and the value is an element of the correct kind, the value will be added to the reference in a position according to the priority
 
* 3) If the feature is an EAttribute and the value is of the correct type, the feature will be set to the value
 
 
 
Priority can be used to control the relative position of the generated elements 
 
* 1 - must come first
 
* 10 - not important
 
* ---user entered items---
 
* 0 must come after user entered items
 
* -10 must come last
 
 
 
Editable - this affects read-only status of the generated element and whether or not it will be preserved or re-generated in a subsequent generation.
 
* false - the element is set as read-only (the user cannot change its attributes nor add/remove children), any existing copy of the element will be deleted and re-generated at each re-generation
 
* true  - the element is not read-only and will not be deleted before re-generation. (N.B. It is the responsibility of the client rules to check whether this element already exists and only only generate a new one if it does not)
 
 
 
If remove is true:
 
* 1) If the feature is a containment and the value is an element of the correct kind, the value will be deleted from the containment
 
* 2) If the feature is a reference and the value is an element of the correct kind, the value will be removed from the reference
 
* 3) If the feature is an EAttribute, the feature will be unset
 
 
 
 
 
=== Implementing Rule Classes ===
 
 
 
Rule classes must implement IRule. It is recommended the rule classes extend ac.soton.eventb.emf.diagrams.generator#AbstractRule which provides some concise constants for the commonly needed containments and defines some default behaviour (always enabled and dependencies ok)Note that the rule will only be attempted for the type of source element defined in the extension point. However, this could be defined as an abstract base class to allow the rule to operate on several types of element.
 
 
 
A rule has 4 methods:
 
 
 
* boolean enabled (final EventBElement sourceElement)
 
* boolean dependenciesOK(EventBElement sourceElement,List<GenerationDescriptor> generatedElements)
 
* boolean fireLate()
 
* List<GenerationDescriptor> fire(EventBElement sourceElement, List<GenerationDescriptor> generatedElements)
 
 
 
The enabled method can be used to restrict when it applies. More than one rule can be defined for the same kind of element allowing the generation to be decomposed in a maintainable way.  
 
 
 
TheDependenciesOK method allows the method to be deferred since the success of rules may depend on what has already been generated. The dependenciesOK method is passed the list of GenerationDescriptors created so far.
 
 
 
The fireLate method forces the rule to be fired when all other rules have been fired. This is usually used when the rules behaviour depends on what other rules have done.
 
 
 
The fire method must return a list of GenerationDescriptors describing what should be generated. The Utility class, Make, provides a convenience method to help construct a GenerationDescriptor from the parent element, the containment feature, the new child and the priority indicator and if needed the editable setting.
 
 
 
Priority may be from 10 to -10, where 1 indicates first in the containment and -10 last in the containment. Elements in the containment that are not (currently) being generated are placed between priorities 10 and 0. Bear in mind that the relative position of different diagrams (extensions)is preserved within each priority band. Also the order of source elements within their containment is preserved within each priority band.
 
 
 
1 2 3 4 5 6 7 8 9 10 <other content> 0 -1 -2 -3 -4 -5 -6 -7 -8 -9 -10
 
 
 
For example, a basic type invariant that doesn't depend on other variables might be placed at position 1 whereas a theorem or invariant included purely for proof purposes might be placed at position -10.
 
 
 
A current limitation of the priority scheme is that there are a limited number of priorities. For example, this could be a problem if a rule needs to calculate positions of each element within a collection based on dependencies of the element instance.
 
 
 
In most cases the generated element should be set as read-only (the default). In this case the element will be deleted and re-generated on each invocation of the generator. The should not change any attributes of the element nor add to its children. In some case, however, it is necessary to generate an element whose contents may be modified by the user. To do this set the editable parameter of the Generation Descriptor. In this case the generated element will not be deleted when the generator is next invoked. The rule must take care not to return another Generation Descriptor if the element has already been generated. It should look for a suitable generated element (to use for adding further generated chldren etc.) and only generate a new one if it doesn't exist.
 
 
 
Where a tree structure is entirely generated within one rule firing (e.g. an event with guards and actions) it is more efficient to construct the entire event and return a single Generation Descriptor that adds that event. It is also possible to do this by returning separate Generation Descriptors to add the event and each guard and action individually.
 
 
 
A typical line from a rule class might look like this:
 
ret.add(Make.descriptor(machine,invariants,Make.invariant("myInvariantName", "myVar >0","my comment"),10));
 
where,
 
ret is the list to be returned and machine is the parent element containing the invariants to be added to.
 

Revision as of 09:45, 11 September 2020

Rodin Update Site

Available from http://rodin-b-sharp.sourceforge.net/updates


Plug-in name Version Status MCV* Release Date Contact Additional info
IUMLB big.png Event-B Class Diagrams 2.0.0 new release 3.x.x 4 Nov 2018 email Class diagrams contained in Event-B Machines.
IUMLB big.png Event-B State-machines 4.0.0 new release 3.x.x 4 Nov 2018 email State-machines contained in Event-B Machines.
IUMLB big.png Event-B State-machine Animation 2.4.0 new release 3.x.x 4 Nov 2018 email Compatible with Event-B statemachines 3.x.x and ProB 3.0.x.
Event-B EMF framework 6.0.0 new release 3.x.x 4 Nov 2018 email Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Event-B EMF support for extensions 6.0.0 new release 3.x.x 17th Dec 2015 email Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Event-B EMF support for diagrams 7.0.0 new release 3.2.x 17th Dec 2015 email Provided for plug-in developers. End users should not need to install this framework. It will be installed automatically by other plug-ins as required.
Rose.gif Rose editor 1.7.0 new release 3.x.x 4 Nov 2018 email Mainly useful for Plug-in developers. Tree-structured editor for Event-B EMF that handles extensions without modification
Project diagram icon s.png Project Diagram 1.0.1 not checked 3.x.x 1st Feb. 2015 email Machine - Context relationship diagram
Umlb32.gif UML-B 2.3.0 not checked 3.x.x 18th Oct. 2014 email Original UML-B modelling environment
Umlb32.gif UML-B Statemachine Animation 1.3.0 not checked 3.x.x 18th Oct. 2014 email Compatible with UML-B 2.3 and ProB 3.0
Teamwork 1.2.0 not checked 3.2.x 5th Sept. 2016 email Provides a synchronised copy of Machines and Contexts for committing into a repository. It is recommended to also install the Rose editor, EMF compare 3.1.0 and a recent repository client (e.g. Egit 4.1.4).
Cmp mch obj.gif Shared Event Composition 1.7.1 not checked 5th July 2017 email Compatible with Rodin 3.x.x (checked by cfs 5/05/17)
DecompositionPlug-in logo.png Decomposition 1.3.1 not checked 4th July 2017 email Compatible with Rodin 3.x.x (checked by cfs 4/05/17)
Refactory 1.3.0 not checked 3.x.x 6th May 2014 email Compatible with Rodin 3.0.x.
Theory Plug-in 3.0.0 not checked 17th Dec 2014 email
Code Generation 0.2.5 not checked 29th Aug. 2013 email For Java, Ada, and OpenMP C code
Relevance Filter 1.1.1 available ?.x.x
Isabelle for Rodin not checked 2.x.x
SMT Solvers 1.4.0 available 15th March 2016 Laurent Voisin
Pattern 0.9.0 not checked 3.x.x 13th March 2015 Thai Son Hoang
Qualitative Probability 0.2.3 available 3.x.x 9th October 2015 Thai Son Hoang
B2Latex export 0.7.0 available 2.5.x 27th May 2015 Laurent Voisin
Generic Instantiation (Soton) 1.0.1 not checked 05th March 2013 email
Records 2.0.0 available 2.x.x 16th Oct. 2010 email

Atelier B Update Site

Available from http://methode-b.com/update_site/atelierb_provers


Plug-in name Version Status MCV* Release Date Contact Additional info
Atelier B provers 2.2.1 available 3.3.0 7 Aug 2017 Provers from Atelier B

ProB Update Site

Available from http://www.stups.hhu.de/prob_updates_rodin3


Plug-in name Version Status MCV* Release Date Contact Additional info
ProB 3.0.10 available 3.5.0 4 Sep 2020 The ProB animator and model checker
ProB (Dis)Prover 3.0.9 available 3.5.0 4 Sep 2020 The ProB counter-example finder and prover
ProB Symbolic constants support 3.0.9 available 3.5.0 4 Sep 2020

Southampton Releases Update Site

Available from http://eventb-soton.github.io/updateSite/releases


Plug-in name Version Status MCV* Release Date Contact Additional info
CmX CamilleX 2.0.0 new version 3.4.0 29 Jul 2020 Thai Son Hoang CamilleX provides text editors for Event-B models and support modelling mechanisms such as machine inclusion.