UML-B Tutorial - Revision history

imported>Colin at 20:07, 18 April 2010

2010-04-18T20:07:34Z

← Older revision		Revision as of 20:07, 18 April 2010
Line 5:		Line 5:
	See http://www.event-b.org/platform.html and http://www.event-b.org/plugins.html for installation instructions		See http://www.event-b.org/platform.html and http://www.event-b.org/plugins.html for installation instructions

			''You may notice that some of these screenshots are a little different from the current version.''

	Getting Started		Getting Started

imported>Colin at 19:53, 18 April 2010

2010-04-18T19:53:56Z

← Older revision		Revision as of 19:53, 18 April 2010
Line 37:		Line 37:
	[[Image:UMLBSleepyPackageDiagram.jpg]]		[[Image:UMLBSleepyPackageDiagram.jpg]]

	''WARNING: Make sure you always save an edited diagram before moving to another diagram in the same UML-B project. There is currently a problem with multiple diagram editors: unsaved changes in the first editor will be lost if you save edits to a second diagram.''

	'''Context Diagram'''		'''Context Diagram'''

imported>Mathieu: Robot: Changing Category:User Documentation

2008-09-10T20:32:04Z

Robot: Changing Category:User Documentation

← Older revision		Revision as of 20:32, 10 September 2008
Line 176:		Line 176:
	''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the 'Translation' property in the properties view.''		''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the 'Translation' property in the properties view.''

			[[Category:User documentation]]

	[[Category:User ~~Documentation~~]]
	[[Category:UML-B]]		[[Category:UML-B]]
	[[Category:Tutorial]]		[[Category:Tutorial]]

imported>Mathieu: Category:UML-B

2008-07-10T07:02:09Z

Category:UML-B

← Older revision		Revision as of 07:02, 10 July 2008
Line 179:		Line 179:

	[[Category:User Documentation]]		[[Category:User Documentation]]
	[[Category:~~AnimB~~]]		[[Category:UML-B]]
	[[Category:Tutorial]]		[[Category:Tutorial]]

imported>Mathieu at 07:00, 10 July 2008

2008-07-10T07:00:13Z

← Older revision		Revision as of 07:00, 10 July 2008
Line 179:		Line 179:

	[[Category:User Documentation]]		[[Category:User Documentation]]
	[[Category:~~Plugin~~]]		[[Category:AnimB]]
	[[Category:Tutorial]]		[[Category:Tutorial]]

imported>Mathieu: Category:User Documentation Category:Plugin Category:Tutorial

2008-07-02T17:22:27Z

Category:User Documentation Category:Plugin Category:Tutorial

← Older revision		Revision as of 17:22, 2 July 2008
Line 175:		Line 175:

	''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the 'Translation' property in the properties view.''		''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the 'Translation' property in the properties view.''



			[[Category:User Documentation]]
			[[Category:Plugin]]
			[[Category:Tutorial]]

imported>Colin at 18:50, 27 May 2008

2008-05-27T18:50:11Z

← Older revision		Revision as of 18:50, 27 May 2008
Line 8:		Line 8:
	Getting Started		Getting Started

	1. Start Rodin by clicking on rodin.exe		1. Start Rodin by clicking on rodin.exe and selecting a suitable workspace.

	2~~. The workspace launcher will appear - Select or create a workspace on your machine~~		2. '''Open the UML-B perspective'''

	~~3. Close the welcome message~~

	4. '''Open the UML-B perspective'''
	a. Click on: Window → Open Perspective → Other…		a. Click on: Window → Open Perspective → Other…
	b. Select UML-B and click OK		b. Select UML-B and click OK

	5. '''Open a new UMLB project'''		3. '''Open a new UMLB project'''
	a. File → New → Project		a. File → New → Project
	b. Select UML-B Project → Next		b. Select UML-B Project → Next
Line 28:		Line 24:
	''Note that the icon, top right, shows that you are in the UML-B perspective''		''Note that the icon, top right, shows that you are in the UML-B perspective''

	~~Creating the Sleepy model~~

	Specification: A person can go to bed and sleep. After at least one hour, an alarm can be sounded which is waking the person. The person should then get up. A person has a maximum number of hours of sleep after which the person will get up without the alarm being sounded.		Specification: A person can go to bed and sleep. After at least one hour, an alarm can be sounded which is waking the person. The person should then get up. A person has a maximum number of hours of sleep after which the person will get up without the alarm being sounded.

	Package Diagram		'''Package Diagram'''

	In the package diagram editor, '''create a machine that sees a context'''.		In the package diagram editor, '''create a machine that sees a context'''.
Line 44:		Line 39:
	''WARNING: Make sure you always save an edited diagram before moving to another diagram in the same UML-B project. There is currently a problem with multiple diagram editors: unsaved changes in the first editor will be lost if you save edits to a second diagram.''		''WARNING: Make sure you always save an edited diagram before moving to another diagram in the same UML-B project. There is currently a problem with multiple diagram editors: unsaved changes in the first editor will be lost if you save edits to a second diagram.''

	Context Diagram		'''Context Diagram'''

	'''Open the context diagram'''		'''Open the context diagram'''

imported>Colin at 18:47, 27 May 2008

2008-05-27T18:47:23Z

← Older revision		Revision as of 18:47, 27 May 2008
Line 1:		Line 1:
			Return to [[UML-B]]

	The tutorial assumes you have downloaded and installed the Rodin platform and then installed the UML-B plug-in extension feature.		The tutorial assumes you have downloaded and installed the Rodin platform and then installed the UML-B plug-in extension feature.

imported>Colin at 18:35, 27 May 2008

2008-05-27T18:35:14Z

← Older revision		Revision as of 18:35, 27 May 2008
Line 94:		Line 94:
	c. Select “guards” in the properties tab and “add guard…”		c. Select “guards” in the properties tab and “add guard…”
	d. In the guard field enter “wakeState(self) = awake” (we only want to put persons into bed that are awake) → OK.		d. In the guard field enter “wakeState(self) = awake” (we only want to put persons into bed that are awake) → OK.
	''Note that you could also enter “self,.wakeState = awake” (the character pair ,. is converted to a special dot symbol). This gives a more object oriented style for guards and actions.''		''Note that you could also enter “self,.wakeState = awake” (the character pair ,. is converted to a special dot symbol). This gives a more object oriented style for guards and actions but is not as easy to relate to proof goals in the Event-B prover.''

	[[Image:UMLBGoToBed.jpg]]		[[Image:UMLBGoToBed.jpg]]
	e. Select “actions” in the properties tab and “add action…”		e. Select “actions” in the properties tab and “add action…”

imported>Colin at 18:18, 27 May 2008

2008-05-27T18:18:15Z

← Older revision		Revision as of 18:18, 27 May 2008
Line 157:		Line 157:
	[[Image:UMLBWakeStateStatemachine_creating.jpg]]		[[Image:UMLBWakeStateStatemachine_creating.jpg]]

	''Note: Two alternative translations of statemachines are provided. To change to the other translation, change the '~~TranslationKind~~' property in the properties view.''		''Note: Two alternative translations of statemachines are provided. To change to the other translation, change the 'Translation' property in the properties view.''
	c. Click “Open StateDiagram…”		c. Click “Open StateDiagram…”

Line 176:		Line 176:
	c. Save the model and view the Event-B as before.		c. Save the model and view the Event-B as before.

	''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the '~~TranslationKind~~' property in the properties view.''		''Note: Two alternative translations of statemachines are provided. To change to the other translation, select the statemachine (either click on the canvas of the statemachine diagram or click on the statemachine in the class diagram) and change the 'Translation' property in the properties view.''