Next(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Temporal next (X) operator. A state satisfies next, if direct successors specified by the quantifier match the direction and satisfy the inner formula.
Note that for the PathQuantifier.A and PathQuantifier.pA this means that all paths must satisfy the direction. See WeakNext for less strict alternative.