LTLSyntax

Syntax for building up LTL propositions.

The type of the "world" -- i.e. the data we are testing the temporal proposition on.

Types

abstract fun always(cond: LTL<W>): LTL<W>

abstract infix fun LTL<W>.and(other: LTL<W>): LTL<W>

abstract fun condition(name: String? = null, cond: ConditionScope<W>.() -> Boolean): LTL<W>

abstract fun eventually(cond: LTL<W>): LTL<W>

abstract infix fun LTL<W>.implies(other: LTL<W>): LTL<W>

abstract fun next(cond: LTL<W>): LTL<W>

abstract operator fun LTL<W>.not(): LTL<W>

abstract infix fun LTL<W>.or(other: LTL<W>): LTL<W>

abstract infix fun LTL<W>.releases(by: LTL<W>): LTL<W>

abstract infix fun LTL<W>.until(cond: LTL<W>): LTL<W>