Rodin User and Developer Workshop 2013 - Tutorial: Difference between revisions

Here are the information we have shown you at the tutorial. If you want to follow this tutorial on your computer you will have to install ProB 2.0 and start an animation. For this tutorial we use a simple scheduler example.

Setup

You will need a fresh copy of ProB 2.0 installed to your Rodin or the sourcecode.

The update site for our builds is: http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/

The sourcecode repository and a description how to setup your Eclipse: https://github.com/bendisposto/prob2

Please note that no matter which installation method you chose, you need to fetch the latest Prolog binaries. The easiest way is to type upgrade latest into the ProB 2.0 Groovy console.

In the following we will intermix some explanations with FAQ style code snippets. We assume that you execute all the code snippets. Some of the snippets rely on the previous execution of other snippets.

Preparation

1. Import the Scheduler project.
2. Start an animation for Scheduler0
3. Perform some random animation steps
4. Type s = space_0 into the Groovy console. space_0 has been created automatically when you loaded the scheduler. Subsequent loading wil result in space_1, space_2, etc.

The model

A model gives you access to the static properties of a Rodin development. Such as contexts, machines, constants, variables, invariants, events, etc. A model is a graph of components and their relationship. Except for Graph handling there are no shared methods between formalisms. The main difference between EventBModel and ClassicalBModel are the artifacts and relationships they can contain. An EventB Model consists of Machines and Contexts and the only relationships are refinement and sees.

How can we get the model for a given state space?

m = s.getModel()}}}

What is the Java type of m?

m.getClass()