Tutorial First Step: Difference between revisions
No edit summary |
|||
| 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]] | |||
Revision as of 14:11, 18 January 2010
Installation
Start off by installing the standalone Tcl/Tk version of ProB. Follow the instructions in Installation.
Starting ProB
Start ProB by double-clicking on ProBWin (for Windows users), or by launching StartProB.sh from a Terminal (for Linux and Mac users).
Mac users may also be able to launch ProB by double-clicking on StartProB.sh.
This should bring up a window as follows (on a Mac):
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):
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:
Inside the samples folder, open the "Lift.mch" machine. Your main ProB window should now look as follows:
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 "INITIALISATION(4)". The 4 indicates that the initialisation will set the main variable of the machine (floor) 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 "INITIALISATION(4)" in the "Enabled Operations" Pane. This has the effect of executing the initialisation and moving the machine into its initialised state:
