ProB supports animation and model-checking for Event-B specifications.
To install the ProB plugin for Rodin, open the "Help" menu in Rodin and click "Install new software".
You see a drop-down list titled "Work with:" at the top of the install dialog. Choose the update site "ProB - ..." and click on "ProB for rodin2" in the field below. Click on the "Next" button at the button on the dialog and proceed with the installation as usual.
Alternativaly, one can use the Tcl/Tk version of ProB but Event-B models must be exported to an .eventb file first (see below).
You can start animation of a model (machine or context) by right-clicking on the model in the Event-B explorer. Choose "Start Animation / Model Checking".
TODO: Here we should add more details about the ProB perspective and views.
You can export a model (machine or context) to an .eventb - file by right-clicking on the model in the Event-B explorer. You can find the corresponding menu item right below the animation item.
Such a .eventb file can be opened by the command line and Tcl/Tk version of ProB.
ProB has (limited) support for theories.
Currently supported are (examples refer to the theory project below):
Axiomatically defined operators are not supported without additional annotations.
ProB has some extra support for certain operators. ProB expects an annotation to an operator that provides the information that it should use a specific implementation for an operator. Such tags are given in a .ptm file (ProB Theory Mapping). The file must have the same name as the theory.
For each annotated operator, the file contains a line of the form
operator Name internal {Tag}
where Name is the name of the operator in the theory and Tag is a ProB internal name.
Currently are the following tags supported: