Handbook/ProB 2
ProB 2.0 Development
Basic Design Principles
One of our main design goals was that we wanted to build our UI on top of a programmatic API. Our goal was to bring the ProB 2.0 API into a scripting language and not to bring the scripting language into the API.
We also attempted to apply functional programming techniques to our project wherever it was possible. This included trying to create small abstractions that could be composed in different ways. For example, we tried to avoid very large interfaces, but instead preferred to have small functions and methods that accomplish one single task. For this same reason, we tried to use immutable data structures wherever possible.
The ProB API needs to deal with many different formalisms (i.e. Classical B, Event B, Z, CSP, etc.). For this reason, we constucted our data structures so that they can be easily adapted for other formalisms.
While developing a particular feature, it is very helpful to be able to easily experiment and interact with the tool. For this reason, we have spent quite a bit of energy developing a developer friendly console for testing out features as they are being developed.
Why Groovy?
The scripting language that we chose is Groovy. It is a dynamically typed JVM language. Because of the seamless integration between Java and Groovy libraries, we can easily integrate any jar library into the ProB API, and the code that we produce can also be fully integrated into any other Java project.
Groovy also has many features that make it an ideal scripting language. It provides closures which allow the definition of higher order functions. It is also possible to perform meta programming and thereby redefine or modify existing groovy or java class files. For example, in ProB 2.0, we redefined the java.lang.String class so that we can specify the correct Parser with which a string should be parsed.
Explanation of the basic programmatic abstractions
The basic programmatic abstractions that are available in the ProB 2.0 API are the Model, Trace, and StateSpace abstractions. The Model provides all the static information about the model that is currently being checked or animated. The StateSpace provides the corresponding label transition system for the Model. The Trace represents exactly one trace throughout the StateSpace. A more detailed description of the different is available here.
Tutorial of the Current Features of ProB 2.0
A tutorial for the current features of ProB 2.0 is available here.
ProB 2.0 within Rodin and a HTML Visualization Example
Installing ProB 2.0 from Rodin 2.7 or later
- Enter the update site http://nightly.cobra.cs.uni-duesseldorf.de/experimental/updatesite/ and install the ProB 2.0 plugin
Obtaining the latest ProB binary
Open a Groovy Console and type upgrade "latest".
If you have trouble with this you can also manually download the latest nightly version of ProB from our downloads area and put the probcli binary and the lib directory into a .prob directory in your home directory.
Import the Lift Project
Select the Rodin "Import…" menu command and import the Lift.zip archive.
Start Animating the Lift
Right-click on the MLift model and select the "Start Animation" command:
Click on setup_constants and initialise in the Events view:
Open HTML Visualization
Go into the BMotion Studio Menu at the top and select Open BMotion Studio Template:
Navigate to the "lift.html" file that is included in the Lift.zip archive.
You can now see a graphical visualisation of the state of the model:
You can also click on the buttons in the HTML page to control the model.
ProB 2.0 Advance Release
ProB 2.0 for Rodin 3.1 can be installed from the update site located at: http://nightly.cobra.cs.uni-duesseldorf.de/prob2/updates/releases/advance-final/
The installation follows the normal Eclipse installation procedure. Choose 'Install New Software...' from Rodin's Help menu.
Enter the update site into the textfield and hit enter. The result is shown in the following screenshot:
Warning: Display title "Handbook/ProB 2" overrides earlier display title "ProB 2.0 Advance Release".