Foreword

This webpage aims to present resources used for our tool presentation. For detailed manual, please see here

To use those resources, first please download the independent compilation of Tinker Core from one of the following links

Then please download the tinkerGUI from here or instead you can download the tinker repo and extract the file

$SOME_PATH/tinker/src/core/src/tinkerGUI/release/tinkerGUI-0.4.jar

You can extract above 2 files to the same directory for your convenience

For the demo project for our tool, please download from here.
This is the third approach of "Wen Su, Jean-Raymond Abrial. Aircraft Landing Gear System: Approaches with Event-B to the Modeling of an Industrial System".

Download 2 psgraph files for the demo from here

Finally download the plugin for Rodin platform from here,
and extract the .jar file into "plugins" folder in Rodin installation directory

Now the files are set, before you rush to use the plugin please set the following

Then you can import the Landing_Dev_3.zip as a project into Rodin workplace

Open the project. In the Event-B Explorer View, find the machine m0,
then for the DEMO 1, you could open the obligation X_act/inv19/INV,
and for the DEMO 2, you could open the obligation X_chg/inv21/INV

To repeat the proof in our demo, first prune all existing proof node

In the Proof Control View, click the to start proving.

If this is the first time you use the Plugin, a window will be prompted for you to select the default psgraph. If it is not the first time and you wish to use other psgraph files, please go to Preference -> Tinker Preference Page -> change default psgraph file to your desired file under the default folder.

On the auto-launched TinkerGUI, the following need to be clicked , once the connection is ready the icon will become . Details on how to start the GUI can be found in Tinker's user guide.

* Note, if you finished proving one obligation, and wish to switch to another one, please click on GUI, then Rodin will stop blocking you. Now you can switch to another obligation such as X_chg/inv21/INV, prune all existing nodes. *

* Note 2, if you wish to change PSGraph, before you click again ,please go to Preference -> Tinker Preference Page, and change "Default psgraph file" to your desired psgraph file, or you can reset it to blank, and the next time you click , you will be able to choose another file. *

* SERIOUS NOTE (WINDOWS Users only), because this is an ongoing project, the communication protocol is not determinined due to various reasons. The current protocol is: when user finish proof, the independent compiled Tinker Core for Rodin will shutdown in 15 seconds. If user wants to use Tinker Proof tool after 15 seconds of clicking , reconnection is required therefore user will need to firstly click and then click to connect again after clicking in Rodin. *

Proof recording

Tool demo