WeakFuture(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Weak temporal future (wF) operator. A state satisfying weak future when all paths (specified by the quantifier) that match the direction also satisfy the inner formula.
Note that this is essentially equivalent to Future, but instead of conjunction, the direction requirement is an implication.
When direction is DirFormula.True, WeakFuture and Future are equivalent.