[lttv.git] / trunk / verif / examples / spin-increment.spin

#define NUMPROCS 2

byte counter = 0;
byte progress[NUMPROCS];

proctype incrementer(byte me)
{
  int temp;

  temp = counter;
  counter = temp + 1;
  progress[me] = 1;
}

init {
  int i = 0;
  int sum = 0;

  atomic {
    i = 0;
    do
    :: i < NUMPROCS ->
      progress[i] = 0;
      run incrementer(i);
      i++
    :: i >= NUMPROCS -> break
    od;
  }
  atomic {
    i = 0;
    sum = 0;
    do
    :: i < NUMPROCS ->
      sum = sum + progress[i];
      i++
    :: i >= NUMPROCS -> break
    od;
    assert(sum < NUMPROCS || counter == NUMPROCS)
  }
}
Commit	Line	Data
0b55f123	1	#define NUMPROCS 2
	2
	3	byte counter = 0;
	4	byte progress[NUMPROCS];
	5
	6	proctype incrementer(byte me)
	7	{
	8	int temp;
	9
	10	temp = counter;
	11	counter = temp + 1;
	12	progress[me] = 1;
	13	}
	14
	15	init {
	16	int i = 0;
	17	int sum = 0;
	18
	19	atomic {
	20	i = 0;
	21	do
	22	:: i < NUMPROCS ->
	23	progress[i] = 0;
	24	run incrementer(i);
	25	i++
	26	:: i >= NUMPROCS -> break
	27	od;
	28	}
	29	atomic {
	30	i = 0;
	31	sum = 0;
	32	do
	33	:: i < NUMPROCS ->
	34	sum = sum + progress[i];
	35	i++
	36	:: i >= NUMPROCS -> break
	37	od;
	38	assert(sum < NUMPROCS \|\| counter == NUMPROCS)
	39	}
	40	}