// time bound property
Pmin
=? [
F
((
s1
=
8
)&(
s2
=
7
))|((
s1
=
7
)&(
s2
=
8
)) ]