Skip to content
No description, website, or topics provided.
Java TeX
Branch: master
Clone or download
Fetching latest commit…
Cannot retrieve the latest commit at this time.


Type Name Latest commit message Commit time
Failed to load latest commit information.


Meeduse was conceived in order to define proved executional semantics of domain specific languages (DSLs). It integrates the formal B method within EMF-based frameworks like XText, Sirius, GMF... The challenge of the TTC case study, for us, is to define and run model transformations as exectutional semantics using our tools: Meeduse for EMF integration and ProB for animation and model-checking.

To Use Meeduse please follow these steps:

  1. Clone this git repository on your computer

  2. Install Eclipse. There are 2 possiblilities

    1. Directly download Eclipse Oxygen (the tool was developed and tested on this eclipse version), from:

      Beware however that Eclipse Oxygen is incompatible with recent versions of openjdk java on Linux (version>9). On Windows and Mac we have tested using Oracle JavaRE (Java8)

    2. Download the latest Eclipse from Eclipse site. With recent versions, you will download an Eclipse installer - In that case install Eclipse Modelling tools

  3. Launch your eclipse and install Meeduse from the update site

    see for instructions on how to install software from update sites

  4. In order to replay the Meeduse solution for TTC'2019, you should import into your main workspace the three projects from folder eclipse_wksp:

    • ttc2019.metamodels: is provided by TTC'2019

    • Meeduse_tt2bdd: is a merging meta-model (Meeduse uses only one meta-model that's why we need to merge the TT meta-model and the BDD meta-model)

    • MeeduseRepo: is a driver that introduces a tt model into the merging model, and extracts a bdd from the merging model to a bdd model.

    see for instructions on importing existing projects into your workspace

  5. From your main eclipse workspace execute a runtime instance of eclipse: Select project Meeduse_tt2bdd, and right click Run As/Eclipse Application

  6. In the new Eclipse runtime instance, import the two projects from folder runtime_wksp:

    • is a sirius design project, if you would like to visualize a TT and a BDD
    • meeduse.tt2bdd.sample contains input models with their solutions.
  7. Follow the tutorial videos that we provide (click on the links bellow) and enjoy Meeduse.

    • it runs randomly the transformation rules until it consumes all the truth table rows and then automatically updates the model. We advise you to start by this tutorial video.

    • this is useful for debugging the transformation rules. This facility of Meeduse allows manual animation with an automatic update of the model at every step of the animation.

    • this solution is useful for big/huge examples, it shows how the ProB model-checker can be used outside Meeduse, and how its outputs can be loaded in Meeduse in order to update the model.

      N.B. If you would like to use ProB outside Meeduse (like in video, you need to install ProB and call command probcli: An example of a prob command is provided in file command.txt

You can find a brief summary of Meeduse with some demonstration videos at:


* Akram Idani: Grenoble INP, France - leader of the Meeduse project.
* German Vega: CNRS France.
* Michael Leuschel: University of Dusseldorf, Germany.


  • We woud like to thank Yves Ledru and Jean-Luc Richier for testing these artifacts on both Windows and Linux.
You can’t perform that action at this time.