yafrl-testing/io.github.yafrl.testing

Package-level declarations

Types

data class ConditionScope<W>(val world: (Int) -> W, val time: Int)

sealed class LTL<W>

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

Results to use for an LTL proposition that has been evaluated for a finite segment of observations.

interface LTLSyntax<W>

Syntax for building up LTL propositions.

fun atArbitraryState(traceLength: Int = 100, clockGenerator: Arb<Duration> = fpsClockGenerator(), check: SampleScope.() -> Unit)

Advances the FRP graph to an arbitrary state in the state space, after which assertions can be run with check.

fun fpsClockGenerator(frameRate: Double = 60.0, delta: Duration = 2.0.milliseconds): Arb<Duration>

Sane default for an Arb that generates clock ticks.

fun <W> testPropositionHoldsFor(setupState: () -> Signal<W>, numIterations: Int = 100, maxTraceLength: Int = 50, clockGenerator: Arb<Duration> = fpsClockGenerator(), proposition: LTLSyntax<W>.() -> LTL<W>)

Randomly execute actions in the state graph, testing a linear temporal logic proposition proposition against the state returned by setupState.