Tutorial Unit Plugin

This tutorial describes, how ProB's integrated plugin for unit analysis can be used to verify the usage of physical units throughout a B machine. This includes

Annotating variables with their physical unit,
Infer the unit of variables without an annotation,
Detect incorrect usage of units, like addition of differently annotated variables.

The plugin is currently a work in progress. Rough edges are to be expected.

We assume that you have a general understanding of B and the usage of ProB.

Activating the Plugin and setting preferences

Currently, the plugin can only be used with classical B machines. Therefore, a B machine needs to be loaded before the plugin can be activated.

Once a machine is loaded, the plugin can be activated through ProB's plugin menu. Choose "Interpreting units stored in pragmas" inside of the activate plugin submenu. Furthermore, the preferences can be accessed through the menu.

At this stage, two preferences can be set:

Activation or deactivation of a static pre-check, that is run once a machine is loaded and performs a fix point analysis of the formerly mentioned usages.
The maximal number of iterations that are performed, before the fix point algorithm stops.

If the static pre-check is activated, the plugin moves the animator into a fix point state, in which possible unit errors are presented to the user through ProB's error reporting facilities.

Annotating variables and animating a machine

To connect a variable with an expected physical unit, a special comment is placed before the variable.

 VARIABLES
   /*@ unit "10**1 * m**1" */ x,
   /*@ unit "m**2" */ y

Following the "unit" keyword is a specification of the unit in form of a B expression. Allowed constructs are multiplication and division as well as exponentiation.

For several often used units like cm, dm, km, etc. an alias can be used.

 VARIABLES
   /*@ unit "mm" */ x,
   /*@ unit "dm" */ y

Once at least one variable is annotated, further units can be inferred.

The unit plugin integrates with ProB's animation facilities. Both results and parameters of operations are displayed with their unit. For variables, the unit is stored inside the machines state space. This enables the plugin to be used in conjunction with the evaluation view, the dot output and most other ProB features.

Converting between units

To distinct between a numerical multiplication, that changes the values without changing the unit and a multiplication meant to convert between units, a second pragma is added. To convert between units, add the respective conversion factor and mark the multiplication as a unit conversion.

See the following B machine for an example operation:

 MACHINE SimpleConversion
 VARIABLES
   /*@ unit "10**-2 * m" */ xx,
   /*@ unit "10**-3 * m" */ yy,
   converted
 INVARIANT
   xx:NAT &
   yy:NAT &
   converted:NAT
 INITIALISATION xx,yy,converted:=0,0,0
 OPERATIONS
   n <-- addToXX = n:=xx+1;
   mmToCm  = converted:=/*@ conversion */(10*yy)
 END

Static analysis

If activated, the results of the static analysis can be accessed from the plugin menu. Currently, the results include the inferred unit of every variable inside the active B machine. Furthermore, a warning is displayed, if multiple units were inferred for a single variable (which usually is caused by wrong usage of the variable). Another warning message is shown for variables, for which no unit could be inferred.