/*
 * An ordered list of integers that is accessed concurrently by an 
 * arbitrary number of `updater' processes. The `monitor' process 
 * checks the list for integrity. 
 * 
 * Wrote by Radu Iosif <iosif@athena.polito.it> Tue Feb 13 15:50:00 GMT 2001
 */

#define MAX 3

#define _lock(n)   n.lock ? 1
#define _unlock(n) n.lock ! 1


typedef node {
  int key;
  chan lock = [1] of { bit };
  node &next;
};


node &root;


function insert(int key)
{
  node &tmp;
  node &n;

  n = new node;
  _unlock(n);
  n.key = key;

  _lock(root);
  tmp = root;

  do
  :: if
     :: tmp.next != null ->
		if
		:: key < tmp.next.key ->
			n.next = tmp.next;
                        tmp.next = n;
                        _unlock(tmp);
                        break;
                :: else ->
			_lock(tmp.next);
                        _unlock(tmp);
			tmp = tmp.next;
		fi;
     :: else ->
		tmp.next = n;
		_unlock(tmp);
		break;
     fi;
  od;
}


proctype updater(int inc)
{
  node &n;
  int k;  

  do 
  :: k < MAX ->
        insert(k * inc);
        k ++;

  :: k == MAX ->
	break;
  od
}


proctype monitor()
{
  node &tmp;

  tmp = root; 
  _lock(tmp);
  do
  :: tmp.next != null -> 
	_lock(tmp.next);
	assert(tmp.key <= tmp.next.key);
        _unlock(tmp);
        tmp = tmp.next;

  :: tmp.next == null -> 
        _unlock(tmp);
	break;
  od;
}


init {
  root = new node;
  _unlock(root);

  atomic {
    run updater(1);
    run updater(2);
    run monitor();
  }
}