LTL

sealed class LTL<W>(source)

A proposition of linear temporal logic of statements about the world W.

Types

data class And<W>(val x: LTL<W>, val y: LTL<W>) : LTL<W>

data class Condition<W>(val name: String?, val cond: ConditionScope<W>.() -> Boolean) : LTL<W>

data class Eventually<W>(val cond: LTL<W>) : LTL<W>

class False<W> : LTL<W>

data class Next<W>(val cond: LTL<W>) : LTL<W>

data class Not<W>(val cond: LTL<W>) : LTL<W>

data class Or<W>(val x: LTL<W>, val y: LTL<W>) : LTL<W>

data class Release<W>(val y: LTL<W>, val x: LTL<W>) : LTL<W>

data class Until<W>(val x: LTL<W>, val y: LTL<W>) : LTL<W>

abstract fun evaluateAtTime(world: (Int) -> W, time: Int, maxTraceLength: Int): LTLResult

Evaluate the given LTL proposition with respect to the given data at a specific time.