No edit summary |
m (add category) |
||
Line 1: | Line 1: | ||
[[Category:Tutorial]] | [[Category:Tutorial]] | ||
[[Category:User Manual]] | [[Category:User Manual]] | ||
[[Category:Physical Units Plugin]] | |||
This tutorial describes, how ProB's integrated plugin for unit analysis can be used with Event-B machines from inside the Rodin platform. This includes | This tutorial describes, how ProB's integrated plugin for unit analysis can be used with Event-B machines from inside the Rodin platform. This includes |
This tutorial describes, how ProB's integrated plugin for unit analysis can be used with Event-B machines from inside the Rodin platform. This includes
Both the plugin itself and the bridge to Rodin are a work in progress. Preliminary support is available in the nightly builds of ProB for Rodin and will be merged in the regular releases in the future.
We assume that you have a general understanding of Event-B and the usage of ProB / Rodin.
You can follow the First Steps Instructions or the Screencast to install ProB for Rodin.
In addition to the "ProB for Rodin2" plugin there is a "ProB for Rodin2 - Physical Units Support" plugin at out Rodin update site. You have to install both to enable physical units support for Rodin.
Once both plugins are installed, ProB allows to annotate both variables and constants with physical units:
We store the user supplied unit and the units inferred by ProB as a new attribute in the Rodin database.
Units can be supplied in two forms:
The supplied units can now be used by ProB to infer missing units, verify the supplied units and detect unit errors. To start the analysis use the context menu of the machine / context you want to analyse:
Necessary machines and contexts will be translated and passed to ProB. Once the analysis is finished, the "inferred unit" text fields are filled with the resulting units.
Inside the Rodin Errors view, several errors might occur:
Furthermore, we output a warning if no unit could be inferred for a variable or constant.