syntactic characterization of PSL subclasses
I think {r_F} and !{r_F} both belong to the φ_F fragment. I'd also add {r_F}[]->φ_F and {r_F}<>->φ_F.
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information