data class Next : Formula, Temporal<Next>
Temporal next (X) operator. A state satisfies next, if direct successors specified by the quantifier match the direction and satisfy the inner formula.
Note that for the PathQuantifier.A and PathQuantifier.pA this means that all paths must satisfy the direction. See WeakNext for less strict alternative.
| <init> |
Next(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Temporal next (X) operator. A state satisfies next, if direct successors specified by the quantifier match the direction and satisfy the inner formula. |
| direction |
val direction: DirFormula
Specifies the direction requirement expected from the selected paths. |
| inner |
val inner: Formula
The singular child element of this object. |
| quantifier |
val quantifier: PathQuantifier
Specifies the condition for selecting paths originating in the inspected state. |
| node |
open val node: Formula
Formula is also the node in the tree, so |
| copy |
fun copy(inner: Formula): Next
Create a copy of the original object but optionally replace the child element. |
| toString |
fun toString(): String
Return string which uniquely represents this formula and can be parsed to create an equivalent object. |