ProB Java API Tutorial: Difference between revisions

ProB 2.0 is currently experimental. This means that the implementation may change during the course of development. However, we have reached the point in development where some of the features have reached a certain level of stability. Therefore, we are writing this tutorial to explain what those features are.

How to get started developing with ProB 2.0

The source code for ProB 2.0 is available via GitHub. Click [[1]] to view the prob2 repository. There is also a short guide available there which will help getting Eclipse set up so that you can get started with the development. Our bugtracker is available [[2]]. There you can view the features that we are currently working on and can submit new feature requests.

How to open the Groovy Shell

The ProB Groovy shell is available in the Eclipse application. To open it, select

Window > Show View > Other..

Then select

ProB > Groovy Console

and hit ok.

How to load a model

Classical B

You can load a Classical B model into the groovy console in two ways. There is a built in load. For example:

load /home/pathToFile/example.mch

would load example.mch into the console (it will automatically save it into a variable named model_NUM, where NUM is a unique identifier). The nice thing about the load command is that it allows code completion. Code completion works the same as in a normal console. Hit <TAB> to see the code completions that are available.

If you are writing a script that you want to run in the console, you will want to use the api variable that is available. There is a method b_load that is available to load Classical B models. For example:

m = api.b_load("/home/pathToFile/example.mch")

will load example.mch into the variable m.

Event B

To load an Event B model into ProB, right click on the model and select

Start Animation / Model Checking

from the context menu that drops down.

How to animate models

The History abstraction is available to carry out animations.

In The Console

There are several different ways that a new transition can be added to the current history. The most important thing to remember is that each History object is completely immutable. This means that when you change a history, you are actually getting a new History back. This means that when you carry out an animation step, you always have to make sure that you save the history object that is returned.

The simplest way to add a transition is to add it via operation id. For instance, if operation 0 is among the enabled operations for the current state, then

h = h.add(0)

will add operation 0 to the current history, create a new history, and return it.

You can also add operations via operation name and a list of the parameters. For instance

h = h.add("new",["PID3"])

will add the transition new(PID3) to the trace.

It is also possible to execute any event by executing

h = h.anyEvent()

and it is also possible to execute any event with name "name". For instance,

h = h.anyEvent("name")

will execute any event with the name "name".

Lastly, it is also possible to execute an event by treating it as if it were a method in the history class. For instance,

h = h.new()

will execute the event new (by default, the first solution for "new" is chosen). It is also possible to add a predicate as a parameter to filter for a particular solution. For instance,

h = h.new("pp=PID1")

will execute new(PID1) as long as pp is the name of the parameter for new.

It also possible to move backwards and forwards within a history.

Move backwards:

h = h.back()

Move forwards:

h = h.forward()

In The UI

In order to animate a loaded model in the UI, double-click on an enabled event in the Events view. Then, the resulting history will automatically be loaded into the different views and it can be further animated. To move backwards and forwards in the history, use the buttons in the upper right hand corner of the Events view.

How to switch from UI to groovy console

There is an easy way to switch from the UI to the groovy console and back. It all happens using the "animations" global variable in the groovy console. What is important to remember, is that in this case, there is no distinction between an animation and a history.

From UI to Console

In the UI, switch to the Current Animations view. Here you can view the different animations that are available. If the desired animation is not available, double click on it in this view and it will be set as the current animation. Now, to move this animation from the UI to the groovy console, simply type

x = animations.getCurrentHistory()

into the groovy console and the current animation will be loaded into the variable x.

From the Console to the UI

If you have a history saved into variable history_0 in the groovy console, you can easily add it to the UI. Simply type

animations.addNewHistory(history_0)

into the groovy console and the history will automatically be added to the list of current animations and all of the views will be updated.

How to carry out evaluations

How to convert between the main abstractions

How to save a history

How to run a groovy script

How to animate with only the StateSpace abstraction