HUCTLp / com.github.sybila.huctl / DirFormula

DirFormula

sealed class DirFormula : TreeNode<DirFormula>

Formulas that are used to describe the direction of the temporal path.

They support basic boolean logic, direction propositions ("var+", "var-", etc.) and a special "loop" predicate, which indicates a self-loop transition.

Note that each formula is either Binary, Unary or an atomic proposition.

Types

And data class And : DirFormula, Binary<And, DirFormula>

Logical conjunction. A path will match this restriction only if it matches both left and right restrictions.
Equals data class Equals : DirFormula, Binary<Equals, DirFormula>

Logical equivalence. A path will match this restriction either when it matches both left and right restriction or none of them.
False object False : DirFormula

Logical contradiction - no path will match this restriction.
Implies data class Implies : DirFormula, Binary<Implies, DirFormula>

Logical implication. A path will match this restriction only if does not match the left restriction or matches both left and right restriction.
Loop object Loop : DirFormula

Special loop proposition - only a self-loop path matches this restriction.
Not data class Not : DirFormula, Unary<Not, DirFormula>

Logical negation. A path will match this restriction if it does not match the inner restriction.
Or data class Or : DirFormula, Binary<Or, DirFormula>

Logical disjunction. A path will match this restriction only if it matches any of the left and right restrictions.
Proposition data class Proposition : DirFormula

General direction proposition. Contains a variable name and a requested direction (increase/up or decrease/down).
Text data class Text : DirFormula

A general purpose proposition that can contain any string value.
True object True : DirFormula

Logical tautology - any path will match this restriction.

Properties

node open val node: DirFormula

DirFormula is also the node in the tree, so node == this

Functions

toString open fun toString(): String

Return string which uniquely represents this formula and can be parsed to create an equivalent object.

Extension Functions

and infix fun DirFormula.and(right: DirFormula): And

Create a conjunction of two direction formulas.
equal infix fun DirFormula.equal(right: DirFormula): DirFormula

Create an equality of two direction 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 DirFormula.implies(right: DirFormula): DirFormula

Create an implication of two direction 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 DirFormula.or(right: DirFormula): DirFormula

Create a disjunction of two direction formulas.

Inheritors

And data class And : DirFormula, Binary<And, DirFormula>

Logical conjunction. A path will match this restriction only if it matches both left and right restrictions.
Equals data class Equals : DirFormula, Binary<Equals, DirFormula>

Logical equivalence. A path will match this restriction either when it matches both left and right restriction or none of them.
False object False : DirFormula

Logical contradiction - no path will match this restriction.
Implies data class Implies : DirFormula, Binary<Implies, DirFormula>

Logical implication. A path will match this restriction only if does not match the left restriction or matches both left and right restriction.
Loop object Loop : DirFormula

Special loop proposition - only a self-loop path matches this restriction.
Not data class Not : DirFormula, Unary<Not, DirFormula>

Logical negation. A path will match this restriction if it does not match the inner restriction.
Or data class Or : DirFormula, Binary<Or, DirFormula>

Logical disjunction. A path will match this restriction only if it matches any of the left and right restrictions.
Proposition data class Proposition : DirFormula

General direction proposition. Contains a variable name and a requested direction (increase/up or decrease/down).
Text data class Text : DirFormula

A general purpose proposition that can contain any string value.
True object True : DirFormula

Logical tautology - any path will match this restriction.