Tutorial First Step - Revision history

Joy Clark: punctuation and spelling errors

2011-04-18T12:11:10Z

punctuation and spelling errors

← Older revision		Revision as of 12:11, 18 April 2011
Line 43:		Line 43:
	** The History pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.		** The History pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.

	Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the ~~initialisation~~ and moving the machine into its ~~initialised~~ state. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):		Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the initialization and moving the machine into its initialized state. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):

	[[file:ProB_LiftAfterInit.png\|center\|\|700px]]		[[file:ProB_LiftAfterInit.png\|center\|\|700px]]

	In the "Enabled Operations" pane we can see that two operations can be executed: <tt>inc</tt> and <tt>dec</tt>. The "History" pane shows us that we have ~~exeucted~~ "<tt>INITIALISATION(4)</tt>" to reach the current state.		In the "Enabled Operations" pane we can see that two operations can be executed: <tt>inc</tt> and <tt>dec</tt>. The "History" pane shows us that we have executed "<tt>INITIALISATION(4)</tt>" to reach the current state.
	In the "State Properties" pane we can see that the variable <tt>floor</tt> now has value 4. The green "OK" button indicates that the invariant of the machine is true. By clicking on the "OK" button, we obtain more details about the invariant of the machine:		In the "State Properties" pane we can see that the variable <tt>floor</tt> now has value 4. The green "OK" button indicates that the invariant of the machine is true. By clicking on the "OK" button, we obtain more details about the invariant of the machine:

Line 56:		Line 56:
	[[file:ProB_LiftAfterDec.png\|center\|\|700px]]		[[file:ProB_LiftAfterDec.png\|center\|\|700px]]

	As you can see, the lift is now on floor 3. You can also see in the "Enabled Operations" pane that the <tt>inc</tt> operation is ~~coloured~~ in blue, while <tt>dec</tt> is still ~~coloured~~ in green. The blue ~~colour~~ indicates that executing this operation would lead us back to a state which we have already explored (namely with <tt>floor=4</tt>).		As you can see, the lift is now on floor 3. You can also see in the "Enabled Operations" pane that the <tt>inc</tt> operation is colored in blue, while <tt>dec</tt> is still colored in green. The blue color indicates that executing this operation would lead us back to a state which we have already explored (namely with <tt>floor=4</tt>).
	In the "Enabled Operations" pane you can also see a backward and forward arrow button. These buttons work similar to a browser. Clicking on the back arrow will "undo" the last animation step and lead us back to the previous state of the machine:		In the "Enabled Operations" pane you can also see a backward and forward arrow button. These buttons work similar to a browser. Clicking on the back arrow will "undo" the last animation step and lead us back to the previous state of the machine:

Joy Clark: /* Starting ProB */ changed list in parentheses

2011-04-12T14:47:37Z

Starting ProB: changed list in parentheses

← Older revision		Revision as of 14:47, 12 April 2011
Line 18:		Line 18:
	[[file:ProBStartWindow.png\|center\|\|500px]]		[[file:ProBStartWindow.png\|center\|\|500px]]

	In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started) and send us a description of what is printed in that window along with a detailed report (which operating system do you use, which version of it, which version of ProB have you downloaded, ...). Normally, it should look as follows (on Windows):		In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started) and send us a description of what is printed in that window along with a detailed report (list which operating system you use, which version it is, which version of ProB have you downloaded, etc.). Normally, it should look as follows (on Windows):
	[[file:ProBStartTerminal.png\|center\|\|400px]]		[[file:ProBStartTerminal.png\|center\|\|400px]]


	== Loading a first B machine ==		== Loading a first B machine ==

Michael Leuschel: /* First Steps in Animation */

2010-01-18T14:25:11Z

First Steps in Animation

← Older revision		Revision as of 14:25, 18 January 2010
Line 46:		Line 46:
	Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the initialisation and moving the machine into its initialised state. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):		Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the initialisation and moving the machine into its initialised state. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):

	[[file:ProB_LiftAfterInit.png\|center]]		[[file:ProB_LiftAfterInit.png\|center\|\|700px]]

	In the "Enabled Operations" pane we can see that two operations can be executed: <tt>inc</tt> and <tt>dec</tt>. The "History" pane shows us that we have exeucted "<tt>INITIALISATION(4)</tt>" to reach the current state.		In the "Enabled Operations" pane we can see that two operations can be executed: <tt>inc</tt> and <tt>dec</tt>. The "History" pane shows us that we have exeucted "<tt>INITIALISATION(4)</tt>" to reach the current state.
