Tutorial Unit Plugin: Difference between revisions

m (newlines)
No edit summary
 
(6 intermediate revisions by one other user not shown)
Line 1: Line 1:
[[Category:Tutorial]]
[[Category:Tutorial]]
[[Category:User Manual]]
[[Category:User Manual]]
[[Category:Physical Units Plugin]]
Note: this feature is not available in ProB 1.9.0 anymore.


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
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
Line 29: Line 32:


   VARIABLES
   VARIABLES
     /*@ unit <nowiki>[1,m,1]</nowiki> */ x,
     /*@ unit "10**1 * m**1" */ x,
     /*@ unit <nowiki>[1,m,1]</nowiki> */ y
     /*@ unit "m**2" */ 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.
# The first number represents the exponent to the units base, i.e. a 1 represents 10^1
# The second entry is the units symbol, and
# 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
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.
  <nowiki>/*@ unit [3,m,1] [0,h,-1] */ </nowiki>
represents km/h.


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


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


Once at least one variable is annotated, further units can be inferred.
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 on.
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 ==
== Converting between units ==
Line 60: Line 54:
   MACHINE SimpleConversion
   MACHINE SimpleConversion
   VARIABLES
   VARIABLES
     /*@ unit <nowiki>[-2,m,1]</nowiki> */ xx,
     /*@ unit "10**-2 * m" */ xx,
     /*@ unit <nowiki>[-3,m,1]</nowiki> */ yy,
     /*@ unit "10**-3 * m" */ yy,
     converted
     converted
   INVARIANT
   INVARIANT

Latest revision as of 08:56, 22 March 2019


Note: this feature is not available in ProB 1.9.0 anymore.

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 can be set:

  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.

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.