SPIN Verifier's Roadmap: Xspin

Google

SPIN VERIFIER's ROADMAP: USING XSPIN

(updated for Spin/Xspin version 3.1.2)

The easiest way to get started with Spin is to use the graphical interface Xspin. The graphical interface runs independently from Spin itself, and helps by generating the proper Spin commands based on menu selections. Xspin runs Spin in the background to obtain the desired output, and wherever possible it will attempt to generate a graphical representation of such output. Xspin knows when and how to compile code for the model checkers that Spin can generate, and it knows when and how to execute it, so there is less to remember. For more information on running Spin directly, see the companion document Roadmap.html.
This description assumes that the appropriate software has been installed on your system and that all relevant commands (such as wish, Spin, Xspin, and an ANSI-C compiler) are within your search path. (If this is not the case, see the README file first.)

One

To start a first session with Xspin, use one of the example Promela specifications from the Test directory of the Spin distribution. For instance: 
    $ xspin leader

xspin:   Spin Version 3.1.2 -- 14 March 1998

xspin:  Xspin Version 3.1.2 -- 14 March 1998

xspin:  TclTk Version 7.6/4.2

xspin:  removing tmp files..

xspin:  done..

xspin:  .open leader.

. . .
The dollar above is the prompt of the command-shell. The next two words are typed by the user. The remainder (in regular font) is printed by Xspin onto the stdout stream, as it starts up.

Two

You should now have the main Spin control window on the display, with a Promela specification of the leader election protocol loaded. First, press the Help.. button to view the available help topics. Select one of the topics, and press Ok when done, to return to the main window.
The main text window that you see offers some rudimentary edit and search capabilities. You can scroll through the specification either with button-2 down (on a 3-button mouse), or with the scroll-bar.
You can select text fragments by sweeping the mouse with button-1 (the left-most button) down. Use the Edit menu for standard Copy, Cut, and Paste operations. If you are more comfortable working with another text-editor, a typical way of working with Xspin is also to have the text of a specification open in your favorite editor; to update the file being edited explicitly after changes; and then to select ReOpen from the File menu before simulation or verification runs are performed.

Three

Next, press the Run.. button and then select Set Simulation Parameters... For now, just accept the default settings that are shown, and press the Start button, to start a first simulation run.

Four

A number of new windows appear. The large panel to the right, labeled Message Sequence Chart is empty at first, but it will display all messages sent and received during the simulation that we are about to start. The lower panel, labeled Variable Values, will print the current values of all variables and channels that are used during the simulation run.
The main panel that appears is labeled Simulation Output. It allows you to perform either a single-step simulation, or a continuous random simulation run. Choose the latter, by pressing the Run button. Let the run proceed until completion. The main panel will show the raw printout from Spin (which is running in the background to perform the actual simulation), prefixed by a step-number in the left margin.

Five

When the run completes, the main panel will print the number of processes that has been created.
Note that the log window, at the bottom of the main text panel now contains the lines: 
    
xspin:  .starting simulation.

xspin:  spin -X -p -v -g -l -s -r -n1 -j0 pan_in