Line 55:		Line 55:
	Now, double click on "<tt>dec</tt>" in the "Enabled Operations" Pane thereby executing the associated operation. The lower half of the ProB window should now look as follows:		Now, double click on "<tt>dec</tt>" in the "Enabled Operations" Pane thereby executing the associated operation. The lower half of the ProB window should now look as follows:

	[[file:ProB_LiftAfterDec.png\|center]]		[[file:ProB_LiftAfterDec.png\|center\|\|700px]]

	As you can see, the lift is now on floor 3. You can also see in the "Enabled Operations" pane that the <tt>inc</tt> operation is coloured in blue, while <tt>dec</tt> is still coloured in green. The blue colour indicates that executing this operation would lead us back to a state which we have already explored (namely with <tt>floor=4</tt>).		As you can see, the lift is now on floor 3. You can also see in the "Enabled Operations" pane that the <tt>inc</tt> operation is coloured in blue, while <tt>dec</tt> is still coloured in green. The blue colour indicates that executing this operation would lead us back to a state which we have already explored (namely with <tt>floor=4</tt>).
	In the "Enabled Operations" pane you can also see a backward and forward arrow button. These buttons work similar to a browser. Clicking on the back arrow will "undo" the last animation step and lead us back to the previous state of the machine:		In the "Enabled Operations" pane you can also see a backward and forward arrow button. These buttons work similar to a browser. Clicking on the back arrow will "undo" the last animation step and lead us back to the previous state of the machine:

	[[file:ProB_LiftAfterDecBack.png\|center]]		[[file:ProB_LiftAfterDecBack.png\|center\|\|700px]]

	This time, the forward button is also enabled which will undo the action of the back button (i.e., re-apply the <tt>dec</tt> operation).		This time, the forward button is also enabled which will undo the action of the back button (i.e., re-apply the <tt>dec</tt> operation).

Michael Leuschel: /* First Steps in Animation */

2010-01-18T14:22:31Z

First Steps in Animation

@@ Line 44: / Line 44: @@
 ** The History pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.
-Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the initialisation and moving the machine into its initialised state:
+Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the initialisation and moving the machine into its initialised state. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):
-[[file:ProB_LiftAfterInit.png|center||500px]]
+[[file:ProB_LiftAfterInit.png|center]]

Michael Leuschel at 14:11, 18 January 2010

2010-01-18T14:11:30Z

← Older revision		Revision as of 14:11, 18 January 2010
Line 33:		Line 33:

	[[file:ProB_LiftAfterLoad.png\|center\|\|500px]]		[[file:ProB_LiftAfterLoad.png\|center\|\|500px]]


			== First Steps in Animation ==

			We have now loaded a first simple B model. Let us look at the contents of the ProB window (ignoring the menu bar).
			* The upper half of the ProB window contains the source code of the model.
			* The lower half contains three panes.
			** The "State Properties" pane contains information about the current state of the model. We will explain the contents of this pane in more detail later.
			** The Pane called "Enabled Operations" contains a list of operations that can be applied to your model. Before a B machine can be animated, we have to initialise it. Hence, initially the only option presented is "<tt>INITIALISATION(4)</tt>". The <tt>4</tt> indicates that the initialisation will set the main variable of the machine (<tt>floor</tt>) to the value 4. This information is useful in case multiple initialisations are possible (in order to distinguish them).
			** The History pane contains the list of operations you have executed to reach the current state of the animator. Obviously, this list is initially empty.

			Now, double click on "<tt>INITIALISATION(4)</tt>" in the "Enabled Operations" Pane. This has the effect of executing the initialisation and moving the machine into its initialised state:

			[[file:ProB_LiftAfterInit.png\|center\|\|500px]]

Michael Leuschel: /* Loading a first B machine */

2010-01-18T14:01:57Z

Loading a first B machine

