data class WeakNext : Formula, Temporal<WeakNext>
Weak temporal next (wX) operator. A state satisfies weak next when all successors (specified by the quantifier) that match the direction also satisfy the inner formula.
Note that this is essentially equivalent to Next, but instead of conjunction, the direction requirement is an implication.
When direction is DirFormula.True, WeakNext and Next are equivalent.
| <init> |
WeakNext(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Weak temporal next (wX) operator. A state satisfies weak next when all successors (specified by the quantifier) that match the direction also 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): WeakNext
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. |