Globally(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Temporal globally (G) operator. A state satisfies globally if the paths specified by the quantifier match the direction and always satisfy the inner formula.