Spinroot

A forum for Spin users

You are not logged in.

#1 2011-11-28 17:20:22

eugen
Member
Registered: 2011-11-28
Posts: 16

acceptance cycles

I have troubles understanding the acceptance cycles. I have a model for which I want to check an LTL property (of the form <>p) specified within the model (using 'ltl'). SPIN complains that there is an acceptance cycle, however the trail seems to be a finite execution: there is a START OF CYCLE, but no END OF CYCLE. Hence, apparently there is no cycle. Second, my understanding is that the corresponding never claim matches a finite execution only when the claim reaches its final state. But the following claim corresponding to the checked LTL property can never reach its end. So I don't see why SPIN is complaining.

never  {    /* ! <> p */
accept_init:
T0_init:
        if
        :: (! ((p))) -> goto T0_init
        fi;
}

I'm using the following sequence of commands:
  spin -a model.pr
  cc -o pan pan.c
  ./pan -a

Offline

#2 2011-11-29 04:16:03

spinroot
forum
Registered: 2010-11-18
Posts: 695
Website

Re: acceptance cycles

the cycle is the part between START OF CYCLE and the end.
(END OF CYCLE is implied by the end of the trail)
the claim matches an infinite execution in this case (hence the cycle), not a finite one
the acceptance cycle cycles through the 'accept_init' label.
To read more about the terminology and methodology used, please check the tutorials that are online, or better still get the text book that explains it all in detail.

Offline

#3 2011-11-29 13:37:04

eugen
Member
Registered: 2011-11-28
Posts: 16

Re: acceptance cycles