← Older revision		Revision as of 14:01, 18 January 2010
Line 24:		Line 24:
	== Loading a first B machine ==		== Loading a first B machine ==

	Use the "Open..." command in the "File" menu ~~and then navigate to the "Examples" directory that came with your ProB installation:~~		Use the "Open..." command in the "File" menu

	[[file:ProBWinOpen.png\|center]]		[[file:ProBWinOpen.png\|center]]
			and then navigate to the "Examples" directory that came with your ProB installation:
	[[file:ProBWinExamplesFolder.png\|center]]		[[file:ProBWinExamplesFolder.png\|center\|\|400px]]

	Inside the samples folder, open the "Lift.mch" machine.		Inside the samples folder, open the "Lift.mch" machine.

Michael Leuschel at 14:00, 18 January 2010

2010-01-18T14:00:19Z

← Older revision		Revision as of 14:00, 18 January 2010
Line 19:		Line 19:

	In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started) and send us a description of what is printed in that window along with a detailed report (which operating system do you use, which version of it, which version of ProB have you downloaded, ...). Normally, it should look as follows (on Windows):		In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started) and send us a description of what is printed in that window along with a detailed report (which operating system do you use, which version of it, which version of ProB have you downloaded, ...). Normally, it should look as follows (on Windows):
	[[file:ProBStartTerminal.png\|center]]		[[file:ProBStartTerminal.png\|center\|\|400px]]


			== Loading a first B machine ==

			Use the "Open..." command in the "File" menu and then navigate to the "Examples" directory that came with your ProB installation:

			[[file:ProBWinOpen.png\|center]]

			[[file:ProBWinExamplesFolder.png\|center]]

			Inside the samples folder, open the "Lift.mch" machine.
			Your main ProB window should now look as follows:

			[[file:ProB_LiftAfterLoad.png\|center\|\|500px]]

Michael Leuschel: /* Starting ProB */

2010-01-18T13:54:09Z

Starting ProB

← Older revision		Revision as of 13:54, 18 January 2010
Line 18:		Line 18:
	[[file:ProBStartWindow.png\|center\|\|500px]]		[[file:ProBStartWindow.png\|center\|\|500px]]

	In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started). Normally, it should look as follows (on Windows):		In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started) and send us a description of what is printed in that window along with a detailed report (which operating system do you use, which version of it, which version of ProB have you downloaded, ...). Normally, it should look as follows (on Windows):
	[[file:ProBStartTerminal.png\|center]]		[[file:ProBStartTerminal.png\|center]]

Michael Leuschel at 13:52, 18 January 2010

2010-01-18T13:52:10Z

← Older revision		Revision as of 13:52, 18 January 2010
Line 10:		Line 10:

	Start ProB by double-clicking on <tt>ProBWin</tt> (for Windows users), or by launching <tt>StartProB.sh</tt> from a Terminal (for Linux and Mac users).		Start ProB by double-clicking on <tt>ProBWin</tt> (for Windows users), or by launching <tt>StartProB.sh</tt> from a Terminal (for Linux and Mac users).

			[[file:ProBWinContents.png\|center]]

	Mac users may also be able to launch ProB by double-clicking on <tt>StartProB.sh</tt>.		Mac users may also be able to launch ProB by double-clicking on <tt>StartProB.sh</tt>.

	This should bring up a window as follows:		This should bring up a window as follows (on a Mac):
	[[file:ProBStartWindow.png\|center\|\|500px]]		[[file:ProBStartWindow.png\|center\|\|500px]]

	In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started). Normally, it should look as follows:		In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started). Normally, it should look as follows (on Windows):
	[[file:ProBStartTerminal.png\|center]]		[[file:ProBStartTerminal.png\|center]]

Michael Leuschel: /* Starting ProB */

2010-01-18T13:47:43Z

Starting ProB

← Older revision		Revision as of 13:47, 18 January 2010
Line 13:		Line 13:

	This should bring up a window as follows:		This should bring up a window as follows:
	[[file:ProBStartWindow.png\|\|500px]]		[[file:ProBStartWindow.png\|center\|\|500px]]

	In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started). Normally, it should look as follows:		In case this does not work, please have a look at the output of ProB in the terminal window (on Windows a separate window will be automatically started). Normally, it should look as follows:
	[[file:ProBStartTerminal.png]]		[[file:ProBStartTerminal.png\|center]]