m (→Starting ProB: changed list in parentheses) |
|||
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 | 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 == |
Start off by installing the standalone Tcl/Tk version of ProB. Follow the instructions in Installation.
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 (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):
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:
We have now loaded a first simple B model. Let us look at the contents of the ProB window (ignoring the menu bar).
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. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):
In the "Enabled Operations" pane we can see that two operations can be executed: inc and dec. The "History" pane shows us that we have exeucted "INITIALISATION(4)" to reach the current state. In the "State Properties" pane we can see that the variable floor 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:
Now, double click on "dec" in the "Enabled Operations" Pane thereby executing the associated operation. The lower half of the ProB window should now look as follows:
As you can see, the lift is now on floor 3. You can also see in the "Enabled Operations" pane that the inc operation is coloured in blue, while dec 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 floor=4). 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:
This time, the forward button is also enabled which will undo the action of the back button (i.e., re-apply the dec operation).