Until(quantifier: PathQuantifier, path: Formula, reach: Formula, direction: DirFormula)
Temporal until (U) operator. A state satisfies until if the paths specified by the quantifier match the direction and always satisfy the path formula until the eventually, the reach formula is satisfied.