/* Version with procedures and global counters p0 and p1 */ var go : bool, counter : uint[2], p0,p1:int; initial counter==uint[2]0 and go; proc barrier(lgo:bool) returns (nlgo:bool) begin lgo = not lgo; counter = counter+uint[2]1; if counter==uint[2]2 then counter=uint[2]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