Program P2
declare r: integer
initially r = 0
assign ([] i: 0 <=i<N :: r := f_i(r)
end {P2}
Program semaphore
declare g: integer
initially g = 1
assign
([] i: 0 <=i<N ::
g, p[i] := g-1, false if g > 0 and p[i]
[] g, v[i] := g+1, false if v[i])
end {semaphore}