pEU

infix fun Formula.pEU(reach: Formula): Until

Create an exists until formula over past paths without direction restriction.

fun Formula.pEU(reach: Formula, dir: DirFormula = DirFormula.True): Until

Create an exists until formula over past paths with optional direction restriction.