var b0,b1,turn:bool,
    g:uint[3],
    x,y:bool;

initial not b0 and not b1 and g==uint[3]0 and not x and not y;

proc acquire(tid:bool) returns ()
begin
  if not tid then
    b0 = true;
    yield;
    turn = tid;
    yield;
    assume (b1==false or turn==not tid);
  else
    b1 = true;
    yield;
    turn = tid;
    yield;
    assume (b0==false or turn==not tid);
  endif;
  yield;
end  

proc release(tid:bool) returns ()
begin
  if not tid then b0 = false; else b1 = false; endif; 
  yield;
end

proc foo(tid:bool,q:bool) returns ()
begin
  if not q then 
    x=true;
    yield;
    y=true;
    yield;
    foo(tid,q);
  else
    acquire(tid);
    yield;
    g = g + uint[3]1;
    release(tid);
  endif;
end

proc main(tid:bool) returns ()
var q:bool;
begin
  q = random;
  foo(tid,q);
  acquire(tid);
  if g==uint[3]0 then fail; endif;
  release(tid);
end  

thread T0:
var tid:bool;
begin
  tid = false;
  main(tid);
end

thread T1:
var tid:bool;
begin
  tid = true;
  main(tid);
end