Defines data structures representing HUCTLp formulas, direction restriction formulas and corresponding atomic propositions.
| CompareOp |
enum class CompareOp
Specifies the type of the comparison operator used by the Formula.Numeric propositions. |
| DirFormula |
sealed class DirFormula : TreeNode<DirFormula>
Formulas that are used to describe the direction of the temporal path. |
| Direction |
enum class Direction
Specifies the direction in which one moves in the transition system. |
| Expression |
sealed class Expression : TreeNode<Expression>
Arithmetic expressions which are used in the Formula.Numeric proposition. |
| Flow |
enum class Flow
Specifies the type of transition between two states. |
| Formula |
sealed class Formula : TreeNode<Formula>
An HUCTLp Formula that can be used to describe general temporal properties. |
| PathQuantifier |
enum class PathQuantifier
Specifies the type of the temporal path quantifier used by the HUCTLp Formula. |
| Temporal |
interface Temporal<out This : Formula> : Unary<This, Formula>
Common interface for temporal Formulas. |