Plug-in Tutorial

>next: Introduction

Tutorial for the extension of the Rodin platform by plugin addition

This tutorial is problem solving oriented. In a first part, we will focus on Rodin extensions to develop a plugin for Probabilistic Termination and Qualitative Reasoning. In a second part, we will study specific problem cases and extend Rodin to solve them. More details can be found in the Introduction.

Outline

• Introduction

First part (Probabilistic Termination and Qualitative Reasoning Plugin):

• 1 Creating our plug-in
• 2 Contributing new elements in the Rodin database
• 3 Adding support for new elements in the Rodin structured editor
• 4 Adding elements to the Event-B explorer
• 5 Providing help

Second part (Various problem solvings):

Projects

The archives of the projects built in this tutorial are available here: // FIXME. Add the links to the .zip files here.

>next: Introduction