var b0,b1,turn:bool;
initial not b0 and not b1;

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

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

proc main(tid:bool) returns ()
begin
  while random do
    acquire(tid);
    release(tid);
  done;
  if random then main(tid); endif;
  acquire(tid);
  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