Tutorial Unit Plugin - Revision history

Michael Leuschel at 08:56, 22 March 2019

2019-03-22T08:56:02Z

← Older revision		Revision as of 08:56, 22 March 2019
Line 2:		Line 2:
	[[Category:User Manual]]		[[Category:User Manual]]
	[[Category:Physical Units Plugin]]		[[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

Sebastian Krings: /* Converting between units */

2015-09-11T09:14:11Z

Converting between units

← Older revision		Revision as of 09:14, 11 September 2015
Line 52:		Line 52:
	MACHINE SimpleConversion		MACHINE SimpleConversion
	VARIABLES		VARIABLES
	/@ unit 10-2 m */ xx,		/@ unit "10-2 m" */ xx,
	/@ unit 10-3 m */ yy,		/@ unit "10-3 m" */ yy,
	converted		converted
	INVARIANT		INVARIANT

Sebastian Krings: /* Annotating variables and animating a machine */

2015-09-11T09:13:58Z

Annotating variables and animating a machine

← Older revision		Revision as of 09:13, 11 September 2015
Line 30:		Line 30:

	VARIABLES		VARIABLES
	/@ unit 101 m*1 / x,		/@ unit "101 m*1" / x,
	/@ unit m2 / y		/@ unit "m2" / 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.		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.
Line 38:		Line 38:

	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.

Sebastian Krings at 12:33, 31 January 2013

2013-01-31T12:33:04Z

← Older revision		Revision as of 12:33, 31 January 2013
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 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

Sebastian Krings: update to new unit format

2012-12-06T12:22:11Z

update to new unit format

← Older revision		Revision as of 12:22, 6 December 2012
Line 51:		Line 51:
	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

Sebastian Krings: update to new unit format

2012-12-06T12:21:28Z

update to new unit format

← Older revision		Revision as of 12:21, 6 December 2012
Line 29:		Line 29:

	VARIABLES		VARIABLES
	/@ unit ~~<nowiki>[~~1,m,1~~]</nowiki>~~ / x,		/@ unit 101 m*1 / x,
	/@ unit ~~<nowiki>[1,~~m~~,1]</nowiki>~~ / y		/@ unit m2 / 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.~~		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.
	~~# 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~~
	~~<nowiki>/@ unit [3,m,1] [0,h,-1] / </nowiki>~~
	~~represents km/h~~.

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

Sebastian Krings: style

2012-10-11T13:10:33Z

style

← Older revision		Revision as of 13:10, 11 October 2012
Line 43:		Line 43:
	represents km/h.		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
Line 51:		Line 51:
	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 ==

Sebastian Krings: newlines

2012-10-11T12:49:05Z

newlines

← Older revision		Revision as of 12:49, 11 October 2012
Line 54:		Line 54:

	== Converting between units ==		== 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:		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		MACHINE SimpleConversion
Line 70:		Line 72:
	mmToCm = converted:=/@ conversion /(10*yy)		mmToCm = converted:=/@ conversion /(10*yy)
	END		END



	== Static analysis ==		== 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.		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.

Sebastian Krings: typo

2012-10-11T12:45:57Z

typo

← Older revision		Revision as of 12:45, 11 October 2012
Line 51:		Line 51:
	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 an.		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.

	== Converting between units ==		== Converting between units ==

Sebastian Krings: add remark about setting the animator to a fixpoint state

2012-10-11T12:44:54Z

add remark about setting the animator to a fixpoint state

← Older revision		Revision as of 12:44, 11 October 2012
Line 18:		Line 18:
	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.		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~~:		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.		# 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.		# 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 ==		== Annotating variables and animating a machine ==