Introduction (Rodin Tutorial)

This tutorial should provide the user with a tour through the most important functionalities of RODIN, so that he gets a understanding of how the program works. The tutorial is divided into 5 sections:

In the first section, a very simple project is created from scratch. The essential steps in working with components are illustrated here.

The second section provides an example that shows how events of different machines can be connected together. It also gives an introduction on working with the prover.

After section 1 and 2, the user should have developed a feel of the basic windows of RODIN, and when they are needed. He might want to combine the two default perspectives into one. Section 3 explains how this can be done. This section may be omitted by users who feel comfortable switching between two perspectives.

Section 4 shows how to use apply reasoning on models in the prover.

Section 5 shows a proof in a mathematical setting, and then provides a few examples, on which the user can work on by himself. In these proofs, everything except the basic rewrite rules has to be done by the user.

Files

For this tutorial, you will be needing 4 example files. They are:

• Celebrity.zip, which will be needed in section 2.
• Doors.zip, which contains the model that is used in section 4.
• Closure.zip. This is the model on which you perform proofs in section 5.
• Galois.zip. This model is not really needed, but serves as an explanation to why the proof in section 5 works.

Categories: User documentation | Rodin Platform | Tutorial