sealed class Formula : TreeNode<Formula>
An HUCTLp Formula that can be used to describe general temporal properties.
It supports Transition and Numeric propositions together with standard true/false literals and boolean logic.
Furthermore, it supports the basic temporal operators: Next (X), Future (F), Globally (G) and Until (U), plus the special weak operators (WeakFuture and WeakNext) together with path quantification (see PathQuantifier) and optional direction modifiers (see DirFormula).
Finally, it also supports first order (ForAll and Exists) and hybrid (Bind and At) operators.
Semantically, an HUCTLp formula is evaluated at a state of a transition system. For full description of the semantics, see the project readme.
Note that each formula is either Binary, Unary or an atomic proposition.
| And |
data class And : Formula, Binary<And, Formula>
Logical conjunction. A state satisfies this formula if it satisfies both left and right. |
| At |
data class At : Formula, Unary<At, Formula>
At operator specifies that a formula holds at the state with the given name. |
| Bind |
data class Bind : Formula, Unary<Bind, Formula>
Hybrid operator which specifies that at the inspected state, the target formula holds with name substituted for the inspected state. |
| Equals |
data class Equals : Formula, Binary<Equals, Formula>
Logical equivalence. A state satisfies this formula if it does not satisfy neither left nor right or if it satisfies both. |
| Exists |
data class Exists : Formula, Binary<Exists, Formula>
First-order exists operator. Specifies that there exists a state in bound, such that when substituted for name, the target formula is valid at the inspected state. |
| False |
object False : Formula
Logical contradiction. No state satisfies this formula. |
| ForAll |
data class ForAll : Formula, Binary<ForAll, Formula>
First-order forall operator. Specifies that for all states in bound substituted for name, the target formula is valid at inspected state. |
| 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. |
| Implies |
data class Implies : Formula, Binary<Implies, Formula>
Logical implication. A state satisfies this formula if it does not satisfy left or if it satisfies both left and right. |
| 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. |
| Not |
data class Not : Formula, Unary<Not, Formula>
Logical negation. A state satisfies this formula if it does not satisfy inner. |
| Numeric |
data class Numeric : Formula
Numeric proposition. The semantics of this proposition are not strictly defined. However, usually each state maps to a certain point/area in a cartesian space. In this case, the proposition outlines an area of valid states. |
| Or |
data class Or : Formula, Binary<Or, Formula>
Logical disjunction. A state satisfies this formula if it satisfies any of the left and right formulas. |
| Reference |
data class Reference : Formula
The Reference proposition represents a special predicate "current state is the
state referenced by name" which can be (together with hybrid operators) used
to define things like cycles (for example |
| Text |
data class Text : Formula
A general purpose proposition that can contain any string value. |
| Transition |
data class Transition : Formula
Transition proposition. A state satisfies this proposition if there is a transition in the specified direction (up/down) and flow in/out of the state. |
| True |
object True : Formula
Logical tautology. Any state satisfies this formula. |
| Until |
data class Until : Formula, Binary<Until, Formula>
Temporal until (U) operator. A state satisfies until if the paths specified by the quantifier match the direction and always satisfy the path formula until the eventually, the reach formula is satisfied. |
| 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. |
| node |
open val node: Formula
Formula is also the node in the tree, so |
| toString |
open fun toString(): String
Return string which uniquely represents this formula and can be parsed to create an equivalent object. |
| AU |
infix fun Formula.AU(reach: Formula): Until
Create an all until formula over future paths without direction restriction. fun Formula.AU(reach: Formula, dir: DirFormula = DirFormula.True): Until
Create an all until formula over future paths with optional direction restriction. |
| EU |
infix fun Formula.EU(reach: Formula): Until
Create an exists until formula over future paths without direction restriction. fun Formula.EU(reach: Formula, dir: DirFormula = DirFormula.True): Until
Create an exists until formula over future paths with optional direction restriction. |
| and |
infix fun Formula.and(other: Formula): And
Create a conjunction of two formulas. |
| equal |
infix fun Formula.equal(other: Formula): Equals
Create an equality of two formulas. |
| 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. |
| implies |
infix fun Formula.implies(other: Formula): Implies
Create an implication of two formulas. |
| 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. |
| or |
infix fun Formula.or(other: Formula): Or
Create a disjunction of two formulas. |
| pAU |
infix fun Formula.pAU(reach: Formula): Until
Create an all until formula over past paths without direction restriction. fun Formula.pAU(reach: Formula, dir: DirFormula = DirFormula.True): Until
Create an all until formula over past paths with optional direction restriction. |
| pEU |
infix fun Formula.pEU(reach: Formula): Until
Create an exists until formula over past paths without direction restriction. fun Formula.pEU(reach: Formula, dir: DirFormula = DirFormula.True): Until
Create an exists until formula over past paths with optional direction restriction. |
| And |
data class And : Formula, Binary<And, Formula>
Logical conjunction. A state satisfies this formula if it satisfies both left and right. |
| At |
data class At : Formula, Unary<At, Formula>
At operator specifies that a formula holds at the state with the given name. |
| Bind |
data class Bind : Formula, Unary<Bind, Formula>
Hybrid operator which specifies that at the inspected state, the target formula holds with name substituted for the inspected state. |
| Equals |
data class Equals : Formula, Binary<Equals, Formula>
Logical equivalence. A state satisfies this formula if it does not satisfy neither left nor right or if it satisfies both. |
| Exists |
data class Exists : Formula, Binary<Exists, Formula>
First-order exists operator. Specifies that there exists a state in bound, such that when substituted for name, the target formula is valid at the inspected state. |
| False |
object False : Formula
Logical contradiction. No state satisfies this formula. |
| ForAll |
data class ForAll : Formula, Binary<ForAll, Formula>
First-order forall operator. Specifies that for all states in bound substituted for name, the target formula is valid at inspected state. |
| 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. |
| Implies |
data class Implies : Formula, Binary<Implies, Formula>
Logical implication. A state satisfies this formula if it does not satisfy left or if it satisfies both left and right. |
| 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. |
| Not |
data class Not : Formula, Unary<Not, Formula>
Logical negation. A state satisfies this formula if it does not satisfy inner. |
| Numeric |
data class Numeric : Formula
Numeric proposition. The semantics of this proposition are not strictly defined. However, usually each state maps to a certain point/area in a cartesian space. In this case, the proposition outlines an area of valid states. |
| Or |
data class Or : Formula, Binary<Or, Formula>
Logical disjunction. A state satisfies this formula if it satisfies any of the left and right formulas. |
| Reference |
data class Reference : Formula
The Reference proposition represents a special predicate "current state is the
state referenced by name" which can be (together with hybrid operators) used
to define things like cycles (for example |
| Text |
data class Text : Formula
A general purpose proposition that can contain any string value. |
| Transition |
data class Transition : Formula
Transition proposition. A state satisfies this proposition if there is a transition in the specified direction (up/down) and flow in/out of the state. |
| True |
object True : Formula
Logical tautology. Any state satisfies this formula. |
| Until |
data class Until : Formula, Binary<Until, Formula>
Temporal until (U) operator. A state satisfies until if the paths specified by the quantifier match the direction and always satisfy the path formula until the eventually, the reach formula is satisfied. |
| 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. |