To be more clear, here is the model I have. (Sorry, it's quite long.)

#define N 3
#define C 1

byte nr_leaders;



ltl p0	{ <> (nr_leaders > 0) }
ltl p1	{ <>[] (nr_leaders == 1) }
ltl p2	{ [] (nr_leaders == 0 U nr_leaders == 1) }
ltl p3	{ ![] (nr_leaders == 0) }


mtype = {IN, OUT};

/* the type of messages: inbound(0)/outbound(1), id, hops */
chan ch1[N] = [C] of {mtype,byte,byte};
chan ch2[N] = [C] of {mtype,byte,byte};


inline send(ch, m, i, h, d) {
  atomic {
    ch ! m, i, h;
    if
      :: d -> printf ("[%d to right] ! %e, %d, %d\n", id, m, i, h);
      :: else -> printf ("[%d to left] ! %e, %d, %d\n", id, m, i, h);
    fi
  }
}

inline recv(ch, m, i, h, d) {
  atomic {
    ch ? m, i, h;
    if
      :: d -> printf ("[%d from right] ? %e, %d, %d\n", id, m, i, h);
      :: else -> printf ("[%d from left] ? %e, %d, %d\n", id, m, i, h);
    fi
  }
}

/* chb = backward channel, chf = forward channel */
/* d is true iff chb = left_snd */
inline comm(chb, chf, d)
{
  if
    :: type == OUT -> /* outbound message */
       if
	 :: ch_id == id ->
	    nr_leaders++;
	    assert(nr_leaders == 1);	    
	    
	 :: ch_id > id ->
	    if
	      :: hops > 1 -> /* forward message */
		 send(chf, OUT, ch_id, (hops-1), d);
	      :: else -> /* last hop, change direction */
		 send(chb, IN, ch_id, 0, !d);
	    fi
	 :: else -> /* discard message */
	    skip
       fi
       
    :: else -> /* all inbound messages are replayed */
       if 
	 :: ch_id == id ->
	    tokens++;
	 :: else ->
	    send(chf, IN, ch_id, 0, d)
       fi
  fi
}

proctype node (chan left_snd, left_rcv, right_snd, right_rcv; byte id)
{
  byte round;
  unsigned tokens : 2;
  byte ch_id;
  byte type;
  byte hops;

  xr left_rcv,right_rcv;
  xs left_snd,right_snd;

  printf ("[%d] started\n", id);

  send(left_snd, OUT, id, 1<<round, false);
  send(right_snd, OUT, id, 1<<round, true);
  
  do
    :: recv(left_rcv, type, ch_id, hops, false) -> 
       comm(left_snd, right_snd, true)

    :: recv(right_rcv, type, ch_id, hops, true) ->
       comm(right_snd, left_snd, false)

    :: tokens == 2 ->
       tokens = 0;
       round++;
       send(left_snd, OUT, id, 1<<round, false);
       send(right_snd, OUT, id, 1<<round, true);
  od;

  printf ("[%d] finished\n", id);
}



init
{  
  atomic {     
    byte uid[6];
    byte i;    
     
    /* randomly generate the _unique_ ids */
    for (i : 1 .. N)
    {
      if /* non-deterministic choice */
	:: uid[0] == 0 && N >= 1 -> uid[0] = i
	:: uid[1] == 0 && N >= 2 -> uid[1] = i
	:: uid[2] == 0 && N >= 3 -> uid[2] = i
	:: uid[3] == 0 && N >= 4 -> uid[3] = i
	:: uid[4] == 0 && N >= 5 -> uid[4] = i
	:: uid[5] == 0 && N >= 6 -> uid[5] = i	/* works for up to N=6 */
      fi;
    }

    /* start the processes */
    for (i : 0 .. N-1) {
      run node(ch1[i], ch2[i], ch2[(i+1)%N], ch1[(i+1)%N], uid[i]);
      printf ("neighbors of node %d:\n  node %d on the left\n  node %d on the right\n",
	      uid[i], uid[(N+i-1)%N], uid[(i+1)%N]);
    }
  }
}

The trail, obtained with spin -t -p leader-bi.pml, ends like this:
  <<<<<START OF CYCLE>>>>>
spin: trail ends after 103 steps
#processes: 4
                nr_leaders = 0
                queue 1 (ch1[0]):
                queue 2 (ch1[1]): [OUT,2,1]
                queue 3 (ch1[2]):
                queue 4 (ch2[0]):
                queue 5 (ch2[1]): [OUT,1,1]
                queue 6 (ch2[2]):
103:    proc  3 (node) leader-bi.pml:65 (state 60)
103:    proc  2 (node) leader-bi.pml:33 (state 36)
103:    proc  1 (node) leader-bi.pml:33 (state 10)
103:    proc  0 (:init:) leader-bi.pml:106 (state 33)

This doesn't look to me like a cycle, but rather like a deadlock.

Offline

#4 2011-11-29 14:22:57

eugen
Member
Registered: 2011-11-28
Posts: 16

Re: acceptance cycles

I think I've finally got it. Actually the same behavior is exhibited by the following program:

int x;
ltl p { <> (x == 1)}
init { 0; x = 1; }

which clearly deadlocks/blocks. As explained on page 130 of the SPIN book (Ch.6, The stutter extension rule), for finite traces, the last state is stuttered, in order to obtain an infinite trace. Then everything makes sense.

This explanation also appears at [url]http://spinroot.com/spin/Man/progress.html[/url]:
[quote]
The standard stutter-extension, to extend finite execution sequences into infinite ones by stuttering (repeating) the final state of the sequence, is applied in the detection of all standard types of acceptance properties, but it is not used for non-progress cycles.
[/quote]
But it does not appear on [url]http://spinroot.com/spin/Man/accept.html[/url] or [url]http://spinroot.com/spin/Man/ltl.html[/url]. Thus I would say that these pages are rather misleading with regard to the treatment of finite traces.

Last edited by eugen (2011-11-29 14:24:09)

Offline

#5 2011-11-30 04:35:34

awesan
Member
Registered: 2011-04-30
Posts: 45

Re: acceptance cycles

Hello eugen, How do you get the scrollable box for the source code of the model?

Offline

#6 2011-11-30 08:47:23

eugen
Member
Registered: 2011-11-28
Posts: 16

Re: acceptance cycles

I've used [ code ] ... [ \code ]. See http://spinroot.com/fluxbb/help.php#bbcode. But some of the other tags don't seem to work.

Offline

Board footer

Powered by FluxBB