Future(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Temporal future (F) operator. A state satisfies future if the paths specified by the quantifier match the direction and eventually satisfy the inner formula.
Note that for the PathQuantifier.A and PathQuantifier.pA this means that all paths must satisfy the direction. See WeakFuture for less strict alternative.