interface Temporal<out This : Formula> : Unary<This, Formula>
Common interface for temporal Formulas.
| direction |
abstract val direction: DirFormula
Specifies the direction requirement expected from the selected paths. |
| quantifier |
abstract val quantifier: PathQuantifier
Specifies the condition for selecting paths originating in the inspected state. |
| inner |
abstract val inner: Tree
The singular child element of this object. |
| copy |
abstract fun copy(quantifier: PathQuantifier = this.quantifier, inner: Formula = this.inner, direction: DirFormula = this.direction): This
Create a copy of the original object, but optionally replace some of the elements. |
| fold |
fun <Tree : TreeNode<Tree>, R> TreeNode<Tree>.fold(atom: Tree.() -> R, unary: Unary<*, Tree>.(R) -> R, binary: Binary<*, Tree>.(R, R) -> R): R
Standard tree fold. You can provide transformation operations for atoms, unary and binary nodes. |
| map |
fun <Tree : TreeNode<Tree>> TreeNode<Tree>.map(atom: Tree.() -> Tree = { this }, unary: Unary<Tree, Tree>.(Tree) -> Tree = { this.copy(inner = it) }, binary: Binary<Tree, Tree>.(Tree, Tree) -> Tree = { left, right -> this.copy(left, right)}): Tree
Change tree structure while preserving tree type. You can provide transformation operations for atoms, unary and binary nodes. The only requirement is that operations don't change the type of the tree. |
| Future |
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. |
| Globally |
data class Globally : Formula, Temporal<Globally>
Temporal globally (G) operator. A state satisfies globally if the paths specified by the quantifier match the direction and always satisfy the inner formula. |
| Next |
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. |
| WeakFuture |
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. |
| WeakNext |
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. |