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