// liveness
P>=1 [ F ((s1=8) & (s2=7)) | ((s1=7) & (s2=8)) ]