View source for Tutorial CSP First Step

[Category:User Manual]]


== Startup ==

Start off by installing the standalone Tcl/Tk version of ProB.
Follow the instructions in [[Installation]].
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).

== Loading a first CSP specification ==

Use the "Open..." command in the "File" menu and then navigate to the "Examples" directory that came with your ProB installation. Inside the "CSP" subfolder, open the "buses.csp" specification.
Your main ProB window should now look as follows:

[[file:ProB_BusesAfterLoad.png|center||500px]]

== First Steps in Animation ==

We have now loaded a first simple CSP 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 events  that your CSP specification offers. At the very first step you have to choose a process to animate. If your CSP specification contains a MAIN process (as is the case in buses.csp), only this process will be shown.
** 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>MAIN</tt>" process in the "Enabled Operations" Pane. This has the effect of computing the events offered by <tt>MAIN</tt>. The lower half of the ProB window should now look as follows (the upper half will remain unchanged):
 
[[file:ProB_CSPAfterInit.png|center||700px]]


In the "Enabled Operations" pane we can see that two tau events are offered: <tt>tau(int_choice_left)</tt> and <tt>tau(int_choice_right)</tt>. The "History" pane shows us that we have started the  "<tt>MAIN</tt>" process to reach the current state. 
By single-clicking on an event, we can see which parts of the CSP specification contributed to the event. For example, single clicking on the first tau event yields in the following picture:

[[file:ProB_CSPAfterTauSingleClick.png|center||500px]]

By repeatedly single clicking on the event you can cycle through the various locations that contributed to the event. To execute an event, simply double-click on it.

== First Steps in Model Checking ==
You can use the model checker to search for certain errors.
Execute the "Model Check" command in the "Verify Menu".
The following dialog box will appear:
[[file:ProB_CSPModelCheck.png|center||200px]]

By default, ProB will search for deadlocks, illegal channel values and events on the "error" channel.
To turn the latter off, uncheck the invariant violation check box.
You can also search for events on the "goal"channel, by checking the corresponding check box.

Now press the "Model Check" button. ProB should find a deadlock and insert the counter-example into the history as follows:
[[file:ProB_CSPAfterModelCheck.png|center||700px]]

== Error Highlighting ==

Now edit the definition of the BUS37 process and add an illegal output of value 1 on the alight37B channel:
BUS37 = board37A -> (pay90 -> alight37B!1 -> STOP
                     [] alight37A -> STOP)

Now save and reload the machine and again choose the "Model Checking" command. Now uncheck the "Deadlock" checkbox and press "Model Check".
ProB will report the following error:

Mismatch in number of arguments for channel synchronisation: Channel:ExtraArgs = alight37B:[int(1)]
 ### Line: 11, Column: 30

and highlight the error location in the source as follows:
[[file:ProB_CSPAfterModelCheck2.png|center||700px]]



== Other Features ==

You can check more sophisticated temporal properties using the LTL model checker of ProB; see the [[LTL_Model_Checking|corresponding part of the tutorial]].
It is also possible to perform trace refinement checks (see [[Refinement_Checking]]).
The state space visualisation features of ProB are also available for CSP; see [[State_Space_Visualization|the corresponding part of the tutorial]].