data class Until : Formula, Binary<Until, Formula>
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.
| <init> |
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. |
| direction |
val direction: DirFormula
Specifies the direction requirement expected from the selected paths. |
| left |
val left: Formula
The child of this element which is the root of the left subtree. |
| path |
val path: Formula
The formula which needs to be valid along a path until reach is found. |
| quantifier |
val quantifier: PathQuantifier
Specifies the condition for selecting paths originating in the inspected state. |
| reach |
val reach: Formula
The formula which needs to be eventually found in the path. |
| right |
val right: Formula
The child of this element which is the root of the right subtree. |
| node |
open val node: Formula
Formula is also the node in the tree, so |
| copy |
fun copy(left: Formula, right: Formula): Until
Create a copy of the original object but optionally replace the left or right child element. |
| toString |
fun toString(): String
Return string which uniquely represents this formula and can be parsed to create an equivalent object. |