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