Create an all future formula over future paths with optional dir direction restriction.

Create an all weak next formula over future paths with optional dir direction restriction.

Create an all until formula over future paths without direction restriction.

Create an all until formula over future paths with optional direction restriction.

Create an all next formula over future paths with optional dir direction restriction.

Create a hybrid At formula valid at the given name.

Create an all weak future formula over future paths with optional dir direction restriction.

Create an all weak next formula over future paths with optional dir direction restriction.

Create a hybrid Bind formula, binding the given name.

Create an exists future formula over future paths with optional dir direction restriction.

Create an exists globally formula over future paths with optional dir direction restriction.

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

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

Create an exists next formula over future paths with optional dir direction restriction.

Create an exists weak future formula over future paths with optional dir direction restriction.

Create an exists weak next formula over future paths with optional dir direction restriction.

Create a first order Exists formula, binding the given name.

Create a first order ForAll formula, binding the given name.

Create a negation of target direction formula.

Create a negation of inner formula.

Create a conjunction of two direction formulas.

Create a conjunction of two formulas.

Create division from two expressions.

Create Formula.Numeric proposition by comparing two expressions using the CompareOp.EQ.

Create an equality of two direction formulas.

Create an equality of two formulas.

Create Formula.Numeric proposition by comparing two expressions using the CompareOp.GE.

Create Formula.Numeric proposition by comparing two expressions using the CompareOp.GT.

Create an implication of two direction formulas.

Create an implication of two formulas.

Create Formula.Numeric proposition by comparing two expressions using the CompareOp.LE.

Create Formula.Numeric proposition by comparing two expressions using the CompareOp.LT.

Create subtraction from two expressions.

Create Formula.Numeric proposition by comparing two expressions using the CompareOp.NEQ.

Create a disjunction of two direction formulas.

Create a disjunction of two formulas.

Create an all future formula over past paths with optional dir direction restriction.

Create an all weak next formula over past paths with optional dir direction restriction.

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

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

Create an all next formula over past paths with optional dir direction restriction.

Create an all weak future formula over past paths with optional dir direction restriction.

Create an all weak next formula over past paths with optional dir direction restriction.

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

Create an exists weak next formula over past paths with optional dir direction restriction.

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

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

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

Create an exists weak future formula over past paths with optional dir direction restriction.

Create an exists weak next formula over past paths with optional dir direction restriction.

Create addition from two expressions.

Create multiplication from two expressions.