N = 8


nametype SetN = {1..N}

channel place: SetN.SetN
channel done

Not(n) = diff(SetN,{n})

Safe(i,j) = { (x,y) |  x<- Not(i), y <- Not(j), (x-y) != (i-j), (x+y) != (i+j)}


Unplaced (i) = place.i?y -> Placed(i,y)
            [] place?x:Not(i)?y -> Unplaced(i)

Placed(i,j) = ([] (x,y): Safe(i,j) @ place.x.y -> Placed(i,j))
            [] done -> STOP


Alpha = union ({done}, {| place |})

Queens = [| Alpha |] q: SetN @ Unplaced(q)



assert STOP [T=  Queens \ diff (Events, {done})