var b0,b1,turn:bool; initial not b0 and not b1; thread T0: begin while true do b0 = true; turn = false; assume(b1==false or turn==true); b0 = false; done; end thread T1: begin while true do b1 = true; turn = true; assume(b0==false or turn==false); b1 = false; done; end