var b0,b1,turn0,turn1:bool;

initial not b0 and not b1;

proc acquire(tid:bool) returns ()
var local:bool;
begin
  if not tid then
    b0 = true;
    local = turn1;
    turn0 = local;
    assume (not b1 or local!=turn1);
  else    
    b1 = true;
    local = not turn0;
    turn1 = local;
    assume (not b0 or local==turn0);
  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