data class Future : Formula, Temporal<Future>
Temporal future (F) operator. A state satisfies future if the paths specified by the quantifier match the direction and eventually satisfy the inner formula.
Note that for the PathQuantifier.A and PathQuantifier.pA this means that all paths must satisfy the direction. See WeakFuture for less strict alternative.
| <init> |
Future(quantifier: PathQuantifier, inner: Formula, direction: DirFormula)
Temporal future (F) operator. A state satisfies future if the paths specified by the quantifier match the direction and eventually 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): Future
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. |