Tutorial Unit Plugin: Difference between revisions

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

1. Annotating variables with their physical unit,
2. Infer the unit of variables without an annotation,
3. 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 are available:

1. 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.
2. The maximal number of iterations that are performed, before the fix point algorithm stops.

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 [1,m,1] */ x,
   /*@ unit [1,m,1] */ y

Following the "unit" keyword is a specification of the unit consisting of a list containing or more lists. Each of the lists has three entries corresponding to different parts of a SI unit.

1. The first number represents the exponent to the units base, i.e. a 1 represents 10^1
2. The second entry is the units symbol, and
3. The third entry for the units exponent.

[1,m,1] for example stands for 10^1 m^1.

The different parameters to the unit pragma are considered as multiplied units. Thus

 /*@ unit [3,m,1] [0,h,-1] */ 

represents km/h.

For several often used units like cm, dm, km and so on 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 so an.

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 [-2,m,1] */ xx,
   /*@ unit [-3,m,1] */ 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.