Hi

I'll give you a quick tour of SPIN and how to debug examples and how
to see system and property automata alternating.  Here are the steps:
 
1. Install SPIN

2. Install xspin which comes with it. Make sure that
xspin is able to launch SPIN

3. Type "xspin test3.pr" which has a
violation. Let's see how to detect the violation

4. Click on Run

5. Click on Set Verification Parameters

6. Click on Run

7. The Verification Output Window shows errors:1 -- that means there
is an error

8. A pop-up comes saying "Suggested Action" which allows
you to Setup Guided Simulation or Run Guided Simulation

9. Click on Run Guided Simulation

10. Click on Single Step

11. The Simulation Output window clearly shows "never" moving, then
"test"moving then "never" moving then "system" moving, with each
Single Step! The final result is that you see how the accept cycle
closes on itself! Try it. You can set up simulation parameters and
watch various windows.

This is what shows how the property automaton and system automaton
alternating.

Basically, these are the facts

a. The never automaton is a pure observer. You can't put a++ or a=2 in
it.  It can have only guards with a==2, a>3, etc

b. The system automaton starts with the system in the initial state.

c. The property automaton moves in ALL POSSIBLE WAYS it can move
. Each possible move of the property automaton is based on its current
"guard".  If the system is in initial state = 3, and the property
automaton has guards x>0 and x>1 and x>3 guarding three transitions,
the PA has two moves possible!  Move the PA along both these moves

d. The PA moves DON'T change the system state. The system is still in
the init state thus

e. Move the SA in ALL POSSIBLE ways (all the non-determinism of the SA
is pursued). Of course Promela does all this as a DFS search, but when
you do by hand, you can pretend it is BFS and draw out all moves

f. Move the PA now trying to match all system states in all possible
ways

e. Repeat all this till the diagram folds onto itself i.e all states
 recur.

=================================================================
Now some notes on Kripke structures
=================================================================

Reading a Kripke structure (KS):

A KS mentions vars that are true in each state.  It does not mention
false vars.

E.g. a KS over vars {a,b} may be this:

->{a} --> {b} --> back to {a}

The initial state is ->{a}

 This produces a single infinite trace

 a=1 a=0 a=1 a=0 a=1 .... to infinity.
 b=0 b=1 b=0 b=1 b=0

=================================================================

Q: What is the example of a SPIN proctype that produces this KS?

A: the following is one.

// Initialize two bool variables as follows: // a=true and b=false //
active proctype test() { bool a=true; bool b=false; do :: atomic
{a=!a; b=!b} od }

=================================================================

Q: What is the KS produced by these two proctypes running in parallel?

bool a,b;
active proctype p1() { a = !a; } active proctype p2() { b = !b; }

A: we have to interleave p1 and p2 in all possible ways. Thus 00
can go to 01 or 10. Then 01 can go to 00 or 01 can go to 11, etc.
etc. This is the interleaving execution space of p1 and p2. This is
the ASYNC PRODUCT that I explained in class. This async product
defines ONE Kripke structure.
=================================================================

SPIN's never automata can NEVER change states. They only observe the
state of the proctypes. Thus you can't put an a=1 or a++ inside a
never automaton. You can put a==b, a>4 etc.

=================================================================

Now consider a KS over vars a, b, c

->{a} --> {b} --> back to {a}
   |
   |----> {c} --> back to {a}

This produces infinitely many infinite traces, three of which are
shown below. Time moves left to right

   ->  ->  ->  ->
 a=1 a=0 a=1 a=0 a=1 .... to infinity.
 b=0 b=1 b=0 b=1 b=0
 c=0 c=0 c=0 c=0 c=0

 a=1 a=0 a=1 a=0 a=1 .... to infinity.
 b=0 b=0 b=0 b=0 b=0
 c=0 c=1 c=0 c=1 c=0

 a=1 a=0 a=1 a=0 a=1 .... to infinity.
 b=0 b=1 b=0 b=0 b=0
 c=0 c=0 c=0 c=1 c=0

=================================================================
The full algorithm

Given a single SA (or do the async product and imagine a single SA)
and a single PA, do this

Init : SA and PA in their init states

turn : turn is that of PA

do { For all current states and automaton with current turn { move the
 current state in all possible ways according to the moves of the
 automaton whose turn it is currently } ;

 Toggle turn (from SA to PA or vice versa) ;

 } while (there are still unvisited states)

Notes:

1. A move of a SA moves according to the Promela execution code
  semantics

2. A move of the PA tries to observe the system state and fire a guard
  of the PA. For all the guards that can be fired, there is a PA move.

=================================================================