/* Version with procedures and local counters p0, p1 */ var go : bool, counter:int; initial counter==0 and go; proc barrier(lgo:bool) returns (nlgo:bool) begin lgo = not lgo; counter = counter+1; if counter==2 then counter=0; go = lgo; else assume(lgo==go); endif; nlgo = lgo; end thread T0: var lgo0:bool,p0:int; begin p0 = 0; lgo0 = true; while p0<=500 do lgo0 = barrier(lgo0); p0 = p0 + 1; done; end thread T1: var lgo1:bool,p1:int; begin p1 = 0; lgo1 = true; while p1<=502 do lgo1 = barrier(lgo1); p1 = p1 + 1; done; fail; end