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.