WeakNext(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Weak temporal next (wX) operator. A state satisfies weak next when all successors (specified by the quantifier) that match the direction also satisfy the inner formula.
Note that this is essentially equivalent to Next, but instead of conjunction, the direction requirement is an implication.
When direction is DirFormula.True, WeakNext and Next are equivalent.