/* Version with procedures and global counters p0 and p1 */

var 	go : bool, counter : int,
	p0,p1:int;

initial counter==0 and go;

proc barrier(lgo:bool) returns (nlgo:bool)
begin
  lgo = not lgo; 
  counter = counter+1;
  if counter==2 then 
    counter=0; 
    go = lgo;
  else
    assume(lgo==go);
  endif;
  nlgo = lgo;
end

thread T0:
var lgo0:bool;
begin
  p0 = 0; lgo0 = true;
  while p0<=500 do
    lgo0 = barrier(lgo0);
    p0 = p0 + 1;
  done;
  lgo0 = barrier(lgo0);  
end

thread T1:
var lgo1:bool;
begin
  p1 = 0; lgo1 = true;
  while p1<=502 do
    lgo1 = barrier(lgo1);
    p1 = p1 + 1;
  done;
  fail;
end