xspin:  .at end of run.
It shows the commandd that Xspin synthesized to perform the simulation run with the parameters that were selected. The advantage of using Xspin is clearly that you do not have to remember the meaning of all the options that Spin recognizes. (Not all the the options used above are critical though, so there's also not need for great concern about using Spin without this interface... You can find out what all the option flags to Spin mean by typing in a regular shell window: spin --.)

Six

Make the main Spin control window that displays the Promela text of the leader election protocol visible again (without closing any of the panels that have been created for the simulation so far).
Move the mouse cursor over the boxes and arrows in the Message Sequence Chart display on the right. You will see that the main text window tracks the movements of the mouse. When the mouse cursor is over a square box in the message sequence chart, the corresponding Promela source line in the text window is indicated, and the source text is shown in the sequence chart. The number that is shown in the square boxes if the mouse is not hovering over them is a simulation step number, that matches the numbers in the left margin of the Simulation Output panel.
Try the same experiment with the yellow rectangles in the message sequence chart, and notice how their display in the message sequence chart chart is triggered in the Promela source (i.e., a printf statement that starts with the letters MSC:).

Seven

Make the Simulation Output panel visible again (it's likely hidden behind the main Spin control panel now), and press Cancel. This removes all new panels that were generated.
The next time you press the Run.. button there will be an extra selectable option, to repeat a simulation with the same setting as you last selected. We'll skip that for now.
Next, select the Set Verification Parameters option from the Run.. menu. Accept the default settings of the parameters and press the Run button. Notice again the commands that Xspin synthesizes, printed in the log. This time, Spin is asked to generate a verifier, the verifier is compiled and executed, and the results are fed back to Xspin for display. If all is well, the results show that there are no errors detected in the specification. If in the verification run, Spin detects that some statements are unreachable for the given parameters, those statements are highlighted in the main Xspin control window with the text of the specification. (The version of the leader election protocol that is being verified contains a correctness requirement that was specified as the LTL formula (<>[]oneLeader) in a separate file called leader.ltl We'll return to this below to show how this is used.)
Close the verification output window.

Eight

Introduce an artificial error in the specification by adding an 
    
assert(false);
statement (don't forget the semi-colon), for instance, immediately following either one of the occurrences of: 
    
:: Active ->
becomes: 
    
:: Active -> assert(0);
Now repeat the verification run. (There is no need to save the file. Xspin always works with the copy of the specification that sits in its edit buffer.) This time, the verification should come back with an error sequence, and a small panel will ask you to either repeat the run with different parameter settings, or to perform a guided simulation. Choose the Guided Simulation option. This now returns you to a simulation parameters panel, but one of the options has now been changed from what you saw before: Xspin has preselected a Guided Simulation instead of a Random Simulation. (A guided simulation can only be done for an error sequence that was produced earlier by the verifier.)

Nine

Select the Execution Bar Panel and change the sub-option in the Time Sequence Panel to One Window per Process, to change the view on the simulation run a little from before.
Press the Start button in the parameters panel, and then the Run button in the Simulation Output window, to inspect the error trail.
This time, the trail ends at the assertion violation and not in a state where all processes have reached the end of their code. (You can in principle step either backwards or forwards through the simulation trail, but the update of the displays is not always intuitive, so defer playing with those options for now.)

Ten

When done, close all the panels again (pressing Cancel in the Simulation Output panel will clear up most of them). Next, select the LTL Property Manage.. option from the Run menu . By default this will read in a file with extension .ltl, with the same name as the main specification: in this case it should open leader.ltl and load the information from within that file. You can also enter a different formula. Let's try that first. Hit the Clear button and enter in the Formula entry box the formula: 
    
[] p
This formula expresses that the boolean condition that is represented by the propositional symbol p is invariantly true. Either this is an error or this is the desired system behavior. In this first case, the option This Property holds for All Execitions applies. In the second case, the opposite choice This Property holds for No Executions applies. Either press the Generate button, or type a carriage return in the Formula entry box. The larger text window should now display the automaton (a never claim in Promela terminology) that corresponds to the LTL formula (either negated or not, depending on the choice for the type of property made above). In the symbol definition box a query will come up for the definition of the propositional symbol p. (If you don't see it right away, try the scroll bar. For safety, old definitions are not removed from this panel on hitting the Clear button.)

Eleven

Adding the definition of the propositional symbol p, is done with a standard macro definition, for instance as follows: 
    
#define p	(nr_leaders == 0 || nr_leaders == 1)
This definition is entered into the Symbol Definitions box (check the top of the specification of the leader election protocol for some other macro definitions of this type).
If you forget the macro definitions for the propositional symbols, Spin will complain about syntax errors (undefined identifiers) when it tries to parse the never claim refers to these symbols.
Run the verification and see what happens. When done, revert to the original never claim (reload it from the leader.ltl file) and repeat a verification.

Spin HomePage (Page Updated: 14 March 1998)